Function Contracts: Support for defining and checking requires and ensures clauses

Cargo.lock

@@ -357,6 +357,26 @@ version = "0.3.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f"
 
+[[package]]
+name = "enum-map"
+version = "2.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9705d8de4776df900a4a0b2384f8b0ab42f775e93b083b42f8ce71bdc32a47e3"
+dependencies = [
+ "enum-map-derive",
+]
+
+[[package]]
+name = "enum-map-derive"
+version = "0.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ccb14d927583dd5c2eac0f2cf264fc4762aefe1ae14c47a8a20fc1939d3a5fc0"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.27",
+]
+
 [[package]]
 name = "equivalent"
 version = "1.0.1"
@@ -495,6 +515,7 @@ version = "0.33.0"
 dependencies = [
  "clap",
  "cprover_bindings",
+ "enum-map",
  "home",
  "itertools",
  "kani_metadata",

kani-compiler/Cargo.toml

@@ -24,6 +24,7 @@ strum_macros = "0.24.0"
 shell-words = "1.0.0"
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
+enum-map = "2.6"
 
 # Future proofing: enable backend dependencies using feature.
 [features]

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -325,6 +325,43 @@ impl<'tcx> GotocHook<'tcx> for MemCmp {
     }
 }
 
+/// A builtin that is essentially a C-style dereference operation, creating an
+/// unsafe challow copy. Importantly either this copy or the original needs to
+/// be `mem::forget`en or a double-free will occur.
+///
+/// Takes in a `&T` reference and returns a `T` (like clone would but without
+/// cloning). Breaks ownership rules and is only used in the context of function
+/// contracts where we can structurally guarantee the use is safe.
+struct UntrackedDeref;
+
+impl<'tcx> GotocHook<'tcx> for UntrackedDeref {
+    fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool {
+        matches_function(tcx, instance, "KaniUntrackedDeref")
+    }
+
+    fn handle(
+        &self,
+        tcx: &mut GotocCtx<'tcx>,
+        _instance: Instance<'tcx>,
+        mut fargs: Vec<Expr>,
+        assign_to: Place<'tcx>,
+        _target: Option<BasicBlock>,
+        span: Option<Span>,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1);
+        let loc = tcx.codegen_span_option(span);
+        Stmt::block(
+            vec![Stmt::assign(
+                unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to))
+                    .goto_expr,
+                fargs.pop().unwrap().dereference(),
+                loc,
+            )],
+            loc,
+        )
+    }
+}
+
 pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
     GotocHooks {
         hooks: vec![
@@ -335,6 +372,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
             Rc::new(Nondet),
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
+            Rc::new(UntrackedDeref),
         ],
     }
 }

kani-compiler/src/kani_compiler.rs

@@ -400,6 +400,9 @@ impl Callbacks for KaniCompiler {
                 queries.unstable_features = features.cloned().collect::<Vec<_>>();
             }
 
+            queries.function_contracts_enabled =
+                queries.unstable_features.iter().any(|s| s == "function-contracts");
+
             if matches.get_flag(parser::ENABLE_STUBBING)
                 && queries.reachability_analysis == ReachabilityType::Harnesses
             {
@@ -419,7 +422,7 @@ impl Callbacks for KaniCompiler {
     ) -> Compilation {
         if self.stage.is_init() {
             self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| {
-                check_crate_items(tcx, self.queries.lock().unwrap().ignore_global_asm);
+                check_crate_items(tcx, &self.queries.lock().unwrap());
                 self.process_harnesses(tcx)
             });
         }