Skip to content

Toolchain update 06-01-2025 - #3814

Merged
remi-delmas-3000 merged 10 commits into
model-checking:mainfrom
remi-delmas-3000:toolchain-update-06-01-2025
Jan 10, 2025
Merged

Toolchain update 06-01-2025#3814
remi-delmas-3000 merged 10 commits into
model-checking:mainfrom
remi-delmas-3000:toolchain-update-06-01-2025

Conversation

@remi-delmas-3000

Copy link
Copy Markdown
Contributor

Please review commit by commit, as each commit propagates an upstream change:

  • SourceRegion was moved from MIR to the LLVM backend and made private, I recreated the type and functionality locally to preserve our handling of regions in coverage assertions,
  • Propagated changes to the representation of uninhabited enums (with no variants),
  • Propagated remove of RValue::Len(place) from MIR (still present in stable MIR, so I used PtrMetadata(Copy(place)) to translate Len(place) back from StableMIR to MIR).
  • Propagated addition of UnsafeBinder enum variant (WIP in rustc, no clear semantics yet, left as TODO)

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@remi-delmas-3000
remi-delmas-3000 requested a review from a team as a code ownerJanuary 6, 2025 23:22
@remi-delmas-3000
remi-delmas-3000 marked this pull request as draft January 6, 2025 23:23
@github-actionsgithub-actionsBot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jan 6, 2025
@qinheping

Copy link
Copy Markdown
Contributor

Could you also include the information about related upstream commits?

@remi-delmas-3000

Copy link
Copy Markdown
ContributorAuthor

Could you also include the information about related upstream commits?

Each commit message contains the link to the upstream change

@remi-delmas-3000
remi-delmas-3000force-pushed the toolchain-update-06-01-2025 branch 2 times, most recently from 47ca3ca to 48b03f0CompareJanuary 7, 2025 17:43
Remi Delmas added 8 commits January 7, 2025 13:19
The original SourceRegion was moved to the llvm backend and made
private by rust-lang/rust#134497.
We implement our own local version of it to maintain our handling
of SourceRegion for coverage properties.
Propagated from rust-lang/rust#133702.
Empty enums now have `Variants::Empty` as variants instead of
`Variants::Single{ index: None }`.
Rustc has started implementing `UnsafeBinder`:
- rust-lang/rust#134625
- rust-lang/rust#130516
Only the enums variants have been added for now, semantics is TBD.
Propagated form rust-lang/rust#134330.
`RValue::Len(place)` is still present in StableMIR,
so we translate it back to MIR as `PtrMetadata(Copy(place))`.
@remi-delmas-3000
remi-delmas-3000force-pushed the toolchain-update-06-01-2025 branch from 77b4ce0 to cc4abe6CompareJanuary 7, 2025 18:19
@remi-delmas-3000
remi-delmas-3000 marked this pull request as ready for review January 7, 2025 18:20
@remi-delmas-3000

Copy link
Copy Markdown
ContributorAuthor

All tests passing now

@celinvalcelinval left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Looks good to me. Thanks!

Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs Outdated

@qinhepingqinheping left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM

@remi-delmas-3000
remi-delmas-3000force-pushed the toolchain-update-06-01-2025 branch from 3cb70d2 to cc4abe6CompareJanuary 8, 2025 18:14
@remi-delmas-3000

remi-delmas-3000 commented Jan 8, 2025

Copy link
Copy Markdown
ContributorAuthor

Reverting from using LineInfo from stable MIR back to using our own SourceRegion as they seem to represent different things:

https://github.com/Zalathar/rust/blob/aced4dcf1047aab08b769b34fae9d4ba7de87f04/compiler/rustc_codegen_llvm/src/coverageinfo/mapgen/spans.rs#L1[…]C33
https://github.com/rust-lang/rust/blob/6afee111c2faf86ba884ea748967130abad37b52/compiler/rustc_smir/src/rustc_smir/context.rs#L300

1 |// Copyright Kani Contributors2 |// SPDX-License-Identifier: Apache-2.0 OR MIT3 |
4 |//! Checks that `check_assert` is fully covered. At present, the coverage for5 |//! this test reports an uncovered single-column region at the end of the `if`6 |//! statement: <https://github.com/model-checking/kani/issues/3455>7 |
8 |#[kani::proof]9 |fn check_assert(){10| let x:u32 = kani::any_where(|val| *val == 5);11| if x > 3{12| assert!(x > 4);13| }14|}
SUMMARY:
** 0 of 7 failed
VERIFICATION:- SUCCESSFUL
Source-based code coverage results:
// using SourceRegion
test.rs (check_assert)
* 9:1 - 10:34 COVERED
* 11:14 - 13:6 COVERED
* 13:5 - 13:6 UNCOVERED <--- difference here
test.rs (check_assert::{closure#0})
* 10:40 - 10:49 COVERED
// using LineInfo
test.rs (check_assert)
* 9:1 - 10:34 COVERED
* 11:14 - 13:6 COVERED
* 13:6 - 13:6 UNCOVERED <--- difference here
test.rs (check_assert::{closure#0})
* 10:40 - 10:49 COVERED

with LineInfo we get 13:6 - 13:6 for the lone closing brace on line 13, SourceRegion gives 13:5 - 13:6.
I'm sticking with SourceRegion for now to preserve the interface to LLVM coverage formatting tool used by kani-coverage. Differences could be on the interpretation of the interval as inclusive or non-inclusive of the upper bound, or the units used for columns (in SourceRegion column indices are in bytes, for line info it could be number of characters).

@remi-delmas-3000
remi-delmas-3000force-pushed the toolchain-update-06-01-2025 branch from 6ff5f3a to f9134c8CompareJanuary 9, 2025 22:22
@remi-delmas-3000
remi-delmas-3000 added this pull request to the merge queueJan 9, 2025
Merged via the queue into model-checking:main with commit bd6ca46Jan 10, 2025
@remi-delmas-3000
remi-delmas-3000 deleted the toolchain-update-06-01-2025 branch January 10, 2025 00:24
@qinhepingqinheping mentioned this pull request Jan 10, 2025
github-merge-queueBot pushed a commit that referenced this pull request Jan 11, 2025
## What's Changed
* Package Docker release step: ensure compiler is installed by
@tautschnig in #3789
* Improve `--jobs` UI by @carolynzech in
#3790
* Update kissat to v4.0.1 by @remi-delmas-3000 in
#3791
* Automatic cargo update to 2024-12-23 by @github-actions in
#3792
* Bump tests/perf/s2n-quic from `0b3f892` to `a54686e` by @dependabot in
#3793
* Upgrade toolchain to nightly-2024-12-18 by @zhassan-aws in
#3794
* Automatic cargo update to 2024-12-30 by @github-actions in
#3800
* fix: clippy by @ShoyuVanilla in
#3806
* Update dependencies (02.01.2025). by @remi-delmas-3000 in
#3809
* Update charon submodule by @zhassan-aws in
#3801
* Upgrade toolchain to 2024-12-19 by @zhassan-aws in
#3810
* Automatic cargo update to 2025-01-06 by @github-actions in
#3812
* Bump tests/perf/s2n-quic from `a54686e` to `ac52a48` by @dependabot in
#3813
* Generate contracts of dependencies as assertions by @carolynzech in
#3802
* Fix hanging command in `std-analysis.sh` by @carolynzech in
#3818
* Add UB checks for ptr_offset_from* intrinsics by @celinval in
#3757
* Toolchain update 06-01-2025 by @remi-delmas-3000 in
#3814
* Automatic toolchain upgrade to nightly-2025-01-07 by @github-actions
in #3820
* Include manifest-path when checking if packages are in the workspace
by @qinheping in #3819
## New Contributors
* @ShoyuVanilla made their first contribution in
#3806
**Full Changelog**:
kani-0.57.0...kani-0.58.0
---------
Co-authored-by: Celina G. Val <celinval@amazon.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCITag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants

@remi-delmas-3000@qinheping@celinval