Replace CProver_Assert with Assert Statment; Adds Property Class (mod…

…el-checking#1002)

* Replace cprover_Asserts

* Add Tests for Property Classes

cprover_bindings/src/goto_program/builtin.rs

@@ -8,7 +8,6 @@ use super::{Expr, Location, Symbol, Type};
 pub enum BuiltinFn {
     Abort,
     Assert,
-    CProverAssert,
     CProverAssume,
     CProverCover,
     Calloc,
@@ -68,7 +67,6 @@ impl ToString for BuiltinFn {
         match self {
             Abort => "abort",
             Assert => "assert",
-            CProverAssert => "__CPROVER_assert",
             CProverAssume => "__CPROVER_assume",
             CProverCover => "__CPROVER_cover",
             Calloc => "calloc",
@@ -132,7 +130,6 @@ impl BuiltinFn {
         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()],
             Calloc => vec![Type::size_t(), Type::size_t()],
@@ -189,7 +186,6 @@ impl BuiltinFn {
         match self {
             Abort => Type::empty(),
             Assert => Type::empty(),
-            CProverAssert => Type::empty(),
             CProverAssume => Type::empty(),
             CProverCover => Type::empty(),
             Calloc => Type::void_pointer(),
@@ -249,7 +245,6 @@ impl BuiltinFn {
         vec![
             Abort,
             Assert,
-            CProverAssert,
             CProverAssume,
             CProverCover,
             Calloc,

cprover_bindings/src/goto_program/location.rs

@@ -23,6 +23,8 @@ pub enum Location {
         comment: InternedString,
         property_class: InternedString,
     },
+    /// Covers cases where Location Details are unknown or set as None but Property Class is needed.
+    PropertyUnknownLocation { comment: InternedString, property_class: InternedString },
 }
 
 /// Getters and predicates
@@ -70,6 +72,7 @@ impl Location {
             Location::Property { file, line, .. } => {
                 format!("<{:?}>:{}", file, line)
             }
+            Location::PropertyUnknownLocation { .. } => "<none>".to_string(),
         }
     }
 }
@@ -140,7 +143,13 @@ impl Location {
                 property_name.into(),
             ),
             Location::Property { .. } => location,
-            Location::None => location,
+            Location::PropertyUnknownLocation { .. } => location,
+            // This converts None type Locations to PropertyUnknownLocation type which inserts Property Class and Description
+            // into the Source Location Irep's without any location details.
+            Location::None => Location::PropertyUnknownLocation {
+                comment: comment.into(),
+                property_class: property_name.into(),
+            },
         }
     }
 

cprover_bindings/src/goto_program/stmt.rs

@@ -191,7 +191,7 @@ impl Stmt {
     }
 
     /// `assert(cond, property_class, commment);`
-    pub fn assert_statement(cond: Expr, property_name: &str, message: &str, loc: Location) -> Self {
+    pub fn assert(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
@@ -201,16 +201,8 @@ impl Stmt {
         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());
-        BuiltinFn::CProverAssert
-            .call(vec![cond, Expr::string_constant(msg)], loc.clone())
-            .as_stmt(loc)
-    }
-
     pub fn assert_false(msg: &str, loc: Location) -> Self {
-        Stmt::assert(Expr::bool_false(), msg, loc)
+        Stmt::assert(Expr::bool_false(), "assert_false", msg, loc)
     }
 
     /// A __CPROVER_assert to sanity check expected components of code
@@ -223,7 +215,7 @@ impl Stmt {
         Stmt::block(
             vec![
                 // Assert our expected true expression.
-                Stmt::assert(expect_true.clone(), &assert_msg, loc.clone()),
+                Stmt::assert(expect_true.clone(), "sanity_check", &assert_msg, loc.clone()),
                 // If expect_true is false, assume false to block any further
                 // exploration of this path.
                 Stmt::assume(expect_true, loc.clone()),

cprover_bindings/src/goto_program/symtab_transformer/identity_transformer.rs

@@ -366,7 +366,7 @@ mod tests {
                 Expr::bool_true(),
                 Location::none(),
             ));
-            add_sym(Stmt::assert(Expr::bool_true(), "", Location::none()));
+            add_sym(Stmt::assert(Expr::bool_true(), "", "", Location::none()));
             add_sym(Stmt::assume(Expr::bool_false(), Location::none()));
             add_sym(Stmt::atomic_block(
                 vec![Stmt::assert_false("", Location::none())],

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -541,7 +541,7 @@ pub trait Transformer: Sized {
         msg: InternedString,
     ) -> Stmt {
         let transformed_cond = self.transform_expr(cond);
-        Stmt::assert_statement(
+        Stmt::assert(
             transformed_cond,
             property_name.to_string().as_str(),
             msg.to_string().as_str(),

cprover_bindings/src/irep/to_irep.rs

@@ -366,6 +366,12 @@ impl ToIrep for Location {
                     Irep::just_string_id(property_class.to_string()),
                 )
             }
+            Location::PropertyUnknownLocation { property_class, comment } => {
+                Irep::just_named_sub(vector_map![
+                    (IrepId::Comment, Irep::just_string_id(comment.to_string())),
+                    (IrepId::PropertyClass, Irep::just_string_id(property_class.to_string()))
+                ])
+            }
         }
     }
 }

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

@@ -2,38 +2,66 @@
 // 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)]
+#[derive(Debug, Clone)]
+#[allow(dead_code)]
 pub enum PropertyClass {
-    ExpectFail,
-    UnsupportedStructs,
+    ArithmeticOverflow,
+    AssertFalse,
+    Assume,
+    Cover,
+    CustomProperty(String),
     DefaultAssertion,
+    ExactDiv,
+    ExpectFail,
+    FiniteCheck,
+    PointerOffset,
+    SanityCheck,
+    Unimplemented,
+    UnsupportedConstruct,
+    Unreachable,
 }
 
-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"),
-        }
-    }
-}
-
+#[allow(dead_code)]
 impl PropertyClass {
     pub fn as_str(&self) -> &str {
         match self {
-            PropertyClass::ExpectFail => "expect_fail",
-            PropertyClass::UnsupportedStructs => "unsupported_struct",
+            PropertyClass::ArithmeticOverflow => "arithmetic_overflow",
+            PropertyClass::AssertFalse => "assert_false",
+            PropertyClass::Assume => "assume",
+            PropertyClass::Cover => "coverage_check",
+            PropertyClass::CustomProperty(property_string) => property_string.as_str(),
             PropertyClass::DefaultAssertion => "assertion",
+            PropertyClass::ExactDiv => "exact_div",
+            PropertyClass::ExpectFail => "expect_fail",
+            PropertyClass::FiniteCheck => "finite_check",
+            PropertyClass::PointerOffset => "pointer_offset",
+            PropertyClass::SanityCheck => "sanity_check",
+            PropertyClass::Unimplemented => "unimplemented",
+            PropertyClass::Unreachable => "unreachable",
+            PropertyClass::UnsupportedConstruct => "unsupported_construct",
+        }
+    }
+
+    pub fn from_str(input: &str) -> PropertyClass {
+        match input {
+            "arithmetic_overflow" => PropertyClass::ArithmeticOverflow,
+            "assert_false" => PropertyClass::AssertFalse,
+            "assume" => PropertyClass::Assume,
+            "assertion" => PropertyClass::DefaultAssertion,
+            "coverage_check" => PropertyClass::Cover,
+            "exact_div" => PropertyClass::ExactDiv,
+            "expect_fail" => PropertyClass::ExpectFail,
+            "finite_check" => PropertyClass::FiniteCheck,
+            "pointer_offset" => PropertyClass::PointerOffset,
+            "sanity_check" => PropertyClass::SanityCheck,
+            "unimplemented" => PropertyClass::Unimplemented,
+            "unreachable" => PropertyClass::Unreachable,
+            "unsupported_construct" => PropertyClass::UnsupportedConstruct,
+            _ => PropertyClass::CustomProperty(input.to_owned()),
         }
     }
 }
@@ -54,6 +82,17 @@ impl<'tcx> GotocCtx<'tcx> {
         let property_location =
             Location::create_location_with_property(message, property_name, loc);
 
-        Stmt::assert_statement(cond, property_name, message, property_location)
+        Stmt::assert(cond, property_name, message, property_location)
+    }
+
+    pub fn codegen_assert_false(&self, message: &str, loc: Location) -> Stmt {
+        // Default assertion class for assert_false
+        let property_name = PropertyClass::DefaultAssertion.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_false(message, property_location)
     }
 }

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

@@ -1,6 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module handles intrinsics
+use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::mir::Place;
@@ -164,8 +165,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 let a = fargs.remove(0);
                 let b = fargs.remove(0);
                 let res = a.$f(b);
-                let check = Stmt::assert(
+                let check = self.codegen_assert(
                     res.overflowed.not(),
+                    PropertyClass::ArithmeticOverflow,
                     format!("attempt to compute {} which would overflow", intrinsic).as_str(),
                     loc,
                 );
@@ -196,8 +198,9 @@ impl<'tcx> GotocCtx<'tcx> {
                         }
                     }
                 }
-                let check_stmt = Stmt::assert(
+                let check_stmt = self.codegen_assert(
                     check.not(),
+                    PropertyClass::ArithmeticOverflow,
                     format!("attempt to compute {} which would overflow", intrinsic).as_str(),
                     loc,
                 );
@@ -316,9 +319,12 @@ impl<'tcx> GotocCtx<'tcx> {
             // https://doc.rust-lang.org/core/intrinsics/fn.assume.html
             // Informs the optimizer that a condition is always true.
             // If the condition is false, the behavior is undefined.
-            "assume" => {
-                Stmt::assert(fargs.remove(0).cast_to(Type::bool()), "assumption failed", loc)
-            }
+            "assume" => self.codegen_assert(
+                fargs.remove(0).cast_to(Type::bool()),
+                PropertyClass::Assume,
+                "assumption failed",
+                loc,
+            ),
             "atomic_and" => codegen_atomic_binop!(bitand),
             "atomic_and_acq" => codegen_atomic_binop!(bitand),
             "atomic_and_acqrel" => codegen_atomic_binop!(bitand),
@@ -533,7 +539,12 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow),
             "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
-            "unreachable" => Stmt::assert_false("unreachable", loc),
+            "unreachable" => self.codegen_assert(
+                Expr::bool_false(),
+                PropertyClass::DefaultAssertion,
+                "unreachable",
+                loc,
+            ),
             "volatile_copy_memory" => codegen_intrinsic_copy!(Memmove),
             "volatile_copy_nonoverlapping_memory" => codegen_intrinsic_copy!(Memcpy),
             "volatile_load" => self.codegen_expr_to_place(p, fargs.remove(0).dereference()),
@@ -579,8 +590,18 @@ impl<'tcx> GotocCtx<'tcx> {
         let msg1 = format!("first argument for {} is finite", intrinsic);
         let msg2 = format!("second argument for {} is finite", intrinsic);
         let loc = self.codegen_span_option(span);
-        let finite_check1 = Stmt::assert(arg1.is_finite(), msg1.as_str(), loc.clone());
-        let finite_check2 = Stmt::assert(arg2.is_finite(), msg2.as_str(), loc.clone());
+        let finite_check1 = self.codegen_assert(
+            arg1.is_finite(),
+            PropertyClass::FiniteCheck,
+            msg1.as_str(),
+            loc.clone(),
+        );
+        let finite_check2 = self.codegen_assert(
+            arg2.is_finite(),
+            PropertyClass::FiniteCheck,
+            msg2.as_str(),
+            loc.clone(),
+        );
         Stmt::block(vec![finite_check1, finite_check2, stmt], loc)
     }
 
@@ -604,12 +625,23 @@ impl<'tcx> GotocCtx<'tcx> {
         let division_does_not_overflow = dividend_is_int_min.and(divisor_is_minus_one).not();
         Stmt::block(
             vec![
-                Stmt::assert(division_is_exact, "exact_div arguments divide exactly", loc.clone()),
-                Stmt::assert(divisor_is_nonzero, "exact_div divisor is nonzero", loc.clone()),
-                Stmt::assert(
+                self.codegen_assert(
+                    division_is_exact,
+                    PropertyClass::ExactDiv,
+                    "exact_div arguments divide exactly",
+                    loc,
+                ),
+                self.codegen_assert(
+                    divisor_is_nonzero,
+                    PropertyClass::ExactDiv,
+                    "exact_div divisor is nonzero",
+                    loc,
+                ),
+                self.codegen_assert(
                     division_does_not_overflow,
+                    PropertyClass::ExactDiv,
                     "exact_div division does not overflow",
-                    loc.clone(),
+                    loc,
                 ),
                 self.codegen_expr_to_place(p, a.div(b)),
             ],
@@ -775,8 +807,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
         Stmt::block(
             vec![
-                Stmt::assert(
+                self.codegen_assert(
                     pointers_to_same_object,
+                    PropertyClass::PointerOffset,
                     "ptr_offset_from: pointers point to same object",
                     loc.clone(),
                 ),
@@ -1034,7 +1067,12 @@ impl<'tcx> GotocCtx<'tcx> {
         let src = fargs.remove(0);
         let typ = instance.substs.type_at(0);
         let align = self.is_aligned(typ, dst.clone());
-        let align_check = Stmt::assert(align, "`dst` is properly aligned", loc.clone());
+        let align_check = self.codegen_assert(
+            align,
+            PropertyClass::DefaultAssertion,
+            "`dst` is properly aligned",
+            loc.clone(),
+        );
         let expr = dst.dereference().assign(src, loc.clone());
         Stmt::block(vec![align_check, expr], loc)
     }