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.

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

Upgrade rust toolchain to nightly-2023-06-20 #2551

Merged
merged 7 commits into from
Jul 4, 2023

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Jun 21, 2023

Description of changes:

Change Kani's compiler and tests to adapt to changes done to the toolchain. The biggest changes were:

  1. Implement overflow checks as part of rvalue.rs instead of intrinsics due to lowering of intrinsics to BinOp.
  2. Add a unsupported check for handling C string literals.

Here is a list of changes that I found that impacted this upgrade:

Resolved issues:

Resolves #2544

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

This is still a draft PR. Before publishing it, I still need to:
1. I'll pull a bunch of the tests changes to a separate PR before publishing it.
2. This is still BLOCKED by a performance degradation on one of our tests. I created #2576 to track a performance issue caused by this upgrade. I modified the regression test to go around the performance issue and created a new test that still captures the issue and is part of the performance CI job instead.

Note: I don't think there is anything complicated to actually implement C string literal support, but decided to keep this simple for now. We would also likely want to add more thorough tests too.

Testing:

  • How is this change tested?

  • Is this a refactor change?

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 celinval mentioned this pull request Jun 21, 2023
4 tasks
celinval added a commit that referenced this pull request Jun 21, 2023
This PR fixes a few flaky tests that started to fail in the ongoing toolchain update (#2551)

- The object bits test itself doesn't create that many objects since an array is represented as the same allocated object. Use LinkedList instead.
- Do not rely on property number.
- Do not rely on the order that failed checks is printed.
@celinval celinval force-pushed the issue-2544-toolchain branch from c9a43ca to 8b3ed9e Compare June 22, 2023 18:45
celinval added 4 commits June 28, 2023 15:04
 - Still need to clean regression
 - We were crashing while compiling the standard library
Use u8 instead of i8 for now and add a performance test to capture this
issue.
@celinval celinval force-pushed the issue-2544-toolchain branch from 8b3ed9e to 8ef1847 Compare June 28, 2023 22:04
@celinval
Copy link
Contributor Author

For the itoa test, I narrowed it down the performance issue to a performance regression when formatting an i8. Updating the test to a u8 makes it much faster. I am adding a new performance test and modifying the itoa test for now. I created #2576 to capture the performance regression.

@celinval celinval marked this pull request as ready for review June 29, 2023 19:42
@celinval celinval requested a review from a team as a code owner June 29, 2023 19:42
kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs Outdated Show resolved Hide resolved
tests/perf/format/src/lib.rs Outdated Show resolved Hide resolved
tests/perf/format/src/lib.rs Outdated Show resolved Hide resolved
tests/cargo-kani/itoa_dep/src/main.rs Outdated Show resolved Hide resolved
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

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

Thanks @celinval for this huge effort!

The situation with the duplicate checks is not ideal (will be confusing for users and may be downgrading performance), but we can improve it later.

@celinval
Copy link
Contributor Author

celinval commented Jul 4, 2023

Thanks @celinval for this huge effort!

The situation with the duplicate checks is not ideal (will be confusing for users and may be downgrading performance), but we can improve it later.

Yeah, sorry about that. The problem already existed, and it just got even worse. Fixing it will take a bit of time. Maybe I'll at least disable the redundant Cbmc checks for now, since that's an easy fix.

@celinval celinval merged commit 7139063 into model-checking:main Jul 4, 2023
@karkhaz karkhaz mentioned this pull request Jul 12, 2023
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Update rust toolchain version to nightly-2023-06-20
2 participants