Allow cloned reachability checks

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

@@ -186,7 +186,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 {
                     Stmt::goto_with_loop_inv(
                         bb_label(*target),
-                        self.loop_contracts_ctx.extract_block(),
+                        self.loop_contracts_ctx.extract_block(loc),
                         loc,
                     )
                 } else {

kani-compiler/src/codegen_cprover_gotoc/context/loop_contracts_ctx.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::codegen_cprover_gotoc::codegen::bb_label;
-use cbmc::goto_program::{CIntType, Expr, Stmt, StmtBody, Type};
+use cbmc::goto_program::{CIntType, Expr, Location, Stmt, StmtBody, Type};
 use stable_mir::mir::BasicBlockIdx;
 use std::collections::HashSet;
 
@@ -73,7 +73,7 @@ impl LoopContractsCtx {
 impl LoopContractsCtx {
     /// Returns the current block as a statement expression.
     /// Exit loop latch block.
-    pub fn extract_block(&mut self) -> Expr {
+    pub fn extract_block(&mut self, loc: Location) -> Expr {
         assert!(self.loop_invariant_lhs.is_some());
         self.stage = LoopContractsStage::UserCode;
         self.invariants_block.push(self.loop_invariant_lhs.as_ref().unwrap().clone());
@@ -85,6 +85,7 @@ impl LoopContractsCtx {
         Expr::statement_expression(
             std::mem::take(&mut self.invariants_block),
             Type::CInteger(CIntType::Bool),
+            loc,
         )
         .cast_to(Type::bool())
         .and(Expr::bool_true())

kani-driver/src/call_goto_instrument.rs

@@ -39,6 +39,15 @@ impl KaniSession {
 
         self.instrument_contracts(harness, output)?;
 
+        if self
+            .args
+            .common_args
+            .unstable_features
+            .contains(kani_metadata::UnstableFeature::LoopContracts)
+        {
+            self.instrument_loop_contracts(output)?;
+        }
+
         if self.args.checks.undefined_function_on() {
             self.add_library(output)?;
             self.undefined_functions(output)?;
@@ -183,6 +192,18 @@ impl KaniSession {
         self.call_goto_instrument(&args)
     }
 
+    /// Apply annotated loop contracts.
+    pub fn instrument_loop_contracts(&self, file: &Path) -> Result<()> {
+        let args: Vec<OsString> = vec![
+            "--apply-loop-contracts".into(),
+            "--loop-contracts-no-unwind".into(),
+            "--disable-loop-contracts-side-effect-check".into(),
+            file.into(),
+            file.into(),
+        ];
+        self.call_goto_instrument(&args)
+    }
+
     /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table
     ///
     /// Currently, only top-level function names and (most) type names are demangled.

kani-driver/src/cbmc_property_renderer.rs

@@ -815,7 +815,7 @@ fn annotate_properties_with_reach_results(
     mut properties: Vec<Property>,
     reach_checks: Vec<Property>,
 ) -> Vec<Property> {
-    let mut reach_map: HashMap<String, CheckStatus> = HashMap::new();
+    let mut reach_map: HashMap<String, Vec<CheckStatus>> = HashMap::new();
     let reach_desc_pat = Regex::new("KANI_CHECK_ID_.*_([0-9])*").unwrap();
     // Collect data (ID, status) from reachability checks
     for reach_check in reach_checks {
@@ -826,8 +826,7 @@ fn annotate_properties_with_reach_results(
         let check_id_str = format!("[{check_id}]");
         // Get the status and insert into `reach_map`
         let status = reach_check.status;
-        let res_ins = reach_map.insert(check_id_str, status);
-        assert!(res_ins.is_none());
+        reach_map.entry(check_id_str).or_insert(Vec::new()).push(status);
     }
 
     for prop in properties.iter_mut() {
@@ -841,7 +840,14 @@ fn annotate_properties_with_reach_results(
             let reach_status_opt = reach_map.get(prop_match_id);
             // Update the reachability status of the property
             if let Some(reach_status) = reach_status_opt {
-                prop.reach = Some(*reach_status);
+                for status in reach_status {
+                    if prop.reach.is_none()
+                        || prop.reach.unwrap() == CheckStatus::Satisfied
+                        || prop.reach.unwrap() == CheckStatus::Success
+                    {
+                        prop.reach = Some(*status);
+                    }
+                }
             }
         }
     }

tests/ui/loop_contracts/small_slice_eq/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/ui/loop_contracts/small_slice_eq/small_slcie_eq.rs

@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts --keep-temps --enable-unstable --cbmc-args --arrays-uf-always --no-standard-checks
+
+// Check if loop contracts are correctly applied.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+#![feature(ptr_sub_ptr)]
+unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
+    debug_assert_eq!(x.len(), y.len());
+    unsafe {
+        let (mut px, mut py) = (x.as_ptr(), y.as_ptr());
+        let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4));
+        #[kani::loop_invariant( px as isize >= x.as_ptr() as isize 
+        && py as isize >= y.as_ptr() as isize
+        && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))]
+        while px < pxend {
+            let vx = (px as *const u32).read_unaligned();
+            let vy = (py as *const u32).read_unaligned();
+            if vx != vy {
+                return false;
+            }
+            px = px.add(4);
+            py = py.add(4);
+        };
+        let vx = (pxend as *const u32).read_unaligned();
+        let vy = (pyend as *const u32).read_unaligned();
+        vx == vy
+    }
+}
+#[kani::proof]
+fn main() {
+    let mut a = [1;2000];
+    let mut b = [1;2000];
+    unsafe{
+    small_slice_eq(&mut a, &mut b);
+    }
+}