Contracts for a few core functions by celinval · Pull Request #3107 · model-checking/kani

celinval · 2024-03-25T23:52:07Z

Adds a new regression test suite that includes safety contracts for core functions.

Call-out

This PR is still incomplete since it depends on a few changes that are still pending. For example, #2997 is a blocker. The relevant changes should be the regression script changes and in the new directory tests/std-checks.

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

This will allow us to re-use contracts between modules. We still cannot compile our contracts due to model-checking#2997

Create a value of `[val; size_of::<T>()]` and check if it is a valid combination of bytes for T.

celinval · 2024-05-14T21:18:32Z

FYI, I'm planning to add more tests to the new intrinsic in a follow up PR together with any possible fix.

- I noticed that invalid values should be checked for copy_nonoverlapping statement. I added an unsupported check for now so we can actually implement the check later.

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.51.0"/version = "0.52.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Bump tests/perf/s2n-quic from `6dd41e0` to `bd37960` by @dependabot in model-checking#3178 * Automatic cargo update to 2024-05-13 by @github-actions in model-checking#3177 * Upgrade toolchain to 2024-04-22 by @zhassan-aws in model-checking#3171 * Upgrade toolchain to 2024-05-14 by @zhassan-aws in model-checking#3183 * Automatic toolchain upgrade to nightly-2024-05-15 by @github-actions in model-checking#3185 * Include `--check-cfg=cfg(kani)` in the rust flags to avoid a warning about an unknown `cfg`. by @zhassan-aws in model-checking#3187 * Automatic toolchain upgrade to nightly-2024-05-16 by @github-actions in model-checking#3189 * Perform cargo update because of yanked libc version by @zhassan-aws in model-checking#3192 * Automatic toolchain upgrade to nightly-2024-05-17 by @github-actions in model-checking#3191 * Automatic cargo update to 2024-05-20 by @github-actions in model-checking#3195 * Bump tests/perf/s2n-quic from `bd37960` to `f5d9d74` by @dependabot in model-checking#3196 * New section about linter configuraton checking in the doc. by @remi-delmas-3000 in model-checking#3198 * Automatic cargo update to 2024-05-27 by @github-actions in model-checking#3201 * Bump tests/perf/s2n-quic from `f5d9d74` to `d03cc47` by @dependabot in model-checking#3202 * Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23 by @remi-delmas-3000 in model-checking#3199 * Fix `{,e}println!()` by @GrigorenkoPV in model-checking#3209 * Contracts for a few core functions by @celinval in model-checking#3107 * Don't crash benchcomp when rounding non-numeric values by @karkhaz in model-checking#3211 * Update Rust toolchain nightly-2024-05-24 by @qinheping in model-checking#3212 * Upgrade Rust toolchain nightly-2024-05-27 by @qinheping in model-checking#3215 * Automatic toolchain upgrade to nightly-2024-05-28 by @github-actions in model-checking#3217 * Automatic cargo update to 2024-06-03 by @github-actions in model-checking#3220 * Bump tests/perf/s2n-quic from `d03cc47` to `d90729d` by @dependabot in model-checking#3222 * Add simple API for shadow memory by @zhassan-aws in model-checking#3200 ## New Contributors * @GrigorenkoPV made their first contribution in model-checking#3209 **Full Changelog**: model-checking/kani@kani-0.51.0...kani-0.52.0

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.51.0"/version = "0.52.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Bump tests/perf/s2n-quic from `6dd41e0` to `bd37960` by @dependabot in #3178 * Automatic cargo update to 2024-05-13 by @github-actions in #3177 * Upgrade toolchain to 2024-04-22 by @zhassan-aws in #3171 * Upgrade toolchain to 2024-05-14 by @zhassan-aws in #3183 * Automatic toolchain upgrade to nightly-2024-05-15 by @github-actions in #3185 * Include `--check-cfg=cfg(kani)` in the rust flags to avoid a warning about an unknown `cfg`. by @zhassan-aws in #3187 * Automatic toolchain upgrade to nightly-2024-05-16 by @github-actions in #3189 * Perform cargo update because of yanked libc version by @zhassan-aws in #3192 * Automatic toolchain upgrade to nightly-2024-05-17 by @github-actions in #3191 * Automatic cargo update to 2024-05-20 by @github-actions in #3195 * Bump tests/perf/s2n-quic from `bd37960` to `f5d9d74` by @dependabot in #3196 * New section about linter configuraton checking in the doc. by @remi-delmas-3000 in #3198 * Automatic cargo update to 2024-05-27 by @github-actions in #3201 * Bump tests/perf/s2n-quic from `f5d9d74` to `d03cc47` by @dependabot in #3202 * Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23 by @remi-delmas-3000 in #3199 * Fix `{,e}println!()` by @GrigorenkoPV in #3209 * Contracts for a few core functions by @celinval in #3107 * Don't crash benchcomp when rounding non-numeric values by @karkhaz in #3211 * Update Rust toolchain nightly-2024-05-24 by @qinheping in #3212 * Upgrade Rust toolchain nightly-2024-05-27 by @qinheping in #3215 * Automatic toolchain upgrade to nightly-2024-05-28 by @github-actions in #3217 * Automatic cargo update to 2024-06-03 by @github-actions in #3220 * Bump tests/perf/s2n-quic from `d03cc47` to `d90729d` by @dependabot in #3222 * Add simple API for shadow memory by @zhassan-aws in #3200 ## New Contributors * @GrigorenkoPV made their first contribution in #3209 **Full Changelog**: kani-0.51.0...kani-0.52.0

github-actionsBot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Mar 25, 2024

celinval added 8 commits March 28, 2024 13:25

Add initial tests for NonNull and mem predicates
19a4769

Improve library and change std tests to use crates.
a9c5f62
This will allow us to re-use contracts between modules. We still cannot compile our contracts due to model-checking#2997

Add support to write_bytes used in MaybeUninit
9a1dccf
Create a value of `[val; size_of::<T>()]` and check if it is a valid combination of bytes for T.

Add contract for replace
86edd76

Add missing Cargo.toml
c38136f

Merge remote-tracking branch 'origin/main' into std-non-null
3c74b6c

Rename a few things
3dffab5

Add a new intrinsic to check value validity
e844934

celinval mentioned this pull request May 14, 2024
Unexpected failure when modifies attribute points to a ZST #3181
Closed

Finish polishing contracts and create expected
7469d61

celinval force-pushed the std-non-null branch from 36042e6 to 7469d61Compare May 14, 2024 21:09

celinval marked this pull request as ready for review May 14, 2024 21:10

celinval requested a review from a team as a code owner May 14, 2024 21:10

celinval added 2 commits May 14, 2024 14:10

revert space changes
e2b4a20

Clean up changes
122e3a8

celinval force-pushed the std-non-null branch from 454e216 to 122e3a8Compare May 14, 2024 21:17

adpaco reviewed May 15, 2024
View reviewed changes

celinval commented May 17, 2024
View reviewed changes

Comment threadtests/std-checks/core/src/ptr.rs Outdated

celinval commented May 17, 2024
View reviewed changes

Comment threadtests/std-checks/core/src/ptr.rs

celinval changed the title ~~Draft: Contracts for a few core functions~~Contracts for a few core functionsMay 17, 2024

qinheping reviewed May 18, 2024
View reviewed changes

Comment threadkani-compiler/src/kani_middle/transform/kani_intrinsics.rs

feliperodri requested changes May 20, 2024
View reviewed changes

celinval added 2 commits May 23, 2024 17:18

Address comments and fix issue in invalid values
5f4a69b
- I noticed that invalid values should be checked for copy_nonoverlapping statement. I added an unsupported check for now so we can actually implement the check later.

Fix regression
c18754d

celinval force-pushed the std-non-null branch from 7769825 to c18754dCompare May 28, 2024 02:06

celinval commented May 28, 2024
View reviewed changes

Comment threadkani-compiler/src/kani_middle/transform/body.rs Outdated

karkhaz mentioned this pull request May 29, 2024
Don't crash benchcomp when rounding non-numeric values #3211
Merged

feliperodri approved these changes May 29, 2024
View reviewed changes

celinval added 2 commits May 29, 2024 09:39

Update kani-compiler/src/kani_middle/transform/body.rs
2a8cfdb

Merge branch 'main' into std-non-null
d295ce3

celinval enabled auto-merge (squash) May 29, 2024 17:01

celinval merged commit 8a2b7e5 into model-checking:mainMay 29, 2024

tautschnig mentioned this pull request Jun 4, 2024
Bump Kani version to 0.52.0 #3224
Merged

feliperodri mentioned this pull request Jun 6, 2024
Create an API to check valid raw pointer #2690
Closed

Navigation Menu

Uh oh!

Contracts for a few core functions - #3107

Contracts for a few core functions#3107
celinval merged 15 commits into
model-checking:mainfrom
celinval:std-non-null

celinval commented Mar 25, 2024•
edited
Loading

Uh oh!

celinval commented May 14, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Uh oh!

Conversation

celinval commented Mar 25, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Call-out

Uh oh!

celinval commented May 14, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

celinval commented Mar 25, 2024•
edited
Loading