Function Contracts: Support for defining and checking requires and ensures clauses (rust-lang#2655)

Co-authored-by: Celina G. Val <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

Author: 3 people

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

@@ -325,6 +325,49 @@ impl<'tcx> GotocHook<'tcx> for MemCmp {
     }
 }
 
+/// A builtin that is essentially a C-style dereference operation, creating an
+/// unsafe shallow 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,
+            "Invariant broken. `untracked_deref` should only be given one argument. \
+            This function should only be called from code generated by kani macros, \
+            as such this is likely a code-generation error."
+        );
+        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 +378,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> {
             Rc::new(Nondet),
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
+            Rc::new(UntrackedDeref),
         ],
     }
 }