Skip to content

Improve assess and regression time #2478

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
celinval merged 2 commits into from
May 26, 2023
Merged

Improve assess and regression time #2478

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c0370fe
Improve assess and regression time
celinval May 25, 2023
6ff3384
Merge branch 'main' into issue-xxxx-assess-time
celinval May 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 16 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 => {}
Expand Down
28 changes: 25 additions & 3 deletions scripts/codegen-firecracker.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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..."
Expand Down