Add unstable option prove-safety-only (#4239)

Compute verification results under the assumption that no panic occurs.
This enables safety verification, i.e., proving the absence of undefined
behavior without being distracted by panics which Kani, otherwise, also
reports as verification failures. #4230 was an efforts towards the same
goal, but required manual annotation of the conditions under which a
panic may occur (and may hide undefined behavior when either the given
specifications are too broad or when undefined behavior arises on a path
to a panic).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

kani-compiler/src/args.rs

@@ -65,6 +65,10 @@ pub struct Arguments {
     /// Option used for suppressing global ASM error.
     #[clap(long)]
     pub ignore_global_asm: bool,
+    /// Compute verification results under the assumption that no panic occurs.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[clap(long)]
+    pub prove_safety_only: bool,
     /// Option name used to select which reachability analysis to perform.
     #[clap(long = "reachability", default_value = "none")]
     pub reachability_analysis: ReachabilityType,

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

@@ -133,11 +133,18 @@ impl GotocCtx<'_> {
         message: &str,
         loc: Location,
     ) -> Stmt {
-        let property_name = property_class.as_str();
-        Stmt::block(
-            vec![Stmt::assert(cond.clone(), property_name, message, loc), Stmt::assume(cond, loc)],
-            loc,
-        )
+        if property_class == PropertyClass::Assertion && self.queries.args().prove_safety_only {
+            Stmt::assume(cond, loc)
+        } else {
+            let property_name = property_class.as_str();
+            Stmt::block(
+                vec![
+                    Stmt::assert(cond.clone(), property_name, message, loc),
+                    Stmt::assume(cond, loc),
+                ],
+                loc,
+            )
+        }
     }
 
     /// Generate code to cover the given condition at the current location

kani-driver/src/args/mod.rs

@@ -330,6 +330,11 @@ pub struct VerificationArgs {
     #[arg(long, hide = true)]
     pub print_llbc: bool,
 
+    /// Compute verification results under the assumption that no panic occurs.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[arg(long, hide_short_help = true)]
+    pub prove_safety_only: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization
@@ -726,6 +731,12 @@ impl ValidateArgs for VerificationArgs {
                 UnstableFeature::FunctionContracts,
             )?;
 
+            self.common_args.check_unstable(
+                self.prove_safety_only,
+                "prove-safety-only",
+                UnstableFeature::UnstableOptions,
+            )?;
+
             Ok(())
         };
 

kani-driver/src/call_single_file.rs

@@ -175,6 +175,10 @@ impl KaniSession {
             flags.extend(args.into_iter().map(KaniArg::from));
         }
 
+        if self.args.prove_safety_only {
+            flags.push("--prove-safety-only".into());
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(KaniArg::from));
 
         flags

tests/kani/Panic/prove_safety_only.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z unstable-options --prove-safety-only
+//! Test that --prove-safety-only works
+
+#[kani::proof]
+fn div0() -> i32 {
+    let x: i32 = kani::any();
+    let y: i32 = kani::any();
+    x / y
+}
+
+#[kani::proof]
+fn assert_hides_ub() {
+    let arr: [u8; 5] = kani::any();
+    let mut bytes = kani::slice::any_slice_of_array(&arr);
+    let slice_offset = unsafe { bytes.as_ptr().offset_from(&arr as *const u8) };
+    let offset: usize = kani::any();
+    assert!(offset <= 4 && (slice_offset as usize) + offset <= 4);
+    let _ = unsafe { *bytes.as_ptr().add(offset) };
+}