Enable build cache in `cargo kani` by celinval · Pull Request #2232 · model-checking/kani

celinval · 2023-02-23T20:49:19Z

Description of changes:

This change re-enable the build cache in Kani. For that, we also added a new dummy option that includes Kani's version, which will ensure that the cache gets refreshed when the user upgrades Kani.

Resolved issues:

Resolves #1736
Resolves #2140
Resolves #2036

Related RFC:

Call-outs:

I added an option to force rebuild as suggested by @zhassan-aws to overcome any instability that we may find with the cache. I also used this new option to overcome a somewhat buggy test. In the test cargo-ui/supported-lib-types/lib-rlib, we declare redundant types which generate a conflict name warning:

warning: output filename collision.                                                                                                        
The lib target `lib` in package `supported-lib v0.1.0 (lib-rlib)` has the same output filename as the lib target `lib` in package `supported-lib v0.1.0 (lib-rlib)`.                                                                   
Colliding filename is: lib-rlib/target/debug/d
eps/liblib-56b09ad964e3cddd.rlib                                                                                                           
The targets should have unique names.                                                                                                      
Consider changing their names to be unique or compiling them separately.                                                                   
This may become a hard error in the future; see <https://github.com/rust-lang/cargo/issues/6313>.

while subsequent runs print the same warning and crash:

thread 'main' panicked at 'assertion failed: mtimes.insert(output.clone(), mtime).is_none()', src/tools/cargo/src/cargo/core/compiler/fingerprint.rs:1013:13

The same behavior can be reproduced using cargo build.

I created a few follow up issues to improve the caching mechanism: Build cache should consider changes to the compiler #2229, Split "codegen" flags to reduce recompilation #2230, and Add a test that the build cache is sensitive to different Kani versions #2231

Testing:

How is this change tested? New tests
Is this a refactor change? No

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

edit: No longer delete the problematic test.

Note: Need to fix model-checking#1478 before pushing this

Conflicts: kani-driver/src/call_cargo.rs Required adjustments: tests/script-based-pre/check_rebuild/rebuild.expected

adpaco-aws

Thanks, @celinval !

The tests in this PR are looking great but I don't know where the first line comes from in, for example, this test:

target/same.log:0
target/same.log: All fresh
target/same.log: No harness
target/same.log: ok

Other than that, only minor comments.

kani-driver/src/call_single_file.rs

tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml

adpaco-aws · 2023-03-03T19:48:34Z

tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml

Are you expecting more work around this particular case?

No... this warning actually explicitly states that Cargo might turn the warning into error in the near future. So I highly doubt they will invest time to fix this issue.

tests/script-based-pre/build-cache-bin/cache_works.sh

tests/script-based-pre/build-cache-bin/cache_works.expected

tests/script-based-pre/build-cache-bin/cache_works.sh

tests/script-based-pre/build-cache-dirty/target_lib/Cargo.lock

tests/script-based-pre/build-cache-dirty/target_lib/src/lib.rs

zhassan-aws

Very cleverly crafted tests! A couple of comments.

zhassan-aws · 2023-03-03T22:15:36Z

tests/script-based-pre/build-cache-dirty/rebuild.expected

+target/initial.log:Checking harness check_u8_u32...
+target/initial.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new argument that affects compilation
+target/enable_checks.log:4


Why did the number go down by 1 from initial.log?

Sorry, I updated the test to use a crate with less dependencies. But that was a great question, so I reverted the test locally to double check. The reason is that one of the crates (autocfg) is a build-dependency. Here is the result of cargo tree for the original test:

└── num-bigint v0.4.3 ├── num-integer v0.1.45 │ └── num-traits v0.2.15 │ [build-dependencies] │ └── autocfg v1.1.0 │ [build-dependencies] │ └── autocfg v1.1.0 └── num-traits v0.2.15 (*) [build-dependencies] └── autocfg v1.1.0

The cache for build dependencies doesn't get affected by the argument change, since the build dependency configuration uses host configuration.

And here is the full compilation log:

Run with a new argument that affects compilation Compiling num-traits v0.2.15 Compiling num-integer v0.1.45 Compiling num-bigint v0.4.3 Compiling target_lib v0.1.0 (/kani/tests/script-based-pre/build-cache-dirty/target/target_lib)

Got it, thanks for clarifying.

zhassan-aws · 2023-03-03T22:19:13Z

tests/script-based-pre/build-cache-fresh/cache_works.sh

+OUT_DIR=target
+
+# Expects two arguments: "kani arguments" "output_file"
+function check_kani {


It might be better to put this function in a different file and source it in each of the scripts to avoid repetition.

I totally agree, but this compiletest mode fails if it finds any subdirectory that is not a test. So to reuse this file, I would have to define the function inside one test folder and make all the other tests point to that folder.

So I decided to keep it simple and just use redundancy for now.

1- Improve test results readability. 2- Fix / improve comments.

zhassan-aws

A few more comments

zhassan-aws · 2023-03-03T22:24:36Z

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

        provide::provide_extern(providers);
    }

+    fn print_version(&self) {


This doesn't seem to be used anywhere.

In theory this is a function that the compiler uses to print the codegen version. Note that it is part of the implementation of the CodegenBackend trait.

There is a limitation in the compiler today where this doesn't get invoked for codegen backend that was configured via the driver, but I figured we might as well implement it and once this issue gets fixed, we get our version printed correctly.

zhassan-aws · 2023-03-03T22:40:15Z

kani-compiler/src/parser.rs

                .action(ArgAction::SetTrue),
+        )
+        .arg(
+            Arg::new("check-version")


Nit: should this be called kani-version?

This is just a dummy argument, so I don't think it matters. I figured that we could eventually ensure that the kani-compiler matches the driver version, but I didn't bother here.

kani-driver/src/call_single_file.rs

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

zhassan-aws

Thanks for all the hard work and numerous PRs to allow re-enabling the cache @celinval!

zhassan-aws · 2023-03-04T00:57:36Z

Oh, one more thing: please make sure to add this to the CHANGELOG under "Major Changes" (perhaps in a follow-up PR) 🙂

celinval added 2 commits February 22, 2023 21:32

Enable build cache once again

5ef456a

Add tests for rebuilding

23d526c

Note: Need to fix model-checking#1478 before pushing this

celinval mentioned this pull request Feb 28, 2023

Remove glob to collect all artifacts introduced by cargo kani #2246

Merged

4 tasks

celinval added 2 commits March 3, 2023 10:15

Merge remote-tracking branch 'origin/main' into issue-2140-version

157bd0e

Conflicts: kani-driver/src/call_cargo.rs Required adjustments: tests/script-based-pre/check_rebuild/rebuild.expected

Add new test + rename other tests

0b41b5b

celinval marked this pull request as ready for review March 3, 2023 19:15

celinval requested a review from a team as a code owner March 3, 2023 19:15

celinval force-pushed the issue-2140-version branch from 91cc8ad to 5577474 Compare March 3, 2023 19:27

Use --force-rebuild for test with conflicting targets

d78e27d

celinval force-pushed the issue-2140-version branch from 5577474 to d78e27d Compare March 3, 2023 19:56

adpaco-aws reviewed Mar 3, 2023

View reviewed changes

zhassan-aws reviewed Mar 3, 2023

View reviewed changes

Address comments

764f83f

1- Improve test results readability. 2- Fix / improve comments.

zhassan-aws reviewed Mar 3, 2023

View reviewed changes

Update kani-driver/src/call_single_file.rs

480ead6

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

zhassan-aws approved these changes Mar 4, 2023

View reviewed changes

Merge branch 'main' into issue-2140-version

980b950

celinval merged commit 035225c into model-checking:main Mar 4, 2023

celinval mentioned this pull request Jul 4, 2024

Cargo kani always rebuilds the entire project #895

Closed

dawidl022 mentioned this pull request May 16, 2025

Kani always rebuilds when running verify-std #4079

Open

Conversation

celinval commented Feb 23, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Related RFC:

Call-outs:

Testing:

Checklist

Uh oh!

adpaco-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

zhassan-aws commented Mar 4, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

celinval commented Feb 23, 2023 •

edited

Loading