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

Make DFCC is_dead_object_update less restrictive #8261

Open
wants to merge 1 commit into
base: develop
Choose a base branch
from

Conversation

tautschnig
Copy link
Collaborator

GOTO programs are free to use different ways to assign to __CPROVER_dead_object. Any such assignment that does not match the expected pattern can then safely be ignored.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

GOTO programs are free to use different ways to assign to
`__CPROVER_dead_object`. Any such assignment that does not match the
expected pattern can then safely be ignored.
@tautschnig
Copy link
Collaborator Author

@remi-delmas-3000 Why are we tracking __CPROVER_dead_object assignments rather than just using DEAD statements?

@remi-delmas-3000
Copy link
Collaborator

remi-delmas-3000 commented Apr 26, 2024

@remi-delmas-3000 Why are we tracking __CPROVER_dead_object assignments rather than just using DEAD statements?

The use of __builtin_alloca for dynamic stack allocation, for instance, produces these __CPROVER_dead_object updates instead of DEAD instructions.

From the point of view of frame condition checking, not failing on an assignment to a dead object is unsound, so instead of having a soundness hole in the contracts instrumentation and defaulting to the underlying CBMC checks for such cases, I chose to error out when instrumenting any assignment to __CPROVER_dead_object that does not match the only pattern I knew when designing the instrumentation. This would mean that there is potentially another way to create stack objects that I don't know about, and I would need to at least take a look and make sure it is handled properly.

@tautschnig
Copy link
Collaborator Author

Ah, thank you for explaining why looking at DEAD wouldn't be sufficient. With the proposed change we'd still be picking up all the updates produced by the C front-end, but won't fail on what Kani intends to produce.

@remi-delmas-3000
Copy link
Collaborator

but won't fail on what Kani intends to produce.
How about abstracting away the details and introducing a __CPROVER_object_dead(ptr) function to signal an object's death instead of directly manipulating the __CPROVER_dead_object variable ?

@tautschnig
Copy link
Collaborator Author

How about abstracting away the details and introducing a __CPROVER_object_dead(ptr) function to signal an object's death instead of directly manipulating the __CPROVER_dead_object variable ?

We could indeed encapsulate this in a (library) function, but either way it will remain an implementation detail of the C front-end. Eventually Kani will create its own tracking variable for Rust checks. Either way, I think this is out of scope for this PR?

@feliperodri feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jun 8, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants