CONTRACTS: separation checks using nondet demonic variable #8576
Conversation
remi-delmas-3000
requested review from
tautschnig,
feliperodri,
kroening and
peterschrammel
as code owners
- Replace bool array indexed by object ID with nondet demonic variable to implement separation checks. - Fix test: don't use is fresh under negation format
remi-delmas-3000
force-pushed
the
contracts-is-fresh-demonic
branch
from
5372a0c to
d490670
Compare
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8576 +/- ##
===========================================
- Coverage 78.92% 78.85% -0.07%
===========================================
Files 1732 1732
Lines 198953 199119 +166
Branches 18560 18560
===========================================
+ Hits 157021 157023 +2
- Misses 41932 42096 +164 ☔ View full report in Codecov by Sentry. |
| __CPROVER_assigns(z, *x) | ||
| __CPROVER_requires( | ||
| __CPROVER_is_fresh(x, sizeof(int)) && | ||
| *x > 0 && | ||
| *x < 4) | ||
| __CPROVER_ensures( | ||
| __CPROVER_is_fresh(y, sizeof(int)) && | ||
| !__CPROVER_is_fresh(x, sizeof(int)) && | ||
| x != NULL && | ||
| x != y && | ||
| __CPROVER_return_value == *x + 5) | ||
| int *foo() | ||
| // clang-format off | ||
| __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value, sizeof(int))) | ||
| // clang-format on | ||
| { | ||
| *x = *x + 4; | ||
| y = malloc(sizeof(*y)); | ||
| *y = *x; | ||
| z = *y; | ||
| return (*x + 5); |
There was a problem hiding this comment.
Precision : I rewrote this test to make it do what the test description says, i.e testing is_fresh in a post condition on the return value.
| typedef struct | ||
| { | ||
| /// \brief Nondet variable ranging over the set of objects allocated | ||
| /// by __CPROVER_contracts_is_fresh. Used to check separation constraints | ||
| /// in __CPROVER_contracts_is_fresh. | ||
| void *fresh_ptr; | ||
| } __CPROVER_contracts_ptr_pred_ctx_t; | ||
|
|
||
| /// \brief Type of pointers to \ref __CPROVER_contracts_ptr_pred_ctx_t. | ||
| typedef __CPROVER_contracts_ptr_pred_ctx_t | ||
| *__CPROVER_contracts_ptr_pred_ctx_ptr_t; | ||
|
|
There was a problem hiding this comment.
This new structure encapsulates context info that's used by pointer predicates and shared across requires and ensures clauses. It is going to be expanded in the future with more fields to support more predicates
There was a problem hiding this comment.
The name is ptr_pret_ctx means "pointer predicate context", it is not specific to is_fresh anymore (will be used by all predicates).
| @@ -84,7 +99,7 @@ typedef struct | |||
| __CPROVER_contracts_obj_set_t deallocated; | |||
| /// \brief Pointer to object set supporting the is_fresh predicate checks | |||
| /// (indexed mode) | |||
| __CPROVER_contracts_obj_set_ptr_t linked_is_fresh; | |||
| __CPROVER_contracts_ptr_pred_ctx_ptr_t linked_ptr_pred_ctx; | |||
There was a problem hiding this comment.
The name is ptr_pret_ctx means "pointer predicate context", it is not specific to is_fresh anymore (will be used by all predicates).
|
@tautschnig this one is ready to merge |
replace bool array indexed by object ID with nondet demonic tracker for
__CPROVER_is_freshseparation checks