Skip to content

Commit c7f7af4

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 4ae9bde commit c7f7af4

File tree

13 files changed

+59
-74
lines changed

13 files changed

+59
-74
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_ok9/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_ok9/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/analyses/goto_check_c.cpp

Lines changed: 4 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -2187,16 +2187,10 @@ void goto_check_ct::goto_check(
21872187
if(local_bitvector_analysis->dirty(variable))
21882188
{
21892189
// need to mark the dead variable as dead
2190-
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2191-
exprt address_of_expr = typecast_exprt::conditional_cast(
2192-
address_of_exprt(variable), lhs.type());
2193-
if_exprt rhs(
2194-
side_effect_expr_nondett(bool_typet(), i.source_location()),
2195-
std::move(address_of_expr),
2196-
lhs);
2190+
exprt lhs = dead_object(address_of_exprt{variable}, ns);
21972191
goto_programt::targett t =
21982192
new_code.add(goto_programt::make_assignment(
2199-
std::move(lhs), std::move(rhs), i.source_location()));
2193+
std::move(lhs), true_exprt{}, i.source_location()));
22002194
t->code_nonconst().add_source_location() = i.source_location();
22012195
}
22022196

@@ -2209,16 +2203,10 @@ void goto_check_ct::goto_check(
22092203
"return_value_alloca"))
22102204
{
22112205
// mark pointer to alloca result as dead
2212-
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
2213-
exprt alloca_result =
2214-
typecast_exprt::conditional_cast(variable, lhs.type());
2215-
if_exprt rhs(
2216-
side_effect_expr_nondett(bool_typet(), i.source_location()),
2217-
std::move(alloca_result),
2218-
lhs);
2206+
exprt lhs = dead_object(variable, ns);
22192207
goto_programt::targett t =
22202208
new_code.add(goto_programt::make_assignment(
2221-
std::move(lhs), std::move(rhs), i.source_location()));
2209+
std::move(lhs), true_exprt{}, i.source_location()));
22222210
t->code_nonconst().add_source_location() = i.source_location();
22232211
}
22242212
}

‎src/analyses/goto_check_java.cpp

Lines changed: 4 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1502,16 +1502,10 @@ void goto_check_javat::goto_check(
15021502
if(local_bitvector_analysis->dirty(variable))
15031503
{
15041504
// need to mark the dead variable as dead
1505-
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1506-
exprt address_of_expr = typecast_exprt::conditional_cast(
1507-
address_of_exprt(variable), lhs.type());
1508-
if_exprt rhs(
1509-
side_effect_expr_nondett(bool_typet(), i.source_location()),
1510-
std::move(address_of_expr),
1511-
lhs);
1505+
exprt lhs = dead_object(address_of_exprt{variable}, ns);
15121506
goto_programt::targett t =
15131507
new_code.add(goto_programt::make_assignment(
1514-
std::move(lhs), std::move(rhs), i.source_location()));
1508+
std::move(lhs), true_exprt{}, i.source_location()));
15151509
t->code_nonconst().add_source_location() = i.source_location();
15161510
}
15171511

@@ -1524,16 +1518,10 @@ void goto_check_javat::goto_check(
15241518
"return_value_alloca"))
15251519
{
15261520
// mark pointer to alloca result as dead
1527-
exprt lhs = ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
1528-
exprt alloca_result =
1529-
typecast_exprt::conditional_cast(variable, lhs.type());
1530-
if_exprt rhs(
1531-
side_effect_expr_nondett(bool_typet(), i.source_location()),
1532-
std::move(alloca_result),
1533-
lhs);
1521+
exprt lhs = dead_object(variable, ns);
15341522
goto_programt::targett t =
15351523
new_code.add(goto_programt::make_assignment(
1536-
std::move(lhs), std::move(rhs), i.source_location()));
1524+
std::move(lhs), true_exprt{}, i.source_location()));
15371525
t->code_nonconst().add_source_location() = i.source_location();
15381526
}
15391527
}

‎src/ansi-c/ansi_c_internal_additions.cpp

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

178178
// malloc
179-
"const void *" CPROVER_PREFIX "deallocated=0;\n"
180-
"const void *" CPROVER_PREFIX "dead_object=0;\n"
179+
CPROVER_PREFIX "bool " CPROVER_PREFIX "deallocated["
180+
CPROVER_PREFIX "constant_infinity_uint];\n"
181+
CPROVER_PREFIX "bool " CPROVER_PREFIX "dead_object["
182+
CPROVER_PREFIX "constant_infinity_uint];\n"
181183
"const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
182184
CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
183185
"const void *" CPROVER_PREFIX "memory_leak=0;\n"

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
typedef __typeof__(sizeof(int)) __CPROVER_size_t;
1313
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
14-
extern const void *__CPROVER_deallocated;
14+
extern _Bool __CPROVER_deallocated[];
1515
extern const void *__CPROVER_new_object;
1616
extern _Bool __CPROVER_malloc_is_new_array;
1717
extern const void *__CPROVER_memory_leak;

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

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

108-
// make sure it's not recorded as deallocated
109-
__CPROVER_deallocated =
110-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
111-
112108
// record the object size for non-determistic bounds checking
113109
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
114110
__CPROVER_malloc_is_new_array =
@@ -167,10 +163,6 @@ __CPROVER_HIDE:;
167163
void *malloc_res;
168164
malloc_res = __CPROVER_allocate(malloc_size, 0);
169165

170-
// make sure it's not recorded as deallocated
171-
__CPROVER_deallocated =
172-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
173-
174166
// record the object size for non-determistic bounds checking
175167
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
176168
__CPROVER_malloc_is_new_array =
@@ -198,9 +190,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
198190
void *res;
199191
res = __CPROVER_allocate(alloca_size, 0);
200192

201-
// make sure it's not recorded as deallocated
202-
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
203-
204193
// record the object size for non-determistic bounds checking
205194
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
206195
__CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
@@ -248,8 +237,9 @@ inline void free(void *ptr)
248237
"free argument has offset zero");
249238

250239
// catch double free
251-
__CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
252-
"double free");
240+
__CPROVER_precondition(
241+
ptr == 0 || !__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)],
242+
"double free");
253243

254244
// catch people who try to use free(...) for stuff
255245
// allocated with new[]
@@ -264,9 +254,7 @@ inline void free(void *ptr)
264254

265255
if(ptr!=0)
266256
{
267-
// non-deterministically record as deallocated
268-
__CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
269-
if(record) __CPROVER_deallocated=ptr;
257+
__CPROVER_deallocated[__CPROVER_POINTER_OBJECT(ptr)] = 1;
270258

271259
// detect memory leaks
272260
if(__CPROVER_memory_leak==ptr)

0 commit comments

Comments
 (0)