modifies Clauses for Function Contracts

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),