Support for requires and ensures clauses (#2555)

Co-authored-by: Celina G. Val <celinval@amazon.com>

cprover_bindings/src/goto_program/expr.rs

@@ -170,6 +170,22 @@ pub enum ExprValue {
     },
 }
 
+/// 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<(InternedString, Type)>,
+    pub body: Expr,
+}
+
 /// Binary operators. The names are the same as in the Irep representation.
 #[derive(Debug, Clone, Copy)]
 pub enum BinaryOperator {

cprover_bindings/src/goto_program/mod.rs

@@ -18,10 +18,11 @@ mod typ;
 pub use builtin::BuiltinFn;
 pub use expr::{
     arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue,
-    SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+    Lambda, SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD,
+    ARITH_OVERFLOW_RESULT_FIELD,
 };
 pub use location::Location;
 pub use stmt::{Stmt, StmtBody, SwitchCase};
-pub use symbol::{Symbol, SymbolValues};
+pub use symbol::{FunctionContract, Symbol, SymbolValues};
 pub use symbol_table::SymbolTable;
 pub use typ::{CIntType, DatatypeComponent, Parameter, Type};

cprover_bindings/src/goto_program/symbol.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::super::utils::aggr_tag;
-use super::{DatatypeComponent, Expr, Location, Parameter, Stmt, Type};
+use super::{DatatypeComponent, Expr, Lambda, Location, Parameter, Stmt, Type};
 use crate::{InternStringOption, InternedString};
 
 /// Based off the CBMC symbol implementation here:
@@ -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,22 @@ pub struct Symbol {
     pub is_weak: bool,
 }
 
+/// The CBMC representation of a function contract with three types of clauses.
+/// See https://diffblue.github.io/cbmc/contracts-user.html for the meaning of
+/// each type of clause.
+#[derive(Clone, Debug)]
+pub struct FunctionContract {
+    pub(crate) requires: Vec<Lambda>,
+    pub(crate) ensures: Vec<Lambda>,
+    pub(crate) assigns: Vec<Lambda>,
+}
+
+impl FunctionContract {
+    pub fn new(requires: Vec<Lambda>, ensures: Vec<Lambda>, assigns: Vec<Lambda>) -> Self {
+        Self { requires, ensures, assigns }
+    }
+}
+
 /// Currently, only C is understood by CBMC.
 // TODO: <https://github.com/model-checking/kani/issues/1>
 #[derive(Clone, Debug)]
@@ -84,6 +102,7 @@ impl Symbol {
             base_name,
             pretty_name,
 
+            contract: None,
             module: None,
             mode: SymbolModes::C,
             // global properties
@@ -107,6 +126,20 @@ 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);
+                prior.requires.extend(contract.requires);
+                prior.ensures.extend(contract.ensures);
+            }
+            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 {

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,15 @@ impl SymbolTable {
         let name = name.into();
         self.symbol_table.get_mut(&name).unwrap().update_fn_declaration_with_definition(body);
     }
+
+    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/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/to_irep.rs

@@ -5,7 +5,9 @@
 use super::super::goto_program;
 use super::super::MachineModel;
 use super::{Irep, IrepId};
+use crate::goto_program::Lambda;
 use crate::linear_map;
+use crate::InternedString;
 use goto_program::{
     BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter,
     SelfOperator, Stmt, StmtBody, SwitchCase, SymbolValues, Type, UnaryOperator,
@@ -169,6 +171,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 {
@@ -297,14 +309,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![] }
             }
@@ -499,10 +504,44 @@ impl ToIrep for SwitchCase {
     }
 }
 
+impl ToIrep for Lambda {
+    fn to_irep(&self, mm: &MachineModel) -> Irep {
+        let (ops_ireps, types) = self
+            .arguments
+            .iter()
+            .map(|(i, ty)| {
+                let ty_rep = ty.to_irep(mm);
+                (Irep::symbol(*i).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::CSpecRequires,
+                Irep::just_sub(contract.requires.iter().map(|c| c.to_irep(mm)).collect()),
+            );
+            typ = typ.with_named_sub(
+                IrepId::CSpecEnsures,
+                Irep::just_sub(contract.ensures.iter().map(|c| c.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),

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

@@ -4,7 +4,8 @@
 //! This file contains functions related to codegenning MIR functions into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{Expr, Stmt, Symbol};
+use crate::kani_middle::contracts::GFnContract;
+use cbmc::goto_program::{Expr, FunctionContract, Lambda, Stmt, Symbol, Type};
 use cbmc::InternString;
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{Body, HasLocalDecls, Local};
@@ -222,6 +223,90 @@ impl<'tcx> GotocCtx<'tcx> {
         );
     }
 
+    /// Convert the Kani level contract into a CBMC level contract by creating a
+    /// lambda that calls the contract implementation function.
+    ///
+    /// For instance say we are processing a contract on `f`
+    ///
+    /// ```rs
+    /// as_goto_contract(..., GFnContract { requires: <contact_impl_fn>, .. })
+    ///     = Contract {
+    ///         requires: [
+    ///             Lambda {
+    ///                 arguments: <return arg, args of f...>,
+    ///                 body: Call(codegen_fn_expr(contract_impl_fn), [args of f..., return arg])
+    ///             }
+    ///         ],
+    ///         ...
+    ///     }
+    /// ```
+    ///
+    /// A spec lambda in GOTO receives as its first argument the return value of
+    /// the annotated function. However at the top level we must receive `self`
+    /// as first argument, because rust requires it. As a result the generated
+    /// lambda takes the return value as first argument and then immediately
+    /// calls the generated spec function, but passing the return value as the
+    /// last argument.
+    fn as_goto_contract(&mut self, fn_contract: &GFnContract<Instance<'tcx>>) -> FunctionContract {
+        use rustc_middle::mir;
+        let mut handle_contract_expr = |instance| {
+            let mir = self.current_fn().mir();
+            assert!(mir.spread_arg.is_none());
+            let func_expr = self.codegen_func_expr(instance, None);
+            let mut mir_arguments: Vec<_> =
+                std::iter::successors(Some(mir::RETURN_PLACE + 1), |i| Some(*i + 1))
+                    .take(mir.arg_count + 1) // one extra for return value
+                    .collect();
+            let return_arg = mir_arguments.pop().unwrap();
+            let mir_operands: Vec<_> =
+                mir_arguments.iter().map(|l| mir::Operand::Copy((*l).into())).collect();
+            let mut arguments = self.codegen_funcall_args(&mir_operands, true);
+            let goto_argument_types: Vec<_> = [mir::RETURN_PLACE]
+                .into_iter()
+                .chain(mir_arguments.iter().copied())
+                .map(|a| self.codegen_ty(self.monomorphize(mir.local_decls()[a].ty)))
+                .collect();
+
+            mir_arguments.insert(0, return_arg);
+            arguments.push(Expr::symbol_expression(
+                self.codegen_var_name(&return_arg),
+                goto_argument_types.first().unwrap().clone(),
+            ));
+            Lambda {
+                arguments: mir_arguments
+                    .into_iter()
+                    .map(|l| self.codegen_var_name(&l).into())
+                    .zip(goto_argument_types)
+                    .collect(),
+                body: func_expr.call(arguments).cast_to(Type::Bool),
+            }
+        };
+
+        let requires =
+            fn_contract.requires().iter().copied().map(&mut handle_contract_expr).collect();
+        let ensures =
+            fn_contract.ensures().iter().copied().map(&mut handle_contract_expr).collect();
+        FunctionContract::new(requires, ensures, vec![])
+    }
+
+    /// Convert the contract to a CBMC contract, then attach it to `instance`.
+    /// `instance` must have previously been declared.
+    ///
+    /// This does not overwrite prior contracts but merges with them.
+    pub fn attach_contract(
+        &mut self,
+        instance: Instance<'tcx>,
+        contract: &GFnContract<Instance<'tcx>>,
+    ) {
+        // This should be safe, since the contract is pretty much evaluated as
+        // though it was the first (or last) assertion in the function.
+        self.set_current_fn(instance);
+        let goto_contract = self.as_goto_contract(contract);
+        let name = self.current_fn().name();
+        self.symbol_table.attach_contract(name, goto_contract);
+        self.reset_current_fn()
+    }
+
     pub fn declare_function(&mut self, instance: Instance<'tcx>) {
         debug!("declaring {}; {:?}", instance, instance);
         self.set_current_fn(instance);

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

@@ -723,8 +723,8 @@ impl<'tcx> GotocCtx<'tcx> {
             trace!(func=?instance, "codegen_func_symbol");
             let func = self.symbol_name(instance);
             self.symbol_table
-                .lookup(func)
-                .expect("Function `{func}` should've been declared before usage")
+                .lookup(&func)
+                .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage"))
         };
         (sym, funct)
     }