From 96d1efb2ec4c2c5e078f9467b2d05893a3ee479a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 May 2022 14:51:14 +0000 Subject: [PATCH 1/2] Remove unnecessary __CPROVER_deallocated updates We always allocated fresh objects, it is impossible for the condition in these assignments to be true. --- src/ansi-c/library/stdlib.c | 11 ----------- src/cpp/library/new.c | 6 ------ 2 files changed, 17 deletions(-) diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 1d7e36616dd..41cb120feb5 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -130,10 +130,6 @@ __CPROVER_HIDE:; // and __CPROVER_allocate doesn't, but no one cares malloc_res = __CPROVER_allocate(alloc_size, 1); - // make sure it's not recorded as deallocated - __CPROVER_deallocated = - (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated; - // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); __CPROVER_malloc_is_new_array = @@ -194,10 +190,6 @@ __CPROVER_HIDE:; void *malloc_res; malloc_res = __CPROVER_allocate(malloc_size, 0); - // make sure it's not recorded as deallocated - __CPROVER_deallocated = - (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated; - // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); __CPROVER_malloc_is_new_array = @@ -225,9 +217,6 @@ void *__builtin_alloca(__CPROVER_size_t alloca_size) void *res; res = __CPROVER_allocate(alloca_size, 0); - // make sure it's not recorded as deallocated - __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated; - // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array; diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c index 673311c60f5..1f623058581 100644 --- a/src/cpp/library/new.c +++ b/src/cpp/library/new.c @@ -10,9 +10,6 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) void *res; res = __CPROVER_allocate(malloc_size, 0); - // ensure it's not recorded as deallocated - __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated; - // non-deterministically record the object for delete/delete[] checking __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object; @@ -37,9 +34,6 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) void *res; res = __CPROVER_allocate(size*count, 0); - // ensure it's not recorded as deallocated - __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated; - // non-deterministically record the object for delete/delete[] checking __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object; From 5be34fb7ee1266fd595f4ff3ed7c046b3c212ff7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 8 Nov 2021 13:47:58 +0000 Subject: [PATCH 2/2] Track deallocated/dead in an array This enables tracking of all deallocations and all dead objects, and thereby use of deallocated/dead_object predicates within assumptions. --- .../test-smt2-outfile.desc | 4 ++-- .../cbmc/pointer-extra-checks/test.desc | 1 - regression/cbmc/r_w_ok10/main.c | 9 ++++++++ regression/cbmc/r_w_ok10/test.desc | 10 +++++++++ regression/cbmc/r_w_ok11/main.c | 21 +++++++++++++++++++ regression/cbmc/r_w_ok11/test.desc | 10 +++++++++ .../test.desc | 2 +- src/ansi-c/ansi_c_internal_additions.cpp | 6 ++++-- src/ansi-c/goto_check_c.cpp | 10 ++------- src/ansi-c/library/cprover.h | 2 +- src/ansi-c/library/stdlib.c | 10 ++++----- src/cpp/cpp_internal_additions.cpp | 8 +++++-- src/cpp/library/new.c | 9 +++++--- src/goto-programs/builtin_functions.cpp | 12 +++-------- src/util/pointer_predicates.cpp | 8 +++++-- 15 files changed, 85 insertions(+), 37 deletions(-) create mode 100644 regression/cbmc/r_w_ok10/main.c create mode 100644 regression/cbmc/r_w_ok10/test.desc create mode 100644 regression/cbmc/r_w_ok11/main.c create mode 100644 regression/cbmc/r_w_ok11/test.desc diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc index ae228a04e44..169786e9dff 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc +++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc @@ -1,13 +1,13 @@ CORE broken-smt-backend main.c --smt2 --outfile - -\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\) +\(= \(select array_of\.\d+ i\) \(ite false #b1 #b0\)\) \(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) \(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) ^EXIT=0$ ^SIGNAL=0$ -- -\(= \(select array_of\.2 i\) false\) +\(= \(select array_of\.\d+ i\) false\) \(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) \(= \(select array\.3 \(_ bv\d+ 64\)\) false\) -- diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc index b793e876bf8..058bfc386ca 100644 --- a/regression/cbmc/pointer-extra-checks/test.desc +++ b/regression/cbmc/pointer-extra-checks/test.desc @@ -10,7 +10,6 @@ main.c ^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$ ^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$ ^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$ -^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$ ^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$ ^\[main.pointer_dereference.10\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$ ^\[main.pointer_dereference.11\] .* dereference failure: invalid integer address in \*s: FAILURE$ diff --git a/regression/cbmc/r_w_ok10/main.c b/regression/cbmc/r_w_ok10/main.c new file mode 100644 index 00000000000..8b74baf904b --- /dev/null +++ b/regression/cbmc/r_w_ok10/main.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + int *p = malloc(sizeof(int)); + free(p); + __CPROVER_assume(__CPROVER_r_ok(p, sizeof(int))); + __CPROVER_assert(0, "should be unreachable"); +} diff --git a/regression/cbmc/r_w_ok10/test.desc b/regression/cbmc/r_w_ok10/test.desc new file mode 100644 index 00000000000..73361501456 --- /dev/null +++ b/regression/cbmc/r_w_ok10/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test checks that __CPROVER_r_ok can safely be used in assumptions. diff --git a/regression/cbmc/r_w_ok11/main.c b/regression/cbmc/r_w_ok11/main.c new file mode 100644 index 00000000000..7bad38cb9e8 --- /dev/null +++ b/regression/cbmc/r_w_ok11/main.c @@ -0,0 +1,21 @@ +#include +#include + +void foo(char *p, char *q) +{ + if(p) + free(p); + if(q) + free(q); +} + +_Bool nondet_bool(); + +int main() +{ + char *p = nondet_bool() ? NULL : malloc(10); + char *q = nondet_bool() ? NULL : malloc(12); + foo(p, q); + // no valid objects live at p or q anymore + assert(!__CPROVER_r_ok(p, 0) & !__CPROVER_r_ok(q, 0)); +} diff --git a/regression/cbmc/r_w_ok11/test.desc b/regression/cbmc/r_w_ok11/test.desc new file mode 100644 index 00000000000..1b709c2066d --- /dev/null +++ b/regression/cbmc/r_w_ok11/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + +VERIFICATION SUCCESSFUL +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test checks that negations of __CPROVER_r_ok can safely be used. diff --git a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc index a5bf8ec70eb..dd51f5a2921 100644 --- a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc +++ b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc @@ -1,7 +1,7 @@ CORE test.c --malloc-may-fail --malloc-fail-null -^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$ +^\[(free.precondition|main.precondition_instance).\d+] line \d+ double free: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 804adf9db67..05419bafea9 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -171,8 +171,10 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "constant_infinity_uint];\n" // malloc - "const void *" CPROVER_PREFIX "deallocated=0;\n" - "const void *" CPROVER_PREFIX "dead_object=0;\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "deallocated[" + CPROVER_PREFIX "constant_infinity_uint];\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "dead_object[" + CPROVER_PREFIX "constant_infinity_uint];\n" "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++ CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++ "const void *" CPROVER_PREFIX "memory_leak=0;\n" diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 355ffa36c19..c72b3316150 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -2214,15 +2214,9 @@ void goto_check_ct::goto_check( if(local_bitvector_analysis->dirty(variable)) { // need to mark the dead variable as dead - exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - exprt address_of_expr = typecast_exprt::conditional_cast( - address_of_exprt(variable), lhs.type()); - if_exprt rhs( - side_effect_expr_nondett(bool_typet(), i.source_location()), - std::move(address_of_expr), - lhs); + exprt lhs = dead_object(address_of_exprt{variable}, ns); new_code.add(goto_programt::make_assignment( - code_assignt{std::move(lhs), std::move(rhs), i.source_location()}, + code_assignt{std::move(lhs), true_exprt{}, i.source_location()}, i.source_location())); } } diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 16b17990ea8..5da68800c5a 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -20,7 +20,7 @@ typedef signed long long __CPROVER_ssize_t; void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); void __CPROVER_deallocate(void *); -extern const void *__CPROVER_deallocated; +extern __CPROVER_bool __CPROVER_deallocated[]; extern const void *__CPROVER_new_object; extern __CPROVER_bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 41cb120feb5..edee48f53e4 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -264,8 +264,9 @@ void free(void *ptr) "free argument has offset zero"); // catch double free - __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, - "double free"); + __CPROVER_precondition( + ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)], + "double free"); // catch people who try to use free(...) for stuff // allocated with new[] @@ -602,10 +603,7 @@ __CPROVER_HIDE:; /* FUNCTION: __CPROVER_deallocate */ -__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); - void __CPROVER_deallocate(void *ptr) { - if(__VERIFIER_nondet___CPROVER_bool()) - __CPROVER_deallocated = ptr; + __CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)] = 1; } diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index c1365387c83..56df1388872 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -88,8 +88,12 @@ void cpp_internal_additions(std::ostream &out) << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n'; // malloc - out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n'; - out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n'; + out << CPROVER_PREFIX "bool " + << CPROVER_PREFIX "deallocated[__CPROVER::constant_infinity_uint];" + << '\n'; + out << CPROVER_PREFIX "bool " + << CPROVER_PREFIX "dead_object[__CPROVER::constant_infinity_uint];" + << '\n'; out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n'; out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;" << '\n'; diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c index 1f623058581..0959de335de 100644 --- a/src/cpp/library/new.c +++ b/src/cpp/library/new.c @@ -71,7 +71,9 @@ inline void __delete(void *ptr) "delete argument must have offset zero"); // catch double delete - __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete"); + __CPROVER_precondition( + ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)], + "double delete"); // catch people who call delete for objects allocated with new[] __CPROVER_precondition( @@ -107,8 +109,9 @@ inline void __delete_array(void *ptr) "delete argument must have offset zero"); // catch double delete - __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, - "double delete"); + __CPROVER_precondition( + ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)], + "double delete"); // catch people who call delete[] for objects allocated with new __CPROVER_precondition( diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 38f6567f41a..95860d2cf84 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -1415,16 +1416,9 @@ void goto_convertt::do_function_call_symbol( make_temp_symbol(new_lhs, "alloca", dest, mode); // mark pointer to alloca result as dead - symbol_exprt dead_object_sym = - ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); - exprt alloca_result = - typecast_exprt::conditional_cast(new_lhs, dead_object_sym.type()); - if_exprt rhs{ - side_effect_expr_nondett{bool_typet(), source_location}, - std::move(alloca_result), - dead_object_sym}; + exprt dead_object_expr = dead_object(new_lhs, ns); code_assignt assign{ - std::move(dead_object_sym), std::move(rhs), source_location}; + std::move(dead_object_expr), true_exprt{}, source_location}; targets.destructor_stack.add(assign); } else diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 2a921fe8316..e228aad8123 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -45,7 +45,9 @@ exprt deallocated(const exprt &pointer, const namespacet &ns) // we check __CPROVER_deallocated! const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "deallocated"); - return same_object(pointer, deallocated_symbol.symbol_expr()); + return index_exprt{ + deallocated_symbol.symbol_expr(), + typecast_exprt::conditional_cast(pointer_object(pointer), index_type())}; } exprt dead_object(const exprt &pointer, const namespacet &ns) @@ -53,7 +55,9 @@ exprt dead_object(const exprt &pointer, const namespacet &ns) // we check __CPROVER_dead_object! const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object"); - return same_object(pointer, deallocated_symbol.symbol_expr()); + return index_exprt{ + deallocated_symbol.symbol_expr(), + typecast_exprt::conditional_cast(pointer_object(pointer), index_type())}; } exprt good_pointer(const exprt &pointer)