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

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)
             });
         }