Add support for loop assigns in loop contracts

cprover_bindings/src/goto_program/stmt.rs

@@ -87,6 +87,7 @@ pub enum StmtBody {
         // 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>,
+        loop_modifies: Option<Vec<Expr>>,
     },
     /// `if (i) { t } else { e }`
     Ifthenelse {
@@ -288,7 +289,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, loop_invariants: None }, loc)
+        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None }, loc)
     }
 
     /// `if (i) { t } else { e }` or `if (i) { t }`
@@ -333,13 +334,36 @@ impl Stmt {
 
     /// `goto dest;` with loop invariant
     pub fn with_loop_contracts(self, inv: Expr) -> Self {
-        if let Goto { dest, loop_invariants } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
             assert!(loop_invariants.is_none());
-            stmt!(Goto { dest: *dest, loop_invariants: Some(inv) }, *self.location())
+            stmt!(
+                Goto {
+                    dest: *dest,
+                    loop_invariants: Some(inv),
+                    loop_modifies: loop_modifies.clone()
+                },
+                *self.location()
+            )
         } else {
             unreachable!("Loop contracts should be annotated only to goto stmt")
         }
     }
+
+    pub fn with_loop_modifies(self, asg: Vec<Expr>) -> Self {
+        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+            assert!(loop_modifies.is_none());
+            stmt!(
+                Goto {
+                    dest: *dest,
+                    loop_invariants: loop_invariants.clone(),
+                    loop_modifies: Some(asg)
+                },
+                *self.location()
+            )
+        } else {
+            unreachable!("Loop assigns should be annotated only to goto stmt")
+        }
+    }
 }
 
 /// Predicates

cprover_bindings/src/irep/to_irep.rs

@@ -548,17 +548,19 @@ impl ToIrep for StmtBody {
                     arguments_irep(arguments.iter(), mm),
                 ],
             ),
-            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::Goto { dest, loop_invariants, loop_modifies } => {
+                let inv = loop_invariants
+                    .clone()
+                    .map(|inv| inv.clone().and(Expr::bool_true()).to_irep(mm));
+                let assigns = loop_modifies.clone().map(|assigns| {
+                    Irep::just_sub(vec![Irep::just_sub(
+                        assigns.iter().map(|assign| assign.to_irep(mm)).collect(),
+                    )])
+                });
+                code_irep(IrepId::Goto, vec![])
+                    .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()))
+                    .with_named_sub_option(IrepId::CSpecLoopInvariant, inv)
+                    .with_named_sub_option(IrepId::CSpecAssigns, assigns.clone())
             }
             StmtBody::Ifthenelse { i, t, e } => code_irep(
                 IrepId::Ifthenelse,

docs/src/reference/experimental/loop-contracts.md

@@ -61,7 +61,7 @@ Check 10: simple_loop_with_loop_contracts.loop_invariant_base.1
          - Description: "Check invariant before entry for loop simple_loop_with_loop_contracts.0"
          - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts
 
-Check 11: simple_loop_with_loop_contracts.loop_assigns.1
+Check 11: simple_loop_with_loop_contracts.loop_modifies.1
          - Status: SUCCESS
          - Description: "Check assigns clause inclusion for loop simple_loop_with_loop_contracts.0"
          - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts
@@ -164,6 +164,69 @@ fn contract_proof() {
 
 When loop contracts and function contracts are both enabled (by flags `-Z loop-contracts -Z function-contracts`), 
 Kani automatically contracts (instead of unwinds) all loops in the functions that we want to prove contracts for.
+
+## Loop modifies clauses: 
+We allow users to manually specified the `loop_modifies` clauses for memory allocated addresses which can be modified inside the loop body.
+The concept is very similar to the `__CPROVER_assigns` clause of CBMC (https://diffblue.github.io/cbmc/contracts-assigns.html).
+However, in Kani, the CBMC target is replaced by three Rust types which can be used in the `loop_modifies` clauses:
+1. `RawPtr`: We don't allow variable names as targets. Users must use pointers to them instead, which also allows checking modification using borrowed references and aliases.
+```Rust
+#[kani::proof]
+fn main() {
+    let mut i = 0;
+    #[kani::loop_invariant(i <= 20)]
+    #[kani::loop_modifies(&i as *const _)]
+    while i < 20 {
+        i = i + 1;
+    }
+}
+```
+2. `Reference`: Similar to RawPtr, but we also can use it to replace  `__CPROVER_object_whole(ptr-expr)`,
+Example 
+```Rust
+#[kani::proof]
+fn main() {
+    let mut i = 0;
+    let mut a: [u8; 20] = kani::any();
+    #[kani::loop_invariant(i <= 20)]
+    #[kani::loop_modifies(&i, &a)]
+    while i < 20 {
+        a[i] = 1;
+        i = i + 1;
+    }
+}
+```
+3. `FatPtr (Slice)`: We use this to replace `__CPROVER_object_from(ptr-expr)`, and `__CPROVER_object_upto(ptr-expr, uint-expr)`.
+```Rust
+#[kani::proof]
+fn main() {
+    let mut i = 3;
+    let mut a: [u8; 100] = kani::any();
+    #[kani::loop_invariant(i >=3 && i <= 20)]
+    #[kani::loop_modifies(&i , &a[3..20])]
+    while i < 20 {
+        a[i] = 1;
+        i = i + 1;
+    }
+}
+```
+or
+
+```Rust
+use std::ptr::slice_from_raw_parts;
+#[kani::proof]
+fn main() {
+    let mut i = 0;
+    let mut a: [u8; 100] = kani::any();
+    #[kani::loop_invariant(i <= 20)]
+    #[kani::loop_modifies(&i , slice_from_raw_parts(a.as_ptr(), 20))]
+    while i < 20 {
+        a[i] = 1;
+        i = i + 1;
+    }
+}
+```
+
 ## Limitations
 
 Loop contracts comes with the following limitations.

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

@@ -6,6 +6,7 @@ use super::{PropertyClass, bb_label};
 use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
+use cbmc::goto_program::ExprValue;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use rustc_abi::Size;
 use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
@@ -17,12 +18,66 @@ use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::{
     AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
-    RETURN_LOCAL, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
+    RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
 use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
 
 impl GotocCtx<'_> {
+    pub fn ty_to_assign_target(&self, ty: Ty, expr: &Expr) -> Expr {
+        match ty.kind() {
+            TyKind::RigidTy(RigidTy::Ref(_, unref_ty, _))
+            | TyKind::RigidTy(RigidTy::RawPtr(unref_ty, _)) => match unref_ty.kind() {
+                TyKind::RigidTy(RigidTy::Slice(slice_ty)) => {
+                    let size = slice_ty.layout().unwrap().shape().size.bytes();
+                    Expr::symbol_expression(
+                        "__CPROVER_object_upto",
+                        Type::code(
+                            vec![
+                                Type::empty().to_pointer().as_parameter(None, Some("ptr".into())),
+                                Type::size_t().as_parameter(None, Some("size".into())),
+                            ],
+                            Type::empty(),
+                        ),
+                    )
+                    .call(vec![
+                        expr.clone()
+                            .member("data", &self.symbol_table)
+                            .cast_to(Type::empty().to_pointer()),
+                        expr.clone()
+                            .member("len", &self.symbol_table)
+                            .mul(Expr::size_constant(size.try_into().unwrap(), &self.symbol_table)),
+                    ])
+                }
+                _ => expr.clone().dereference(),
+            },
+            _ => expr.clone().dereference(),
+        }
+    }
+
+    pub fn rvalue_to_assign_targets(&mut self, rvalue: &Rvalue, location: Location) -> Vec<Expr> {
+        let assigns = self.codegen_rvalue_stable(rvalue, location);
+        let assigns_value = assigns.value().clone();
+        let assign_exprs = if let ExprValue::Struct { values } = assigns_value {
+            values.clone()
+        } else {
+            vec![assigns.clone()]
+        };
+        match rvalue {
+            Rvalue::Aggregate(_agg_kind, operands) => {
+                let mut ptr_exprs = Vec::new();
+                for (operand, expr) in operands.iter().zip(assign_exprs.iter()) {
+                    let operand_ty = self.operand_ty_stable(operand);
+                    debug!("Ty {:?}", operand_ty);
+                    let ptr_expr = self.ty_to_assign_target(operand_ty, expr);
+                    ptr_exprs.push(ptr_expr)
+                }
+                ptr_exprs
+            }
+            _ => vec![assigns.dereference()],
+        }
+    }
+
     /// Generate Goto-C for MIR [Statement]s.
     /// This does not cover all possible "statements" because MIR distinguishes between ordinary
     /// statements and [Terminator]s, which can exclusively appear at the end of a basic block.
@@ -36,6 +91,12 @@ impl GotocCtx<'_> {
             StatementKind::Assign(lhs, rhs) => {
                 let lty = self.place_ty_stable(lhs);
                 let rty = self.rvalue_ty_stable(rhs);
+                let localname = self.codegen_var_name(&lhs.local);
+                if localname.contains("kani_loop_modifies") {
+                    let assigns = self.rvalue_to_assign_targets(rhs, location);
+                    self.current_loop_modifies = assigns.clone();
+                    return Stmt::skip(location);
+                }
                 // we ignore assignment for all zero size types
                 if self.is_zst_stable(lty) {
                     Stmt::skip(location)

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

@@ -78,6 +78,8 @@ pub struct GotocCtx<'tcx> {
     pub transformer: BodyTransformation,
     /// If there exist some usage of loop contracts int context.
     pub has_loop_contracts: bool,
+    /// Track loop assign clause
+    pub current_loop_modifies: Vec<Expr>,
 }
 
 /// Constructor
@@ -108,6 +110,7 @@ impl<'tcx> GotocCtx<'tcx> {
             concurrent_constructs: FxHashMap::default(),
             transformer,
             has_loop_contracts: false,
+            current_loop_modifies: Vec::new(),
         }
     }
 }

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

@@ -728,16 +728,22 @@ impl GotocHook for LoopInvariantRegister {
             // free(0)
             // goto target --- with loop contracts annotated.
 
+            let mut stmt = Stmt::goto(bb_label(target.unwrap()), loc)
+                .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)));
+            let assigns = gcx.current_loop_modifies.clone();
+            if !assigns.is_empty() {
+                stmt = stmt.with_loop_modifies(assigns.clone());
+                gcx.current_loop_modifies.clear();
+            }
+
             // Add `free(0)` to make sure the body of `free` won't be dropped to
             // satisfy the requirement of DFCC.
             Stmt::block(
                 vec![
                     BuiltinFn::Free
                         .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
                         .as_stmt(loc),
-                    Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts(
-                        func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
-                    ),
+                    stmt,
                 ],
                 loc,
             )

library/kani_macros/src/lib.rs

@@ -440,6 +440,10 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::loop_invariant(attr, item)
 }
 
+#[proc_macro_attribute]
+pub fn loop_modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
+    attr_impl::loop_modifies(attr, item)
+}
 /// This module implements Kani attributes in a way that only Kani's compiler can understand.
 /// This code should only be activated when pre-building Kani's sysroot.
 #[cfg(kani_sysroot)]
@@ -450,7 +454,7 @@ mod sysroot {
     mod loop_contracts;
 
     pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified};
-    pub use loop_contracts::loop_invariant;
+    pub use loop_contracts::{loop_invariant, loop_modifies};
 
     use super::*;
 
@@ -629,4 +633,5 @@ mod regular {
     no_op!(proof_for_contract);
     no_op!(stub_verified);
     no_op!(loop_invariant);
+    no_op!(loop_modifies);
 }

library/kani_macros/src/sysroot/loop_contracts/mod.rs

@@ -7,9 +7,13 @@
 use proc_macro::TokenStream;
 use proc_macro_error2::abort_call_site;
 use quote::{format_ident, quote};
+use syn::punctuated::Punctuated;
 use syn::spanned::Spanned;
 use syn::token::AndAnd;
-use syn::{BinOp, Block, Expr, ExprBinary, Ident, Stmt, parse_quote, visit_mut::VisitMut};
+use syn::{
+    BinOp, Block, Expr, ExprBinary, Ident, Stmt, Token, parse_macro_input, parse_quote,
+    visit_mut::VisitMut,
+};
 
 /*
     Transform the loop to support on_entry(expr) : the value of expr before entering the loop
@@ -389,3 +393,22 @@ fn generate_unique_id_from_span(stmt: &Stmt) -> String {
     // Create a tuple of location information (file path, start line, start column, end line, end column)
     format!("_{:?}_{:?}_{:?}_{:?}", start.line(), start.column(), end.line(), end.column())
 }
+
+pub fn loop_modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let assigns = parse_macro_input!(attr with Punctuated::<Expr, Token![,]>::parse_terminated)
+        .into_iter()
+        .collect::<Vec<Expr>>();
+    let loop_assign_name: String = "kani_loop_modifies".to_owned();
+    let loop_assign_ident = format_ident!("{}", loop_assign_name);
+    let loop_assign_stmt: Stmt = parse_quote! {
+        let #loop_assign_ident = (#(#assigns),*);
+    };
+    let loop_stmt: Stmt = syn::parse(item.clone()).unwrap();
+    let ret: TokenStream = quote!(
+    {
+        #loop_assign_stmt
+        #loop_stmt
+    })
+    .into();
+    ret
+}

tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected

@@ -0,0 +1,13 @@
+main.assigns.1\
+	 - Status: SUCCESS\
+	 - Description: "Check that a[var_15] is assignable"
+
+main.assigns.2\
+	 - Status: SUCCESS\
+	 - Description: "Check that i is assignable"
+
+main.loop_invariant_step.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant after step for loop main.0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check the use of loop_modifies for Rust's Fat ptr
+
+#![feature(proc_macro_hygiene)]
+#![feature(stmt_expr_attributes)]
+
+use std::ptr::slice_from_raw_parts;
+
+#[kani::proof]
+fn main() {
+    let mut i = 0;
+    let mut a: [u8; 100] = kani::any();
+    #[kani::loop_invariant(i <= 20)]
+    #[kani::loop_modifies(&i , slice_from_raw_parts(a.as_ptr(), 20))]
+    while i < 20 {
+        a[i] = 1;
+        i = i + 1;
+    }
+}