Create an RMC crate and load it as part of rmc-rustc by celinval · Pull Request #597 · model-checking/kani

celinval · 2021-10-29T00:36:49Z

Description of changes:

Users should now be able to use rmc::nondet(), rmc::assume(bool) and rmc::expect_fail as part of their test harnesses. RMC will automatically load the rmc library as part of any crate compilation.

Resolved issues:

Resolves #231 and #589.

Call-outs:

This PR also include updates to enable this change.

I have also updated rmc-rustc to include the flags required by rmc so we don't need to maintain them in so many different places.
I updated the tests to use the new definition.s
I fixed an issue in the rmc codegen that was ignoring no-codegen option. This was breaking the compiletest check.

Testing:

How is this change tested? In all tests that were updated.
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.

- Create an rmc crate (model-checking#231). - Used rust compliant names for the functions (model-checking#589). - Changed rmc-rustc to inject the rmc prelude as part of the compilation as well as other rmc configuration flags. - Added options to rmc-rustc to print binary path and flags so it can be used in other scripts.

RMC code generation was creating artifacts even if rustc was run with -Z no-codegen. I changed the codegen to check for this option before writing the json files. This issue was uncovered by my change to move the rmc flags to rmc-rustc. This script is used during compiletest. In the check stage, the test runs rustc with --no-codegen.

adpaco-aws

This is awesome! Some comments.

library/rmc/src/lib.rs

compiler/rustc_codegen_rmc/src/overrides/hooks.rs

library/rmc/src/lib.rs

adpaco-aws · 2021-10-29T13:44:52Z

.github/workflows/rmc.yml

          ./x.py build -i --stage 1 library/std

+      - name: Build RMC Library
+        run: bash -x ./scripts/setup/build_rmc_lib.sh


Is there any advantage to having -x written here and not in the script itself?

I was wondering if this script will be helpful for users to build RMC library. In this case, we can keep the trace turned off by default, but still turn them on in the CI. What do you think?

Makes sense.

library/rmc/src/lib.rs

zhassan-aws · 2021-10-29T17:06:10Z

compiler/rustc_codegen_rmc/src/compiler_interface.rs

-        // "path.o"
-        let base_filename = outputs.path(OutputType::Object);
+        // No output should be generated if user selected no_codegen.
+        if !sess.opts.debugging_opts.no_codegen && sess.opts.output_types.should_codegen() {


Does this need to be in the same PR?

Yes. The regression will fail if this is not here.

I can submit a separate PR and merge it first if that makes more sense.

https://github.com/model-checking/rmc/pull/601/files

adpaco-aws

LGTM! My only concern now is that compiling the RMC library is necessary to use these predicates, so we should update the documentation accordingly. But we can have that in a follow-up PR.

adpaco-aws · 2021-10-29T19:48:23Z

.github/workflows/rmc.yml

          ./x.py build -i --stage 1 library/std

+      - name: Build RMC Library
+        run: bash -x ./scripts/setup/build_rmc_lib.sh


Makes sense.

celinval · 2021-10-29T20:28:05Z

LGTM! My only concern now is that compiling the RMC library is necessary to use these predicates, so we should update the documentation accordingly. But we can have that in a follow-up PR.

Good point. I'll submit a PR for that!

camshaft · 2021-10-29T22:49:14Z

library/rmc/src/lib.rs

+/// ```
+#[inline(never)]
+#[rustc_diagnostic_item = "RmcNonDet"]
+pub fn nondet<T>() -> T {


This really needs to be marked as unsafe as callers need to ensure all of the type's invariants are met.

I have pushed this code already, but I created #607 to capture the work to fix this. Thanks

@camshaft #657

camshaft · 2021-10-29T22:51:45Z

library/rmc/src/lib.rs

+/// ```
+#[inline(never)]
+#[rustc_diagnostic_item = "RmcAssume"]
+pub fn assume(_cond: bool) {}


For a better docs and IDE experience, it would be preferable to do something like:

pub fn assume(cond: bool) { let _ = cond; }

Same goes for the other arguments.

Sure. I'll fix this next time I push some updates to this crate. Thanks for the suggestion.

) * Adding support to new rmc prelude definitions - Create an rmc crate (model-checking#231). - Used rust compliant names for the functions (model-checking#589). - Changed rmc-rustc to inject the rmc prelude as part of the compilation as well as other rmc configuration flags. - Added options to rmc-rustc to print binary path and flags so it can be used in other scripts. * Add a script to build rmc library * Update tests to use new injected prelude.

* Adding support to new rmc prelude definitions - Create an rmc crate (#231). - Used rust compliant names for the functions (#589). - Changed rmc-rustc to inject the rmc prelude as part of the compilation as well as other rmc configuration flags. - Added options to rmc-rustc to print binary path and flags so it can be used in other scripts. * Add a script to build rmc library * Update tests to use new injected prelude.

celinval added 4 commits October 28, 2021 10:48

Add a script to build rmc library

f05a451

Update tests to use new injected prelude.

25d1a54

adpaco-aws reviewed Oct 29, 2021

View reviewed changes

Address PR comments.

2f22516

zhassan-aws reviewed Oct 29, 2021

View reviewed changes

Fix typos

ba6ebff

celinval mentioned this pull request Oct 29, 2021

Fix rmc codegen to check for no-codegen option #601

Merged

4 tasks

adpaco-aws approved these changes Oct 29, 2021

View reviewed changes

celinval merged commit b5f2044 into model-checking:main Oct 29, 2021

celinval deleted the issue-231 branch October 29, 2021 20:28

celinval mentioned this pull request Oct 29, 2021

Update installation guide to include rmc lib build #604

Merged

4 tasks

camshaft reviewed Oct 29, 2021

View reviewed changes

Conversation

celinval commented Oct 29, 2021

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

adpaco-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

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!

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!

adpaco-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

celinval commented Oct 29, 2021

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

celinval Oct 29, 2021 •

edited

Loading