Pass config from cargo-kani to kani-compiler by tedinski · Pull Request #999 · model-checking/kani

tedinski · 2022-03-30T22:11:30Z

Description of changes:

This change is a bit of a mash-up of things I need to start making things releasable, mostly centering around how we find certain environment/config info in kani-compiler.

In roughly github diff display order you will see:

Addition of the home crate to compute RUSTUP_HOME the same way rustup does.
The addition of passing --sysroot and --kani-lib arguments to kani-compiler from cargo-kani
(To keep things accurate, this required switching that function to accumulating a list of OsString now, instead of String, now that' we're including Paths.)
A smattering of clippy warnings that I fixed.
Fixing how we construct a lot of PathBufs to get cleaner code.
The addition of a new RPATH for kani-compiler, corresponding to where it should search for the rustc libraries in a release bundle. (Basically: next to bin/kani-compiler will be a symlink toolchain to the rustup-installed toolchain we require. Hence, ../toolchain/lib)
I removed the /deps path being provided to the linker with -L. This was how it used to work, but this directory didn't exist anymore.
SYSROOT accidentally didn't take an argument!

Call-outs:

There is no clean way currently to figure out where the kani libraries are being built, so I'm unfortunately not passing that down in development builds. The path is currently something like /home/ubuntu/rmc/target/debug/build/kani-compiler-b8c35844f7600bbf/out/lib and I wish we could change that outdir to something more predicable, so we could make this unconditional, but I couldn't figure out how.
Since we aren't yet using the RPATH for a release build, I manually verified that the executable ends up with the correct config:

RUNPATH              /home/ubuntu/.rustup/toolchains/nightly-2022-03-09-x86_64-unknown-linux-gnu/lib:$ORIGIN/../toolchain/lib

Testing:

How is this change tested? existing suite
Is this a refactor change? not quite

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.

celinval

It looks good, but I think we should be able to just use relative paths everywhere. When we run cargo build, cargo will put all workspace artifacts in the same directory, doesn't it? So for dev builds you should be able to use executable directory.

I think we are building the libraries twice right now, which isn't ideal.

celinval · 2022-03-30T22:50:14Z

src/cargo-kani/build.rs

+
+    // rustup also seems to set some environment variables, but this is not clearly documented.
+    // https://github.com/rust-lang/rustup/blob/master/src/toolchain.rs (search for RUSTUP_HOME)
+    // We make use of RUSTUP_TOOLCHAIN in this crate, to avoid needing to otherwise repeat this information


This comment seems a bit out of place. Can you please move that to where you implement this logic?

celinval · 2022-03-30T23:02:46Z

src/cargo-kani/src/session.rs

+    pub fn rust_toolchain(&self) -> Result<PathBuf> {
+        // This is a compile-time constant, not a dynamic lookup at runtime,
+        // so we get the toolchain we're built with (i.e. that from rust_toolchain.toml)
+        let toolchain = env!("RUSTUP_TOOLCHAIN");


This is a tricky one, eh? We should be careful with custom toolchain override and users setting up this variable in the first place. That said, as long as we automate our releases to not do that, we should be OK.

celinval · 2022-03-30T23:04:56Z

src/kani-compiler/src/parser.rs

+        .arg(
+            Arg::with_name(SYSROOT)
+                .long("--sysroot")
+                .takes_value(true)


tedinski · 2022-03-30T23:52:38Z

It looks good, but I think we should be able to just use relative paths everywhere. When we run cargo build, cargo will put all workspace artifacts in the same directory, doesn't it? So for dev builds you should be able to use executable directory.

I think we are building the libraries twice right now, which isn't ideal.

Are you just talking about --kani-lib? (I think I forgot to write this up as part of the callout, oops)

I agree it's not ideal. I avoided changing anything in this PR because I wasn't sure what to do. The issue with using the regular build directory is that it has a lot of other stuff in the directory (other dependencies, etc), whereas using the lib outputs we currently use we end up with just the 3 files only: the 2 rlib and the 1 so. (kani, std, and kani_macros, respectively.)

If we use the regular output directory I was slightly worried we might end up with those other dependencies mattering, somehow. On the other hand, this only matters for development builds, since release will distribute only the relevant 3 files. If you think it's probably fine, I'll switch over to doing that.

tedinski · 2022-03-31T16:20:31Z

Ah, actually the bigger problem is that they aren't built with --cfg=kani and so don't behave correctly when we build them "normally"

celinval · 2022-03-31T17:32:09Z

Ah, actually the bigger problem is that they aren't built with --cfg=kani and so don't behave correctly when we build them "normally"

What about adding a cargo config file that passes --cfg=kani to the build? That said, I'm OK doing that in a separate PR.

celinval

I am OK to push further improvements to a separate PR. Can you please move the comment out of src/cargo-kani/build.rs before pushing the change though?

Pass config from cargo-kani to kani-compiler

81efec0

tedinski requested a review from a team as a code owner March 30, 2022 22:11

celinval suggested changes Mar 30, 2022

View reviewed changes

celinval approved these changes Mar 31, 2022

View reviewed changes

tedinski added 2 commits April 1, 2022 17:39

Merge remote-tracking branch 'origin/main' into fixup-state

5297068

move a comment around

f4cc9b6

tedinski merged commit dfe6481 into model-checking:main Apr 1, 2022

tedinski deleted the fixup-state branch April 1, 2022 18:14

tedinski added a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Pass config from cargo-kani to kani-compiler (model-checking#999)

4608b23

tedinski added a commit that referenced this pull request Apr 27, 2022

Pass config from cargo-kani to kani-compiler (#999)

35842ca

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pass config from cargo-kani to kani-compiler#999

Pass config from cargo-kani to kani-compiler#999
tedinski merged 3 commits intomodel-checking:mainfrom
tedinski:fixup-state

tedinski commented Mar 30, 2022

Uh oh!

celinval left a comment

Uh oh!

celinval Mar 30, 2022

Uh oh!

celinval Mar 30, 2022

Uh oh!

celinval Mar 30, 2022

Uh oh!

tedinski commented Mar 30, 2022

Uh oh!

tedinski commented Mar 31, 2022

Uh oh!

celinval commented Mar 31, 2022

Uh oh!

celinval left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

tedinski commented Mar 30, 2022

Description of changes:

Call-outs:

Testing:

Checklist

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

celinval Mar 30, 2022

Choose a reason for hiding this comment

Uh oh!

celinval Mar 30, 2022

Choose a reason for hiding this comment

Uh oh!

celinval Mar 30, 2022

Choose a reason for hiding this comment

Uh oh!

tedinski commented Mar 30, 2022

Uh oh!

tedinski commented Mar 31, 2022

Uh oh!

celinval commented Mar 31, 2022

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants