Loop Contracts Annotation for While-Loop

cprover_bindings/src/goto_program/stmt.rs

@@ -82,7 +82,12 @@ pub enum StmtBody {
         arguments: Vec<Expr>,
     },
     /// `goto dest;`
-    Goto(InternedString),
+    Goto {
+        dest: InternedString,
+        // The loop invariants annotated to the goto, which can be
+        // applied as loop contracts in CBMC if it is a backward goto.
+        loop_invariants: Option<Expr>,
+    },
     /// `if (i) { t } else { e }`
     Ifthenelse {
         i: Expr,
@@ -179,7 +184,7 @@ impl Stmt {
         stmt!(Assign { lhs, rhs }, loc)
     }
 
-    /// `assert(cond, property_class, commment);`
+    /// `assert(cond, property_class, comment);`
     pub fn assert(cond: Expr, property_name: &str, message: &str, loc: Location) -> Self {
         assert!(cond.typ().is_bool());
         assert!(!property_name.is_empty() && !message.is_empty());
@@ -188,7 +193,7 @@ impl Stmt {
         let loc_with_property =
             Location::create_location_with_property(message, property_name, loc);
 
-        // Chose InternedString to seperate out codegen from the cprover_bindings logic
+        // Chose InternedString to separate out codegen from the cprover_bindings logic
         let property_class = property_name.intern();
         let msg = message.into();
 
@@ -283,7 +288,7 @@ impl Stmt {
     pub fn goto<T: Into<InternedString>>(dest: T, loc: Location) -> Self {
         let dest = dest.into();
         assert!(!dest.is_empty());
-        stmt!(Goto(dest), loc)
+        stmt!(Goto { dest, loop_invariants: None }, loc)
     }
 
     /// `if (i) { t } else { e }` or `if (i) { t }`
@@ -325,6 +330,16 @@ impl Stmt {
         assert!(!label.is_empty());
         stmt!(Label { label, body: self }, *self.location())
     }
+
+    /// `goto dest;` with loop invariant
+    pub fn with_loop_contracts(self, inv: Expr) -> Self {
+        if let Goto { dest, loop_invariants } = self.body() {
+            assert!(loop_invariants.is_none());
+            stmt!(Goto { dest: *dest, loop_invariants: Some(inv) }, *self.location())
+        } else {
+            unreachable!("Loop contracts should be annotated only to goto stmt")
+        }
+    }
 }
 
 /// Predicates

cprover_bindings/src/irep/to_irep.rs

@@ -516,8 +516,18 @@ impl ToIrep for StmtBody {
                     arguments_irep(arguments.iter(), mm),
                 ],
             ),
-            StmtBody::Goto(dest) => code_irep(IrepId::Goto, vec![])
-                .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())),
+            StmtBody::Goto { dest, loop_invariants } => {
+                let stmt_goto = code_irep(IrepId::Goto, vec![])
+                    .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()));
+                if let Some(inv) = loop_invariants {
+                    stmt_goto.with_named_sub(
+                        IrepId::CSpecLoopInvariant,
+                        inv.clone().and(Expr::bool_true()).to_irep(mm),
+                    )
+                } else {
+                    stmt_goto
+                }
+            }
             StmtBody::Ifthenelse { i, t, e } => code_irep(
                 IrepId::Ifthenelse,
                 vec![

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 super::loop_contracts_hooks::LoopInvariantRegister;
 use crate::codegen_cprover_gotoc::codegen::{bb_label, PropertyClass};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::matches_diagnostic as matches_function;
@@ -555,6 +556,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),
             Rc::new(InitContracts),
+            Rc::new(LoopInvariantRegister),
         ],
     }
 }

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

@@ -0,0 +1,37 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use super::hooks::GotocHook;
+use crate::codegen_cprover_gotoc::codegen::bb_label;
+use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle::attributes::KaniAttributes;
+use cbmc::goto_program::{CIntType, Expr, Stmt, Type};
+use rustc_middle::ty::TyCtxt;
+use rustc_span::Symbol;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{BasicBlockIdx, Place};
+use stable_mir::ty::Span;
+
+pub struct LoopInvariantRegister;
+
+impl GotocHook for LoopInvariantRegister {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        KaniAttributes::for_instance(tcx, instance).fn_marker()
+            == Some(Symbol::intern("kani_register_loop_contract"))
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        instance: Instance,
+        fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        let loc = gcx.codegen_span_stable(span);
+        let func_exp = gcx.codegen_func_expr(instance, loc);
+        Stmt::goto(bb_label(target.unwrap()), loc)
+            .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)))
+    }
+}

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

@@ -7,5 +7,6 @@
 //! Instead, we use a "hook" to generate the correct CBMC intrinsic.
 
 mod hooks;
+mod loop_contracts_hooks;
 
 pub use hooks::{fn_hooks, GotocHooks};