get core to compile everything but proof_for_contract

model-checking · jaisnan · Jun 11, 2024 · May 31, 2024 · Jun 3, 2024 · Jun 4, 2024
commit 4614e65623515ddcebae3e02984cd5cb452e20c6
@@ -496,6 +496,10 @@ dependencies = [
  "strum_macros",
 ]
 
+[[package]]
+name = "kani_verify_std"
+version = "0.1.0"
+
 [[package]]
 name = "lazy_static"
 version = "1.4.0"

diff --git a/Cargo.toml b/Cargo.toml
@@ -44,7 +44,7 @@ members = [
   "kani-driver",
   "kani-compiler",
   "kani_metadata",
-  "library/kani_core",
+  "library/kani_core", "target/kani_verify_std",
 ]
 
 # This indicates what package to e.g. build with 'cargo build' without --workspace

@@ -39,14 +39,21 @@ impl<'tcx> GotocCtx<'tcx> {
         let recursion_wrapper_id =
             function_under_contract_attrs.checked_with_id().unwrap().unwrap();
         let expected_name = format!("{}::REENTRY", tcx.item_name(recursion_wrapper_id));
-        let mut recursion_tracker = items.iter().filter_map(|i| match i {
+        let mut recursion_tracker = items.iter().filter_map(|i| { tracing::error!(?i, "++++++++++++++++++++++"); match i {
             MonoItem::Static(recursion_tracker)
                 if (*recursion_tracker).name().contains(expected_name.as_str()) =>
             {
                 Some(*recursion_tracker)
             }
             _ => None,
-        });
+        }});
+
+        let names = items.iter().filter_map(|item| { let MonoItem::Fn(i) = item else { return None };
+            Some(i.name())
+        }).collect::<Vec<_>>();
+
+        tracing::error!(?names, ?recursion_wrapper_id, "******************");
+
         let recursion_tracker_def = recursion_tracker
             .next()
             .expect("There should be at least one recursion tracker (REENTRY) in scope");

diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -75,6 +75,7 @@ impl BodyTransformation {
             Some(TransformationResult::Modified(body)) => body.clone(),
             Some(TransformationResult::NotModified) => instance.body().unwrap(),
             None => {
+                println!("****** INSTANCE NAME {:?}***********", instance.name());
                 let mut body = instance.body().unwrap();
                 let mut modified = false;
                 for pass in self.opt_passes.iter().chain(self.inst_passes.iter()) {

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
@@ -57,8 +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());
 
-        let mut cargo_args: Vec<OsString> = vec!["build".into()];
+        let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
         cargo_args.append(&mut cargo_config_args());
 
         // Configuration needed to parse cargo compilation status.
@@ -71,6 +73,9 @@ impl KaniSession {
             cargo_args.push("-v".into());
         }
 
+        // cargo_args.push("--".into());
+        // cargo_args.push("-Zunpretty=expanded".into());
+
         // Since we are verifying the standard library, we set the reachability to all crates.
         let mut cmd = setup_cargo_command()?;
         cmd.args(&cargo_args)
@@ -103,8 +108,8 @@ impl KaniSession {
             fs::remove_dir_all(&target_dir)?;
         }
 
-        let lib_path = lib_folder().unwrap();
-        let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
+        let lib_path = lib_no_core_folder().unwrap();
+        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());
 
         let mut cargo_args: Vec<OsString> = vec!["rustc".into()];

diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
@@ -407,6 +407,10 @@ pub(crate) fn std_project(std_path: &Path, session: &KaniSession) -> Result<Proj
     }
     session.cargo_init_lib(&dummy_crate)?;
 
+    let mut input = String::new();
+    println!("Press ENTER: ");
+    let _n = std::io::stdin().read_line(&mut input).unwrap();
+
     // Build cargo project for dummy crate.
     let std_path = std_path.canonicalize()?;
     let outputs = session.cargo_build_std(std_path.parent().unwrap(), &dummy_crate)?;

diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
@@ -9,7 +9,7 @@ license = "MIT OR Apache-2.0"
 publish = false
 
 [dependencies]
-kani_macros = { path = "../kani_macros" }
+kani_macros = { path = "../kani_macros", default-features = false }
 
 [features]
 concrete_playback = []
@@ -10,7 +10,7 @@ publish = false
 description = "Define core constructs to use with Kani"
 
 [dependencies]
-kani_macros = { path = "../kani_macros" }
+kani_macros = { path = "../kani_macros", default-features = false }
 
 [features]
 no_core=["kani_macros/no_core"]
diff --git a/library/kani_core/src/internal.rs b/library/kani_core/src/internal.rs
@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[macro_export]
+macro_rules! kani_internals {
+
+
+
+}
@@ -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);)*),
     )
 }
 

diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh
@@ -92,6 +92,7 @@ RUST_FLAGS=(
     "-L"
     "${KANI_DIR}/target/kani/no_core/lib"
     "--cfg=kani"
+    "--cfg=no_core"
 )
 export RUSTFLAGS="${RUST_FLAGS[@]}"
 export RUSTC_LOGS="info"