modifies Clauses for Function Contracts (#2800)

Extends the function contract functionality with a `modifies` clause. 

The design is different from #2594 but serves a similar purpose. The
`modifies` clause allows the user to specify which parts of a structure
a function may assign to. Essentially refining the `mut` annotation.

We allow arbitrary (side-effect free) expressions in the `modifies`
clause. The expressions are evaluated as part of the preconditions and
passed to the function-under-verification as additional arguments. CBMC
is then instructed to check that those locations are assigned. Aliasing
means that this also adds the location in the original structure to the
write set.

Each expression must return a pointer to a value that implements
`Arbitrary`. On replacement we then simply assign `*ptr = kani::any()`,
relying again on aliasing to update the original structure.

Additional tests for the new functionality are provided.

Resolves #2594 

## Open Questions

### API divergence from CBMC (accepted)

The current design goes roughly as follows: We start with a `modifies`
annotation on a function

```rs
#[modifies(obj.some_expr())]
fn target(obj: ...) { ... }
```

And from this we generate code to the effect of (simplified here)

```rs
fn target_check(obj: ...) {
    // Undo the lifetime entanglements
    let modified_1 = std::mem::transmute::<&'a _, &'b _>(obj.some_expr());
    target_wrapper(obj, modified_1);
}

#[cbmc::assigns(*modified_1)]
fn target_wrapper(obj: ..., modified_1: &impl kani::Arbitrary) { ... }
```

Unlike CBMC we expect `obj.some_expr()` to be of a **pointer type**
(`*const`, `*mut`, `&mut` or `&`) that points to the object which is
target of the modification. So if we had a `t : &mut T` that was
modified, CBMC would expect its assigns clause to say `*t`, but we
expect `t` (no dereference).

The reason is that the code we generate uses the workaround of creating
an alias to whichever part of `obj` is modified and registers the alias
with CBMC (thereby registering the original also). If we generated code
where the right side of `let modified_1 =` is not of pointer type, then
the object is moved to the stack and the aliasing destroyed.

The open questions is whether we are happy with this change in API.
(Yes)

### Test cases when expressions are used in the clause.

With more complex expressions in the modifies clause it becomes hard to
define good test cases because they reference generated code as in this
case:

```rs
#[kani::requires(**ptr < 100)]
#[kani::modifies(ptr.as_ref())]
fn modify(ptr: &mut Box<u32>) {
    *ptr.as_mut() += 1;
}
```

This passes (as it should) and when commenting out the `modifies` clause
we get this error:

```
Check 56: modify_wrapper_895c4e.assigns.2
	 - Status: FAILURE
	 - Description: "Check that *var_2 is assignable"
	 - Location: assigns_expr_pass.rs:8:5 in function modify_wrapper_895c4e
```

The information in this error is very non-specific, hard to read and
brittle. How should we define robust "expected" test cases for such
errors?

### Corner Cases / Future Improvements

- #2907 
- #2908 
- #2909 

## TODOs

- [ ] Test Cases where the clause contains
  - [x] `Rc` + (`RefCell` or `unsafe`) (see #2907)
  - [x] Fields
  - [x] Statement expressions
  - [x] `Vec` (see #2909)
  - [ ] Fat pointers
- [ ] update contracts documentation
- [x] Make sure the wrapper arguments are unique.
- [x] Ensure `nondet-static-exclude` always uses the correct filepath
(relative or absolute)
- [ ] Test case for multiple `modifies` clauses.

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

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

cprover_bindings/src/goto_program/mod.rs

@@ -22,6 +22,6 @@ pub use expr::{
 };
 pub use location::Location;
 pub use stmt::{Stmt, StmtBody, SwitchCase};
-pub use symbol::{Symbol, SymbolValues};
+pub use symbol::{FunctionContract, Lambda, Symbol, SymbolValues};
 pub use symbol_table::SymbolTable;
 pub use typ::{CIntType, DatatypeComponent, Parameter, Type};

cprover_bindings/src/goto_program/symbol.rs

@@ -13,6 +13,8 @@ pub struct Symbol {
     pub location: Location,
     pub typ: Type,
     pub value: SymbolValues,
+    /// Contracts to be enforced (only supported for functions)
+    pub contract: Option<Box<FunctionContract>>,
 
     /// Optional debugging information
 
@@ -44,6 +46,57 @@ pub struct Symbol {
     pub is_weak: bool,
 }
 
+/// The equivalent of a "mathematical function" in CBMC. Semantically this is an
+/// anonymous function object, similar to a closure, but without closing over an
+/// environment.
+///
+/// This is only valid for use as a function contract. It may not perform side
+/// effects, a property that is enforced on the CBMC side.
+///
+/// The precise nomenclature is that in CBMC a contract value has *type*
+/// `mathematical_function` and values of that type are `lambda`s. Since this
+/// struct represents such values it is named `Lambda`.
+#[derive(Debug, Clone)]
+pub struct Lambda {
+    pub arguments: Vec<Parameter>,
+    pub body: Expr,
+}
+
+impl Lambda {
+    pub fn as_contract_for(
+        fn_ty: &Type,
+        return_var_name: Option<InternedString>,
+        body: Expr,
+    ) -> Self {
+        let arguments = match fn_ty {
+            Type::Code { parameters, return_type } => {
+                [Parameter::new(None, return_var_name, (**return_type).clone())]
+                    .into_iter()
+                    .chain(parameters.iter().cloned())
+                    .collect()
+            }
+            _ => panic!(
+                "Contract lambdas can only be generated for `Code` types, received {fn_ty:?}"
+            ),
+        };
+        Self { arguments, body }
+    }
+}
+
+/// The CBMC representation of a function contract. Represents
+/// https://diffblue.github.io/cbmc/contracts-user.html but currently only assigns clauses are
+/// supported.
+#[derive(Clone, Debug)]
+pub struct FunctionContract {
+    pub(crate) assigns: Vec<Lambda>,
+}
+
+impl FunctionContract {
+    pub fn new(assigns: Vec<Lambda>) -> Self {
+        Self { assigns }
+    }
+}
+
 /// Currently, only C is understood by CBMC.
 // TODO: <https://github.com/model-checking/kani/issues/1>
 #[derive(Clone, Debug)]
@@ -84,6 +137,7 @@ impl Symbol {
             base_name,
             pretty_name,
 
+            contract: None,
             module: None,
             mode: SymbolModes::C,
             // global properties
@@ -107,6 +161,18 @@ impl Symbol {
         }
     }
 
+    /// Add this contract to the symbol (symbol must be a function) or fold the
+    /// conditions into an existing contract.
+    pub fn attach_contract(&mut self, contract: FunctionContract) {
+        assert!(self.typ.is_code());
+        match self.contract {
+            Some(ref mut prior) => {
+                prior.assigns.extend(contract.assigns);
+            }
+            None => self.contract = Some(Box::new(contract)),
+        }
+    }
+
     /// The symbol that defines the type of the struct or union.
     /// For a struct foo this is the symbol "tag-foo" that maps to the type struct foo.
     pub fn aggr_ty<T: Into<InternedString>>(t: Type, pretty_name: T) -> Symbol {
@@ -319,6 +385,12 @@ impl Symbol {
         self.is_auxiliary = hidden;
         self
     }
+
+    /// Set `is_property`.
+    pub fn with_is_property(mut self, v: bool) -> Self {
+        self.is_property = v;
+        self
+    }
 }
 
 /// Predicates

cprover_bindings/src/goto_program/symbol_table.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::super::{env, MachineModel};
-use super::{BuiltinFn, Stmt, Symbol};
+use super::{BuiltinFn, FunctionContract, Stmt, Symbol};
 use crate::InternedString;
 use std::collections::BTreeMap;
 /// This is a typesafe implementation of the CBMC symbol table, based on the CBMC code at:
@@ -79,6 +79,17 @@ impl SymbolTable {
         let name = name.into();
         self.symbol_table.get_mut(&name).unwrap().update_fn_declaration_with_definition(body);
     }
+
+    /// Attach a contract to the symbol identified by `name`. If a prior
+    /// contract exists it is extended with additional clauses.
+    pub fn attach_contract<T: Into<InternedString>>(
+        &mut self,
+        name: T,
+        contract: FunctionContract,
+    ) {
+        let sym = self.symbol_table.get_mut(&name.into()).unwrap();
+        sym.attach_contract(contract);
+    }
 }
 
 /// Getters

cprover_bindings/src/goto_program/typ.rs

@@ -228,6 +228,17 @@ impl Parameter {
     }
 }
 
+/// Constructor
+impl Parameter {
+    pub fn new<S: Into<InternedString>>(
+        base_name: Option<S>,
+        identifier: Option<S>,
+        typ: Type,
+    ) -> Self {
+        Self { base_name: base_name.map(Into::into), identifier: identifier.map(Into::into), typ }
+    }
+}
+
 impl CIntType {
     pub fn sizeof_in_bits(&self, st: &SymbolTable) -> u64 {
         match self {

cprover_bindings/src/irep/irep.rs

@@ -6,6 +6,7 @@ use super::super::goto_program::{Location, Type};
 use super::super::MachineModel;
 use super::{IrepId, ToIrep};
 use crate::cbmc_string::InternedString;
+use crate::linear_map;
 use linear_map::LinearMap;
 use num::BigInt;
 use std::fmt::Debug;
@@ -141,4 +142,12 @@ impl Irep {
     pub fn zero() -> Irep {
         Irep::just_id(IrepId::Id0)
     }
+
+    pub fn tuple(sub: Vec<Irep>) -> Self {
+        Irep {
+            id: IrepId::Tuple,
+            sub,
+            named_sub: linear_map![(IrepId::Type, Irep::just_id(IrepId::Tuple))],
+        }
+    }
 }

cprover_bindings/src/irep/irep_id.rs

@@ -593,6 +593,7 @@ pub enum IrepId {
     CSpecLoopInvariant,
     CSpecRequires,
     CSpecEnsures,
+    CSpecAssigns,
     VirtualFunction,
     ElementType,
     WorkingDirectory,
@@ -1462,6 +1463,7 @@ impl ToString for IrepId {
             IrepId::CSpecLoopInvariant => "#spec_loop_invariant",
             IrepId::CSpecRequires => "#spec_requires",
             IrepId::CSpecEnsures => "#spec_ensures",
+            IrepId::CSpecAssigns => "#spec_assigns",
             IrepId::VirtualFunction => "virtual_function",
             IrepId::ElementType => "element_type",
             IrepId::WorkingDirectory => "working_directory",

cprover_bindings/src/irep/to_irep.rs

@@ -6,8 +6,9 @@ use super::super::goto_program;
 use super::super::MachineModel;
 use super::{Irep, IrepId};
 use crate::linear_map;
+use crate::InternedString;
 use goto_program::{
-    BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter,
+    BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Lambda, Location, Parameter,
     SelfOperator, Stmt, StmtBody, SwitchCase, SymbolValues, Type, UnaryOperator,
 };
 
@@ -16,10 +17,10 @@ pub trait ToIrep {
 }
 
 /// Utility functions
-fn arguments_irep(arguments: &[Expr], mm: &MachineModel) -> Irep {
+fn arguments_irep<'a>(arguments: impl Iterator<Item = &'a Expr>, mm: &MachineModel) -> Irep {
     Irep {
         id: IrepId::Arguments,
-        sub: arguments.iter().map(|x| x.to_irep(mm)).collect(),
+        sub: arguments.map(|x| x.to_irep(mm)).collect(),
         named_sub: linear_map![],
     }
 }
@@ -169,6 +170,16 @@ impl ToIrep for Expr {
     }
 }
 
+impl Irep {
+    pub fn symbol(identifier: InternedString) -> Self {
+        Irep {
+            id: IrepId::Symbol,
+            sub: vec![],
+            named_sub: linear_map![(IrepId::Identifier, Irep::just_string_id(identifier))],
+        }
+    }
+}
+
 impl ToIrep for ExprValue {
     fn to_irep(&self, mm: &MachineModel) -> Irep {
         match self {
@@ -245,7 +256,7 @@ impl ToIrep for ExprValue {
             }
             ExprValue::FunctionCall { function, arguments } => side_effect_irep(
                 IrepId::FunctionCall,
-                vec![function.to_irep(mm), arguments_irep(arguments, mm)],
+                vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
             ),
             ExprValue::If { c, t, e } => Irep {
                 id: IrepId::If,
@@ -297,14 +308,7 @@ impl ToIrep for ExprValue {
                 sub: values.iter().map(|x| x.to_irep(mm)).collect(),
                 named_sub: linear_map![],
             },
-            ExprValue::Symbol { identifier } => Irep {
-                id: IrepId::Symbol,
-                sub: vec![],
-                named_sub: linear_map![(
-                    IrepId::Identifier,
-                    Irep::just_string_id(identifier.to_string()),
-                )],
-            },
+            ExprValue::Symbol { identifier } => Irep::symbol(*identifier),
             ExprValue::Typecast(e) => {
                 Irep { id: IrepId::Typecast, sub: vec![e.to_irep(mm)], named_sub: linear_map![] }
             }
@@ -456,7 +460,7 @@ impl ToIrep for StmtBody {
                 vec![
                     lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)),
                     function.to_irep(mm),
-                    arguments_irep(arguments, mm),
+                    arguments_irep(arguments.iter(), mm),
                 ],
             ),
             StmtBody::Goto(dest) => code_irep(IrepId::Goto, vec![])
@@ -499,10 +503,50 @@ impl ToIrep for SwitchCase {
     }
 }
 
+impl ToIrep for Lambda {
+    /// At the moment this function assumes that this lambda is used for a
+    /// `modifies` contract. It should work for any other lambda body, but
+    /// the parameter names use "modifies" in their generated names.
+    fn to_irep(&self, mm: &MachineModel) -> Irep {
+        let (ops_ireps, types) = self
+            .arguments
+            .iter()
+            .enumerate()
+            .map(|(index, param)| {
+                let ty_rep = param.typ().to_irep(mm);
+                (
+                    Irep::symbol(
+                        param.identifier().unwrap_or_else(|| format!("_modifies_{index}").into()),
+                    )
+                    .with_named_sub(IrepId::Type, ty_rep.clone()),
+                    ty_rep,
+                )
+            })
+            .unzip();
+        let typ = Irep {
+            id: IrepId::MathematicalFunction,
+            sub: vec![Irep::just_sub(types), self.body.typ().to_irep(mm)],
+            named_sub: Default::default(),
+        };
+        Irep {
+            id: IrepId::Lambda,
+            sub: vec![Irep::tuple(ops_ireps), self.body.to_irep(mm)],
+            named_sub: linear_map!((IrepId::Type, typ)),
+        }
+    }
+}
+
 impl goto_program::Symbol {
     pub fn to_irep(&self, mm: &MachineModel) -> super::Symbol {
+        let mut typ = self.typ.to_irep(mm);
+        if let Some(contract) = &self.contract {
+            typ = typ.with_named_sub(
+                IrepId::CSpecAssigns,
+                Irep::just_sub(contract.assigns.iter().map(|req| req.to_irep(mm)).collect()),
+            );
+        }
         super::Symbol {
-            typ: self.typ.to_irep(mm),
+            typ,
             value: match &self.value {
                 SymbolValues::Expr(e) => e.to_irep(mm),
                 SymbolValues::Stmt(s) => s.to_irep(mm),