Clean up property class and reclassify some checks (rust-lang#1299)

* Clean up property class and mark sanity checks

1. Remove the property classes that weren't being used.
2. Provide a tighter definition for DefaultAssert and reclassify things
   accordingly.
3. Renamed KaniCheck to SafetyCheck to make it a more meaningful name.

* Use strum to convert PropertyClass <-> &str

Author: celinval

Cargo.lock

@@ -319,6 +319,12 @@ dependencies = [
  "unicode-segmentation",
 ]
 
+[[package]]
+name = "heck"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2540771e65fc8cb83cd6e8a237f70c319bd5c29f78ed1084ba5d50eeac86f7f9"
+
 [[package]]
 name = "hermit-abi"
 version = "0.1.19"
@@ -397,6 +403,8 @@ dependencies = [
  "serde",
  "serde_json",
  "shell-words",
+ "strum",
+ "strum_macros",
  "tracing",
  "tracing-subscriber",
  "tracing-tree",
@@ -864,6 +872,12 @@ dependencies = [
  "tracing-tree",
 ]
 
+[[package]]
+name = "rustversion"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a0a5f7c728f5d284929a1cccb5bc19884422bfe6ef4d6c409da2c41838983fcf"
+
 [[package]]
 name = "ryu"
 version = "1.0.9"
@@ -984,13 +998,32 @@ version = "0.4.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "dcb5ae327f9cc13b68763b5749770cb9e048a99bd9dfdfa58d0cf05d5f64afe0"
 dependencies = [
- "heck",
+ "heck 0.3.3",
  "proc-macro-error",
  "proc-macro2",
  "quote",
  "syn",
 ]
 
+[[package]]
+name = "strum"
+version = "0.24.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "063e6045c0e62079840579a7e47a355ae92f60eb74daaf156fb1e84ba164e63f"
+
+[[package]]
+name = "strum_macros"
+version = "0.24.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6878079b17446e4d3eba6192bb0a2950d5b14f0ed8424b852310e5a94345d0ef"
+dependencies = [
+ "heck 0.4.0",
+ "proc-macro2",
+ "quote",
+ "rustversion",
+ "syn",
+]
+
 [[package]]
 name = "syn"
 version = "1.0.91"

kani-compiler/Cargo.toml

@@ -22,6 +22,8 @@ object = { version = "0.27.0", default-features = false, features = ["std", "rea
 rustc-demangle = { version = "0.1.21", optional = true }
 serde = { version = "1", optional = true }
 serde_json = { version = "1", optional = true }
+strum = {version = "0.24.0", optional = true}
+strum_macros = {version = "0.24.0", optional = true}
 shell-words = "1.0.0"
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
@@ -30,7 +32,8 @@ tracing-tree = "0.2.0"
 # Future proofing: enable backend dependencies using feature.
 [features]
 default = ['cprover']
-cprover = ['ar', 'bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'object', 'rustc-demangle', 'serde', 'serde_json']
+cprover = ['ar', 'bitflags', 'cbmc', 'kani_metadata', 'libc', 'num', 'object', 'rustc-demangle', 'serde',
+    'serde_json', "strum", "strum_macros"]
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

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

@@ -4,23 +4,27 @@
 //! 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::convert::AsRef;
+use strum_macros::{AsRefStr, EnumString};
 
 /// The Property Class enum stores all viable options for classifying asserts, cover assume and other related statements
-#[derive(Debug, Clone)]
-#[allow(dead_code)]
+#[derive(Debug, Clone, EnumString, AsRefStr)]
+#[strum(serialize_all = "snake_case")]
 pub enum PropertyClass {
     ArithmeticOverflow,
-    AssertFalse,
     Assume,
     Cover,
-    CustomProperty(String),
-    DefaultAssertion,
+    /// Assertions and Panic that are not specific to Kani. In a concrete execution, we expect
+    /// these assertions to be available to the user.
+    /// E.g.: User assertions, compiler invariant checks
+    Assertion,
     ExactDiv,
     ExpectFail,
     FiniteCheck,
-    /// Checks added by Kani compiler to detect UB or unstable behavior.
-    KaniCheck,
-    PointerOffset,
+    /// Checks added by Kani compiler to detect safety conditions violation.
+    /// E.g., things that trigger UB or unstable behavior.
+    SafetyCheck,
+    /// Checks to ensure that Kani's code generation is correct.
     SanityCheck,
     Unimplemented,
     UnsupportedConstruct,
@@ -30,43 +34,7 @@ pub enum PropertyClass {
 #[allow(dead_code)]
 impl PropertyClass {
     pub fn as_str(&self) -> &str {
-        match self {
-            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::KaniCheck => "kani_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,
-            "kani_check" => PropertyClass::KaniCheck,
-            "pointer_offset" => PropertyClass::PointerOffset,
-            "sanity_check" => PropertyClass::SanityCheck,
-            "unimplemented" => PropertyClass::Unimplemented,
-            "unreachable" => PropertyClass::Unreachable,
-            "unsupported_construct" => PropertyClass::UnsupportedConstruct,
-            _ => PropertyClass::CustomProperty(input.to_owned()),
-        }
+        self.as_ref()
     }
 }
 

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

@@ -106,14 +106,12 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!("codegen_never_return_intrinsic:\n\tinstance {:?}\n\tspan {:?}", instance, span);
 
         match intrinsic {
-            "abort" => self.codegen_fatal_error(
-                PropertyClass::DefaultAssertion,
-                "reached intrinsic::abort",
-                span,
-            ),
+            "abort" => {
+                self.codegen_fatal_error(PropertyClass::Assertion, "reached intrinsic::abort", span)
+            }
             // Transmuting to an uninhabited type is UB.
             "transmute" => self.codegen_fatal_error(
-                PropertyClass::DefaultAssertion,
+                PropertyClass::SafetyCheck,
                 "transmuting to uninhabited type has undefined behavior",
                 span,
             ),
@@ -763,7 +761,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // precise error message
         if layout.abi.is_uninhabited() {
             return self.codegen_fatal_error(
-                PropertyClass::DefaultAssertion,
+                PropertyClass::SafetyCheck,
                 &format!("attempted to instantiate uninhabited type `{}`", ty),
                 span,
             );
@@ -775,7 +773,7 @@ impl<'tcx> GotocCtx<'tcx> {
             && !layout.might_permit_raw_init(self, InitKind::Zero, false)
         {
             return self.codegen_fatal_error(
-                PropertyClass::DefaultAssertion,
+                PropertyClass::SafetyCheck,
                 &format!("attempted to zero-initialize type `{}`, which is invalid", ty),
                 span,
             );
@@ -785,7 +783,7 @@ impl<'tcx> GotocCtx<'tcx> {
             && !layout.might_permit_raw_init(self, InitKind::Uninit, false)
         {
             return self.codegen_fatal_error(
-                PropertyClass::DefaultAssertion,
+                PropertyClass::SafetyCheck,
                 &format!("attempted to leave type `{}` uninitialized, which is invalid", ty),
                 span,
             );
@@ -928,14 +926,14 @@ impl<'tcx> GotocCtx<'tcx> {
         let src_align = self.is_ptr_aligned(farg_types[0], src.clone());
         let src_align_check = self.codegen_assert(
             src_align,
-            PropertyClass::DefaultAssertion,
+            PropertyClass::SafetyCheck,
             "`src` must be properly aligned",
             loc,
         );
         let dst_align = self.is_ptr_aligned(farg_types[1], dst.clone());
         let dst_align_check = self.codegen_assert(
             dst_align,
-            PropertyClass::DefaultAssertion,
+            PropertyClass::SafetyCheck,
             "`dst` must be properly aligned",
             loc,
         );
@@ -1061,7 +1059,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let non_negative_check = self.codegen_assert_assume(
             offset_overflow.result.is_non_negative(),
-            PropertyClass::KaniCheck,
+            PropertyClass::SafetyCheck,
             "attempt to compute unsigned offset with negative distance",
             loc,
         );
@@ -1341,7 +1339,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let align = self.is_ptr_aligned(dst_typ, dst.clone());
         let align_check = self.codegen_assert(
             align,
-            PropertyClass::DefaultAssertion,
+            PropertyClass::SafetyCheck,
             "`dst` must be properly aligned",
             loc,
         );
@@ -1372,7 +1370,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let align = self.is_ptr_aligned(dst_typ, dst.clone());
         let align_check = self.codegen_assert(
             align,
-            PropertyClass::DefaultAssertion,
+            PropertyClass::SafetyCheck,
             "`dst` must be properly aligned",
             loc,
         );

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

@@ -51,7 +51,7 @@ impl<'tcx> GotocCtx<'tcx> {
             let ret_type = Type::Bool;
             let body = vec![
                 self.codegen_assert_false(
-                    PropertyClass::KaniCheck,
+                    PropertyClass::SafetyCheck,
                     format!("Reached unstable vtable comparison '{:?}'", op).as_str(),
                     loc,
                 ),

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

@@ -124,7 +124,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             None,
                             loc,
                         ),
-                        self.codegen_assert_false(PropertyClass::DefaultAssertion, &msg_str, loc),
+                        self.codegen_assert_false(PropertyClass::Assertion, &msg_str, loc),
                         Stmt::goto(self.current_fn().find_label(target), loc),
                     ],
                     loc,
@@ -496,7 +496,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let call_is_nonnull = fn_ptr.clone().is_nonnull();
         let assert_msg = format!("Non-null virtual function call for {:?}", vtable_field_name);
         let assert_nonnull =
-            self.codegen_assert(call_is_nonnull, PropertyClass::DefaultAssertion, &assert_msg, loc);
+            self.codegen_assert(call_is_nonnull, PropertyClass::SanityCheck, &assert_msg, loc);
 
         // Virtual function call and corresponding nonnull assertion.
         let call = fn_ptr.dereference().call(fargs.to_vec());
@@ -530,7 +530,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "This is a placeholder message; Kani doesn't support message formatted at runtime",
         ));
 
-        self.codegen_fatal_error(PropertyClass::DefaultAssertion, &msg, span)
+        self.codegen_fatal_error(PropertyClass::Assertion, &msg, span)
     }
 
     // Generate code for fatal error which should trigger an assertion failure and abort the

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

@@ -168,7 +168,7 @@ impl<'tcx> GotocHook<'tcx> for Assert {
             vec![
                 reach_stmt,
                 Stmt::decl(tmp.clone(), Some(cond), caller_loc),
-                tcx.codegen_assert(tmp.clone(), PropertyClass::DefaultAssertion, &msg, caller_loc),
+                tcx.codegen_assert(tmp.clone(), PropertyClass::Assertion, &msg, caller_loc),
                 Stmt::assume(tmp, caller_loc),
                 Stmt::goto(tcx.current_fn().find_label(&target), caller_loc),
             ],