From d490670c9fcb4c1210f070202d53a9400dd08b60 Mon Sep 17 00:00:00 2001 From: Remi Delmas 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 -#include -#include - -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 &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 &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 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 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();