Skip to content

Commit be59b58

Browse files
tautschnigtautschnig
committed
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.
1 parent bb08494 commit be59b58

File tree

14 files changed

+58
-63
lines changed

14 files changed

+58
-63
lines changed

‎regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
CORE broken-smt-backend
22
main.c
33
--smt2 --outfile -
4-
\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
4+
\(= \(select array_of\.\d+ i\) \(ite false #b1 #b0\)\)
55
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
66
\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
77
^EXIT=0$
88
^SIGNAL=0$
99
--
10-
\(= \(select array_of\.2 i\) false\)
10+
\(= \(select array_of\.\d+ i\) false\)
1111
\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
1212
\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
1313
--

‎regression/cbmc/pointer-extra-checks/test.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ main.c
1010
^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
1111
^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$
1212
^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$
13-
^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
1413
^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
1514
^\[main.pointer_dereference.10\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
1615
^\[main.pointer_dereference.11\] .* dereference failure: invalid integer address in \*s: FAILURE$

‎regression/cbmc/r_w_ok10/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <stdlib.h>
2+
3+
int main()
4+
{
5+
int *p = malloc(sizeof(int));
6+
free(p);
7+
__CPROVER_assume(__CPROVER_r_ok(p, sizeof(int)));
8+
__CPROVER_assert(0, "should be unreachable");
9+
}

‎regression/cbmc/r_w_ok10/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
4+
VERIFICATION SUCCESSFUL
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
This test checks that __CPROVER_r_ok can safely be used in assumptions.

‎regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
test.c
33
--malloc-may-fail --malloc-fail-null
4-
^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$
4+
^\[(free.precondition|main.precondition_instance).\d+] line \d+ double free: SUCCESS$
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$
77
^SIGNAL=0$

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -171,8 +171,10 @@ void ansi_c_internal_additions(std::string &code)
171171
CPROVER_PREFIX "constant_infinity_uint];\n"
172172

173173
// malloc
174-
"const void *" CPROVER_PREFIX "deallocated=0;\n"
175-
"const void *" CPROVER_PREFIX "dead_object=0;\n"
174+
CPROVER_PREFIX "bool " CPROVER_PREFIX "deallocated["
175+
CPROVER_PREFIX "constant_infinity_uint];\n"
176+
CPROVER_PREFIX "bool " CPROVER_PREFIX "dead_object["
177+
CPROVER_PREFIX "constant_infinity_uint];\n"
176178
"const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
177179
CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
178180
"const void *" CPROVER_PREFIX "memory_leak=0;\n"

‎src/ansi-c/goto_check_c.cpp

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2176,16 +2176,10 @@ void goto_check_ct::goto_check(
21762176
if(local_bitvector_analysis->dirty(variable))
21772177
{
21782178
// need to mark the dead variable as dead
2179-
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2180-
exprt address_of_expr = typecast_exprt::conditional_cast(
2181-
address_of_exprt(variable), lhs.type());
2182-
if_exprt rhs(
2183-
side_effect_expr_nondett(bool_typet(), i.source_location()),
2184-
std::move(address_of_expr),
2185-
lhs);
2179+
exprt lhs = dead_object(address_of_exprt{variable}, ns);
21862180
goto_programt::targett t =
21872181
new_code.add(goto_programt::make_assignment(
2188-
std::move(lhs), std::move(rhs), i.source_location()));
2182+
std::move(lhs), true_exprt{}, i.source_location()));
21892183
t->code_nonconst().add_source_location() = i.source_location();
21902184
}
21912185
}

‎src/ansi-c/library/cprover.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
1919
typedef signed long long __CPROVER_ssize_t;
2020

2121
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
22-
extern const void *__CPROVER_deallocated;
22+
extern _Bool __CPROVER_deallocated[];
2323
extern const void *__CPROVER_new_object;
2424
extern __CPROVER_bool __CPROVER_malloc_is_new_array;
2525
extern const void *__CPROVER_memory_leak;

‎src/ansi-c/library/mman.c

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -112,8 +112,7 @@ int munmap(void *addr, __CPROVER_size_t length)
112112
{
113113
(void)length;
114114

115-
if(__VERIFIER_nondet___CPROVER_bool())
116-
__CPROVER_deallocated = addr;
115+
__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(addr)] = 1;
117116

118117
return 0;
119118
}
@@ -126,8 +125,7 @@ int _munmap(void *addr, __CPROVER_size_t length)
126125
{
127126
(void)length;
128127

129-
if(__VERIFIER_nondet___CPROVER_bool())
130-
__CPROVER_deallocated = addr;
128+
__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(addr)] = 1;
131129

132130
return 0;
133131
}

‎src/ansi-c/library/stdlib.c

Lines changed: 4 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -112,10 +112,6 @@ __CPROVER_HIDE:;
112112
// and __CPROVER_allocate doesn't, but no one cares
113113
malloc_res = __CPROVER_allocate(alloc_size, 1);
114114

115-
// make sure it's not recorded as deallocated
116-
__CPROVER_deallocated =
117-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
118-
119115
// record the object size for non-determistic bounds checking
120116
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
121117
__CPROVER_malloc_is_new_array =
@@ -174,10 +170,6 @@ __CPROVER_HIDE:;
174170
void *malloc_res;
175171
malloc_res = __CPROVER_allocate(malloc_size, 0);
176172

177-
// make sure it's not recorded as deallocated
178-
__CPROVER_deallocated =
179-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
180-
181173
// record the object size for non-determistic bounds checking
182174
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
183175
__CPROVER_malloc_is_new_array =
@@ -205,9 +197,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
205197
void *res;
206198
res = __CPROVER_allocate(alloca_size, 0);
207199

208-
// make sure it's not recorded as deallocated
209-
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
210-
211200
// record the object size for non-determistic bounds checking
212201
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
213202
__CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
@@ -255,8 +244,9 @@ inline void free(void *ptr)
255244
"free argument has offset zero");
256245

257246
// catch double free
258-
__CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
259-
"double free");
247+
__CPROVER_precondition(
248+
ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)],
249+
"double free");
260250

261251
// catch people who try to use free(...) for stuff
262252
// allocated with new[]
@@ -271,9 +261,7 @@ inline void free(void *ptr)
271261

272262
if(ptr!=0)
273263
{
274-
// non-deterministically record as deallocated
275-
__CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
276-
if(record) __CPROVER_deallocated=ptr;
264+
__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)] = 1;
277265

278266
// detect memory leaks
279267
if(__CPROVER_memory_leak==ptr)

0 commit comments

Comments
 (0)