Merge branch 'main' into issue-1781-cffi-mismatch

kani-compiler/kani_queries/src/lib.rs

@@ -9,8 +9,6 @@ use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 pub enum ReachabilityType {
     /// Start the cross-crate reachability analysis from all harnesses in the local crate.
     Harnesses,
-    /// Use standard rustc monomorphizer algorithm.
-    Legacy,
     /// Don't perform any reachability analysis. This will skip codegen for this crate.
     #[default]
     None,

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -30,7 +30,7 @@ use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
-use rustc_middle::mir::mono::{CodegenUnit, MonoItem};
+use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::mir::write_mir_pretty;
 use rustc_middle::ty::query::Providers;
 use rustc_middle::ty::{self, InstanceDef, TyCtxt};
@@ -400,15 +400,6 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
     let reach = gcx.queries.get_reachability_analysis();
     debug!(?reach, "collect_codegen_items");
     match reach {
-        ReachabilityType::Legacy => {
-            // Use rustc monomorphizer to retrieve items to codegen.
-            let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1;
-            codegen_units
-                .iter()
-                .flat_map(|cgu| cgu.items_in_deterministic_order(tcx))
-                .map(|(item, _)| item)
-                .collect()
-        }
         ReachabilityType::Harnesses => {
             // Cross-crate collecting of all items that are reachable from the crate harnesses.
             let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(gcx.tcx, def_id));

scripts/kani-regression.sh

@@ -69,8 +69,11 @@ for testp in "${TESTS[@]}"; do
       --quiet --no-fail-fast
 done
 
-# Check codegen for the standard library
-time "$SCRIPT_DIR"/std-lib-regression.sh
+# Don't run std regression if using JSON symtab to avoid OOM issues.
+if [[ -z "${KANI_ENABLE_WRITE_JSON_SYMTAB-}" ]]; then
+    # Check codegen for the standard library
+    time "$SCRIPT_DIR"/std-lib-regression.sh
+fi
 
 # We rarely benefit from re-using build artifacts in the firecracker test,
 # and we often end up with incompatible leftover artifacts:

scripts/std-lib-regression.sh

@@ -70,9 +70,10 @@ export RUSTC_LOG=error
 RUST_FLAGS=(
     "--kani-compiler"
     "-Cpanic=abort"
+    "-Zalways-encode-mir"
     "-Cllvm-args=--goto-c"
     "-Cllvm-args=--ignore-global-asm"
-    "-Cllvm-args=--reachability=legacy"
+    "-Cllvm-args=--reachability=pub_fns"
 )
 export RUSTFLAGS="${RUST_FLAGS[@]}"
 export RUSTC="$KANI_DIR/target/kani/bin/kani-compiler"