Property class comment expect fail (model-checking#925)

* Adding Property Class and Comments, through expect_fail tracer bullet

cprover_bindings/src/goto_program/builtin.rs

@@ -7,6 +7,7 @@ use super::{Expr, Location, Symbol, Type};
 #[derive(Debug, Clone, Copy)]
 pub enum BuiltinFn {
     Abort,
+    Assert,
     CProverAssert,
     CProverAssume,
     CProverCover,
@@ -66,6 +67,7 @@ impl ToString for BuiltinFn {
     fn to_string(&self) -> String {
         match self {
             Abort => "abort",
+            Assert => "assert",
             CProverAssert => "__CPROVER_assert",
             CProverAssume => "__CPROVER_assume",
             CProverCover => "__CPROVER_cover",
@@ -129,6 +131,7 @@ impl BuiltinFn {
     pub fn param_types(&self) -> Vec<Type> {
         match self {
             Abort => vec![],
+            Assert => vec![Type::bool()],
             CProverAssert => vec![Type::bool(), Type::c_char().to_pointer()],
             CProverAssume => vec![Type::bool()],
             CProverCover => vec![Type::bool()],
@@ -185,6 +188,7 @@ impl BuiltinFn {
     pub fn return_type(&self) -> Type {
         match self {
             Abort => Type::empty(),
+            Assert => Type::empty(),
             CProverAssert => Type::empty(),
             CProverAssume => Type::empty(),
             CProverCover => Type::empty(),
@@ -244,6 +248,7 @@ impl BuiltinFn {
     pub fn list_all() -> Vec<BuiltinFn> {
         vec![
             Abort,
+            Assert,
             CProverAssert,
             CProverAssume,
             CProverCover,

cprover_bindings/src/goto_program/location.rs

@@ -14,6 +14,15 @@ pub enum Location {
     /// Location in user code.
     /// `function` is `None` for global, `Some(function_name)` for function local.
     Loc { file: InternedString, function: Option<InternedString>, line: u64, col: Option<u64> },
+    /// Location for Statements that use Property Class and Description - Assert, Assume, Cover etc.
+    Property {
+        file: InternedString,
+        function: Option<InternedString>,
+        line: u64,
+        col: Option<u64>,
+        comment: InternedString,
+        property_class: InternedString,
+    },
 }
 
 /// Getters and predicates
@@ -58,6 +67,9 @@ impl Location {
                 format!("<{}>", function_name)
             }
             Location::Loc { file, line, .. } => format!("{}:{}", file, line),
+            Location::Property { file, line, .. } => {
+                format!("<{:?}>:{}", file, line)
+            }
         }
     }
 }
@@ -81,6 +93,57 @@ impl Location {
         Location::Loc { file, function, line, col }
     }
 
+    /// Create a Property type Location
+    pub fn property_location<T, U>(
+        file: Option<U>,
+        function: Option<U>,
+        line: T,
+        col: Option<T>,
+        comment: U,
+        property_name: U,
+    ) -> Location
+    where
+        T: TryInto<u64>,
+        T::Error: Debug,
+        U: Into<InternedString>,
+    {
+        let file = file.unwrap().into();
+        let line = line.try_into().unwrap();
+        let col = col.map(|x| x.try_into().unwrap());
+        let function = function.intern();
+        let property_class = property_name.into();
+        let comment = comment.into();
+        Location::Property { file, function, line, col, comment, property_class }
+    }
+
+    /// Create a Property type Location from an already existing Location type
+    pub fn create_location_with_property<T: Into<InternedString>>(
+        comment: T,
+        property_name: T,
+        location: Self,
+    ) -> Self {
+        match location {
+            Location::BuiltinFunction { function_name, line } => Location::property_location(
+                None,
+                Some(function_name),
+                line.unwrap(),
+                None,
+                comment.into(),
+                property_name.into(),
+            ),
+            Location::Loc { file, function, line, col } => Location::property_location(
+                file.into(),
+                function.intern(),
+                line,
+                col.map(|x| x.try_into().unwrap()),
+                comment.into(),
+                property_name.into(),
+            ),
+            Location::Property { .. } => location,
+            Location::None => location,
+        }
+    }
+
     pub fn none() -> Location {
         Location::None
     }

cprover_bindings/src/goto_program/stmt.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use self::StmtBody::*;
 use super::{BuiltinFn, Expr, Location};
-use crate::InternedString;
+use crate::{InternString, InternedString};
 use std::fmt::Debug;
 use tracing::debug;
 
@@ -40,6 +40,12 @@ pub enum StmtBody {
         lhs: Expr,
         rhs: Expr,
     },
+    /// `assert(cond)`
+    Assert {
+        cond: Expr,
+        property_class: InternedString,
+        msg: InternedString,
+    },
     /// `__CPROVER_assume(cond);`
     Assume {
         cond: Expr,
@@ -184,6 +190,17 @@ impl Stmt {
         stmt!(Assign { lhs, rhs }, loc)
     }
 
+    /// `assert(cond, property_class, commment);`
+    pub fn assert_statement(cond: Expr, property_name: &str, message: &str, loc: Location) -> Self {
+        assert!(cond.typ().is_bool());
+
+        // Chose InternedString to seperate out codegen from the cprover_bindings logic
+        let property_class = property_name.to_string().intern();
+        let msg = message.into();
+
+        stmt!(Assert { cond, property_class, msg }, loc)
+    }
+
     /// `__CPROVER_assert(cond, msg);`
     pub fn assert(cond: Expr, msg: &str, loc: Location) -> Self {
         assert!(cond.typ().is_bool());

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -497,6 +497,9 @@ pub trait Transformer: Sized {
     fn transform_stmt(&mut self, stmt: &Stmt) -> Stmt {
         match stmt.body() {
             StmtBody::Assign { lhs, rhs } => self.transform_stmt_assign(lhs, rhs),
+            StmtBody::Assert { cond, property_class, msg } => {
+                self.transform_stmt_assert(cond, *property_class, *msg)
+            }
             StmtBody::Assume { cond } => self.transform_stmt_assume(cond),
             StmtBody::AtomicBlock(block) => self.transform_stmt_atomic_block(block),
             StmtBody::Block(block) => self.transform_stmt_block(block),
@@ -530,6 +533,22 @@ pub trait Transformer: Sized {
         transformed_lhs.assign(transformed_rhs, Location::none())
     }
 
+    /// Transforms a assert stmt (`Assert(cond, property_class, message);`)
+    fn transform_stmt_assert(
+        &mut self,
+        cond: &Expr,
+        property_name: InternedString,
+        msg: InternedString,
+    ) -> Stmt {
+        let transformed_cond = self.transform_expr(cond);
+        Stmt::assert_statement(
+            transformed_cond,
+            property_name.to_string().as_str(),
+            msg.to_string().as_str(),
+            Location::none(),
+        )
+    }
+
     /// Transforms a CPROVER assume stmt (`__CPROVER_assume(cond);`)
     fn transform_stmt_assume(&mut self, cond: &Expr) -> Stmt {
         let transformed_cond = self.transform_expr(cond);

cprover_bindings/src/irep/to_irep.rs

@@ -329,6 +329,19 @@ impl ToIrep for Location {
             ])
             .with_named_sub_option(IrepId::Column, col.map(Irep::just_int_id))
             .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id)),
+            Location::Property { file, function, line, col, property_class, comment } => {
+                Irep::just_named_sub(vector_map![
+                    (IrepId::File, Irep::just_string_id(file.to_string())),
+                    (IrepId::Line, Irep::just_int_id(*line)),
+                ])
+                .with_named_sub_option(IrepId::Column, col.map(Irep::just_int_id))
+                .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id))
+                .with_named_sub(IrepId::Comment, Irep::just_string_id(comment.to_string()))
+                .with_named_sub(
+                    IrepId::PropertyClass,
+                    Irep::just_string_id(property_class.to_string()),
+                )
+            }
         }
     }
 }
@@ -357,6 +370,7 @@ impl ToIrep for StmtBody {
             StmtBody::Assign { lhs, rhs } => {
                 code_irep(IrepId::Assign, vec![lhs.to_irep(mm), rhs.to_irep(mm)])
             }
+            StmtBody::Assert { cond, .. } => code_irep(IrepId::Assert, vec![cond.to_irep(mm)]),
             StmtBody::Assume { cond } => code_irep(IrepId::Assume, vec![cond.to_irep(mm)]),
             StmtBody::AtomicBlock(stmts) => {
                 let mut irep_stmts = vec![code_irep(IrepId::AtomicBegin, vec![])];

src/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -0,0 +1,59 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This file contains the code that acts as a wrapper to create the new assert and related statements
+
+use crate::codegen_cprover_gotoc::GotocCtx;
+use cbmc::goto_program::{Expr, Location, Stmt};
+use std::str::FromStr;
+
+/// The Property Class enum stores all viable options for classifying asserts, cover assume and other related statements
+#[derive(Copy, Debug, Clone)]
+pub enum PropertyClass {
+    ExpectFail,
+    UnsupportedStructs,
+    DefaultAssertion,
+}
+
+impl FromStr for PropertyClass {
+    type Err = &'static str;
+
+    fn from_str(input: &str) -> Result<PropertyClass, Self::Err> {
+        match input {
+            "expect_fail" => Ok(PropertyClass::ExpectFail),
+            "unsupported_struct" => Ok(PropertyClass::UnsupportedStructs),
+            "assertion" => Ok(PropertyClass::DefaultAssertion),
+            _ => Err("No such property class"),
+        }
+    }
+}
+
+impl PropertyClass {
+    pub fn as_str(&self) -> &str {
+        match self {
+            PropertyClass::ExpectFail => "expect_fail",
+            PropertyClass::UnsupportedStructs => "unsupported_struct",
+            PropertyClass::DefaultAssertion => "assertion",
+        }
+    }
+}
+
+impl<'tcx> GotocCtx<'tcx> {
+    pub fn codegen_assert(
+        &self,
+        cond: Expr,
+        property_class: PropertyClass,
+        message: &str,
+        loc: Location,
+    ) -> Stmt {
+        assert!(cond.typ().is_bool());
+
+        let property_name = property_class.as_str();
+
+        // Create a Property Location Variant from any given Location type
+        let property_location =
+            Location::create_location_with_property(message, property_name, loc);
+
+        Stmt::assert_statement(cond, property_name, message, property_location)
+    }
+}

src/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs

@@ -4,6 +4,7 @@
 //! This module does that actual translation of MIR constructs to goto constructs.
 //! Each subfile is named for the MIR construct it translates.
 
+mod assert;
 mod block;
 mod function;
 mod intrinsic;
@@ -15,4 +16,5 @@ mod statement;
 mod static_var;
 mod typ;
 
+pub use assert::PropertyClass;
 pub use typ::TypeExt;

src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -8,6 +8,7 @@
 //! It would be too nasty if we spread around these sort of undocumented hooks in place, so
 //! this module addresses this issue.
 
+use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::utils;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
@@ -98,13 +99,17 @@ impl<'tcx> GotocHook<'tcx> for ExpectFail {
         assert_eq!(fargs.len(), 2);
         let target = target.unwrap();
         let cond = fargs.remove(0).cast_to(Type::bool());
-        // add "EXPECTED FAIL" to the message because compiletest relies on it
+
+        // Add "EXPECTED FAIL" to the message because compiletest relies on it
         let msg =
             format!("EXPECTED FAIL: {}", utils::extract_const_message(&fargs.remove(0)).unwrap());
+
+        let property_class = PropertyClass::ExpectFail;
+
         let loc = tcx.codegen_span_option(span);
         Stmt::block(
             vec![
-                Stmt::assert(cond, &msg, loc.clone()),
+                tcx.codegen_assert(cond, property_class, &msg, loc.clone()),
                 Stmt::goto(tcx.current_fn().find_label(&target), loc.clone()),
             ],
             loc,

tests/ui/expect-fail-property-class/expected

@@ -0,0 +1,3 @@
+Check 1: main.expect_fail.1
+Status: FAILURE
+Description: "EXPECTED FAIL: Blocked by assumption above."

tests/ui/expect-fail-property-class/main.rs

@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check if expect_fail uses new property class and description in it's check id
+
+#[kani::proof]
+fn main() {
+    let i: i32 = kani::any();
+    kani::assume(i < 10);
+    kani::expect_fail(i > 20, "Blocked by assumption above.");
+}