Documentation

cprover_bindings/src/goto_program/expr.rs

@@ -170,6 +170,9 @@ pub enum ExprValue {
     },
 }
 
+/// The equivalent of a "mathematical function" in CBMC but spiritually it is more like a function object.
+///
+/// This is only used to implement function contracts and values of this sort are otherwise not constructible.
 #[derive(Debug, Clone)]
 pub struct Lambda {
     pub arguments: Vec<(InternedString, Type)>,

cprover_bindings/src/goto_program/symbol.rs

@@ -13,6 +13,7 @@ pub struct Symbol {
     pub location: Location,
     pub typ: Type,
     pub value: SymbolValues,
+    /// Contracts to be enforced (only supported for functions)
     pub contract: Option<Box<Contract>>,
 
     /// Optional debugging information
@@ -45,6 +46,9 @@ 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 Contract {
     pub(crate) requires: Vec<Lambda>,
@@ -122,7 +126,10 @@ 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) {
+        assert!(self.typ.is_code());
         match self.contract {
             Some(ref mut prior) => {
                 prior.assigns.extend(contract.assigns);

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

@@ -223,6 +223,24 @@ 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
@@ -271,6 +289,10 @@ impl<'tcx> GotocCtx<'tcx> {
         Contract::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>,

kani-compiler/src/codegen_cprover_gotoc/utils/names.rs

@@ -87,6 +87,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 }
 
+/// The actual function name used in the symbol table
 pub fn symbol_name_for_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> String {
     let llvm_mangled = tcx.symbol_name(instance).name.to_string();
     debug!(
@@ -104,6 +105,7 @@ pub fn symbol_name_for_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx
     if pretty == "main" { pretty } else { llvm_mangled }
 }
 
+/// A human readable name in Rust for reference, should not be used as a key.
 pub fn readable_name_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> String {
     with_no_trimmed_paths!(tcx.def_path_str_with_substs(instance.def_id(), instance.substs))
 }

kani-compiler/src/kani_compiler.rs

@@ -322,6 +322,7 @@ impl KaniCompiler {
     }
 }
 
+/// Find all functions reachable from this harness that have a contract attached to them.
 fn contracts_for_harness<'tcx>(tcx: TyCtxt<'tcx>, harness: MonoItem<'tcx>) -> Vec<String> {
     collect_reachable_items(tcx, &[harness])
         .into_iter()

kani-compiler/src/kani_middle/attributes.rs

@@ -157,6 +157,13 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut
     })
 }
 
+/// Extract function contracts on this item.
+///
+/// This parses the annotation and resolves the mentioned implementation
+/// functions for the contract.
+///
+/// If no contract annotations are found the return value of this function will
+/// simply not be [`enforceable()`](super::contracts::GFnContract::enforceable) and can be ignored.
 pub fn extract_contract(tcx: TyCtxt, local_def_id: LocalDefId) -> super::contracts::FnContract {
     use rustc_ast::ExprKind;
     use rustc_hir::{Item, ItemKind, Mod, Node};

kani-compiler/src/kani_middle/contracts.rs

@@ -1,5 +1,8 @@
 use rustc_hir::def_id::DefId;
 
+/// Generic representation for a function contract. This is so that we can reuse
+/// this type for different resolution stages if the implementation functions
+/// (`C`).
 #[derive(Default)]
 pub struct GFnContract<C> {
     requires: Vec<C>,
@@ -10,10 +13,12 @@ pub struct GFnContract<C> {
 pub type FnContract = GFnContract<DefId>;
 
 impl<C> GFnContract<C> {
+    /// Read access to all preondition clauses.
     pub fn requires(&self) -> &[C] {
         &self.requires
     }
 
+    /// Read access to all postcondition clauses.
     pub fn ensures(&self) -> &[C] {
         &self.ensures
     }
@@ -22,6 +27,8 @@ impl<C> GFnContract<C> {
         Self { requires, ensures, assigns }
     }
 
+    /// Perform a transformation on each implementation item. Usually these are
+    /// resolution steps.
     pub fn map<C0, F: FnMut(&C) -> C0>(&self, mut f: F) -> GFnContract<C0> {
         GFnContract {
             requires: self.requires.iter().map(&mut f).collect(),
@@ -30,6 +37,7 @@ impl<C> GFnContract<C> {
         }
     }
 
+    /// If this is false, then this contract has no clauses and can safely be ignored.
     pub fn enforceable(&self) -> bool {
         !self.requires().is_empty() || !self.ensures().is_empty()
     }

kani-driver/src/call_goto_instrument.rs

@@ -164,6 +164,7 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    /// Make CBMC enforce a function contract.
     pub fn enforce_contract(&self, file: &Path, function: &str) -> Result<()> {
         println!("enforcing {function} contract");
         self.call_goto_instrument(vec![

library/kani/src/lib.rs

@@ -66,6 +66,7 @@ pub fn assume(cond: bool) {
     assert!(cond, "`kani::assume` should always hold");
 }
 
+/// If the `premise` is true, so must be the `conclusion`
 pub fn implies(premise: bool, conclusion: bool) -> bool {
     !premise || conclusion
 }

library/kani_macros/src/lib.rs

@@ -89,11 +89,28 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
     derive::expand_derive_arbitrary(item)
 }
 
+/// Add a precondition to this function.
+///
+/// This is part of the function contract API, together with [`ensures`].
+///
+/// The contents of the attribute is a condtition over the input values to the
+/// annotated function. All Rust syntax is supported, even calling other
+/// functions, but the computations must be side effect free, e.g. it cannot
+/// perform I/O or use mutable memory.
 #[proc_macro_attribute]
 pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::requires(attr, item)
 }
 
+/// Add a postcondition to this function.
+///
+/// This is part of the function contract API, together with [`requires`].
+///
+/// The contents of the attribute is a condtition over the input values to the
+/// annotated function *and* its return value, accessible as a variable called
+/// `result`. All Rust syntax is supported, even calling other functions, but
+/// the computations must be side effect free, e.g. it cannot perform I/O or use
+/// mutable memory.
 #[proc_macro_attribute]
 pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::ensures(attr, item)
@@ -112,6 +129,8 @@ mod sysroot {
 
     use proc_macro2::Ident;
 
+    /// Create a unique hash for a token stream (basically a [`std::hash::Hash`]
+    /// impl for `proc_macro2::TokenStream`).
     fn hash_of_token_stream<H: std::hash::Hasher>(
         hasher: &mut H,
         stream: proc_macro2::TokenStream,
@@ -215,6 +234,30 @@ mod sysroot {
         }
     }
 
+    /// Rewrites function contract annotations (`requires`, `ensures`) by lifing
+    /// the condition into a separate function. As an example: (using `ensures`)
+    ///
+    /// ```rs
+    /// #[kani::ensures(x < result)]
+    /// fn foo(x: u32) -> u32 { .. }
+    /// ```
+    ///
+    /// Is rewritten to
+    ///
+    /// ```rs
+    /// fn foo_enusres_<hash of foo>(x: u32, result: u32) {
+    ///     x < result
+    /// }
+    ///
+    /// #[kanitook::ensures = "foo_ensures_<hash of foo>"]
+    /// fn foo(x: u32) -> u32 { .. }
+    /// ```
+    ///
+    /// Note that CBMC's contracts always pass the return value (even for
+    /// `requires`) and so we also append it here.
+    ///
+    /// 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 {