Generate contracts of dependencies as assertions

kani-compiler/src/args.rs

@@ -36,6 +36,9 @@ pub enum ReachabilityType {
 /// with. Usually stored in and accessible via [`crate::kani_queries::QueryDb`].
 #[derive(Debug, Default, Clone, clap::Parser)]
 pub struct Arguments {
+    /// Option used to disable asserting function contracts.
+    #[clap(long)]
+    pub no_assert_contracts: bool,
     /// Option name used to enable assertion reachability checks.
     #[clap(long = "assertion-reach-checks")]
     pub check_assertion_reachability: bool,

kani-compiler/src/kani_middle/attributes.rs

@@ -42,6 +42,9 @@ enum KaniAttributeKind {
     /// contract, e.g. the contract check is substituted for the target function
     /// before the the verification runs.
     ProofForContract,
+    /// Internal attribute of the contracts implementation. Identifies the
+    /// code implementing the function with its contract clauses asserted.
+    AssertedWith,
     /// Attribute on a function with a contract that identifies the code
     /// implementing the check for this contract.
     CheckedWith,
@@ -94,6 +97,7 @@ impl KaniAttributeKind {
             | KaniAttributeKind::RecursionCheck
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::ModifiesWrapper
+            | KaniAttributeKind::AssertedWith
             | KaniAttributeKind::IsContractGenerated
             | KaniAttributeKind::DisableChecks => false,
         }
@@ -136,6 +140,8 @@ pub struct ContractAttributes {
     pub replaced_with: Symbol,
     /// The name of the inner check used to modify clauses.
     pub modifies_wrapper: Symbol,
+    /// The name of the contract assert closure
+    pub asserted_with: Symbol,
 }
 
 impl std::fmt::Debug for KaniAttributes<'_> {
@@ -264,17 +270,19 @@ impl<'tcx> KaniAttributes<'tcx> {
         let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith);
         let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith);
         let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper);
+        let asserted_with = self.attribute_value(KaniAttributeKind::AssertedWith);
 
         let total = recursion_check
             .iter()
             .chain(&checked_with)
             .chain(&replace_with)
             .chain(&modifies_wrapper)
+            .chain(&asserted_with)
             .count();
-        if total != 0 && total != 4 {
+        if total != 0 && total != 5 {
             self.tcx.sess.dcx().err(format!(
                 "Failed to parse contract instrumentation tags in function `{}`.\
-                Expected `4` attributes, but was only able to process `{total}`",
+                Expected `5` attributes, but was only able to process `{total}`",
                 self.tcx.def_path_str(self.item)
             ));
         }
@@ -284,6 +292,7 @@ impl<'tcx> KaniAttributes<'tcx> {
             checked_with: checked_with?,
             replaced_with: replace_with?,
             modifies_wrapper: modifies_wrapper?,
+            asserted_with: asserted_with?,
         })
     }
 
@@ -377,6 +386,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 | KaniAttributeKind::CheckedWith
                 | KaniAttributeKind::ModifiesWrapper
                 | KaniAttributeKind::RecursionCheck
+                | KaniAttributeKind::AssertedWith
                 | KaniAttributeKind::ReplacedWith => {
                     self.attribute_value(kind);
                 }
@@ -529,6 +539,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 | KaniAttributeKind::ModifiesWrapper
                 | KaniAttributeKind::RecursionCheck
                 | KaniAttributeKind::RecursionTracker
+                | KaniAttributeKind::AssertedWith
                 | KaniAttributeKind::ReplacedWith => {
                     self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
                 }

kani-compiler/src/kani_middle/transform/contracts.rs

@@ -224,6 +224,7 @@ impl AnyModifiesPass {
 /// #[kanitool::recursion_check = "__kani_recursion_check_modify"]
 /// #[kanitool::checked_with = "__kani_check_modify"]
 /// #[kanitool::replaced_with = "__kani_replace_modify"]
+/// #[kanitool::asserted_with = "__kani_assert_modify"]
 /// #[kanitool::modifies_wrapper = "__kani_modifies_modify"]
 /// fn name_fn(ptr: &mut u32) {
 ///     #[kanitool::fn_marker = "kani_register_contract"]
@@ -247,6 +248,11 @@ impl AnyModifiesPass {
 ///             let mut __kani_check_name_fn = || { /* check body */ };
 ///             kani_register_contract(__kani_check_name_fn)
 ///         }
+///         kani::internal::ASSERT => {
+///             #[kanitool::is_contract_generated(assert)]
+///             let mut __kani_check_name_fn = || { /* assert body */ };
+///             kani_register_contract(__kani_assert_name_fn)
+///         }
 ///         _ => { /* original body */ }
 ///     }
 /// }
@@ -267,6 +273,8 @@ pub struct FunctionWithContractPass {
     check_fn: Option<InternalDefId>,
     /// Functions that should be stubbed by their contract.
     replace_fns: HashSet<InternalDefId>,
+    /// Should we interpret contracts as assertions? (true iff the no-assert-contracts option is not passed)
+    assert_contracts: bool,
     /// Functions annotated with contract attributes will contain contract closures even if they
     /// are not to be used in this harness.
     /// In order to avoid bringing unnecessary logic, we clear their body.
@@ -346,6 +354,7 @@ impl FunctionWithContractPass {
             FunctionWithContractPass {
                 check_fn,
                 replace_fns,
+                assert_contracts: !queries.args().no_assert_contracts,
                 unused_closures: Default::default(),
                 run_contract_fn,
             }
@@ -371,6 +380,9 @@ impl FunctionWithContractPass {
     ///        kani::internal::SIMPLE_CHECK => {
     ///            // same as above
     ///        }
+    ///        kani::internal::ASSERT => {
+    ///            // same as above
+    ///        }
     ///        _ => { /* original code */}
     ///    }
     /// }
@@ -431,6 +443,9 @@ impl FunctionWithContractPass {
     }
 
     /// Return which contract mode to use for this function if any.
+    /// Note that the Check and Replace modes take precedence over the Assert mode.
+    /// This precedence ensures that a given `target` of a proof_for_contract(target) or stub_verified(target)
+    /// use their Check or Replace closures, respectively, rather than the Assert closure.
     fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option<ContractMode> {
         let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id());
         kani_attributes.has_contract().then(|| {
@@ -443,6 +458,8 @@ impl FunctionWithContractPass {
                 }
             } else if self.replace_fns.contains(&fn_def_id) {
                 ContractMode::Replace
+            } else if self.assert_contracts {
+                ContractMode::Assert
             } else {
                 ContractMode::Original
             }
@@ -456,24 +473,34 @@ impl FunctionWithContractPass {
         let recursion_closure = find_closure(tcx, fn_def, &body, contract.recursion_check.as_str());
         let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str());
         let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str());
+        let assert_closure = find_closure(tcx, fn_def, &body, contract.asserted_with.as_str());
         match mode {
             ContractMode::Original => {
                 // No contract instrumentation needed. Add all closures to the list of unused.
                 self.unused_closures.insert(recursion_closure);
                 self.unused_closures.insert(check_closure);
                 self.unused_closures.insert(replace_closure);
+                self.unused_closures.insert(assert_closure);
             }
             ContractMode::RecursiveCheck => {
                 self.unused_closures.insert(replace_closure);
                 self.unused_closures.insert(check_closure);
+                self.unused_closures.insert(assert_closure);
             }
             ContractMode::SimpleCheck => {
                 self.unused_closures.insert(replace_closure);
                 self.unused_closures.insert(recursion_closure);
+                self.unused_closures.insert(assert_closure);
             }
             ContractMode::Replace => {
                 self.unused_closures.insert(recursion_closure);
                 self.unused_closures.insert(check_closure);
+                self.unused_closures.insert(assert_closure);
+            }
+            ContractMode::Assert => {
+                self.unused_closures.insert(recursion_closure);
+                self.unused_closures.insert(check_closure);
+                self.unused_closures.insert(replace_closure);
             }
         }
     }
@@ -488,6 +515,7 @@ enum ContractMode {
     RecursiveCheck = 1,
     SimpleCheck = 2,
     Replace = 3,
+    Assert = 4,
 }
 
 fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef {

kani-driver/src/args/mod.rs

@@ -309,6 +309,10 @@ pub struct VerificationArgs {
     )]
     pub synthesize_loop_contracts: bool,
 
+    /// Do not assert the function contracts of dependencies. Requires -Z function-contracts.
+    #[arg(long, hide_short_help = true)]
+    pub no_assert_contracts: bool,
+
     //Harness Output into individual files
     #[arg(long, hide_short_help = true)]
     pub output_into_files: bool,
@@ -702,6 +706,17 @@ impl ValidateArgs for VerificationArgs {
                 ),
             ));
         }
+
+        if !self.is_function_contracts_enabled() && self.no_assert_contracts {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `--no-assert-contracts` option requires `-Z {}`.",
+                    UnstableFeature::FunctionContracts
+                ),
+            ));
+        }
+
         Ok(())
     }
 }
@@ -1000,4 +1015,11 @@ mod tests {
         let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
     }
+
+    #[test]
+    fn check_no_assert_contracts() {
+        let args = "kani input.rs --no-assert-contracts".split_whitespace();
+        let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
+        assert_eq!(err.kind(), ErrorKind::MissingRequiredArgument);
+    }
 }

kani-driver/src/call_cargo.rs

@@ -188,6 +188,9 @@ crate-type = ["lib"]
         if let Some(backend_arg) = self.backend_arg() {
             pkg_args.push(backend_arg);
         }
+        if self.args.no_assert_contracts {
+            pkg_args.push("--no-assert-contracts".into());
+        }
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;

kani-driver/src/call_single_file.rs

@@ -93,7 +93,7 @@ impl KaniSession {
         Ok(())
     }
 
-    /// Create a compiler option that represents the reachability mod.
+    /// Create a compiler option that represents the reachability mode.
     pub fn reachability_arg(&self) -> String {
         to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())])
     }
@@ -152,6 +152,10 @@ impl KaniSession {
             flags.push("--print-llbc".into());
         }
 
+        if self.args.no_assert_contracts {
+            flags.push("--no-assert-contracts".into());
+        }
+
         flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string));
 
         flags

library/kani_core/src/lib.rs

@@ -496,6 +496,9 @@ macro_rules! kani_intrinsics {
             /// Stub the body with its contract.
             pub const REPLACE: Mode = 3;
 
+            /// Insert the contract into the body of the function as assertion(s).
+            pub const ASSERT: Mode = 4;
+
             /// Creates a non-fatal property with the specified condition and message.
             ///
             /// This check will not impact the program control flow even when it fails.

library/kani_macros/src/sysroot/contracts/assert.rs

@@ -0,0 +1,97 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Logic used for generating the code that generates contract preconditions and postconditions as assertions.
+
+use proc_macro2::{Ident, Span, TokenStream as TokenStream2};
+use quote::quote;
+use std::mem;
+use syn::{Stmt, parse_quote};
+
+use super::{
+    ContractConditionsData, ContractConditionsHandler, ContractMode, INTERNAL_RESULT_IDENT,
+    helpers::*,
+    shared::{build_ensures, split_for_remembers},
+};
+
+impl<'a> ContractConditionsHandler<'a> {
+    /// Generate a token stream that represents the assert closure.
+    ///
+    /// See [`Self::make_assert_body`] for the most interesting parts of this
+    /// function.
+    pub fn assert_closure(&self) -> TokenStream2 {
+        let assert_ident = Ident::new(&self.assert_name, Span::call_site());
+        let sig = &self.annotated_fn.sig;
+        let output = &sig.output;
+        let body_stmts = self.initial_assert_stmts();
+        let body = self.make_assert_body(body_stmts);
+
+        quote!(
+            #[kanitool::is_contract_generated(assert)]
+            #[allow(dead_code, unused_variables, unused_mut)]
+            let mut #assert_ident = || #output #body;
+        )
+    }
+
+    /// Expand the assert closure body.
+    pub fn expand_assert(&self, closure: &mut Stmt) {
+        let body = closure_body(closure);
+        *body = syn::parse2(self.make_assert_body(mem::take(&mut body.block.stmts))).unwrap();
+    }
+
+    /// Initialize the list of statements for the assert closure body.
+    /// Construct a closure that wraps the body of the function, then invoke it and return the result.
+    fn initial_assert_stmts(&self) -> Vec<Stmt> {
+        let body_wrapper_ident = Ident::new("body_wrapper", Span::call_site());
+        let output = &self.annotated_fn.sig.output;
+        let return_type = return_type_to_type(&output);
+        let stmts = &self.annotated_fn.block.stmts;
+        let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
+
+        parse_quote!(
+            let mut body_wrapper = || #output {
+                #(#stmts)*
+            };
+            let #result : #return_type = #body_wrapper_ident();
+            #result
+        )
+    }
+
+    /// Create the body of an assert closure.
+    ///
+    /// Wraps the conditions from this attribute around `self.body`.
+    fn make_assert_body(&self, mut body_stmts: Vec<Stmt>) -> TokenStream2 {
+        let Self { attr_copy, .. } = self;
+        match &self.condition_type {
+            ContractConditionsData::Requires { attr } => {
+                quote!({
+                    kani::assert(#attr, stringify!(#attr_copy));
+                    #(#body_stmts)*
+                })
+            }
+            ContractConditionsData::Ensures { attr } => {
+                let (remembers, ensures_clause) = build_ensures(attr);
+
+                let exec_postconditions = quote!(
+                    kani::assert(#ensures_clause, stringify!(#attr_copy));
+                );
+
+                let return_expr = body_stmts.pop();
+
+                let (asserts, rest_of_body) =
+                    split_for_remembers(&body_stmts[..], ContractMode::Assert);
+
+                quote!({
+                    #(#asserts)*
+                    #remembers
+                    #(#rest_of_body)*
+                    #exec_postconditions
+                    #return_expr
+                })
+            }
+            ContractConditionsData::Modifies { .. } => {
+                quote!({#(#body_stmts)*})
+            }
+        }
+    }
+}