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

Disable removal of storage markers #3083

Merged
merged 1 commit into from
Mar 18, 2024

Conversation

zhassan-aws
Copy link
Contributor

@zhassan-aws zhassan-aws commented Mar 15, 2024

Instead of turning on the address sanitizer to ensure storage markers (StorageLive and StorageDead) are kept in MIR, directly disable the MIR pass that removes them from MIR (https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Keeping.20MIR's.20storage.20markers). This is to ensure we don't get additional instrumentation that is not relevant for Kani, and may unnecessarily increase the code size and compilation time.

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

@zhassan-aws zhassan-aws added the Z-BenchCI Tag a PR to run benchmark CI label Mar 15, 2024
@zhassan-aws zhassan-aws requested a review from a team as a code owner March 15, 2024 19:44
@zhassan-aws zhassan-aws enabled auto-merge (squash) March 15, 2024 21:38
Copy link
Member

@karkhaz karkhaz left a comment

Choose a reason for hiding this comment

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

Thank you!

@zhassan-aws zhassan-aws merged commit b5ddbb8 into model-checking:main Mar 18, 2024
20 checks passed
@zhassan-aws zhassan-aws deleted the keep-storage-markers branch March 18, 2024 14:44
tautschnig added a commit that referenced this pull request Apr 5, 2024
Updated version in all `Cargo.toml` files (via
`find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version =
"0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files
updated.

GitHub generated release notes:

## What's Changed
* Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in
#3081
* Disable removal of storage markers by @zhassan-aws in
#3083
* Automatic cargo update to 2024-03-18 by @github-actions in
#3086
* Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in
#3087
* Upgrade toolchain to nightly-2024-03-15 by @celinval in
#3084
* Add optional scatterplot to benchcomp output by @tautschnig in
#3077
* Benchcomp scatterplots: quote axis labels by @tautschnig in
#3097
* Expand ${var} in benchcomp variant `env` by @karkhaz in
#3090
* Add test for #3099 by @zhassan-aws in
#3100
* Automatic cargo update to 2024-03-25 by @github-actions in
#3103
* Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in
#3104
* Implement validity checks by @celinval in
#3085
* Add `benchcomp filter` command by @karkhaz in
#3105
* Add CI test for --use-local-toolchain by @jaisnan in
#3074
* Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in
#3102
* Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in
#3114
* Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in
#3118
* Allow modifies clause for verification only by @feliperodri in
#3098
* Automatic cargo update to 2024-04-01 by @github-actions in
#3117
* Automatic cargo update to 2024-04-04 by @github-actions in
#3122
* Remove bookrunner by @tautschnig in
#3123
* Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in
#3116
* Remove unnecessary build step for some workflows by @zhassan-aws in
#3124
* Ensure storage markers are kept in std code by @zhassan-aws in
#3080


**Full Changelog**:
kani-0.48.0...kani-0.49.0
zpzigi754 pushed a commit to zpzigi754/kani that referenced this pull request May 8, 2024
Updated version in all `Cargo.toml` files (via
`find . -name Cargo.toml -exec sed -i 's/version = "0.48.0"/version =
"0.49.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files
updated.

GitHub generated release notes:

## What's Changed
* Upgrade Rust toolchain to 2024-03-14 by @zhassan-aws in
model-checking#3081
* Disable removal of storage markers by @zhassan-aws in
model-checking#3083
* Automatic cargo update to 2024-03-18 by @github-actions in
model-checking#3086
* Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` by @dependabot in
model-checking#3087
* Upgrade toolchain to nightly-2024-03-15 by @celinval in
model-checking#3084
* Add optional scatterplot to benchcomp output by @tautschnig in
model-checking#3077
* Benchcomp scatterplots: quote axis labels by @tautschnig in
model-checking#3097
* Expand ${var} in benchcomp variant `env` by @karkhaz in
model-checking#3090
* Add test for model-checking#3099 by @zhassan-aws in
model-checking#3100
* Automatic cargo update to 2024-03-25 by @github-actions in
model-checking#3103
* Bump tests/perf/s2n-quic from `1a7faa8` to `0a60ec1` by @dependabot in
model-checking#3104
* Implement validity checks by @celinval in
model-checking#3085
* Add `benchcomp filter` command by @karkhaz in
model-checking#3105
* Add CI test for --use-local-toolchain by @jaisnan in
model-checking#3074
* Upgrade Rust toolchain to `nightly-2024-03-21` by @adpaco-aws in
model-checking#3102
* Use `intrinsic_name` to get the intrinsic name by @adpaco-aws in
model-checking#3114
* Bump tests/perf/s2n-quic from `0a60ec1` to `2d5e891` by @dependabot in
model-checking#3118
* Allow modifies clause for verification only by @feliperodri in
model-checking#3098
* Automatic cargo update to 2024-04-01 by @github-actions in
model-checking#3117
* Automatic cargo update to 2024-04-04 by @github-actions in
model-checking#3122
* Remove bookrunner by @tautschnig in
model-checking#3123
* Upgrade Rust toolchain to nightly-2024-03-29 by @feliperodri in
model-checking#3116
* Remove unnecessary build step for some workflows by @zhassan-aws in
model-checking#3124
* Ensure storage markers are kept in std code by @zhassan-aws in
model-checking#3080


**Full Changelog**:
model-checking/kani@kani-0.48.0...kani-0.49.0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants