Update to CBMC version 6.1.1 by tautschnig · Pull Request #2995 · model-checking/kani

tautschnig · 2024-02-06T13:08:35Z

Updates to match changes to the GOTO binary format.

This includes changes our handling of storage markers to be marking is-alive only rather than treating StorageLive as creating a new object. That is, object instances are now tied to their Mir-provided declarations (which, at present, only appear once per function). To still account for when Rust scopes deem an object to be alive, we use StorageLive and StorageDead to update __CPROVER_dead_object. This (global) variable is used by CBMC's pointer checks to track when a pointer may not be safe to dereference for it could be pointing to an object that no longer is in scope.

Resolves: #3099

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

Updates to match changes to the GOTO binary format. Resolves: model-checking#2972

This reverts commit e95e689.

This reverts commit 5d73a67.

This reverts commit d6e78a8.

This reverts commit d591c4d.

This changes our handling of storage markers to be marking is-alive only rather than treating StorageLive as creating a new object. That is, object instances are now tied to their Mir-provided declarations (which, at present, only appear once per function). To still account for when Rust scopes deem an object to be alive, we use StorageLive and StorageDead to update `__CPROVER_dead_object`. This (global) variable is used by CBMC's pointer checks to track when a pointer may not be safe to dereference for it could be pointing to an object that no longer is in scope. Resolves: model-checking#3099

zhassan-aws

Thanks for making this happen!

How does the change in CBMC's default verbosity affect the Kani output? Is the change worth pointing out in the CHANGELOG.md?

tautschnig · 2024-07-26T11:46:14Z

How does the change in CBMC's default verbosity affect the Kani output? Is the change worth pointing out in the CHANGELOG.md?

I think we used to see loop-unwinding information while running Kani, that is now no longer the case. Other than this, I don't think Kani is impacted.

zhassan-aws · 2024-07-26T16:13:08Z

I think we used to see loop-unwinding information while running Kani, that is now no longer the case.

While I'm happy to see that, users may have depended on this output to see when CBMC is unwinding forever. So, I think we should at least point this change out in the CHANGELOG.md.

I would also suggest adding a Kani option (e.g. --cbmc-stats or --solver-stats?) that would turn on --verbosity 9 in case users want to restore the old behavior. What do you think?

feliperodri

🚢 it! (after @zhassan-aws comments)

This reverts commit b7b3b15.

CBMC v6 included changes to hide timing information and loop unwinding status output at the default verbosity. To not impact Kani users, model-checking#2995 included changes to make Kani run CBMC with `--verbosity 9`. This change now makes Kani run CBMC with just the default verbosity, hiding timing information and loop unwinding status by default. If users still wish to see this information, they can invoke Kani with `--cbmc args --verbosity 9`.

@artemagvanian

## 0.54.0 ### Major Changes * We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. * We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. * We enabled support for concrete playback for harness that contains stubs or function contracts. * We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. ### Breaking Changes * The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. ## What's Changed * Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in #3332 * Fix visibility of some Kani intrinsics by @artemagvanian in #3323 * Function Contracts: Modify Slices by @pi314mm in #3295 * Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in #3344 * Add support for global transformations by @artemagvanian in #3348 * Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in #3283 * Fix contract handling of promoted constants and constant static by @celinval in #3305 * Bump CBMC Viewer to 3.9 by @tautschnig in #3373 * Update to CBMC version 6.1.1 by @tautschnig in #2995 * Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in #3270 * Enable concrete playback for contract and stubs by @celinval in #3389 * Add code scanner tool by @celinval in #3120 * Enable contracts in associated functions by @celinval in #3363 * Enable log2*, log10* intrinsics by @tautschnig in #3001 * Enable powif* intrinsics by @tautschnig in #2999 * Enable fma* intrinsics by @tautschnig in #3002 * Enable sqrt* intrinsics by @tautschnig in #3000 * Remove assigns clause for ZST pointers by @carolynzech in #3417 * Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in #3374 * Unify kani library and kani core logic by @jaisnan in #3333 * Stabilize pointer-to-reference cast validity checks by @artemagvanian in #3426 * Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri ## New Contributors * @carolynzech made their first contribution in #3387 **Full Changelog**: kani-0.53.0...kani-0.54.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

In some cases, Kani would report a spurious counter example for cases where a match arm contained more than one pattern. This was fixed by changing how we handle storage lifecycle in #2995. This PR is only adding the related test to the regression. Resolves#3432 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

These tests were moved while working towards model-checking#2995, but do not appear to be excessively slow even with the final version committed when completing that PR. (`copy_empty_string_by_intrinsic.rs` completes within a few seconds, `push_slow.rs` takes one minute and around 4 GB of memory, but this is still well below what other tests in our regression test suite take.)

These tests were moved while working towards #2995, but do not appear to be excessively slow even with the final version committed when completing that PR. (`copy_empty_string_by_intrinsic.rs` completes within a few seconds, `push_slow.rs` takes one minute and around 4 GB of memory, but this is still well below what other tests in our regression test suite take.) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Update to CBMC version 6.0.0
da76cb3
Updates to match changes to the GOTO binary format. Resolves: model-checking#2972

tautschnig self-assigned this Feb 6, 2024

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

tautschnig added 27 commits June 18, 2024 11:00

Merge remote-tracking branch 'origin/main' into cbmc-6
2f37c6f

Force tests to pass
d6e78a8

Merge remote-tracking branch 'origin/main' into cbmc-6
1bc0129

Add overlay files to enable performance data output
5d73a67

Enable verbosity 9 for performance numbers
e95e689

Revert "Enable verbosity 9 for performance numbers"
7feccd5
This reverts commit e95e689.

Revert "Add overlay files to enable performance data output"
0125a23
This reverts commit 5d73a67.

Verbosity 9 for perf tests
9a68859

Separate flags
7dd43d8

benchcomp test with verbosity
a55167a

Merge remote-tracking branch 'origin/main' into cbmc-6
952841d

Revert "Force tests to pass"
e32e3c6
This reverts commit d6e78a8.

Set higher verbosity for tests as needed
383a6f4

Update interface to CBMC v6
11b1dd1

Regression test workarounds
d591c4d

Revert "Regression test workarounds"
3abf589
This reverts commit d591c4d.

Debugging storage markers
d07841b

WIP
c179663

Revertmodel-checking#3080except for std enablement
bb5dc8f

Mark failure that is not yet understood as FIXME
e29d024

Mark newly slow tests as such
6480755

Update property configuration for CBMC v6
445f363

fixup! Set higher verbosity for tests as needed
bb373f2

Use CBMC version 6.0.1
fda6424

Use PPA with GCC-9 to build CBMC v6+ on Ubuntu 18.04
125473d

Use older pip version to remain compatible with Python 3.7
e7242f2

Merge remote-tracking branch 'origin/main' into cbmc-6
8127e5c

zhassan-aws reviewed Jul 26, 2024
View reviewed changes

tautschnig added 3 commits July 26, 2024 11:46

Merge remote-tracking branch 'origin/main' into cbmc-6
8bb15ce

Use Local
7ab6f60

Use constant
e902354

feliperodri approved these changes Jul 30, 2024
View reviewed changes

Comment threadtests/expected/shadow/unsupported_num_objects/test.rs
Comment threadtests/expected/shadow/slices/slice_of_array/test.rs Outdated
Comment threadkani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Merge branch 'main' into cbmc-6
007b1e9

tautschnig changed the title ~~Update to CBMC version 6.1.0~~Update to CBMC version 6.1.1Jul 31, 2024

tautschnig added 4 commits July 31, 2024 06:57

Merge remote-tracking branch 'origin/main' into cbmc-6
2a3fd06

Use CBMC 6.1.1
c968d65

Revert "Test performance with CBMC using CaDiCaL 2.0.0"
2de6464
This reverts commit b7b3b15.

Use verbosity 9 by default
f878fd9

tautschnig merged commit e4078b4 into model-checking:mainJul 31, 2024

tautschnig deleted the cbmc-6 branch July 31, 2024 09:55

This was referenced Jul 31, 2024
Reduce CBMC verbosity to CBMC's default #3398
Draft
Disable Divide by 0 Checks for Floats #3327
Open
Use box in shadow memory test for reliable object count #3380
Closed

feliperodri mentioned this pull request Aug 8, 2024
Bump Kani version to 0.54.0 #3430
Merged

This was referenced Aug 14, 2024
Match expressions with | and variables causing spurious failure. #3432
Closed
Add test related to issue 3432 #3439
Merged

tautschnig mentioned this pull request Nov 1, 2024
[CONTRACTS] Detect loop locals with goto_rw in DFCC diffblue/cbmc#8489
Merged
7 tasks

tautschnig mentioned this pull request Jul 4, 2025
Move tests from slow/kani back to regular suite #4202
Merged

Navigation Menu

Uh oh!

Update to CBMC version 6.1.1 - #2995

Update to CBMC version 6.1.1#2995
tautschnig merged 62 commits into
model-checking:mainfrom
tautschnig:cbmc-6

tautschnig commented Feb 6, 2024•
edited
Loading

Uh oh!

zhassan-aws left a comment •
edited
Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig commented Jul 26, 2024

Uh oh!

zhassan-aws commented Jul 26, 2024•
edited
Loading

Uh oh!

feliperodri left a comment •
edited
Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

tautschnig commented Feb 6, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

zhassan-aws left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig commented Jul 26, 2024

Uh oh!

zhassan-aws commented Jul 26, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

feliperodri left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tautschnig commented Feb 6, 2024•
edited
Loading

zhassan-aws left a comment •
edited
Loading

zhassan-aws commented Jul 26, 2024•
edited
Loading

feliperodri left a comment •
edited
Loading