Addressing comments

Added `requires` test case
Made tests `expected` tests
Changes `requires_ensures` macro to function

cprover_bindings/src/goto_program/expr.rs

@@ -170,9 +170,16 @@ pub enum ExprValue {
     },
 }
 
-/// The equivalent of a "mathematical function" in CBMC but spiritually it is more like a function object.
+/// 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 used to implement function contracts and values of this sort are otherwise not constructible.
+/// 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)>,

cprover_bindings/src/goto_program/mod.rs

@@ -23,6 +23,6 @@ pub use expr::{
 };
 pub use location::Location;
 pub use stmt::{Stmt, StmtBody, SwitchCase};
-pub use symbol::{Contract, 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

@@ -14,7 +14,7 @@ pub struct Symbol {
     pub typ: Type,
     pub value: SymbolValues,
     /// Contracts to be enforced (only supported for functions)
-    pub contract: Option<Box<Contract>>,
+    pub contract: Option<Box<FunctionContract>>,
 
     /// Optional debugging information
 
@@ -50,13 +50,13 @@ pub struct Symbol {
 /// See https://diffblue.github.io/cbmc/contracts-user.html for the meaning of
 /// each type of clause.
 #[derive(Clone, Debug)]
-pub struct Contract {
+pub struct FunctionContract {
     pub(crate) requires: Vec<Lambda>,
     pub(crate) ensures: Vec<Lambda>,
     pub(crate) assigns: Vec<Lambda>,
 }
 
-impl Contract {
+impl FunctionContract {
     pub fn new(requires: Vec<Lambda>, ensures: Vec<Lambda>, assigns: Vec<Lambda>) -> Self {
         Self { requires, ensures, assigns }
     }
@@ -128,7 +128,7 @@ 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: Contract) {
+    pub fn attach_contract(&mut self, contract: FunctionContract) {
         assert!(self.typ.is_code());
         match self.contract {
             Some(ref mut prior) => {

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, Contract, 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:
@@ -80,7 +80,11 @@ impl SymbolTable {
         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: Contract) {
+    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);
     }

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

@@ -5,7 +5,7 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::contracts::GFnContract;
-use cbmc::goto_program::{Contract, Expr, Lambda, Stmt, Symbol, Type};
+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};
@@ -247,7 +247,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// 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>>) -> Contract {
+    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();
@@ -286,7 +286,7 @@ impl<'tcx> GotocCtx<'tcx> {
             fn_contract.requires().iter().copied().map(&mut handle_contract_expr).collect();
         let ensures =
             fn_contract.ensures().iter().copied().map(&mut handle_contract_expr).collect();
-        Contract::new(requires, ensures, vec![])
+        FunctionContract::new(requires, ensures, vec![])
     }
 
     /// Convert the contract to a CBMC contract, then attach it to `instance`.

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -123,8 +123,9 @@ impl GotocCodegenBackend {
                     }
                 }
 
-                // Gets its own loop, because the functions used in the contract
-                // expressions must have been declared before
+                // Attaching the contrcts gets its own loop, because the
+                // functions used in the contract expressions must have been
+                // declared before
                 for (item, contract) in &items_with_contracts {
                     if let Some(contract) = contract {
                         let instance = match item {

library/kani_macros/src/lib.rs

@@ -237,14 +237,14 @@ mod sysroot {
     /// Rewrites function contract annotations (`requires`, `ensures`) by lifing
     /// the condition into a separate function. As an example: (using `ensures`)
     ///
-    /// ```rs
+    /// ```ignore
     /// #[kani::ensures(x < result)]
     /// fn foo(x: u32) -> u32 { .. }
     /// ```
     ///
     /// Is rewritten to
     ///
-    /// ```rs
+    /// ```ignore
     /// fn foo_ensures_<hash of foo>(x: u32, result: u32) {
     ///     x < result
     /// }
@@ -258,66 +258,68 @@ mod sysroot {
     ///
     /// This macro is supposed to be called with the name of the procedural
     /// macro it should generate, e.g. `requires_ensures(requires)`
-    macro_rules! requires_ensures {
-        ($name: ident) => {
-            pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream {
-                use syn::{FnArg, PatType, PatIdent, Pat, Signature, Token, ReturnType, TypeTuple, punctuated::Punctuated, Type};
-                use proc_macro2::Span;
-                let attr = proc_macro2::TokenStream::from(attr);
+    fn handle_requires_ensures(name: &str, attr: TokenStream, item: TokenStream) -> TokenStream {
+        use proc_macro2::Span;
+        use syn::{
+            punctuated::Punctuated, FnArg, Pat, PatIdent, PatType, ReturnType, Signature, Token,
+            Type, TypeTuple,
+        };
+        let attr = proc_macro2::TokenStream::from(attr);
 
-                let a_short_hash = short_hash_of_token_stream(&item);
+        let a_short_hash = short_hash_of_token_stream(&item);
 
-                let item_fn @ ItemFn { sig, .. } = &parse_macro_input!(item as ItemFn);
-                let Signature { inputs, output , .. } = sig;
+        let item_fn @ ItemFn { sig, .. } = &parse_macro_input!(item as ItemFn);
+        let Signature { inputs, output, .. } = sig;
 
-                let gen_fn_name = identifier_for_generated_function(item_fn, stringify!($name), a_short_hash);
-                let attribute = format_ident!("{}", stringify!($name));
-                let kani_attributes = quote!(
-                    #[allow(dead_code)]
-                    #[kanitool::#attribute = stringify!(#gen_fn_name)]
-                );
-
-                let typ = match output {
-                    ReturnType::Type(_, t) => t.clone(),
-                    _ => Box::new(TypeTuple { paren_token: Default::default(), elems: Punctuated::new() }.into()),
-                };
-
-                let mut gen_fn_inputs = inputs.clone();
-                gen_fn_inputs.push(
-                    FnArg::Typed(PatType {
-                        attrs: vec![],
-                        pat: Box::new(Pat::Ident(PatIdent{
-                            attrs: vec![],
-                            by_ref: None,
-                            mutability: None,
-                            ident: Ident::new("result", Span::call_site()),
-                            subpat: None,
-                        })),
-                        colon_token: Token![:](Span::call_site()),
-                        ty: typ,
-                    })
-                );
-
-                assert!(sig.variadic.is_none(), "Varaidic signatures are not supported");
-
-                let mut gen_sig = sig.clone();
-                gen_sig.inputs = gen_fn_inputs;
-                gen_sig.output = ReturnType::Type(Default::default(), Box::new(Type::Verbatim(quote!(bool))));
-                gen_sig.ident = gen_fn_name;
+        let gen_fn_name = identifier_for_generated_function(item_fn, name, a_short_hash);
+        let attribute = format_ident!("{name}");
+        let kani_attributes = quote!(
+            #[allow(dead_code)]
+            #[kanitool::#attribute = stringify!(#gen_fn_name)]
+        );
 
-                quote!(
-                    #gen_sig {
-                        #attr
-                    }
-
-                    #kani_attributes
-                    #item_fn
-                )
-                .into()
+        let typ = match output {
+            ReturnType::Type(_, t) => t.clone(),
+            _ => Box::new(
+                TypeTuple { paren_token: Default::default(), elems: Punctuated::new() }.into(),
+            ),
+        };
+
+        let mut gen_fn_inputs = inputs.clone();
+        gen_fn_inputs.push(FnArg::Typed(PatType {
+            attrs: vec![],
+            pat: Box::new(Pat::Ident(PatIdent {
+                attrs: vec![],
+                by_ref: None,
+                mutability: None,
+                ident: Ident::new("result", Span::call_site()),
+                subpat: None,
+            })),
+            colon_token: Token![:](Span::call_site()),
+            ty: typ,
+        }));
+
+        assert!(sig.variadic.is_none(), "Variadic signatures are not supported");
+
+        let mut gen_sig = sig.clone();
+        gen_sig.inputs = gen_fn_inputs;
+        gen_sig.output =
+            ReturnType::Type(Default::default(), Box::new(Type::Verbatim(quote!(bool))));
+        gen_sig.ident = gen_fn_name;
+
+        quote!(
+            #gen_sig {
+                #attr
             }
-        }
+
+            #kani_attributes
+            #item_fn
+        )
+        .into()
     }
 
+    /// Hash this `TokenStream` and return an integer that is at most digits
+    /// long when hex formatted.
     fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 {
         use std::hash::Hasher;
         let mut hasher = std::collections::hash_map::DefaultHasher::default();
@@ -326,6 +328,9 @@ mod sysroot {
         long_hash % 0x1_000_000 // six hex digits
     }
 
+    /// Makes consistent names for a generated function which was created for
+    /// `purpose`, from an attribute that decorates `related_function` with the
+    /// hash `hash`.
     fn identifier_for_generated_function(
         related_function: &ItemFn,
         purpose: &str,
@@ -335,8 +340,13 @@ mod sysroot {
         Ident::new(&identifier, proc_macro2::Span::mixed_site())
     }
 
-    requires_ensures!(requires);
-    requires_ensures!(ensures);
+    pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
+        handle_requires_ensures("requires", attr, item)
+    }
+
+    pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
+        handle_requires_ensures("ensures", attr, item)
+    }
 
     kani_attribute!(should_panic, no_args);
     kani_attribute!(solver);

tests/expected/function-contract/arbitrary_ensures_fail.expected

@@ -0,0 +1,5 @@
+RESULTS:
+Check 1: arbitrary_ensures_fail::max.missing_definition.1
+	 - Status: FAILURE
+	 - Description: "Function `arbitrary_ensures_fail::max` with missing definition is unreachable"
+	 - Location: Unknown file in function arbitrary_ensures_fail::max

tests/expected/function-contract/arbitrary_ensures_pass.expected

@@ -0,0 +1,5 @@
+RESULTS:
+Check 1: arbitrary_ensures_pass::max.missing_definition.1
+	 - Status: SUCCESS
+	 - Description: "Function `arbitrary_ensures_pass::max` with missing definition is unreachable"
+	 - Location: Unknown file in function arbitrary_ensures_pass::max

tests/expected/function-contract/arbitrary_requires_fail.expected

@@ -0,0 +1,10 @@
+RESULTS:
+Check 1: div.assertion.1
+	 - Status: FAILURE
+	 - Description: "attempt to divide by zero"
+	 - Location: arbitrary_requires_fail.rs:6:5 in function div
+
+Check 2: div.division-by-zero.1
+	 - Status: SUCCESS
+	 - Description: "division by zero"
+	 - Location: arbitrary_requires_fail.rs:6:5 in function div

tests/expected/function-contract/arbitrary_requires_fail.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+fn div(dividend: u32, divisor: u32) -> u32 {
+    dividend / divisor
+}
+
+#[kani::proof]
+fn main() {
+    div(kani::any(), kani::any());
+}

tests/expected/function-contract/arbitrary_requires_pass.expected

@@ -0,0 +1,10 @@
+RESULTS:
+Check 1: div.assertion.1
+	 - Status: SUCCESS
+	 - Description: "attempt to divide by zero"
+	 - Location: arbitrary_requires_pass.rs:6:5 in function div
+
+Check 2: div.division-by-zero.1
+	 - Status: SUCCESS
+	 - Description: "division by zero"
+	 - Location: arbitrary_requires_pass.rs:6:5 in function div

tests/expected/function-contract/arbitrary_requires_pass.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::requires(divisor != 0)]
+fn div(dividend: u32, divisor: u32) -> u32 {
+    dividend / divisor
+}
+
+#[kani::proof]
+fn main() {
+    div(kani::any(), kani::any());
+}

tests/expected/function-contract/simple_ensures_fail.expected

@@ -0,0 +1,5 @@
+RESULTS:
+Check 1: simple_ensures_fail::max.missing_definition.1
+	 - Status: FAILURE
+	 - Description: "Function `simple_ensures_fail::max` with missing definition is unreachable"
+	 - Location: Unknown file in function simple_ensures_fail::max

tests/expected/function-contract/simple_ensures_pass.expected

@@ -0,0 +1,5 @@
+RESULTS:
+Check 1: simple_ensures_pass::max.missing_definition.1
+	 - Status: SUCCESS
+	 - Description: "Function `simple_ensures_pass::max` with missing definition is unreachable"
+	 - Location: Unknown file in function simple_ensures_pass::max