From e48f079ab9c7ac0e91f4c375577b625924a5d562 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 02:34:46 -0500 Subject: [PATCH 1/5] CONTRACTS: Add --dfcc-debug-lib CLI switch --- doc/man/cbmc.1 | 3 ++ doc/man/goto-analyzer.1 | 3 ++ doc/man/goto-instrument.1 | 3 ++ src/ansi-c/cprover_library.cpp | 3 ++ src/ansi-c/library/cprover_contracts.c | 72 +++++++++++++------------- src/util/config.cpp | 5 ++ src/util/config.h | 11 +++- 7 files changed, 62 insertions(+), 38 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index e4caf9a7c14..0969878c38b 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -334,6 +334,9 @@ set malloc failure mode to return null \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination .TP +\fB\-\-dfcc\-debug\-lib\fR +enable debug assertions in the cprover contracts library +.TP \fB\-\-reachability\-slice\fR remove instructions that cannot appear on a trace from entry point to a property diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index 4b0c79cf275..3709894958c 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -585,6 +585,9 @@ set malloc failure mode to return null .TP \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination +.TP +\fB\-\-dfcc\-debug\-lib\fR +enable debug assertions in the cprover contracts library .SS "Standard Checks" From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools apply some checks to the program by default (called the "standard checks"), with the diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 437ec15b1dd..c428ade73fc 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -706,6 +706,9 @@ do not allow malloc calls to fail by default \fB\-\-string\-abstraction\fR track C string lengths and zero\-termination .TP +\fB\-\-dfcc\-debug\-lib\fR +enable debug assertions in the cprover contracts library +.TP \fB\-\-model\-argc\-argv\fR \fIn\fR Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index f9b932f53d6..464ba4ddd96 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -45,6 +45,9 @@ static std::string get_cprover_library_text( if(config.ansi_c.string_abstraction) library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n"; + if(config.ansi_c.dfcc_debug_lib) + library_text << "#define " CPROVER_PREFIX "DFCC_DEBUG_LIB\n"; + // cprover_library.inc may not have been generated when running Doxygen, thus // make Doxygen skip this part /// \cond diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 90be51494ad..2f8c4fd203a 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -136,7 +136,7 @@ void __CPROVER_contracts_car_set_create( __CPROVER_size_t max_elems) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_car_set_t)), "set writable"); @@ -159,7 +159,7 @@ void __CPROVER_contracts_car_set_insert( __CPROVER_size_t size) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access"); #endif __CPROVER_assert( @@ -239,7 +239,7 @@ void __CPROVER_contracts_obj_set_create_indexed_by_object_id( __CPROVER_contracts_obj_set_ptr_t set) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)), "set writable"); @@ -274,7 +274,7 @@ void __CPROVER_contracts_obj_set_create_append( __CPROVER_size_t max_elems) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)), "set writable"); @@ -292,7 +292,7 @@ __CPROVER_HIDE:; void __CPROVER_contracts_obj_set_release(__CPROVER_contracts_obj_set_ptr_t set) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_obj_set_t)), "set readable"); @@ -311,7 +311,7 @@ void __CPROVER_contracts_obj_set_add( { __CPROVER_HIDE:; __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); __CPROVER_assert(object_id < set->max_elems, "no OOB access"); #endif @@ -329,7 +329,7 @@ void __CPROVER_contracts_obj_set_append( void *ptr) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(!(set->indexed_by_object_id), "not indexed by object id"); __CPROVER_assert(set->watermark < set->max_elems, "no OOB access"); #endif @@ -349,7 +349,7 @@ void __CPROVER_contracts_obj_set_remove( { __CPROVER_HIDE:; __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); __CPROVER_assert(object_id < set->max_elems, "no OOB access"); #endif @@ -369,7 +369,7 @@ __CPROVER_bool __CPROVER_contracts_obj_set_contains( { __CPROVER_HIDE:; __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); __CPROVER_assert(object_id < set->max_elems, "no OOB access"); #endif @@ -386,7 +386,7 @@ __CPROVER_bool __CPROVER_contracts_obj_set_contains_exact( { __CPROVER_HIDE:; __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(set->indexed_by_object_id, "indexed by object id"); __CPROVER_assert(object_id < set->max_elems, "no OOB access"); #endif @@ -421,7 +421,7 @@ void __CPROVER_contracts_write_set_create( __CPROVER_bool allow_deallocate) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_w_ok(set, sizeof(__CPROVER_contracts_write_set_t)), "set writable"); @@ -450,7 +450,7 @@ void __CPROVER_contracts_write_set_release( __CPROVER_contracts_write_set_ptr_t set) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_rw_ok(set, sizeof(__CPROVER_contracts_write_set_t)), "set readable"); @@ -574,7 +574,7 @@ __CPROVER_HIDE:; // store pointer __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_add(&(set->contract_frees), ptr); __CPROVER_assert(object_id < set->contract_frees.max_elems, "no OOB access"); @@ -587,7 +587,7 @@ __CPROVER_HIDE:; #endif // append pointer if available -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_contracts_obj_set_append(&(set->contract_frees_append), ptr); #else set->contract_frees_append.nof_elems = set->contract_frees_append.watermark; @@ -606,7 +606,7 @@ void __CPROVER_contracts_write_set_add_allocated( { __CPROVER_HIDE:; __CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed"); -#if DFCC_DEBUG +#if __CPROVER_DFCC_DEBUG_LIB // call inlined below __CPROVER_contracts_obj_set_add(&(set->allocated), ptr); #else @@ -627,7 +627,7 @@ void __CPROVER_contracts_write_set_add_decl( void *ptr) { __CPROVER_HIDE:; -#if DFCC_DEBUG +#if __CPROVER_DFCC_DEBUG_LIB // call inlined below __CPROVER_contracts_obj_set_add(&(set->allocated), ptr); #else @@ -652,7 +652,7 @@ void __CPROVER_contracts_write_set_record_dead( void *ptr) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_remove(&(set->allocated), ptr); #else @@ -677,7 +677,7 @@ void __CPROVER_contracts_write_set_record_deallocated( void *ptr) { __CPROVER_HIDE:; -#if DFCC_DEBUG +#if __CPROVER_DFCC_DEBUG_LIB // we record the deallocation to be able to evaluate was_freed post conditions __CPROVER_contracts_obj_set_add(&(set->deallocated), ptr); __CPROVER_contracts_obj_set_remove(&(set->allocated), ptr); @@ -745,7 +745,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_assignment( __CPROVER_contracts_write_set_ptr_t set, void *ptr, __CPROVER_size_t size) -#if DFCC_DEBUG +#if __CPROVER_DFCC_DEBUG_LIB // manually inlined below { __CPROVER_HIDE:; @@ -926,7 +926,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_deallocate( __CPROVER_HIDE:; __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( set->contract_frees.indexed_by_object_id, "set->contract_frees is indexed by object id"); @@ -984,7 +984,7 @@ __CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion( __CPROVER_contracts_write_set_ptr_t candidate) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( reference->contract_frees.indexed_by_object_id, "reference->contract_frees is indexed by object id"); @@ -1067,7 +1067,7 @@ void __CPROVER_contracts_link_is_fresh( __CPROVER_contracts_obj_set_ptr_t is_fresh_set) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(write_set != 0, "write_set not NULL"); #endif if((is_fresh_set != 0)) @@ -1089,7 +1089,7 @@ void __CPROVER_contracts_link_allocated( __CPROVER_contracts_write_set_ptr_t write_set_to_link) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( write_set_postconditions != 0, "write_set_postconditions not NULL"); #endif @@ -1114,7 +1114,7 @@ void __CPROVER_contracts_link_deallocated( __CPROVER_contracts_write_set_ptr_t write_set_to_link) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( write_set_postconditions != 0, "write_set_postconditions not NULL"); #endif @@ -1168,7 +1168,7 @@ __CPROVER_HIDE:; (write_set->assume_ensures_ctx == 1) | (write_set->assert_ensures_ctx == 1)), "__CPROVER_is_fresh is used only in requires or ensures clauses"); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)), "set readable"); @@ -1177,7 +1177,7 @@ __CPROVER_HIDE:; #endif if(write_set->assume_requires_ctx) { -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( (write_set->assert_requires_ctx == 0) & (write_set->assume_ensures_ctx == 0) & @@ -1219,7 +1219,7 @@ __CPROVER_HIDE:; // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; // record fresh object in the object set -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr); #else @@ -1235,7 +1235,7 @@ __CPROVER_HIDE:; } else if(write_set->assume_ensures_ctx) { -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( (write_set->assume_requires_ctx == 0) & (write_set->assert_requires_ctx == 0) & @@ -1274,7 +1274,7 @@ __CPROVER_HIDE:; __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; // record fresh object in the caller's write set -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr); #else __CPROVER_size_t object_id = __CPROVER_POINTER_OBJECT(ptr); @@ -1289,7 +1289,7 @@ __CPROVER_HIDE:; } else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx) { -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert( (write_set->assume_requires_ctx == 0) & (write_set->assume_ensures_ctx == 0), @@ -1298,7 +1298,7 @@ __CPROVER_HIDE:; __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 DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr))) return 0; @@ -1312,7 +1312,7 @@ __CPROVER_HIDE:; return 0; #endif // record fresh object in the object set -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_add(seen, ptr); #else @@ -1385,7 +1385,7 @@ void *__CPROVER_contracts_write_set_havoc_get_assignable_target( __CPROVER_size_t idx) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(write_set != 0, "write_set not NULL"); #endif @@ -1417,7 +1417,7 @@ void __CPROVER_contracts_write_set_havoc_slice( __CPROVER_size_t idx) { __CPROVER_HIDE:; -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access"); #endif __CPROVER_contracts_car_t car = set->contract_assigns.elems[idx]; @@ -1478,7 +1478,7 @@ __CPROVER_HIDE:; "__CPROVER_was_freed is used only in ensures clauses"); __CPROVER_assert( (set->linked_deallocated != 0), "linked_deallocated is not null"); -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below return __CPROVER_contracts_obj_set_contains_exact( set->linked_deallocated, ptr); @@ -1504,7 +1504,7 @@ __CPROVER_HIDE:; if(set->assume_ensures_ctx) { -#ifdef DFCC_DEBUG +#ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_assert( __CPROVER_contracts_obj_set_contains_exact(&(set->contract_frees), ptr), diff --git a/src/util/config.cpp b/src/util/config.cpp index 34654d2780a..fd3a4382ebf 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1164,6 +1164,11 @@ bool configt::set(const cmdlinet &cmdline) else ansi_c.string_abstraction=false; + if(cmdline.isset("dfcc-debug-lib")) + ansi_c.dfcc_debug_lib = true; + else + ansi_c.dfcc_debug_lib = false; + if(cmdline.isset("no-library")) ansi_c.lib=configt::ansi_ct::libt::LIB_NONE; diff --git a/src/util/config.h b/src/util/config.h index d62c01d5c9f..e7a12b072cf 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -72,7 +72,8 @@ class symbol_table_baset; #define OPT_CONFIG_LIBRARY \ "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \ "(no-malloc-may-fail)" \ - "(string-abstraction)" + "(string-abstraction)" \ + "(dfcc-debug-lib)" #define HELP_CONFIG_LIBRARY \ " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \ @@ -80,7 +81,9 @@ class symbol_table_baset; " {y--malloc-fail-assert} \t " \ "set malloc failure mode to assert-then-assume\n" \ " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \ - " {y--string-abstraction} \t track C string lengths and zero-termination\n" + " {y--string-abstraction} \t track C string lengths and zero-termination\n" \ + " {y--dfcc-debug-lib} \t enable debug assertions in the cprover contracts " \ + "library\n" #define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)" @@ -282,6 +285,10 @@ class configt bool string_abstraction; bool malloc_may_fail = true; + /// enable debug code in cprover_contracts library + bool dfcc_debug_lib = false; + + enum malloc_failure_modet { malloc_failure_mode_none = 0, From 4161fd177687f78b5483d10e46be6dfe24b7e98e Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 02:44:42 -0500 Subject: [PATCH 2/5] Add "make invalid pointer" utility function and havoc mode Operates in two sub-modes, controlled by CLI switch `--dfcc-simple-invalid-pointer-model` --- doc/man/cbmc.1 | 4 ++ doc/man/goto-analyzer.1 | 4 ++ doc/man/goto-instrument.1 | 4 ++ src/ansi-c/cprover_library.cpp | 4 ++ src/ansi-c/library/cprover_contracts.c | 27 ++++++++++ .../dynamic-frames/dfcc_instrument_loop.cpp | 1 + .../dynamic-frames/dfcc_spec_functions.cpp | 50 +++++++++++++++---- .../dynamic-frames/dfcc_spec_functions.h | 26 ++++++++-- src/util/config.cpp | 5 ++ src/util/config.h | 9 +++- 10 files changed, 118 insertions(+), 16 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 0969878c38b..f1a295674bf 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -337,6 +337,10 @@ track C string lengths and zero\-termination \fB\-\-dfcc\-debug\-lib\fR enable debug assertions in the cprover contracts library .TP +\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR +use simplified invalid pointer model in the cprover contracts library +(faster, unsound) +.TP \fB\-\-reachability\-slice\fR remove instructions that cannot appear on a trace from entry point to a property diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index 3709894958c..582ff022060 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -588,6 +588,10 @@ track C string lengths and zero\-termination .TP \fB\-\-dfcc\-debug\-lib\fR enable debug assertions in the cprover contracts library +.TP +\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR +use simplified invalid pointer model in the cprover contracts library +(faster, unsound) .SS "Standard Checks" From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools apply some checks to the program by default (called the "standard checks"), with the diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index c428ade73fc..f787ab7f26d 100644 --- a/doc/man/goto-instrument.1 +++ b/doc/man/goto-instrument.1 @@ -709,6 +709,10 @@ track C string lengths and zero\-termination \fB\-\-dfcc\-debug\-lib\fR enable debug assertions in the cprover contracts library .TP +\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR +use simplified invalid pointer model in the cprover contracts library +(faster, unsound) +.TP \fB\-\-model\-argc\-argv\fR \fIn\fR Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp index 464ba4ddd96..80a18ad2b95 100644 --- a/src/ansi-c/cprover_library.cpp +++ b/src/ansi-c/cprover_library.cpp @@ -48,6 +48,10 @@ static std::string get_cprover_library_text( if(config.ansi_c.dfcc_debug_lib) library_text << "#define " CPROVER_PREFIX "DFCC_DEBUG_LIB\n"; + if(config.ansi_c.simple_invalid_pointer_model) + library_text << "#define " CPROVER_PREFIX + "DFCC_SIMPLE_INVALID_POINTER_MODEL\n"; + // cprover_library.inc may not have been generated when running Doxygen, thus // make Doxygen skip this part /// \cond diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 2f8c4fd203a..8b7446b3acc 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1136,6 +1136,33 @@ void *__CPROVER_contracts_malloc( __CPROVER_size_t, __CPROVER_contracts_write_set_ptr_t); +/// \brief Makes the given pointer invalid. +/// +/// Used to craft invalid pointers when pointer predicates return false +/// in "assume" mode. +/// We have two models for invalid pointers: +/// - default: pointer is uninitialized (empty value set, nondet bit pattern). +/// - simple: pointer is either null or pointing to a dead object of size zero. +/// The simple model is activated by a CLI switch in goto-instrument. +void __CPROVER_contracts_make_invalid_pointer(void **ptr) +{ +#ifdef __CPROVER_DFCC_SIMPLE_INVALID_POINTER_MODEL + void *dummy = __CPROVER_allocate(0, 0); + __CPROVER_deallocated = + __VERIFIER_nondet___CPROVER_bool() ? dummy : __CPROVER_deallocated; + *ptr = __VERIFIER_nondet___CPROVER_bool() ? dummy : (void *)0; +#else +# pragma GCC diagnostic push +# pragma GCC diagnostic ignored "-Wuninitialized" + // We have to silence this warning to be able to generate and use an + // invalid pointer. + void *invalid; + *ptr = invalid; +# pragma GCC diagnostic pop +#endif +} + + /// \brief Implementation of the `is_fresh` front-end predicate. /// /// The behaviour depends on the boolean flags carried by \p set diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp index 7f6acd75e7f..08d7a497a1c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp @@ -121,6 +121,7 @@ void dfcc_instrument_loopt::operator()( function_id, write_set_populate_instrs, loop.addr_of_write_set_var, + dfcc_ptr_havoc_modet::NONDET, havoc_instrs, nof_targets); spec_functions.to_spec_assigns_instructions( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 1772647fc94..265a99ad924 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -103,6 +103,7 @@ void dfcc_spec_functionst::generate_havoc_function( havoc_function_id, original_program, write_set_symbol.symbol_expr(), + dfcc_ptr_havoc_modet::INVALID, havoc_program, nof_targets); @@ -144,6 +145,7 @@ void dfcc_spec_functionst::generate_havoc_instructions( const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, + dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets) { @@ -191,8 +193,9 @@ void dfcc_spec_functionst::generate_havoc_instructions( // DECL __havoc_target; // CALL __havoc_target = havoc_hook(set, next_idx); // IF !__havoc_target GOTO label; - // ASSIGN *__havoc_target = nondet(target_type); - // label: DEAD __havoc_target; + // .... add code for scalar or pointer targets ... + // label: + // DEAD __havoc_target; // ``` // declare a local var to store targets havoced via nondet assignment auto &target_type = get_target_type(ins_it->call_arguments().at(0)); @@ -213,13 +216,42 @@ void dfcc_spec_functionst::generate_havoc_instructions( havoc_program.add(goto_programt::make_incomplete_goto( dfcc_utilst::make_null_check_expr(target_expr), location)); - // create nondet assignment to the target - side_effect_expr_nondett nondet(target_type, location); - havoc_program.add(goto_programt::make_assignment( - dereference_exprt{typecast_exprt::conditional_cast( - target_expr, pointer_type(target_type))}, - nondet, - location)); + if( + ptr_havoc_mode == dfcc_ptr_havoc_modet::INVALID && + target_type.id() == ID_pointer) + { + // ``` + // DECL *__invalid_ptr; + // ASSIGN *__havoc_target = __invalid_ptr; + // DEAD __invalid_ptr; + // ``` + const auto invalid_ptr_expr = dfcc_utilst::create_symbol( + goto_model.symbol_table, + target_type, + function_id, + "__invalid_ptr", + location); + + havoc_program.add(goto_programt::make_assignment( + dereference_exprt{typecast_exprt::conditional_cast( + target_expr, pointer_type(target_type))}, + invalid_ptr_expr, + location)); + havoc_program.add( + goto_programt::make_dead(invalid_ptr_expr, location)); + } + else + { + // ``` + // ASSIGN *__havoc_target = nondet(target_type); + // ``` + side_effect_expr_nondett nondet(target_type, location); + havoc_program.add(goto_programt::make_assignment( + dereference_exprt{typecast_exprt::conditional_cast( + target_expr, pointer_type(target_type))}, + nondet, + location)); + } auto label = havoc_program.add(goto_programt::make_dead(target_expr, location)); goto_instruction->complete_goto(label); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index e75f025f800..5b3b1e7ee11 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -32,6 +32,19 @@ class message_handlert; class symbolt; class conditional_target_group_exprt; +/// \brief Represents the different ways to havoc pointers. +/// +/// Remark: +/// - Function contracts use invalid +/// - Loop contracts use nondet +enum class dfcc_ptr_havoc_modet +{ + /// havocs the pointer to an invalid pointer + INVALID, + /// havocs the pointer to an nondet pointer + NONDET +}; + /// This class rewrites GOTO functions that use the built-ins: /// - `__CPROVER_assignable`, /// - `__CPROVER_object_whole`, @@ -48,6 +61,9 @@ class dfcc_spec_functionst message_handlert &message_handler, dfcc_libraryt &library); + /// Generates the havoc function for a function contract. + /// Pointer-typed targets are turned into invalid pointers by the havoc. + /// /// From a function: /// /// ``` @@ -62,10 +78,9 @@ class dfcc_spec_functionst /// /// Which havocs the targets specified by `function_id`, passed /// - /// \param function_id function to generate instructions from - /// \param havoc_function_id write set variable to havoc - /// \param nof_targets maximum number of targets to havoc - /// + /// \param[in] function_id function to generate instructions from + /// \param[in] havoc_function_id write set variable to havoc + /// \param[out] nof_targets maximum number of targets to havoc void generate_havoc_function( const irep_idt &function_id, const irep_idt &havoc_function_id, @@ -89,13 +104,14 @@ class dfcc_spec_functionst /// \param[in] function_id function id to use for prefixing fresh variables /// \param[in] original_program program from which to derive the havoc program /// \param[in] write_set_to_havoc write set symbol to havoc + /// \param[in] ptr_havoc_mode havocing mode for pointers /// \param[out] havoc_program destination program for havoc instructions /// \param[out] nof_targets max number of havoc targets discovered - /// void generate_havoc_instructions( const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, + dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets); diff --git a/src/util/config.cpp b/src/util/config.cpp index fd3a4382ebf..49afdc2e3d3 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1169,6 +1169,11 @@ bool configt::set(const cmdlinet &cmdline) else ansi_c.dfcc_debug_lib = false; + if(cmdline.isset("dfcc-simple-invalid-pointer-model")) + ansi_c.simple_invalid_pointer_model = true; + else + ansi_c.simple_invalid_pointer_model = false; + if(cmdline.isset("no-library")) ansi_c.lib=configt::ansi_ct::libt::LIB_NONE; diff --git a/src/util/config.h b/src/util/config.h index e7a12b072cf..f1ef547cc4a 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -73,7 +73,8 @@ class symbol_table_baset; "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \ "(no-malloc-may-fail)" \ "(string-abstraction)" \ - "(dfcc-debug-lib)" + "(dfcc-debug-lib)" \ + "(dfcc-simple-invalid-pointer-model)" #define HELP_CONFIG_LIBRARY \ " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \ @@ -83,7 +84,9 @@ class symbol_table_baset; " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \ " {y--string-abstraction} \t track C string lengths and zero-termination\n" \ " {y--dfcc-debug-lib} \t enable debug assertions in the cprover contracts " \ - "library\n" + "library\n" \ + " {y--dfcc-simple-invalid-pointer-model} \t use simplified invalid pointer " \ + "model in the cprover contracts library (faster, unsound)\n" #define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)" @@ -288,6 +291,8 @@ class configt /// enable debug code in cprover_contracts library bool dfcc_debug_lib = false; + /// use simplified invalid pointer model in cprover_contracts library + bool simple_invalid_pointer_model = false; enum malloc_failure_modet { From e979772c1797e710959a4f46f1af5013e6a47ac5 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 02:53:00 -0500 Subject: [PATCH 3/5] Soudness fix: pointer predicates can fail in assume contexts. Make failed predicates yield invalid pointers (instead of nondet). Mark peformance regressing test as FUTURE. --- .../test.desc | 8 +++- src/ansi-c/library/cprover_contracts.c | 41 +++++++++++++++++-- 2 files changed, 44 insertions(+), 5 deletions(-) diff --git a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc index 540f1b7402b..0bc2a52f471 100644 --- a/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc +++ b/regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc @@ -1,4 +1,4 @@ -CORE dfcc-only smt-backend broken-cprover-smt-backend +FUTURE dfcc-only smt-backend broken-cprover-smt-backend main.c --dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula --no-standard-checks ^EXIT=0$ @@ -7,6 +7,12 @@ main.c -- ^warning: ignoring -- + +Marked as FUTURE because: +- z3 >v4.12 and up can solve the problem with `--dfcc-simple-invalid-pointer-model`, + but the CI uses older versions; +- bitwuzla >v0.6 can solve the problem but we don't run bitwuzla in CI. + Tests support for quantifiers in loop contracts with the SMT backend. When quantified loop invariants are used, they are inserted three times in the transformed program (base case assertion, step case assumption, diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 8b7446b3acc..e662bbbd599 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1165,7 +1165,7 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr) /// \brief Implementation of the `is_fresh` front-end predicate. /// -/// The behaviour depends on the boolean flags carried by \p set +/// 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 First argument of the `is_fresh` predicate @@ -1232,6 +1232,13 @@ __CPROVER_HIDE:; __CPROVER_assume(size <= __CPROVER_max_malloc_size); } + // SOUNDNESS: allow predicate to fail + if(__VERIFIER_nondet___CPROVER_bool()) + { + __CPROVER_contracts_make_invalid_pointer(elem); + return 0; + } + void *ptr = __CPROVER_allocate(size, 0); *elem = ptr; @@ -1245,7 +1252,6 @@ __CPROVER_HIDE:; // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; - // record fresh object in the object set #ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr); @@ -1286,6 +1292,13 @@ __CPROVER_HIDE:; __CPROVER_assume(size <= __CPROVER_max_malloc_size); } + // SOUNDNESS: allow predicate to fail + if(__VERIFIER_nondet___CPROVER_bool()) + { + __CPROVER_contracts_make_invalid_pointer(elem); + return 0; + } + void *ptr = __CPROVER_allocate(size, 0); *elem = ptr; @@ -1300,7 +1313,6 @@ __CPROVER_HIDE:; __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak; - // record fresh object in the caller's write set #ifdef __CPROVER_DFCC_DEBUG_LIB __CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr); #else @@ -1338,7 +1350,7 @@ __CPROVER_HIDE:; if(seen->elems[object_id] != 0) return 0; #endif - // record fresh object in the object set + #ifdef __CPROVER_DFCC_DEBUG_LIB // manually inlined below __CPROVER_contracts_obj_set_add(seen, ptr); @@ -1360,6 +1372,23 @@ __CPROVER_HIDE:; } } +/// \brief Implementation of the `pointer_in_range_dfcc` 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 lb Lower bound pointer +/// \param ptr Target pointer of the predicate +/// \param ub Upper bound pointer +/// \param write_set Write set in which seen/allocated objects are recorded; +/// +/// \details The behaviour is as follows: +/// - When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`, +/// the predicate checks that \p lb and \p ub are valid, into the same object, +/// ordered, and checks that \p ptr is between \p lb and \p ub. +/// - When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`, +/// the predicate checks that \p lb and \p ub are valid, into the same object, +/// ordered, and assigns \p ptr to some nondet offset between \p lb and \p ub. __CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc( void *lb, void **ptr, @@ -1386,7 +1415,11 @@ __CPROVER_HIDE:; if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) { if(__VERIFIER_nondet___CPROVER_bool()) + { + // SOUNDNESS: allow predicate to fail + __CPROVER_contracts_make_invalid_pointer(ptr); return 0; + } // add nondet offset __CPROVER_size_t offset = __VERIFIER_nondet_size(); From a8f6aa4b59336058a260d21879520e1bf7ad3c5c Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 02:55:09 -0500 Subject: [PATCH 4/5] Add tests for pointer predicates under disjunctions in assume contexts --- .../main.c | 14 +++++ .../test.desc | 20 ++++++++ .../main.c | 30 +++++++++++ .../test.desc | 30 +++++++++++ .../main.c | 15 ++++++ .../test.desc | 17 +++++++ .../main.c | 41 +++++++++++++++ .../test.desc | 30 +++++++++++ .../main.c | 16 ++++++ .../test.desc | 20 ++++++++ .../main.c | 34 +++++++++++++ .../test.desc | 32 ++++++++++++ .../main.c | 30 +++++++++++ .../test.desc | 17 +++++++ .../main.c | 51 +++++++++++++++++++ .../test.desc | 32 ++++++++++++ 16 files changed, 429 insertions(+) create mode 100644 regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc create mode 100644 regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c new file mode 100644 index 00000000000..604aef643ac --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/main.c @@ -0,0 +1,14 @@ +void foo(int *x) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) || 1) + __CPROVER_assigns(*x) +// clang-format on +{ + *x = 0; +} + +void main() +{ + int *x; + foo(x); +} diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc new file mode 100644 index 00000000000..b97ad84cbab --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$ +^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (FAILURE|UNKNOWN)$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: (FAILURE|UNKNOWN)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (FAILURE|UNKNOWN) +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (FAILURE|UNKNOWN)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (FAILURE|UNKNOWN) +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (FAILURE|UNKNOWN) +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (FAILURE|UNKNOWN) +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (FAILURE|UNKNOWN)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_is_fresh` is used in disjunctions, +the program accepts models where `__CPROVER_is_fresh` evaluates to false +and no object gets allocated, and pointers remain invalid. diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c new file mode 100644 index 00000000000..204e3e3e9cc --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/main.c @@ -0,0 +1,30 @@ +#include +void foo(int *x, int *y) + // clang-format off + __CPROVER_requires( + (__CPROVER_is_fresh(x, sizeof(*x)) && y == NULL) || + (x == NULL && __CPROVER_is_fresh(y, sizeof(*y))) + ) + __CPROVER_assigns(y == NULL: *x) + __CPROVER_assigns(x == NULL: *y) +// clang-format on +{ + if(y == NULL) + { + assert(0); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + *y = 0; + } +} + +void main() +{ + int *x; + int *y; + foo(x, y); +} diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc new file mode 100644 index 00000000000..f5d0da4c552 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc @@ -0,0 +1,30 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$ +^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$ +^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts. +The precondition of `foo` describes a disjunction of cases, either `x` is fresh and `y` is null, +or `x` is null and `y` is fresh. The function `foo` branches on `y == NULL`. +The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows +that both cases of the disjunction expressed in the requires clause are reachable. diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c new file mode 100644 index 00000000000..c5b856e6110 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/main.c @@ -0,0 +1,15 @@ +int *foo() + // clang-format off + __CPROVER_ensures( + __CPROVER_is_fresh(__CPROVER_return_value, sizeof(int)) || 1); +// clang-format on + +void bar() +{ + int *x = foo(); + *x = 0; //expected to fail +} +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc new file mode 100644 index 00000000000..45828926d6a --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_is_fresh` is used in disjunctions, +the program accepts models where `__CPROVER_is_fresh` evaluates to false +and no object gets allocated, and pointers remain invalid. diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c new file mode 100644 index 00000000000..c592dc8f4de --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/main.c @@ -0,0 +1,41 @@ +#include +typedef struct +{ + int *x; + int *y; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(( + __CPROVER_is_fresh(__CPROVER_return_value.x, sizeof(int)) && + __CPROVER_return_value.y == NULL + ) || ( + __CPROVER_return_value.x == NULL && + __CPROVER_is_fresh(__CPROVER_return_value.y, sizeof(int)) + )) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *x = ret.x; + int *y = ret.y; + if(y == NULL) + { + assert(0); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + *y = 0; + } +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc new file mode 100644 index 00000000000..295434501f9 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc @@ -0,0 +1,30 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$ +^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$ +^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_is_fresh` under disjunctions in assume contexts. +The postcondition of `foo` describes a disjunction of cases: either `x` is fresh and `y` is null, +or `x` is null and `y` is fresh. The function `bar` branches on `y == NULL`. +The test succeeds if the two `assert(0)` are falsifiable, which which shows that +both cases of the disjunction expressed in the ensures clause of `foo` are reachable. diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c new file mode 100644 index 00000000000..b4ad7f4386c --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/main.c @@ -0,0 +1,16 @@ +void foo(int *x, int *y) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(x, 8*sizeof(int))) + __CPROVER_requires(__CPROVER_pointer_in_range_dfcc(x, y, x+7) || 1) + __CPROVER_assigns(*y) +// clang-format on +{ + *y = 0; +} + +void main() +{ + int *x; + int *y; + foo(x, y); +} diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc new file mode 100644 index 00000000000..50338575985 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$ +^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_equals` is used in disjunctions, +the program accepts models where `__CPROVER_pointer_equals` evaluates to +false and the target pointer remains invalid. diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c new file mode 100644 index 00000000000..2c16b83c11a --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/main.c @@ -0,0 +1,34 @@ +#include +void foo(int *a, int *x, int *y) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(a, 8*sizeof(int))) + __CPROVER_requires( + (__CPROVER_pointer_in_range_dfcc(a, x, a+7) && y == NULL) || + (x == NULL && __CPROVER_pointer_in_range_dfcc(a, y, a+7)) + ) + __CPROVER_assigns(y == NULL: *x) + __CPROVER_assigns(x == NULL: *y) +// clang-format on +{ + if(y == NULL) + { + assert(0); + assert(__CPROVER_same_object(a, x)); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + assert(__CPROVER_same_object(a, y)); + *y = 0; + } +} + +void main() +{ + int *a; + int *x; + int *y; + foo(a, x, y); +} diff --git a/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc new file mode 100644 index 00000000000..97ba8f9024d --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_pass/test.desc @@ -0,0 +1,32 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line 16 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$ +^\[foo.assigns.\d+\] line 17 Check that \*x is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer NULL in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer invalid in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: dead object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 17 dereference failure: invalid integer address in \*x: SUCCESS$ +^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line 22 assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[foo.assertion.\d+\] line 23 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$ +^\[foo.assigns.\d+\] line 24 Check that \*y is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_in_range_dfcc` under disjunctions in assume contexts. +The precondition of `foo` describes a disjunction of cases, either `x` is in range of `a` and `y` is null, +or `x` is null and `y` is in range of `a`. The function `foo` branches on `y == NULL`. +The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows +that both cases of the disjunction expressed in the requires clause are reachable. diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c new file mode 100644 index 00000000000..ffd3b7457af --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/main.c @@ -0,0 +1,30 @@ + +typedef struct +{ + int *a; + int *x; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, 8*sizeof(int))) + __CPROVER_ensures( + __CPROVER_pointer_in_range_dfcc( + __CPROVER_return_value.a, + __CPROVER_return_value.x, + __CPROVER_return_value.a + 7 + ) || 1) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *x = ret.x; + *x = 0; //expected to fail +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc new file mode 100644 index 00000000000..b639707f5f5 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_in_range_dfcc` is used in disjunctions, +the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to +false and the target pointer remains invalid. diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c new file mode 100644 index 00000000000..c2a62e7f31e --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/main.c @@ -0,0 +1,51 @@ +#include +typedef struct +{ + int *a; + int *x; + int *y; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, 8*sizeof(int))) + __CPROVER_ensures(( + __CPROVER_pointer_in_range_dfcc( + __CPROVER_return_value.a, + __CPROVER_return_value.x, + __CPROVER_return_value.a + 7) && + __CPROVER_return_value.y == NULL + ) || ( + __CPROVER_return_value.x == NULL && + __CPROVER_pointer_in_range_dfcc( + __CPROVER_return_value.a, + __CPROVER_return_value.y, + __CPROVER_return_value.a + 7))) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *a = ret.a; + int *x = ret.x; + int *y = ret.y; + if(y == NULL) + { + assert(0); + assert(__CPROVER_same_object(x, a)); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + assert(__CPROVER_same_object(y, a)); + *y = 0; + } +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc new file mode 100644 index 00000000000..d0f29a67b8a --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_pass/test.desc @@ -0,0 +1,32 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.assertion.\d+\] line 35 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line 36 assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line 37 Check that \*x is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer NULL in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer invalid in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: dead object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 37 dereference failure: invalid integer address in \*x: SUCCESS$ +^\[bar.assertion.\d+\] line 41 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line 42 assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[bar.assertion.\d+\] line 43 assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line 44 Check that \*y is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer NULL in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer invalid in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: dead object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line 44 dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_in_range` under disjunctions in assume contexts. +The postcondition of `foo` describes a disjunction of cases: either `x` is in range of `a` and `y` is null, +or `x` is null and `y` is in range of `a`. The function `bar` branches on `y == NULL`. +The test succeeds if the two `assert(0)` are falsifiable, which which shows that +both cases of the disjunction expressed in the ensures clause of `foo` are reachable. From e965339ec0d2cb482427fc1bf722592c835f9af9 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 17 Jan 2025 03:01:28 -0500 Subject: [PATCH 5/5] Add new `__CPROVER_pointer_equals(p, q)` predicate Meant to replace `p == q in contract clauses, works as a hook to override equality behaviour in assume contexts to make it constructive. Add TODOs to remember overriding built-in ptr equality with new predicate in requires/ensures clauses expressions and user-defined ptr predicates bodies. --- .../main.c | 16 ++ .../test.desc | 20 +++ .../main.c | 34 ++++ .../test.desc | 32 ++++ .../main.c | 28 ++++ .../test.desc | 17 ++ .../main.c | 49 ++++++ .../test.desc | 32 ++++ src/ansi-c/c_typecheck_expr.cpp | 14 +- src/ansi-c/cprover_builtin_headers.h | 1 + src/ansi-c/library/cprover_contracts.c | 56 +++++++ src/goto-instrument/Makefile | 1 + .../doc/developer/contracts-dev-arch.md | 1 + .../contracts-dev-spec-dfcc-instrument.md | 3 + ...ts-dev-spec-memory-predicates-rewriting.md | 3 + .../contracts-dev-spec-pointer-equals.md | 25 +++ .../contracts-dev-spec-pointer-in-range.md | 2 +- .../doc/user/contracts-memory-predicates.md | 43 ++++++ .../dynamic-frames/dfcc_instrument.cpp | 6 + .../dynamic-frames/dfcc_is_cprover_symbol.cpp | 1 + .../contracts/dynamic-frames/dfcc_library.cpp | 1 + .../contracts/dynamic-frames/dfcc_library.h | 2 + .../dfcc_lift_memory_predicates.cpp | 17 +- .../dynamic-frames/dfcc_pointer_equals.cpp | 145 ++++++++++++++++++ .../dynamic-frames/dfcc_pointer_equals.h | 65 ++++++++ .../dynamic-frames/dfcc_wrapper_program.cpp | 6 +- 26 files changed, 615 insertions(+), 5 deletions(-) create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c create mode 100644 regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc create mode 100644 src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp create mode 100644 src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c new file mode 100644 index 00000000000..479d5b4e916 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/main.c @@ -0,0 +1,16 @@ +void foo(int *x, int *y) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int))) + __CPROVER_requires(__CPROVER_pointer_equals(y, x) || 1) + __CPROVER_assigns(*y) +// clang-format on +{ + *y = 0; +} + +void main() +{ + int *x; + int *y; + foo(x, y); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc new file mode 100644 index 00000000000..50338575985 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_fail/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$ +^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_equals` is used in disjunctions, +the program accepts models where `__CPROVER_pointer_equals` evaluates to +false and the target pointer remains invalid. diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c new file mode 100644 index 00000000000..52dd0486677 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/main.c @@ -0,0 +1,34 @@ +#include +void foo(int *a, int *x, int *y) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(a, sizeof(int))) + __CPROVER_requires( + (__CPROVER_pointer_equals(x,a) && y == NULL) || + (x == NULL && __CPROVER_pointer_equals(y,a)) + ) + __CPROVER_assigns(y == NULL: *x) + __CPROVER_assigns(x == NULL: *y) +// clang-format on +{ + if(y == NULL) + { + assert(0); + assert(__CPROVER_same_object(a, x)); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + assert(__CPROVER_same_object(a, y)); + *y = 0; + } +} + +void main() +{ + int *a; + int *x; + int *y; + foo(a, x, y); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc new file mode 100644 index 00000000000..bd71dc7d63a --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_enforce_requires_disjunction_pass/test.desc @@ -0,0 +1,32 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$ +^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$ +^\[foo.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts. +The precondition of `foo` describes a disjunction of cases, either `x` equals `a` and `y` is null, +or `x` is null and `y` equals `a`. The function `foo` branches on `y == NULL`. +The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows +that both cases of the disjunction expressed in the requires clause are reachable. diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c new file mode 100644 index 00000000000..27b35453c39 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/main.c @@ -0,0 +1,28 @@ + +typedef struct +{ + int *a; + int *x; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int))) + __CPROVER_ensures( + __CPROVER_pointer_equals( + __CPROVER_return_value.x, + __CPROVER_return_value.a) || 1) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *x = ret.x; + *x = 0; //expected to fail +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc new file mode 100644 index 00000000000..03832485dc2 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_fail/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when `__CPROVER_pointer_equals` is used in disjunctions, +the program accepts models where `__CPROVER_pointer_equals` evaluates to +false and the target pointer remains invalid. diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c new file mode 100644 index 00000000000..fb853f061f7 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/main.c @@ -0,0 +1,49 @@ +#include +typedef struct +{ + int *a; + int *x; + int *y; +} ret_t; + +ret_t foo() + // clang-format off + __CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int))) + __CPROVER_ensures(( + __CPROVER_pointer_equals( + __CPROVER_return_value.x, + __CPROVER_return_value.a) && + __CPROVER_return_value.y == NULL + ) || ( + __CPROVER_return_value.x == NULL && + __CPROVER_pointer_equals( + __CPROVER_return_value.y, + __CPROVER_return_value.a))) + // clang-format on + ; + +void bar() +{ + ret_t ret = foo(); + int *a = ret.a; + int *x = ret.x; + int *y = ret.y; + if(y == NULL) + { + assert(0); + assert(__CPROVER_same_object(x, a)); + *x = 0; + } + else + { + assert(0); + assert(x == NULL); + assert(__CPROVER_same_object(y, a)); + *y = 0; + } +} + +void main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc new file mode 100644 index 00000000000..1c5c5f7bc57 --- /dev/null +++ b/regression/contracts-dfcc/test_pointer_equals_replace_ensures_disjunction_pass/test.desc @@ -0,0 +1,32 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract foo +^\[bar.assertion.\d+\] line 33 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$ +^\[bar.assertion.\d+\] line 39 assertion 0: FAILURE$ +^\[bar.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$ +^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$ +^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$ +^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts. +The postcondition of `foo` describes a disjunction of cases: either `x` equals `a` and `y` is null, +or `x` is null and `y` equals `a`. The function `bar` branches on `y == NULL`. +The test succeeds if the two `assert(0)` are falsifiable, which which shows that +both cases of the disjunction expressed in the ensures clause of `foo` are reachable. diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 35bc45cb257..dea0fdc1b1d 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2591,7 +2591,19 @@ exprt c_typecheck_baset::do_special_functions( const irep_idt &identifier=to_symbol_expr(f_op).get_identifier(); - if(identifier == CPROVER_PREFIX "is_fresh") + if(identifier == CPROVER_PREFIX "pointer_equals") + { + if(expr.arguments().size() != 2) + { + error().source_location = f_op.source_location(); + error() << CPROVER_PREFIX "pointer_equals expects two operands; " + << expr.arguments().size() << "provided." << eom; + throw 0; + } + typecheck_function_call_arguments(expr); + return nil_exprt(); + } + else if(identifier == CPROVER_PREFIX "is_fresh") { if(expr.arguments().size() != 2) { diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index f0ae5e74004..d2d96df9d97 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -44,6 +44,7 @@ void __CPROVER_fence(const char *kind, ...); // contract-related functions __CPROVER_bool __CPROVER_is_freeable(const void *mem); __CPROVER_bool __CPROVER_was_freed(const void *mem); +__CPROVER_bool __CPROVER_pointer_equals(void *p, void *q); __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); __CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void)); // same as pointer_in_range with experimental support in contracts diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index e662bbbd599..5a64466659e 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1162,6 +1162,62 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr) #endif } +/// \brief Implementation of the `pointer_equals` front-end predicate. +/// +/// \param ptr1 First argument of the `pointer_equals` predicate +/// \param ptr2 Second argument of the `pointer_equals` predicate +/// \param write_set Write set which conveys the invocation context +/// (requires/ensures clause, assert/assume context); +/// +/// \details The behaviour is as follows: +/// When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`, +/// the predicate nondeterministically invalidates `*ptr1` and returns `false`, +/// or checks that `ptr2` is either NULL or valid, and assigns `*ptr1` to `ptr2`. +/// When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`, +/// the predicate checks that both `*ptr1` and `ptr2` are either NULL or valid, +/// and returns the value of (*ptr1 == ptr2). +__CPROVER_bool __CPROVER_contracts_pointer_equals( + void **ptr1, + void *ptr2, + __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"); +#endif + if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) + { + if(__VERIFIER_nondet___CPROVER_bool()) + { + __CPROVER_contracts_make_invalid_pointer(ptr1); + return 0; + } + __CPROVER_assert( + (ptr2 == 0) || __CPROVER_r_ok(ptr2, 0), + "pointer_equals is only called with valid pointers"); + *ptr1 = ptr2; + return 1; + } + else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */ + { + void *derefd = *ptr1; + __CPROVER_assert( + (derefd == 0) || __CPROVER_r_ok(derefd, 0), + "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; + } +} /// \brief Implementation of the `is_fresh` front-end predicate. /// diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index dfacdd636ee..b33c52692f0 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -29,6 +29,7 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_instrument_loop.cpp \ contracts/dynamic-frames/dfcc_library.cpp \ contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \ + contracts/dynamic-frames/dfcc_pointer_equals.cpp \ contracts/dynamic-frames/dfcc_is_fresh.cpp \ contracts/dynamic-frames/dfcc_pointer_in_range.cpp \ contracts/dynamic-frames/dfcc_is_freeable.cpp \ diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md index b1b5230962e..039c622067f 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md @@ -29,6 +29,7 @@ Each of these translation passes is implemented in a specific class: @ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt @ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh @ref dfcc_pointer_in_ranget | Implements @ref contracts-dev-spec-pointer-in-range + @ref dfcc_pointer_equalst | Implements @ref contracts-dev-spec-pointer-equals @ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting @ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable @ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md index 22c64d14402..072fc75af0f 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md @@ -174,6 +174,9 @@ Calls to `__CPROVER_obeys_contract` are rewritten as described in Calls to `__CPROVER_pointer_in_range_dfcc` are rewritten as described in @subpage contracts-dev-spec-pointer-in-range +Calls to `__CPROVER_pointer_equals` are rewritten as described in +@subpage contracts-dev-spec-pointer-equals + For all other function or function pointer calls, we proceed as follows. If the function call has an LHS (i.e. its result is assigned to a return value diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md index 56f23746c0b..2f689dabd98 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md @@ -8,6 +8,9 @@ The C extensions for contract specification provide three pointer-related memory predicates: ```c +// Holds iff ptr1 and ptr2 are both either null or valid and are equal. +__CPROVER_bool __CPROVER_pointer_equals(void *ptr1, void* ptr2); + // Holds iff ptr is pointing to an object distinct to all objects pointed to by // other __CPROVER_is_fresh occurrences in the contract's pre and post conditions __CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size); diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md new file mode 100644 index 00000000000..c5a03bbe7b1 --- /dev/null +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md @@ -0,0 +1,25 @@ +# Rewriting Calls to the __CPROVER_pointer_equals Predicate {#contracts-dev-spec-pointer-equals} + +Back to top @ref contracts-dev-spec + +@tableofcontents + +In goto programs encoding pre or post conditions (generated from the contract +clauses) and in all user-defined functions, we simply replace calls to +`__CPROVER_pointer_equals` with calls to the library implementation. + +```c +__CPROVER_contracts_pointer_equals( + void **ptr1, + void *ptr2, + __CPROVER_contracts_write_set_ptr_t write_set); +``` + +This function implements the `__CPROVER_pointer_equals` behaviour in all +possible contexts (contract checking vs replacement, requires vs ensures clause +context, as described by the flags carried by the write set parameter). + +--- + Prev | Next +:-----|:------ + @ref contracts-dev | @ref contracts-dev-spec-reminder \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md index c8f06d4a174..5c97a1a893a 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md @@ -23,4 +23,4 @@ context, as described by the flags carried by the write set parameter). --- Prev | Next :-----|:------ - @ref contracts-dev | @ref contracts-dev-spec-reminder \ No newline at end of file + @ref contracts-dev | @ref contracts-dev-spec-pointer-equals \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md index 2f966f83582..e2c526bd840 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -9,6 +9,49 @@ let users describe the shape of the memory accessed through pointers in _requires clauses_ and _ensures clauses_. Attempting to call these predicates outside of a requires or ensures clause context will result in a verification error. + +## The __CPROVER_pointer_equals predicate +### Syntax + +```c +bool __CPROVER_pointer_equals(void *p, void *q); +``` +This predicate can only be used in ensures and requires clauses and checks for +pointer validity and equality. + +#### Parameters + +`__CPROVER_pointer_equals` takes two pointers as arguments. + +#### Return Value + +It returns a `bool` value: +- `true` iff pointers are both null or valid and are equal, +- `false` otherwise. + +### Semantics + +#### Enforcement + +When checking a contract using `--enforce-contract foo`: +- used in a _requires_ clause, the predicate will check that `ptr2` is always + either null or valid, and it will make `ptr1` equal to `ptr2`. + This results in a state resulting in a state where both pointers are either + null or valid and equal; +- used in an _ensures_ clause it will check that memory both pointers are always + either null or valid and equal. + +#### Replacement + +When checking a contract using `--replace-call-with-contract foo`, we get the +dual behaviour: +- used in a _requires_ clause it will check that memory both pointers are always + either null or valid and equal, +- used in an _ensures_ clause, the predicate will check that `ptr2` is always + either null or valid, and it will make `ptr1` equal to `ptr2`. + This results in a state resulting in a state where both pointers are either + null or valid and equal. + ## The __CPROVER_is_fresh predicate ### Syntax diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index ea0417d3371..4b7302cd2c2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -37,6 +37,7 @@ Author: Remi Delmas, delmarsd@amazon.com #include "dfcc_is_fresh.h" #include "dfcc_library.h" #include "dfcc_obeys_contract.h" +#include "dfcc_pointer_equals.h" #include "dfcc_pointer_in_range.h" #include "dfcc_spec_functions.h" #include "dfcc_utils.h" @@ -525,6 +526,11 @@ void dfcc_instrumentt::instrument_instructions( dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts) { + // rewrite pointer_equals calls + dfcc_pointer_equalst pointer_equals(library, message_handler); + pointer_equals.rewrite_calls( + goto_program, first_instruction, last_instruction, cfg_info); + // rewrite pointer_in_range calls dfcc_pointer_in_ranget pointer_in_range(library, message_handler); pointer_in_range.rewrite_calls( 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 1da53f0245f..2c945eb8acd 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 @@ -53,6 +53,7 @@ init_function_symbols(std::unordered_set &function_symbols) "contracts_obj_set_create_indexed_by_object_id"); function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_release"); function_symbols.insert(CPROVER_PREFIX "contracts_obj_set_remove"); + function_symbols.insert(CPROVER_PREFIX "contracts_pointer_equals"); function_symbols.insert(CPROVER_PREFIX "contracts_pointer_in_range_dfcc"); function_symbols.insert(CPROVER_PREFIX "contracts_was_freed"); function_symbols.insert(CPROVER_PREFIX "contracts_write_set_add_allocated"); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 242b330b4d3..efa62681c5f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -125,6 +125,7 @@ const std::map create_dfcc_fun_to_name() {dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"}, {dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"}, {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"}, + {dfcc_funt::POINTER_EQUALS, CONTRACTS_PREFIX "pointer_equals"}, {dfcc_funt::IS_FRESH, CONTRACTS_PREFIX "is_fresh"}, {dfcc_funt::POINTER_IN_RANGE_DFCC, CONTRACTS_PREFIX "pointer_in_range_dfcc"}, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index aa49b9fe536..68e243200b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -126,6 +126,8 @@ enum class dfcc_funt LINK_ALLOCATED, /// \see __CPROVER_contracts_link_deallocated LINK_DEALLOCATED, + /// \see __CPROVER_contracts_pointer_equals + POINTER_EQUALS, /// \see __CPROVER_contracts_is_fresh IS_FRESH, /// \see __CPROVER_contracts_pointer_in_range_dfcc diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index ef8300f1182..52034128cd6 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -7,6 +7,10 @@ Date: August 2022 \*******************************************************************/ +// TODO when scanning the goto functions to detect pointer predicates, +// replace pointer equality p == q with __CPROVER_pointer_equals(p,q) +// in all user-defined memory predicates. + #include "dfcc_lift_memory_predicates.h" #include @@ -44,7 +48,8 @@ bool dfcc_lift_memory_predicatest::is_lifted_function( /// True iff function_id is a core memory predicate static bool is_core_memory_predicate(const irep_idt &function_id) { - return (function_id == CPROVER_PREFIX "is_fresh") || + return (function_id == CPROVER_PREFIX "pointer_equals") || + (function_id == CPROVER_PREFIX "is_fresh") || (function_id == CPROVER_PREFIX "pointer_in_range_dfcc") || (function_id == CPROVER_PREFIX "obeys_contract"); } @@ -231,7 +236,15 @@ void dfcc_lift_memory_predicatest::collect_parameters_to_lift( { const irep_idt &callee_id = to_symbol_expr(it.call_function()).get_identifier(); - if(callee_id == CPROVER_PREFIX "is_fresh") + if(callee_id == CPROVER_PREFIX "pointer_equals") + { + auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); + if(opt_rank.has_value()) + { + lifted_parameters[function_id].insert(opt_rank.value()); + } + } + else if(callee_id == CPROVER_PREFIX "is_fresh") { auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank); if(opt_rank.has_value()) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp new file mode 100644 index 00000000000..a5fbfea3fa7 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.cpp @@ -0,0 +1,145 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: Jan 2025 + +\*******************************************************************/ + +#include "dfcc_pointer_equals.h" + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "dfcc_cfg_info.h" +#include "dfcc_library.h" + +dfcc_pointer_equalst::dfcc_pointer_equalst( + dfcc_libraryt &library, + message_handlert &message_handler) + : library(library), message_handler(message_handler), log(message_handler) +{ +} + +void dfcc_pointer_equalst::rewrite_calls( + goto_programt &program, + dfcc_cfg_infot cfg_info) +{ + rewrite_calls( + program, + program.instructions.begin(), + program.instructions.end(), + cfg_info); +} + +void dfcc_pointer_equalst::rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + dfcc_cfg_infot cfg_info) +{ + auto &target = first_instruction; + while(target != last_instruction) + { + if(target->is_function_call()) + { + const auto &function = target->call_function(); + + if(function.id() == ID_symbol) + { + const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + + if(fun_name == CPROVER_PREFIX "pointer_equals") + { + // add address on first operand + target->call_arguments()[0] = + address_of_exprt(target->call_arguments()[0]); + + // fix the function name. + to_symbol_expr(target->call_function()) + .set_identifier( + library.dfcc_fun_symbol[dfcc_funt::POINTER_EQUALS].name); + + // pass the write_set + target->call_arguments().push_back(cfg_info.get_write_set(target)); + } + } + } + target++; + } +} + +class pointer_equality_visitort : public expr_visitort +{ +private: + std::vector equality_exprs_to_transform; + +public: + void visit_expr(exprt &expr) + { + if(expr.id() == ID_equal) + { + const equal_exprt &equal_expr = to_equal_expr(expr); + + // Check if both operands are pointers + if( + equal_expr.lhs().type().id() == ID_pointer && + equal_expr.rhs().type().id() == ID_pointer) + { + equality_exprs_to_transform.push_back(&expr); + } + } + } + + // Apply the transformations after visiting + void transform() + { + const code_typet pointer_equals_type( + {code_typet::parametert(pointer_type(void_type())), + code_typet::parametert(pointer_type(void_type()))}, + bool_typet()); + + symbol_exprt pointer_equals("ID_pointer_equals", pointer_equals_type); + + for(exprt *expr_ptr : equality_exprs_to_transform) + { + const equal_exprt &equal_expr = to_equal_expr(*expr_ptr); + + // Create the function call to __CPROVER_pointer_equals + // Add the original equality operands as arguments + side_effect_expr_function_callt result( + pointer_equals, + {equal_expr.lhs(), equal_expr.rhs()}, + bool_typet(), + equal_expr.source_location()); + + result.arguments().push_back(equal_expr.lhs()); + result.arguments().push_back(equal_expr.rhs()); + + // Set the type of the function call + result.type() = bool_typet(); + + // Replace the original expression + *expr_ptr = result; + } + } +}; + +// Usage function +void rewrite_equal_exprt_to_pointer_equals(exprt &expr) +{ + pointer_equality_visitort visitor; + + // First collect all equality expressions + expr.visit(visitor); + + // Then transform them + visitor.transform(); +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h new file mode 100644 index 00000000000..350d87d03c7 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_equals.h @@ -0,0 +1,65 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: Jan 2025 + +\*******************************************************************/ + +/// \file +/// Instruments occurrences of pointer_equals predicates in programs +/// encoding requires and ensures clauses of contracts. + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_POINTER_EQUALS_H + +#include + +#include + +class goto_modelt; +class message_handlert; +class dfcc_libraryt; +class dfcc_cfg_infot; +class exprt; + +/// Rewrites `equal_exprt` over pointers into calls +/// to the front-end function `__CPROVER_pointer_equals`, +/// at the expression level. Meant to be Applied before GOTO conversion +/// of function contract clauses, followed by `rewrite_calls`. +void rewrite_equal_exprt_to_pointer_equals(exprt &expr); + +/// Rewrites calls to pointer_equals predicates into calls +/// to the library implementation. +class dfcc_pointer_equalst +{ +public: + /// \param library The contracts instrumentation library + /// \param message_handler Used for messages + dfcc_pointer_equalst( + dfcc_libraryt &library, + message_handlert &message_handler); + + /// Rewrites calls to pointer_equals predicates into calls + /// to the library implementation in the given program, passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info); + + /// Rewrites calls to pointer_equals predicates into calls + /// to the library implementation in the given program between + /// first_instruction (included) and last_instruction (excluded), passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + dfcc_cfg_infot cfg_info); + +protected: + dfcc_libraryt &library; + message_handlert &message_handler; + messaget log; +}; + +#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 45d83370521..a625383f182 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -27,6 +27,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_lift_memory_predicates.h" +#include "dfcc_pointer_equals.h" #include "dfcc_utils.h" /// Generate the contract write set @@ -563,6 +564,8 @@ void dfcc_wrapper_programt::encode_requires_clauses() "Check requires clause of contract " + id2string(contract_symbol.name) + " for function " + id2string(wrapper_id)); } + // // rewrite pointer equalities before goto conversion + // TODO rewrite_equal_exprt_to_pointer_equals(requires_lmbd); codet requires_statement(statement_type, {std::move(requires_lmbd)}, sl); converter.goto_convert(requires_statement, requires_program, language_mode); } @@ -614,7 +617,8 @@ void dfcc_wrapper_programt::encode_ensures_clauses() "Check ensures clause of contract " + id2string(contract_symbol.name) + " for function " + id2string(wrapper_id)); } - + // // rewrite pointer equalities before goto conversion + // TODO rewrite_equal_exprt_to_pointer_equals(ensures); codet ensures_statement(statement_type, {std::move(ensures)}, sl); converter.goto_convert(ensures_statement, ensures_program, language_mode); }