From d490670c9fcb4c1210f070202d53a9400dd08b60 Mon Sep 17 00:00:00 2001
From: Remi Delmas <delmasrd@amazon.com>
Date: Sat, 25 Jan 2025 14:39:45 -0500
Subject: [PATCH] CONTRACTS: separation checks using nondet demonic variable
- 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
---
.../test_aliasing_ensure/main.c | 34 +--
.../test_aliasing_ensure/test.desc | 4 -
.../test_scalar_memory_enforce/main.c | 1 -
src/ansi-c/library/cprover_contracts.c | 194 +++++++++---------
.../contracts-dev-spec-dfcc-runtime.md | 4 +-
.../dynamic-frames/dfcc_is_cprover_symbol.cpp | 4 +-
.../contracts/dynamic-frames/dfcc_library.cpp | 36 +++-
.../contracts/dynamic-frames/dfcc_library.h | 34 ++-
.../dynamic-frames/dfcc_wrapper_program.cpp | 56 ++---
.../dynamic-frames/dfcc_wrapper_program.h | 29 +--
10 files changed, 210 insertions(+), 186 deletions(-)
diff --git a/regression/contracts-dfcc/test_aliasing_ensure/main.c b/regression/contracts-dfcc/test_aliasing_ensure/main.c
index 9b66c5589cd..d59bfe7deb1 100644
--- a/regression/contracts-dfcc/test_aliasing_ensure/main.c
+++ b/regression/contracts-dfcc/test_aliasing_ensure/main.c
@@ -1,35 +1,15 @@
-#include <assert.h>
-#include <stdbool.h>
-#include <stdlib.h>
-
-int z;
-
-// clang-format off
-int foo(int *x, int *y)
- __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);
+ int *ret = malloc(sizeof(int));
+ __CPROVER_assume(ret);
+ return ret;
}
int main()
{
- int n = 4;
- n = foo(&n, &n);
- assert(!(n < 4));
+ foo();
return 0;
}
diff --git a/regression/contracts-dfcc/test_aliasing_ensure/test.desc b/regression/contracts-dfcc/test_aliasing_ensure/test.desc
index 11f828e0e09..f4672b8a3ee 100644
--- a/regression/contracts-dfcc/test_aliasing_ensure/test.desc
+++ b/regression/contracts-dfcc/test_aliasing_ensure/test.desc
@@ -4,10 +4,6 @@ main.c
^EXIT=0$
^SIGNAL=0$
\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
-\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS
-\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS
-\[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS
^VERIFICATION SUCCESSFUL$
--
--
diff --git a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
index b22c93fe00f..ff6bbd8a739 100644
--- a/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
+++ b/regression/contracts-dfcc/test_scalar_memory_enforce/main.c
@@ -21,7 +21,6 @@ int foo(int *x)
ptr_ok(x))
__CPROVER_ensures(
!ptr_ok(x) &&
- !__CPROVER_is_fresh(x, sizeof(int)) &&
return_ok(__CPROVER_return_value, x))
// clang-format on
{
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
index 03c9abb1b3f..c98d73cb890 100644
--- a/src/ansi-c/library/cprover_contracts.c
+++ b/src/ansi-c/library/cprover_contracts.c
@@ -64,9 +64,24 @@ typedef struct
void **elems;
} __CPROVER_contracts_obj_set_t;
-/// \brief Type of pointers to \ref __CPROVER_contracts_car_set_t.
+/// \brief Type of pointers to \ref __CPROVER_contracts_obj_set_t.
typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t;
+/// \brief Stores context information supporting the evaluation of pointer
+/// predicates in both assume and assert contexts for all predicates:
+/// pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract.
+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;
+
/// \brief Runtime representation of a write set.
typedef struct
{
@@ -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;
/// \brief Object set recording the is_fresh allocations in post conditions
__CPROVER_contracts_obj_set_ptr_t linked_allocated;
/// \brief Object set recording the deallocations (used by was_freed)
@@ -393,6 +408,26 @@ __CPROVER_HIDE:;
return set->elems[object_id] == ptr;
}
+/// \brief Resets the nondet tracker for pointer predicates in \p set.
+/// Invoked between requires and ensures clauses evaluation to allow ensures
+/// clauses to establish different pointer predicates on the same pointers.
+void __CPROVER_contracts_ptr_pred_ctx_init(
+ __CPROVER_contracts_ptr_pred_ctx_ptr_t set)
+{
+__CPROVER_HIDE:;
+ set->fresh_ptr = (void *)0;
+}
+
+/// \brief Resets the nondet tracker for pointer predicates in \p set.
+/// Invoked right between requires and ensures clauses to allow ensures clauses
+/// to establish a different pointer predicates on the same pointers.
+void __CPROVER_contracts_ptr_pred_ctx_reset(
+ __CPROVER_contracts_ptr_pred_ctx_ptr_t set)
+{
+__CPROVER_HIDE:;
+ (void)set;
+}
+
/// \brief Initialises a \ref __CPROVER_contracts_write_set_t object.
/// \param[inout] set Pointer to the object to initialise
/// \param[in] contract_assigns_size Max size of the assigns clause
@@ -434,7 +469,7 @@ __CPROVER_HIDE:;
&(set->contract_frees_append), contract_frees_size);
__CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->allocated));
__CPROVER_contracts_obj_set_create_indexed_by_object_id(&(set->deallocated));
- set->linked_is_fresh = 0;
+ set->linked_ptr_pred_ctx = 0;
set->linked_allocated = 0;
set->linked_deallocated = 0;
set->assume_requires_ctx = assume_requires_ctx;
@@ -473,8 +508,8 @@ __CPROVER_HIDE:;
__CPROVER_deallocate(set->contract_frees_append.elems);
__CPROVER_deallocate(set->allocated.elems);
__CPROVER_deallocate(set->deallocated.elems);
- // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
- // since they are owned by someone else.
+ // do not free set->linked_ptr_pred_ctx->elems or
+ // set->deallocated_linked->elems since they are owned by someone else.
}
/// \brief Inserts a snapshot of the range starting at \p ptr of size \p size
@@ -542,9 +577,6 @@ void __CPROVER_contracts_write_set_insert_object_from(
/// \brief Inserts a snapshot of the range of bytes starting at \p ptr of
/// \p size bytes in \p set->contact_assigns at index \p idx.
///
-/// - The start address is `ptr`
-/// - The size in bytes is `size`
-///
/// \param[inout] set The set to update
/// \param[in] idx Insertion index
/// \param[in] ptr Pointer to the start of the range
@@ -567,10 +599,8 @@ void __CPROVER_contracts_write_set_add_freeable(
void *ptr)
{
__CPROVER_HIDE:;
- // we don't check yet that the pointer satisfies
- // the __CPROVER_contracts_is_freeable as precondition.
- // preconditions will be checked if there is an actual attempt
- // to free the pointer.
+ // Preconditions will be checked if there is an actual attempt
+ // to free the pointer, don't check preemptively.
// store pointer
__CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
@@ -1060,23 +1090,23 @@ __CPROVER_HIDE:;
}
/// \brief Links \p is_fresh_set to
-/// \p write_set->linked_is_fresh so that the is_fresh predicates
-/// can be evaluated in requires and ensures clauses.
-void __CPROVER_contracts_link_is_fresh(
+/// \p write_set->linked_ptr_pred_ctx to share evaluation context between
+/// requires and ensures clauses for separation checks.
+void __CPROVER_contracts_link_ptr_pred_ctx(
__CPROVER_contracts_write_set_ptr_t write_set,
- __CPROVER_contracts_obj_set_ptr_t is_fresh_set)
+ __CPROVER_contracts_ptr_pred_ctx_ptr_t ptr_pred_ctx)
{
__CPROVER_HIDE:;
#ifdef __CPROVER_DFCC_DEBUG_LIB
__CPROVER_assert(write_set != 0, "write_set not NULL");
#endif
- if((is_fresh_set != 0))
+ if((ptr_pred_ctx != 0))
{
- write_set->linked_is_fresh = is_fresh_set;
+ write_set->linked_ptr_pred_ctx = ptr_pred_ctx;
}
else
{
- write_set->linked_is_fresh = 0;
+ write_set->linked_ptr_pred_ctx = 0;
}
}
@@ -1205,7 +1235,7 @@ __CPROVER_HIDE:;
}
__CPROVER_assert(
(ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
- "pointer_equals is only called with valid pointers");
+ "__CPROVER_pointer_equals is only called with valid pointers");
*ptr1 = ptr2;
return 1;
}
@@ -1214,35 +1244,33 @@ __CPROVER_HIDE:;
void *derefd = *ptr1;
__CPROVER_assert(
(derefd == 0) || __CPROVER_r_ok(derefd, 0),
- "pointer_equals is only called with valid pointers");
+ "__CPROVER_pointer_equals is only called with valid pointers");
__CPROVER_assert(
(ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
- "pointer_equals is only called with valid pointers");
- return derefd == ptr2;
+ "__CPROVER_pointer_equals is only called with valid pointers");
+ if(derefd != ptr2)
+ {
+ return 0;
+ }
+ return 1;
}
}
/// \brief Implementation of the `is_fresh` front-end predicate.
///
-/// The behaviour depends on the boolean flags carried by \p write_set
-/// which reflect the invocation context: checking vs. replacing a contract,
-/// in a requires or an ensures clause context.
/// \param elem Pointer to the target pointer of the check
-/// \param size Size to check for
+/// \param size Size to check
/// \param may_fail Allow predicate to fail in assume mode
-/// \param write_set Write set in which seen/allocated objects are recorded;
+/// \param write_set Write set (carries assert/assume requires/ensures context
+/// flags, sets to allocated/seen objects for separation checks)
///
/// \details The behaviour is as follows:
-/// - When \p set->assume_requires_ctx is `true`, the predicate allocates a new
-/// object, records the object in \p set->linked_is_fresh, updates \p *elem to
-/// point to the fresh object and returns `true`;
-/// - When \p set->assume_ensures_ctx is `true`, the predicate allocates a new
-/// object, records the object in \p set->linked_allocated, updates \p *elem
-/// to point to the fresh object and returns `true`;
-/// - When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`,
-/// the predicate first computes wether \p *elem is in \p set->linked_is_fresh
-/// and returns false if it is. Otherwise it records the object in
-/// \p set->linked_is_fresh and returns the value of r_ok(*elem, size).
+/// - In assume contexts, returns false if another pointer predicate is already
+/// assumed, otherwise, allocates a fresh object, mark *elem and elem as seen
+/// in the write set.
+/// - In assert contexts, returns false if another pointer predicate is already
+/// succesfully asserted, otherwise checks separation and size, mark *elem and
+/// elem as seen in the write set.
__CPROVER_bool __CPROVER_contracts_is_fresh(
void **elem,
__CPROVER_size_t size,
@@ -1250,19 +1278,6 @@ __CPROVER_bool __CPROVER_contracts_is_fresh(
__CPROVER_contracts_write_set_ptr_t write_set)
{
__CPROVER_HIDE:;
- __CPROVER_assert(
- (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
- (write_set->assert_requires_ctx == 1) |
- (write_set->assume_ensures_ctx == 1) |
- (write_set->assert_ensures_ctx == 1)),
- "__CPROVER_is_fresh is used only in requires or ensures clauses");
-#ifdef __CPROVER_DFCC_DEBUG_LIB
- __CPROVER_assert(
- __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)),
- "set readable");
- __CPROVER_assert(
- write_set->linked_is_fresh, "set->linked_is_fresh is not NULL");
-#endif
if(write_set->assume_requires_ctx)
{
#ifdef __CPROVER_DFCC_DEBUG_LIB
@@ -1299,7 +1314,6 @@ __CPROVER_HIDE:;
__CPROVER_contracts_make_invalid_pointer(elem);
return 0;
}
-
void *ptr = __CPROVER_allocate(size, 0);
*elem = ptr;
@@ -1307,24 +1321,10 @@ __CPROVER_HIDE:;
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
__CPROVER_malloc_is_new_array =
record_malloc ? 0 : __CPROVER_malloc_is_new_array;
-
// do not detect memory leaks when assuming a precondition of a contract
// for contract checking
// __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
// __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
-
-#ifdef __CPROVER_DFCC_DEBUG_LIB
- // manually inlined below
- __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
-#else
- __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
- write_set->linked_is_fresh->nof_elems =
- (write_set->linked_is_fresh->elems[object_id] != 0)
- ? write_set->linked_is_fresh->nof_elems
- : write_set->linked_is_fresh->nof_elems + 1;
- write_set->linked_is_fresh->elems[object_id] = ptr;
- write_set->linked_is_fresh->is_empty = 0;
-#endif
return 1;
}
else if(write_set->assume_ensures_ctx)
@@ -1362,6 +1362,10 @@ __CPROVER_HIDE:;
void *ptr = __CPROVER_allocate(size, 0);
*elem = ptr;
+ write_set->linked_ptr_pred_ctx->fresh_ptr =
+ __VERIFIER_nondet___CPROVER_bool()
+ ? ptr
+ : write_set->linked_ptr_pred_ctx->fresh_ptr;
// record the object size for non-determistic bounds checking
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1395,34 +1399,19 @@ __CPROVER_HIDE:;
(write_set->assume_ensures_ctx == 0),
"only one context flag at a time");
#endif
- __CPROVER_contracts_obj_set_ptr_t seen = write_set->linked_is_fresh;
void *ptr = *elem;
- // null pointers or already seen pointers are not fresh
-#ifdef __CPROVER_DFCC_DEBUG_LIB
- // manually inlined below
- if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
- return 0;
-#else
- if(ptr == 0)
- return 0;
-
- __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr);
-
- if(seen->elems[object_id] != 0)
- return 0;
-#endif
-
-#ifdef __CPROVER_DFCC_DEBUG_LIB
- // manually inlined below
- __CPROVER_contracts_obj_set_add(seen, ptr);
-#else
- seen->nof_elems =
- (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1;
- seen->elems[object_id] = ptr;
- seen->is_empty = 0;
-#endif
- // check size
- return __CPROVER_r_ok(ptr, size);
+ if(
+ ptr != (void *)0 &&
+ !__CPROVER_same_object(write_set->linked_ptr_pred_ctx->fresh_ptr, ptr) &&
+ __CPROVER_r_ok(ptr, size))
+ {
+ write_set->linked_ptr_pred_ctx->fresh_ptr =
+ __VERIFIER_nondet___CPROVER_bool()
+ ? ptr
+ : write_set->linked_ptr_pred_ctx->fresh_ptr;
+ return 1;
+ }
+ return 0;
}
else
{
@@ -1496,8 +1485,16 @@ __CPROVER_HIDE:;
else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
{
__CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
- return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
- offset <= ub_offset;
+ if(
+ __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
+ offset <= ub_offset)
+ {
+ return 1;
+ }
+ else
+ {
+ return 0;
+ }
}
}
@@ -1668,7 +1665,6 @@ __CPROVER_HIDE:;
// SOUDNESS: allow predicate to fail
if(may_fail && __VERIFIER_nondet___CPROVER_bool())
return 0;
-
// must hold, assign the function pointer to the contract function
*function_pointer = contract;
return 1;
@@ -1676,7 +1672,11 @@ __CPROVER_HIDE:;
else
{
// in assumption contexts, the pointer gets checked for equality
- return *function_pointer == contract;
+ if(*function_pointer == contract)
+ {
+ return 1;
+ }
+ return 0;
}
}
#endif // __CPROVER_contracts_library_defined
diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md
index f1456324578..6b0b4f225c5 100644
--- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md
+++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-runtime.md
@@ -112,8 +112,8 @@ typedef struct __CPROVER_contracts_write_set_t
// Set of objects deallocated by the function under analysis (indexed mode)
__CPROVER_contracts_obj_set_t deallocated;
- // Object set supporting the is_fresh predicate checks (indexed mode)
- __CPROVER_contracts_obj_set_ptr_t linked_is_fresh;
+ // Object set supporting the pointer predicate checks
+ __CPROVER_contracts_ptr_pred_ctx_ptr_t linked_ptr_pred_ctx;
// Object set recording the is_fresh allocations in post conditions
// (replacement mode only)
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
index 649e3e0cee9..321a6bdbadb 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp
@@ -30,6 +30,8 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
function_symbols.insert(CPROVER_PREFIX "assert");
function_symbols.insert(CPROVER_PREFIX "assignable");
function_symbols.insert(CPROVER_PREFIX "assume");
+ function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_init");
+ function_symbols.insert(CPROVER_PREFIX "contracts_ptr_pred_ctx_reset");
function_symbols.insert(CPROVER_PREFIX "contracts_car_create");
function_symbols.insert(CPROVER_PREFIX "contracts_car_set_contains");
function_symbols.insert(CPROVER_PREFIX "contracts_car_set_create");
@@ -42,7 +44,7 @@ init_function_symbols(std::unordered_set<irep_idt> &function_symbols)
function_symbols.insert(CPROVER_PREFIX "contracts_is_fresh");
function_symbols.insert(CPROVER_PREFIX "contracts_link_allocated");
function_symbols.insert(CPROVER_PREFIX "contracts_link_deallocated");
- function_symbols.insert(CPROVER_PREFIX "contracts_link_is_fresh");
+ function_symbols.insert(CPROVER_PREFIX "contracts_link_ptr_pred_ctx");
function_symbols.insert(CPROVER_PREFIX "contracts_obeys_contract");
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_add");
function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_append");
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
index efa62681c5f..f9a5f51c2fe 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp
@@ -52,6 +52,8 @@ const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name()
{dfcc_typet::CAR, CONTRACTS_PREFIX "car_t"},
{dfcc_typet::CAR_SET, CONTRACTS_PREFIX "car_set_t"},
{dfcc_typet::CAR_SET_PTR, CONTRACTS_PREFIX "car_set_ptr_t"},
+ {dfcc_typet::PTR_PRED_CTX, CONTRACTS_PREFIX "ptr_pred_ctx_t"},
+ {dfcc_typet::PTR_PRED_CTX_PTR, CONTRACTS_PREFIX "ptr_pred_ctx_ptr_t"},
{dfcc_typet::OBJ_SET, CONTRACTS_PREFIX "obj_set_t"},
{dfcc_typet::OBJ_SET_PTR, CONTRACTS_PREFIX "obj_set_ptr_t"},
{dfcc_typet::WRITE_SET, CONTRACTS_PREFIX "write_set_t"},
@@ -122,9 +124,11 @@ const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
CONTRACTS_PREFIX "write_set_havoc_object_whole"},
{dfcc_funt::WRITE_SET_HAVOC_SLICE,
CONTRACTS_PREFIX "write_set_havoc_slice"},
- {dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"},
+ {dfcc_funt::LINK_PTR_PRED_CTX, CONTRACTS_PREFIX "link_ptr_pred_ctx"},
{dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"},
{dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"},
+ {dfcc_funt::PTR_PRED_CTX_INIT, CONTRACTS_PREFIX "ptr_pred_ctx_init"},
+ {dfcc_funt::PTR_PRED_CTX_RESET, CONTRACTS_PREFIX "ptr_pred_ctx_reset"},
{dfcc_funt::POINTER_EQUALS, CONTRACTS_PREFIX "pointer_equals"},
{dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"},
{dfcc_funt::POINTER_IN_RANGE_DFCC,
@@ -810,14 +814,14 @@ const code_function_callt dfcc_libraryt::write_set_deallocate_freeable_call(
return call;
}
-const code_function_callt dfcc_libraryt::link_is_fresh_call(
+const code_function_callt dfcc_libraryt::link_ptr_pred_ctx_call(
const exprt &write_set_ptr,
- const exprt &is_fresh_obj_set_ptr,
+ const exprt &ptr_pred_ctx_ptr,
const source_locationt &source_location)
{
code_function_callt call(
- dfcc_fun_symbol[dfcc_funt::LINK_IS_FRESH].symbol_expr(),
- {write_set_ptr, is_fresh_obj_set_ptr});
+ dfcc_fun_symbol[dfcc_funt::LINK_PTR_PRED_CTX].symbol_expr(),
+ {write_set_ptr, ptr_pred_ctx_ptr});
call.add_source_location() = source_location;
return call;
}
@@ -882,3 +886,25 @@ const code_function_callt dfcc_libraryt::obj_set_release_call(
call.add_source_location() = source_location;
return call;
}
+
+const code_function_callt dfcc_libraryt::ptr_pred_ctx_init_call(
+ const exprt &ptr_pred_ctx_ptr,
+ const source_locationt &source_location)
+{
+ code_function_callt call(
+ dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(),
+ {ptr_pred_ctx_ptr});
+ call.add_source_location() = source_location;
+ return call;
+}
+
+const code_function_callt dfcc_libraryt::ptr_pred_ctx_reset_call(
+ const exprt &ptr_pred_ctx_ptr,
+ const source_locationt &source_location)
+{
+ code_function_callt call(
+ dfcc_fun_symbol[dfcc_funt::PTR_PRED_CTX_INIT].symbol_expr(),
+ {ptr_pred_ctx_ptr});
+ call.add_source_location() = source_location;
+ return call;
+}
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
index 68e243200b7..d119fc1926b 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h
@@ -31,6 +31,10 @@ enum class dfcc_typet
CAR_SET,
/// type of pointers to sets of CAR
CAR_SET_PTR,
+ /// type of context info for pointer predicates evaluation
+ PTR_PRED_CTX,
+ /// type of pointers to context info for pointer predicates evaluation
+ PTR_PRED_CTX_PTR,
/// type of sets of object identifiers
OBJ_SET,
/// type of pointers to sets of object identifiers
@@ -62,6 +66,10 @@ enum class dfcc_funt
OBJ_SET_CREATE_APPEND,
/// \see __CPROVER_contracts_obj_set_release
OBJ_SET_RELEASE,
+ /// \see __CPROVER_contracts_ptr_pred_ctx_init
+ PTR_PRED_CTX_INIT,
+ /// \see __CPROVER_contracts_ptr_pred_ctx_reset
+ PTR_PRED_CTX_RESET,
/// \see __CPROVER_contracts_obj_set_add
OBJ_SET_ADD,
/// \see __CPROVER_contracts_obj_set_append
@@ -120,8 +128,8 @@ enum class dfcc_funt
WRITE_SET_HAVOC_OBJECT_WHOLE,
/// \see __CPROVER_contracts_write_set_havoc_slice
WRITE_SET_HAVOC_SLICE,
- /// \see __CPROVER_contracts_link_is_fresh
- LINK_IS_FRESH,
+ /// \see __CPROVER_contracts_link_ptr_pred_ctx
+ LINK_PTR_PRED_CTX,
/// \see __CPROVER_contracts_link_allocated
LINK_ALLOCATED,
/// \see __CPROVER_contracts_link_deallocated
@@ -155,9 +163,7 @@ class typet;
class dfcc_libraryt
{
public:
- dfcc_libraryt(
- goto_modelt &goto_model,
- message_handlert &lmessage_handler);
+ dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler);
protected:
/// True iff the contracts library symbols are loaded
@@ -413,10 +419,10 @@ class dfcc_libraryt
const source_locationt &source_location);
/// \brief Builds call to
- /// \ref __CPROVER_contracts_link_is_fresh
- const code_function_callt link_is_fresh_call(
+ /// \ref __CPROVER_contracts_link_ptr_pred_ctx
+ const code_function_callt link_ptr_pred_ctx_call(
const exprt &write_set_ptr,
- const exprt &is_fresh_obj_set_ptr,
+ const exprt &ptr_pred_ctx_ptr,
const source_locationt &source_location);
/// \brief Builds call to
@@ -451,6 +457,18 @@ class dfcc_libraryt
const code_function_callt obj_set_release_call(
const exprt &obj_set_ptr,
const source_locationt &source_location);
+
+ /// \brief Builds call to
+ /// \ref __CPROVER_contracts_ptr_pred_ctx_init
+ const code_function_callt ptr_pred_ctx_init_call(
+ const exprt &ptr_pred_ctx_ptr,
+ const source_locationt &source_location);
+
+ /// \brief Builds call to
+ /// \ref __CPROVER_contracts_ptr_pred_ctx_init
+ const code_function_callt ptr_pred_ctx_reset_call(
+ const exprt &ptr_pred_ctx_ptr,
+ const source_locationt &source_location);
};
#endif
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
index 17b2f07d195..9124f954e8d 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp
@@ -116,30 +116,30 @@ static symbol_exprt create_addr_of_ensures_write_set(
}
/// Generate object set used to support is_fresh predicates
-static symbol_exprt create_is_fresh_set(
+static symbol_exprt create_ptr_pred_ctx(
symbol_table_baset &symbol_table,
dfcc_libraryt &library,
const symbolt &wrapper_symbol)
{
return dfcc_utilst::create_symbol(
symbol_table,
- library.dfcc_type[dfcc_typet::OBJ_SET],
+ library.dfcc_type[dfcc_typet::PTR_PRED_CTX],
wrapper_symbol.name,
- "__is_fresh_set",
+ "__ptr_pred_ctx",
wrapper_symbol.location);
}
/// Generate object set pointer used to support is_fresh predicates
-static symbol_exprt create_addr_of_is_fresh_set(
+static symbol_exprt create_addr_of_ptr_pred_ctx(
symbol_table_baset &symbol_table,
dfcc_libraryt &library,
const symbolt &wrapper_symbol)
{
return dfcc_utilst::create_symbol(
symbol_table,
- library.dfcc_type[dfcc_typet::OBJ_SET_PTR],
+ library.dfcc_type[dfcc_typet::PTR_PRED_CTX_PTR],
wrapper_symbol.name,
- "__address_of_is_fresh_set",
+ "__address_of_ptr_pred_ctx",
wrapper_symbol.location);
}
@@ -187,9 +187,9 @@ dfcc_wrapper_programt::dfcc_wrapper_programt(
goto_model.symbol_table,
library,
wrapper_symbol)),
- is_fresh_set(
- create_is_fresh_set(goto_model.symbol_table, library, wrapper_symbol)),
- addr_of_is_fresh_set(create_addr_of_is_fresh_set(
+ ptr_pred_ctx(
+ create_ptr_pred_ctx(goto_model.symbol_table, library, wrapper_symbol)),
+ addr_of_ptr_pred_ctx(create_addr_of_ptr_pred_ctx(
goto_model.symbol_table,
library,
wrapper_symbol)),
@@ -227,7 +227,7 @@ dfcc_wrapper_programt::dfcc_wrapper_programt(
// encode all contract clauses
encode_requires_write_set();
encode_ensures_write_set();
- encode_is_fresh_set();
+ encode_ptr_pred_ctx();
encode_requires_clauses();
encode_contract_write_set();
encode_function_call();
@@ -247,7 +247,7 @@ void dfcc_wrapper_programt::add_to_dest(goto_programt &dest)
{
// add code to dest in the right order
dest.destructive_append(preamble);
- dest.destructive_append(link_is_fresh);
+ dest.destructive_append(link_ptr_pred_ctx);
dest.destructive_append(preconditions);
dest.destructive_append(history);
dest.destructive_append(write_set_checks);
@@ -501,39 +501,39 @@ void dfcc_wrapper_programt::encode_contract_write_set()
goto_programt::make_dead(addr_of_contract_write_set, wrapper_sl));
}
-void dfcc_wrapper_programt::encode_is_fresh_set()
+void dfcc_wrapper_programt::encode_ptr_pred_ctx()
{
- preamble.add(goto_programt::make_decl(is_fresh_set, wrapper_sl));
+ preamble.add(goto_programt::make_decl(ptr_pred_ctx, wrapper_sl));
- preamble.add(goto_programt::make_decl(addr_of_is_fresh_set, wrapper_sl));
+ preamble.add(goto_programt::make_decl(addr_of_ptr_pred_ctx, wrapper_sl));
preamble.add(goto_programt::make_assignment(
- addr_of_is_fresh_set, address_of_exprt(is_fresh_set), wrapper_sl));
+ addr_of_ptr_pred_ctx, address_of_exprt(ptr_pred_ctx), wrapper_sl));
- // CALL obj_set_create_indexed_by_object_id(is_fresh_set) in preamble
+ // CALL ptr_pred_ctx_init(ptr_pred_ctx) in preamble
preamble.add(goto_programt::make_function_call(
- library.obj_set_create_indexed_by_object_id_call(
- addr_of_is_fresh_set, wrapper_sl),
+ library.ptr_pred_ctx_init_call(addr_of_ptr_pred_ctx, wrapper_sl),
wrapper_sl));
// link to requires write set
- link_is_fresh.add(goto_programt::make_function_call(
- library.link_is_fresh_call(
- addr_of_requires_write_set, addr_of_is_fresh_set, wrapper_sl),
+ link_ptr_pred_ctx.add(goto_programt::make_function_call(
+ library.link_ptr_pred_ctx_call(
+ addr_of_requires_write_set, addr_of_ptr_pred_ctx, wrapper_sl),
wrapper_sl));
// link to ensures write set
- link_is_fresh.add(goto_programt::make_function_call(
- library.link_is_fresh_call(
- addr_of_ensures_write_set, addr_of_is_fresh_set, wrapper_sl),
+ link_ptr_pred_ctx.add(goto_programt::make_function_call(
+ library.link_ptr_pred_ctx_call(
+ addr_of_ensures_write_set, addr_of_ptr_pred_ctx, wrapper_sl),
wrapper_sl));
- // release call in postamble
- postamble.add(goto_programt::make_function_call(
- library.obj_set_release_call(addr_of_is_fresh_set, wrapper_sl),
+ // reset tracking of target pointers to allow ensures clause to
+ // post different predicates.
+ link_deallocated_contract.add(goto_programt::make_function_call(
+ library.ptr_pred_ctx_reset_call(addr_of_ptr_pred_ctx, wrapper_sl),
wrapper_sl));
// DEAD instructions in postamble
- postamble.add(goto_programt::make_dead(is_fresh_set, wrapper_sl));
+ postamble.add(goto_programt::make_dead(ptr_pred_ctx, wrapper_sl));
}
/// Recursively traverses expression, adding "no_fail" attributes to pointer
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
index 224bdf8f795..cd6910507d0 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h
@@ -41,14 +41,15 @@ class conditional_target_group_exprt;
/// \details The body of the wrapper is divided into a number of sections
/// represented as separate goto_programs:
/// - \ref preamble
-/// - create is_fresh_set, requires_write_set, ensures_write_set,
+/// - create ptr_pred_ctx, requires_write_set, ensures_write_set,
/// contract_write_set variables
-/// - \ref link_is_fresh
-/// - link the is_fresh_set to requires_write_set and ensures_write_set
+/// - \ref link_ptr_pred_ctx
+/// - link the ptr_pred_ctx to requires_write_set and ensures_write_set
/// - in REPLACE mode, link the caller_write_set to the contract_write_set
/// so that deallocations and allocations are reflected in the caller
/// - \ref preconditions
-/// - evaluate preconditions, checking side effects against requires_write_set
+/// - evaluate preconditions, while checking the absence of side effects
+/// against the empty requires_write_set
/// - \ref history
/// - declare and snapshot history variables
/// - \ref write_set_checks
@@ -82,7 +83,8 @@ class conditional_target_group_exprt;
/// CALL link_allocated(ensures_write_set, caller_write_set);
/// ```
/// - \ref postconditions
-/// - evaluate preconditions, checking side effects against ensures_write_set
+/// - reset pointer predicate context object, evaluate preconditions while
+/// checking absence of side effects against the empty ensures_write_set
/// - \ref postamble
/// - release all object sets and write set variables
///
@@ -159,10 +161,10 @@ class dfcc_wrapper_programt
const symbol_exprt addr_of_ensures_write_set;
/// Symbol for the object set used to evaluate is_fresh predicates.
- const symbol_exprt is_fresh_set;
+ const symbol_exprt ptr_pred_ctx;
/// Symbol for the pointer to the is_fresh object set.
- const symbol_exprt addr_of_is_fresh_set;
+ const symbol_exprt addr_of_ptr_pred_ctx;
/// Set of required or ensured contracts for function pointers discovered
/// when processing the contract of interest.
@@ -187,7 +189,7 @@ class dfcc_wrapper_programt
// in the declaration order below.
goto_programt preamble;
- goto_programt link_is_fresh;
+ goto_programt link_ptr_pred_ctx;
goto_programt preconditions;
goto_programt history;
goto_programt write_set_checks;
@@ -224,11 +226,12 @@ class dfcc_wrapper_programt
/// - Adds release function call in \ref postamble
void encode_contract_write_set();
- /// Encodes the object set used to evaluate is fresh predicates,
- /// - Adds declaration of object set and pointer to set to \ref preamble
- /// - Adds initialisation function call in \ref preamble
- /// - Adds release function call in \ref postamble
- void encode_is_fresh_set();
+ /// Encodes the pointer predicates evaluation context object.
+ /// - Adds declaration of context object and pointer to \ref preamble
+ /// - Adds init function call in \ref preamble
+ /// - Adds reset function call in \ref link_deallocated_contract
+ /// - Adds dead instruction in \ref postamble
+ void encode_ptr_pred_ctx();
/// Encodes preconditions, instruments them to check for side effects
void encode_requires_clauses();