Add rmc-compiler binary to drive rust compilation by celinval · Pull Request #722 · model-checking/kani

celinval · 2021-12-29T23:54:06Z

Description of changes:

I have created a new compilation driver (rmc-compiler) that no longer depends on a modified version of the rust compiler, neither depends on the bootstrap script.

Resolved issues:

Resolves #42 and #658

Call-outs:

I'm not quite happy with a few things in this change, but it is getting way too big to manage in a separate branch. It is also getting quite big to be reviewed. Thus, I created the following issues to track a few improvements:

Improve project layout #719: Improve the layout of our packages and create a new workspace.
RMC libraries should be build and put into a standard place #720: Improve how we are building our libraries. For now, the rmc-compiler has a build-dependency that ensures the libraries get built with the same toolchain as rmc-compiler.
Improve rmc-compiler configuration when using cargo rmc #721: Improve the interface between cargo rmc and the rmc-compiler. The solution here is a bit hacky. There are a few tricky things here. Cargo invoke rustc to retrieve its version as well as to compile build scripts which shouldn't use the goto-c backend.

Testing:

How is this change tested? All our tests.
Is this a refactor change? Yes

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.

library/rmc_macros/src/lib.rs

src/rmc-compiler/build.rs

src/rmc-compiler/src/main.rs

tedinski · 2021-12-30T18:26:02Z

scripts/rmc-rustc

what is ${RMCFLAGS} here. I mean, I can search this diff, but there should be a comment saying what's happening here.

It's set by rmc.py because cargo does some funny stuff with RUSTFLAGS.

tedinski · 2021-12-30T18:45:36Z

Also, if I'm not mistaken, if we eliminate our remaining use of x.py (just compiletest and dashboard/bookrunner, right?) CI runtimes are about to be outstanding!

celinval · 2021-12-30T20:28:56Z

Also, if I'm not mistaken, if we eliminate our remaining use of x.py (just compiletest and dashboard/bookrunner, right?) CI runtimes are about to be outstanding!

For sure! This change reduced the CI in about 10min. @adpaco-aws and I are working on the second piece. After that, we should be able to prune our repository, remove the bootstrap script and no longer depend on the rust upstream. :)

src/rmc-compiler/rust-toolchain.toml

Follow the instructions to compile the code using cargo. Need to investigate how to use rustup for std and how to manage rustc version. We need to match the version of rustc that we consume and that we use to compile the code.

Next: Need to move rmc codegen crate.

Still need to fix the change we made to CodegenBackend trait.

Note: Still need to add options to rustc_codegen_rmc

\o/\o/

We would like to allow users to enable / disable the rmc configuraiton in our prelude libraries. Cargo can only do that if the configuration uses feature statement. Hence, I replaced #[cfg(rmc)] by \#[cfg(feature = rmc)]. Note that we only need this because we use regular rustc to pre-compile our libraries.

This is a temporary fix to ensure that our libraries are compiled with the same version as the rmc-compiler. We can remove this once we have a proper workspace configured.

- Add support to the rmc codegen flags - Fix cargo regression (NEED TO DO BETTER)

Instead of building the libraries as part of the build dependencies, we now build them using the build.rs script.

tedinski

LGTM. Think DSN should review too?

src/rmc-compiler/src/main.rs

celinval · 2022-01-03T23:50:07Z

LGTM. Think DSN should review too?

I think it would be nice to have someone else reviewing it. Let me ping @danielsn.

danielsn

Some questions, but LGTM

.github/workflows/rmc.yml

scripts/cargo-rmc

danielsn · 2022-01-04T23:24:05Z

src/rmc-compiler/cbmc/src/lib.rs

 //!
 //! Speical [id]s include:
 //! 1. [Empty] and [Nil] behaves like [null].
+#![feature(rustc_private)]


What does this do?

It allow us to use rustc crates.

src/rmc-compiler/cbmc/src/lib.rs

src/rmc-compiler/rust-toolchain.toml

src/rmc-compiler/src/main.rs

danielsn · 2022-01-05T20:02:11Z

src/rmc-compiler/src/main.rs

+    );
+    let sysroot = sysroot_path(args.value_of("sysroot")).unwrap();
+    rustc_args.push(String::from("--sysroot"));
+    rustc_args.push(sysroot.to_string_lossy().to_string());


Is to_string_lossy what we want here? If there are non-valid characters, shouldn't we just fail?

Sure. We can fail.

danielsn · 2022-01-05T20:04:11Z

src/rmc-compiler/README.md

+
+### Notes for developers:
+
+This binary can be build like a regular cargo package. There is no need to


- Replace lossy translation of args by error check. - Add more comments. - Fix typo.

Conflicts: Cargo.lock compiler/cbmc/Cargo.toml

danielsn

I think there is an issue where you meant to say . and write .. for a directory path. Not sure, but blocking merge till we look at it

danielsn · 2022-01-07T15:11:06Z

src/rmc-compiler/build.rs

+
+macro_rules! path_str {
+    ($input:expr) => {
+        &$input.iter().collect::<PathBuf>().to_string_lossy().into_owned()


Did we want to do a lossy conversion, or to fail fast here?

Sure, I can fall fast.

src/rmc-compiler/build.rs

…g#722 yet)

This change introduces a new compilation driver (rmc-compiler) that no longer depends on a modified version of the rust compiler, neither depends on the bootstrap script. The rmc-compiler binary can be build using regular cargo build and can be used as a replacement to rustc with additional options that allow us to compile rust into goto-c.

celinval requested a review from a team as a code owner December 29, 2021 23:54

tedinski reviewed Dec 30, 2021

View reviewed changes

src/rmc-compiler/rust-toolchain.toml Outdated Show resolved Hide resolved

celinval added 17 commits January 3, 2022 10:05

Start a package for the rmc-compiler driver

5a71db1

Follow the instructions to compile the code using cargo. Need to investigate how to use rustup for std and how to manage rustc version. We need to match the version of rustc that we consume and that we use to compile the code.

Integrated rustc to rmc-compiler

759efc1

Next: Need to move rmc codegen crate.

Move cbmc and rustc_codegen_rmc to rmc-compiler.

736dc93

Still need to fix the change we made to CodegenBackend trait.

Remove all changes from rustc compiler.

d8a31b2

Note: Still need to add options to rustc_codegen_rmc

Upgrading toolchain after rebase

82deaa2

Initial working driver.

40cabae

\o/\o/

RMC now works with rmc-compiler binary

38e1ffb

Compiler rmc libraries as part of rmc-compiler

e6bc34f

This is a temporary fix to ensure that our libraries are compiled with the same version as the rmc-compiler. We can remove this once we have a proper workspace configured.

A bunch of stuff

20afb59

- Add support to the rmc codegen flags - Fix cargo regression (NEED TO DO BETTER)

Fix regression

dea733f

Update rust toolchain version

4da4f7c

Fix regression after adding rmc-compiler

344b90e

Better documentation.

094a52d

Adding tests to parser

b41f8f4

Ignore Cargo.lock format check

749910e

Revert change to rmc libraries

a99804d

Instead of building the libraries as part of the build dependencies, we now build them using the build.rs script.

celinval force-pushed the rmc-compiler branch from d270afe to a99804d Compare January 3, 2022 21:21

tedinski approved these changes Jan 3, 2022

View reviewed changes

src/rmc-compiler/src/main.rs Show resolved Hide resolved

danielsn approved these changes Jan 5, 2022

View reviewed changes

celinval added 3 commits January 6, 2022 16:11

Address PR comments.

6536629

- Replace lossy translation of args by error check. - Add more comments. - Fix typo.

Merge remote-tracking branch 'origin/main' into rmc-compiler

cbb16b5

Merge remote-tracking branch 'origin/main' into rmc-compiler

33f705c

Conflicts: Cargo.lock compiler/cbmc/Cargo.toml

danielsn suggested changes Jan 7, 2022

View reviewed changes

danielsn self-requested a review January 7, 2022 17:38

danielsn approved these changes Jan 7, 2022

View reviewed changes

celinval added 2 commits January 7, 2022 12:51

Remove lossy conversion + add queries to GotoCtx

2e2c29e

Fix comment on rmc-rustc

65205fc

celinval merged commit 1534ee4 into model-checking:main Jan 7, 2022

zhassan-aws mentioned this pull request Jan 12, 2022

Remove mention of missing installation script #744

Closed

4 tasks

adpaco-aws mentioned this pull request Jan 12, 2022

Book runner is broken #748

Closed

tedinski added a commit to tedinski/rmc that referenced this pull request Jan 18, 2022

rename to cargo-kani (not yet working, must account for model-checkin…

2dfa3d2

…g#722 yet)


		### Notes for developers:

		This binary can be build like a regular cargo package. There is no need to

Conversation

celinval commented Dec 29, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

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!

tedinski commented Dec 30, 2021

Uh oh!

celinval commented Dec 30, 2021

Uh oh!

Uh oh!

tedinski left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

celinval commented Jan 3, 2022

Uh oh!

danielsn 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!

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!

danielsn 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!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

celinval commented Dec 29, 2021 •

edited

Loading