Implement validity checks #3085

celinval · 2024-03-16T06:38:05Z

This is still incomplete, but hopefully it can be merged as an unstable feature. I'll publish an RFC shortly.

This instruments the function body with assertion checks to see if users are generating invalid values. This covers:

Union access
Raw pointer dereference
Transmute value
Field assignment of struct with invalid values
Aggregate assignment

Things not covered today should trigger ICE or a delayed verification failure due to unsupported feature.

Design

This change has two main design changes which are inside the new kani_compiler::kani_middle::transform module:
1- Instance body should now be retrieved from the BodyTransformation structure. This structure will run transformation passes on instance bodies (i.e.: monomorphic instances) and cache the result.
2- Create a new transformation pass that instruments the body of a function for every potential invalid value generation.
3- Create a body builder which contains all elements of a function body and mutable functions to modify them accordingly.

Call-outs

I am planning to add expected tests in a follow up PR.
This PR is currently blocked since it requires toolchain nightly-2024-03-15.
One potential improvement for later is to replace most of the build check logic by an internal Kani library function that handle the comparison.

Related to #2998
Fixes #301

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

This is still incomplete, but hopefully it can be merged as an unstable feature. This instruments the function body with assertion checks to see if users are generating invalid values. This covers: - Union access - Raw pointer dereference - Transmute value - Field assignment of struct with invalid values - Aggregate assignment Things not covered today should trigger ICE or verification failure.

zhassan-aws

The first round of comments. I haven't finished reviewing the entire PR yet.

kani-compiler/src/args.rs

kani_metadata/src/unstable.rs

tests/kani/ValidValues/custom_niche.rs

tests/kani/ValidValues/write_invalid.rs

zhassan-aws

Some nits

kani-compiler/src/kani_middle/transform/check_values.rs

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

This check today was relying on the tuple layout, which is not guaranteed. Instead, only check for the first operand. This is actually simpler.

zhassan-aws

Awesome work, @celinval!

kani-compiler/src/kani_middle/transform/mod.rs

@zhassan-aws

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

In the previous PR #3085, we did not support checks for `write_bytes` which is added in this PR. I am waiting for #3092 to add expected tests.

@zhassan-aws

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

In the previous PR model-checking#3085, we did not support checks for `write_bytes` which is added in this PR. I am waiting for model-checking#3092 to add expected tests.

celinval requested a review from a team as a code owner March 16, 2024 06:38

celinval marked this pull request as draft March 16, 2024 06:38

github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Mar 16, 2024

celinval mentioned this pull request Mar 18, 2024

Kani should detect Rust specific undefined behavior #3089

Open

3 tasks

Merge branch 'main' into invalid_values

28c0a5a

celinval marked this pull request as ready for review March 18, 2024 22:32

celinval linked an issue Mar 19, 2024 that may be closed by this pull request

Advise on verifying state machines with kani #3016

Open

celinval removed a link to an issue Mar 19, 2024

Advise on verifying state machines with kani #3016

Open

celinval mentioned this pull request Mar 19, 2024

Missing check for object correctness invariants #301

Closed

celinval self-assigned this Mar 19, 2024

zhassan-aws reviewed Mar 19, 2024

View reviewed changes

zhassan-aws reviewed Mar 21, 2024

View reviewed changes

kani-compiler/src/kani_middle/transform/check_values.rs Outdated Show resolved Hide resolved

kani-compiler/src/kani_middle/transform/check_values.rs Outdated Show resolved Hide resolved

kani-compiler/src/kani_middle/transform/check_values.rs Outdated Show resolved Hide resolved

celinval and others added 6 commits March 21, 2024 12:13

Apply suggestions from code review

3386248

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Apply suggestions from PR review

067e2c8

Rename BodyBuilder to MutableBody

08ea850

Fix build

4f8d007

Make aggregate check more robust

84c88e2

This check today was relying on the tuple layout, which is not guaranteed. Instead, only check for the first operand. This is actually simpler.

Merge branch 'main' into invalid_values

3f54ee3

zhassan-aws approved these changes Mar 22, 2024

View reviewed changes

kani-compiler/src/kani_middle/transform/mod.rs Outdated Show resolved Hide resolved

celinval added 2 commits March 22, 2024 16:07

Return body instead of Option<Body>

97d6c76

Merge remote-tracking branch 'origin/main' into invalid_values

f1423af

celinval enabled auto-merge (squash) March 22, 2024 23:09

celinval and others added 2 commits March 25, 2024 10:45

Merge branch 'main' into invalid_values

a2bb65f

Merge branch 'main' into invalid_values

f600a52

celinval merged commit e4a90e9 into model-checking:main Mar 25, 2024
19 of 20 checks passed

celinval mentioned this pull request Mar 26, 2024

Implement check for write_bytes #3108

Merged

adpaco-aws mentioned this pull request Mar 27, 2024

Unexpected Alias type with -Z valid-value-checks #3113

Closed

tautschnig mentioned this pull request Apr 5, 2024

Bump Kani version to 0.49.0 #3126

Merged

tautschnig pushed a commit that referenced this pull request Apr 5, 2024

Implement check for write_bytes (#3108)

b329c85

In the previous PR #3085, we did not support checks for `write_bytes` which is added in this PR. I am waiting for #3092 to add expected tests.

celinval mentioned this pull request May 27, 2024

Implement validity checks for unsupported constructs #3203

Open

4 tasks

zhassan-aws mentioned this pull request Sep 13, 2024

Challenge 6: Safety of NonNull model-checking/verify-rust-std#53

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement validity checks #3085

Implement validity checks #3085

celinval commented Mar 16, 2024 •

edited

Loading

zhassan-aws left a comment

zhassan-aws left a comment

zhassan-aws left a comment

Implement validity checks #3085

Implement validity checks #3085

Conversation

celinval commented Mar 16, 2024 • edited Loading

Design

Call-outs

zhassan-aws left a comment

Choose a reason for hiding this comment

zhassan-aws left a comment

Choose a reason for hiding this comment

zhassan-aws left a comment

Choose a reason for hiding this comment

celinval commented Mar 16, 2024 •

edited

Loading