Improve assess and regression time (#2478)

The per-reachability analysis can have a overhead on the compilation time when assessing a project that has lots of tests. Disable it for now when analyzing tests.

Despite that improvement, assessing the firecracker still takes a long time, even with --only-codegen, due to the number of calls done to goto-cc. Thus, don't use assess here.

Author: celinval

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -256,14 +256,26 @@ impl CodegenBackend for GotocCodegenBackend {
                         false
                     }
                 });
+                // Codegen still takes a considerable amount, thus, we only generate one model for
+                // all harnesses and copy them for each harness.
+                // We will be able to remove this once we optimize all calls to CBMC utilities.
+                // https://github.com/model-checking/kani/issues/1971
+                let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
+                let (gcx, items) =
+                    self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model);
+                results.extend(gcx, items, None);
+
                 for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
                     let instance =
                         if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
                     let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
-                    let model_path = &metadata.goto_file.as_ref().unwrap();
-                    let (gcx, items) =
-                        self.codegen_items(tcx, &[*test_fn], model_path, &results.machine_model);
-                    results.extend(gcx, items, Some(metadata));
+                    let test_model_path = &metadata.goto_file.as_ref().unwrap();
+                    std::fs::copy(&model_path, &test_model_path).expect(&format!(
+                        "Failed to copy {} to {}",
+                        model_path.display(),
+                        test_model_path.display()
+                    ));
+                    results.harnesses.push(metadata);
                 }
             }
             ReachabilityType::None => {}

scripts/codegen-firecracker.sh

@@ -6,7 +6,13 @@ set -eu
 
 # Test for platform
 PLATFORM=$(uname -sp)
-if [[ $PLATFORM != "Linux x86_64" ]]; then
+
+if [[ $PLATFORM == "Linux x86_64" ]]
+then
+  TARGET="x86_64-unknown-linux-gnu"
+  # 'env' necessary to avoid bash built-in 'time'
+  WRAPPER="env time -v"
+else
   echo
   echo "Firecracker codegen regression only works on Linux x86 platform, skipping..."
   echo
@@ -23,11 +29,27 @@ echo
 
 # At the moment, we only test codegen for the virtio module
 cd $KANI_DIR/firecracker/src/devices/src/virtio/
+
+# Clean first
+cargo clean
+
 export KANI_LOG=error
 export RUSTC_LOG=error
 export RUST_BACKTRACE=1
-# Use cargo assess since this is now our default way of assessing Kani suitability to verify a crate.
-cargo kani --enable-unstable --only-codegen assess
+
+# Compile rust to iRep
+RUST_FLAGS=(
+    "--kani-compiler"
+    "-Cpanic=abort"
+    "-Zalways-encode-mir"
+    "-Cllvm-args=--goto-c"
+    "-Cllvm-args=--ignore-global-asm"
+    "-Cllvm-args=--reachability=pub_fns"
+    "--sysroot=${KANI_DIR}/target/kani"
+)
+export RUSTFLAGS="${RUST_FLAGS[@]}"
+export RUSTC="$KANI_DIR/target/kani/bin/kani-compiler"
+$WRAPPER cargo build --verbose --lib --target $TARGET
 
 echo
 echo "Finished Firecracker codegen regression successfully..."