Skip to content
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

Jump to bottom

Enable MIR Linker by default and adjust tests #1785

Merged
merged 3 commits into from
Oct 17, 2022
Merged

Enable MIR Linker by default and adjust tests #1785

merged 3 commits into from
Oct 17, 2022

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Oct 14, 2022 •
edited
Loading

Description of changes:

Enable --mir-linker by default. This change doesn't remove the option yet though to avoid breaking users harnesses. Introduce a --legacy-linker to allow users to switch to the older linker to overcome performance issues as well as any possible issue with the MIR Linker.

Resolved issues:

Resolves #1677
Resolves #1738
Resolves #1720

Related RFC:

#1588

Call-outs:

I had to adjust a bunch of tests for the following reasons:

Testing:

  • How is this change tested? The regression

  • 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.

@celinval
Enable MIR Linker by default and adjust tests
0a5606e 
  - intrinsics: Use legacy linker for some of them because of not so
    friendly messages.
  - performance: A few test are taking too long because of the new
    symbols being included in the analysis. Keep legacy linker for now.
  - integ-test: Using --tests with integration tests fail with MIR Linker.
  - fixme: Enable a few fixme tests and tests that were marked as
    verify-fail due to missing symbols. These run fine now with the
    linker.
@celinval celinval requested a review from a team as a code owner October 14, 2022 02:54
@tedinski
Copy link
Contributor

Using --tests with integration tests fail with MIR Linker

I'm worried this might be a blocker. How much of a bother is this to fix? Do we need a fully solution to:

i.e. Understanding the build graph better in kani-driver?

@celinval
Copy link
Contributor Author

Yeah, that's in the top of my list. I'll see if I can get a fix in today. Now that I think about it it would break whenever integration tests exists even without any proof harness.

@adpaco-aws adpaco-aws mentioned this pull request Oct 14, 2022
Closed
@celinval
Copy link
Contributor Author

I created #1789 to fix the tests issue. Once that gets merged, I'll update the test in this PR to also use the MIR Linker

tedinski
tedinski reviewed Oct 16, 2022
View reviewed changes
kani-driver/src/args.rs Outdated
/// The MIR Linker affects how Kani prunes the code to be analyzed. It also fixes previous
/// issues with missing `std` function definitions.
/// See <https://model-checking.github.io/kani/rfc/rfcs/0001-mir-linker.html> for more details.
#[structopt(long, conflicts_with("legacy_linker"))]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we "hide" this option?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure

scripts/codegen-firecracker.sh Show resolved Hide resolved
tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs
//!
//! When enabling "--mir-linker", the error we currently get is:
//! > Failed checks: Called `Option::unwrap()` on a `None` value
//! This happens because of std debug checks. The `is_nonoverlapping` check has a
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Honestly I wonder if we should just disable debug_assert in our build of std for now?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's an interesting idea. It would help with this for now. It would be interesting to see how much more UB checks the std encode as debug_assert().

tests/kani/Refs/main.rs Outdated
//! * working_directory: /Users/dsn/ws/RustToCBMC/src/RustToCBMC/rust-tests/cbmc-reg/Refs
//! * value: 0
//!
//! Note: This test takes too long with all the std symbols. Use --legacy-linker for now
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please move the comment closer to the flag.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

will do. I am actually tempted to remove this random log from the comments. I can make sure the original ticket has it and just point to the ticket for more details. I didn't bother doing this here because I was worried about the size of this PR.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please do, I don't think the log is that helpful.

tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs Outdated Show resolved Hide resolved
tests/kani/Slice/pathbuf.rs Show resolved Hide resolved
tests/kani/Strings/parse.rs Show resolved Hide resolved
tests/ui/missing-function/rust-by-example-description/main.rs
// SPDX-License-Identifier: Apache-2.0 OR MIT

// kani-flags: --enable-unstable --cbmc-args --unwind 4 --object-bits 9
// This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While this one doesn't work, shouldn't we keep a test for the property description? IIRC we had difficulty detecting it in the past. Or did this get replaced with a different test and I didn't notice

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did keep two test for that. There is one test for the case of an extern function and one for the --legacy-linker

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@celinval
Merge remote-tracking branch 'origin/main' into issue-1738-default-li…
0c3b62e 
…nker
@celinval
Addressing PR feedback
1f4f130 
 1. Hide new arguments from `kani (-h|--help)`.
 2. Update `cargo kani --tests` test to use the MIR Linker.
 3. Update a few comments.
tedinski
tedinski approved these changes Oct 17, 2022
View reviewed changes
Copy link
Contributor

@tedinski tedinski left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. I would vote for temporarily disabling std debug_assert since the UX is bad, but I don't think that needs to be folded into this PR, and maybe is something we can slip to the next release.

@celinval celinval merged commit fc43543 into model-checking:main Oct 17, 2022
@celinval celinval mentioned this pull request Oct 25, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@adpaco-aws adpaco-aws adpaco-aws left review comments

@tedinski tedinski tedinski approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
3 participants
@celinval @tedinski @adpaco-aws