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.

Sign up for GitHub

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

Jump to bottom

Support for disabling automatically generated pointer checks to avoid reinstrumentation #3344

Merged
merged 14 commits into from
Jul 19, 2024
Merged

Support for disabling automatically generated pointer checks to avoid reinstrumentation #3344

merged 14 commits into from
Jul 19, 2024

Conversation

artemagvanian
Copy link
Contributor

@artemagvanian artemagvanian commented Jul 15, 2024 •
edited
Loading

Recently added memory initialization checks (see #3300 for an overview) code suffers from re-instrumentation due to automatically added pointer checks to the instrumentation code.

This PR adds an internal kanitool::disable_checks attribute to disable automatically generated CBMC checks inside internal instrumentation. This, in turn, relies on CBMC pragmas (https://www.cprover.org/cprover-manual/properties/#usinggotoinstrument).

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

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jul 15, 2024
@artemagvanian artemagvanian self-assigned this Jul 15, 2024
@artemagvanian artemagvanian marked this pull request as ready for review July 15, 2024 17:34
@artemagvanian artemagvanian requested a review from a team as a code owner July 15, 2024 17:34
qinheping
qinheping reviewed Jul 17, 2024
View reviewed changes
Copy link
Contributor

@qinheping qinheping left a comment

Choose a reason for hiding this comment

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

Could you add some tests to illustrate that the checks are actually disabled in the GOTO programs?

kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
@artemagvanian
Copy link
Contributor Author

Could you add some tests to illustrate that the checks are actually disabled in the GOTO programs?

I wonder what's a good way to test this: if there is a way to somehow retrieve the internal output of goto-instrument, we could check that the appropriate pragmas are added? Since this attribute is supposed to be internal, we would need to test it indirectly

@qinheping
Copy link
Contributor

internal output of goto-instrument, we could check that the appropriate pragmas are added? Since this attribute is supposed to be internal, we would need to test it indirectly

Could you elaborate a bit more about what will happen if we don't disable the pointer checks in the instrumentation code. Is there any test failed without this PR? If so, we can use them to test this PR indirectly.

Directly testing checks being disabled requires extending .expected with exclude-tag --- specifying lines that we don't want to see in the Kani output.

@artemagvanian
Copy link
Contributor Author

Could you elaborate a bit more about what will happen if we don't disable the pointer checks in the instrumentation code. Is there any test failed without this PR? If so, we can use them to test this PR indirectly.

No test will fail, but extra checks will be added to the instrumentation code itself, which negatively affects verification performance.

Directly testing checks being disabled requires extending .expected with exclude-tag --- specifying lines that we don't want to see in the Kani output.

That could work, let me look into that

@adpaco-aws
Copy link
Contributor

if there is a way to somehow retrieve the internal output of goto-instrument, we could check that the appropriate pragmas are added?

IIRC the human-readable output of goto-instrument (via --show-functions or something like that) doesn't pretty-print pragmas, so I'd suggest exploring other options.

Directly testing checks being disabled requires extending .expected with exclude-tag --- specifying lines that we don't want to see in the Kani output.

For more complex behaviors we often recommend the exec mode, which allows you to run a script to determine the outcome and optionally check the output and exit code.

@artemagvanian
Copy link
Contributor Author

@qinheping @adpaco-aws thanks for the pointers. I added a test that checks that automatic checks are not added in the module where we disable it. This feels clunky, but I can't think of a better way since the attribute is private

qinheping
qinheping approved these changes Jul 18, 2024
View reviewed changes
Copy link
Contributor

@qinheping qinheping left a comment

Choose a reason for hiding this comment

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

LGTM. Thank you!

tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected Outdated Show resolved Hide resolved
@artemagvanian artemagvanian merged commit 96d1147 into model-checking:main Jul 19, 2024
25 checks passed
@artemagvanian artemagvanian deleted the kani-pragmas branch July 19, 2024 15:57
@feliperodri feliperodri mentioned this pull request Aug 8, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Aug 9, 2024
@feliperodri
Bump Kani version to 0.54.0 (#3430)
7a6f1a4 
## 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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@celinval celinval celinval left review comments

@qinheping qinheping qinheping approved these changes

Assignees

@artemagvanian artemagvanian

Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@artemagvanian @qinheping @adpaco-aws @celinval