Add -Zfunction-contracts and cfg(no_core)

model-checking · jaisnan · Jun 11, 2024 · May 31, 2024 · Jun 3, 2024 · Jun 4, 2024
commit 18a556e4589b8a8bcc8a9ba24c42bbb817c8bdc6
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
@@ -57,6 +57,10 @@ impl KaniSession {
         let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path));
         rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
         rustc_args.push(self.reachability_arg().into());
+        rustc_args.push(to_rustc_arg(vec!["--ignore-global-asm".to_string()]).into());
+        rustc_args.push(to_rustc_arg(vec!["-Zfunction-contracts".to_string()]).into());
+        rustc_args.push(to_rustc_arg(vec!["--enable-stubbing".to_string()]).into());
+
 
         let mut cargo_args: Vec<OsString> = vec!["build".into()];
         cargo_args.append(&mut cargo_config_args());

@@ -255,5 +255,30 @@ macro_rules! kani_intrinsics {
             #[allow(clippy::empty_loop)]
             loop {}
         }
-    };
+
+        pub mod internal {
+            /// A way to break the ownerhip rules. Only used by contracts where we can
+            /// guarantee it is done safely.
+            #[inline(never)]
+            #[doc(hidden)]
+            #[rustc_diagnostic_item = "KaniUntrackedDeref"]
+            pub fn untracked_deref<T>(_: &T) -> T {
+                todo!()
+            }
+
+            /// CBMC contracts currently has a limitation where `free` has to be in scope.
+            /// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
+            /// scope.
+            ///
+            /// Thus, this function will basically translate into:
+            /// ```c
+            /// // This is a no-op.
+            /// free(NULL);
+            /// ```
+            #[inline(never)]
+            #[doc(hidden)]
+            #[rustc_diagnostic_item = "KaniInitContracts"]
+            pub fn init_contracts() {}
+        }
+    }
 }
@@ -82,10 +82,10 @@ pub fn make_unsafe_argument_copies(
     let arg_values = renaming_map.keys();
     (
         quote!(#(let #arg_names = kani::internal::untracked_deref(&#arg_values);)*),
-        #[cfg(feature = "no_core")]
-        quote!(#(crate::mem::block(#also_arg_names);)*),
         #[cfg(not(feature = "no_core"))]
         quote!(#(std::mem::forget(#also_arg_names);)*),
+        #[cfg(feature = "no_core")]
+        quote!(#(core::mem::forget(#also_arg_names);)*),
     )
 }