Skip to content

Commit 113bcdd

Browse files
tautschnigtautschnig
committed
Remove __CPROVER_malloc_object
Its use was deprecated since 2021-05-06. The only remaining need for tracking this object is to distinguish new vs new[] (and delete vs delete[]). This specific case is now handled via __CPROVER_new_object.
1 parent 8aab2e5 commit 113bcdd

File tree

16 files changed

+29
-88
lines changed

16 files changed

+29
-88
lines changed

‎doc/architectural/memory-bounds-checking.md

+4-14
Original file line numberDiff line numberDiff line change
@@ -30,19 +30,10 @@ inline void *malloc(__CPROVER_size_t malloc_size)
3030
{
3131
void *malloc_res;
3232
malloc_res = __CPROVER_allocate(malloc_size, 0);
33-
34-
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
35-
__CPROVER_malloc_object = record_malloc ? malloc_res : __CPROVER_malloc_object;
36-
3733
return malloc_res;
3834
}
3935
```
4036
41-
The internal variable `__CPROVER_malloc_object`
42-
is initialized to 0 in the `__CPROVER_initialize()` function of a goto program.
43-
The nondeterministic switch controls whether the address of the memory
44-
block allocated in this particular invocation of `malloc()` is recorded.
45-
4637
When the option `--pointer-check` is used, cbmc generates the following
4738
verification condition for each pointer dereference expression (e.g.,
4839
`*pointer`):
@@ -73,8 +64,7 @@ int main()
7364
```
7465

7566
Here the verification condition generated for the pointer dereference should
76-
fail. In the approach outlined above it indeed can, as one can choose true for
77-
`__VERIFIER_nondet___CPROVER_bool()` in the first call
78-
to `malloc()`, and false for `__VERIFIER_nondet___CPROVER_bool()` in the second
79-
call to `malloc()`. Thus, the object address of the first call to
80-
`malloc()` is recorded in `__CPROVER_malloc_object`.
67+
fail: for `p1` in `*p1`, `__CPROVER_POINTER_OFFSET` will evaluate to 1 (owing to
68+
the increment `p1++`, and `__CPROVER_OBJECT_SIZE` will also evaluate to 1.
69+
Consequently, the less-than comparison in the verification condition evaluates
70+
to false.

‎jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp

-14
Original file line numberDiff line numberDiff line change
@@ -36,20 +36,6 @@ void java_internal_additions(symbol_table_baset &dest)
3636
dest.add(symbol);
3737
}
3838

39-
// add __CPROVER_malloc_object
40-
41-
{
42-
symbolt symbol;
43-
symbol.base_name = CPROVER_PREFIX "malloc_object";
44-
symbol.name=CPROVER_PREFIX "malloc_object";
45-
symbol.type = pointer_type(java_void_type());
46-
symbol.mode=ID_C;
47-
symbol.is_lvalue=true;
48-
symbol.is_state_var=true;
49-
symbol.is_thread_local=true;
50-
dest.add(symbol);
51-
}
52-
5339
{
5440
auxiliary_symbolt symbol;
5541
symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;

‎regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[5\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[6\]
1111
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
12-
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
13-
__CPROVER_memory_leak \(\) -> TOP @ \[12\]
12+
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
13+
__CPROVER_new_object \(\) -> TOP @ \[12\]
1414
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
1515
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
1616
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]

‎regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[5\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[6\]
1111
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
12-
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
13-
__CPROVER_memory_leak \(\) -> TOP @ \[12\]
12+
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
13+
__CPROVER_new_object \(\) -> TOP @ \[12\]
1414
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
1515
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
1616
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]

‎regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ main#return_value \(\) -> TOP @ \[1\]
99
__CPROVER_dead_object \(\) -> TOP @ \[5\]
1010
__CPROVER_deallocated \(\) -> TOP @ \[6\]
1111
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
12-
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
13-
__CPROVER_memory_leak \(\) -> TOP @ \[12\]
12+
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
13+
__CPROVER_new_object \(\) -> TOP @ \[12\]
1414
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
1515
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
1616
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]

‎regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ __CPROVER_alloca_object \(\) -> TOP @ \[4\]
88
__CPROVER_dead_object \(\) -> TOP @ \[5\]
99
__CPROVER_deallocated \(\) -> TOP @ \[6\]
1010
__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
11-
__CPROVER_malloc_object \(\) -> TOP @ \[10\]
12-
__CPROVER_memory_leak \(\) -> TOP @ \[12\]
11+
__CPROVER_memory_leak \(\) -> TOP @ \[11\]
12+
__CPROVER_new_object \(\) -> TOP @ \[12\]
1313
__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
1414
__CPROVER_pipe_count \(\) -> 0u @ \[15\]
1515
__CPROVER_rounding_mode \(\) -> 0 @ \[16\]

‎src/analyses/escape_analysis.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ bool escape_domaint::is_tracked(const symbol_exprt &symbol)
1919
const irep_idt &identifier=symbol.get_identifier();
2020
if(
2121
identifier == CPROVER_PREFIX "memory_leak" ||
22-
identifier == CPROVER_PREFIX "malloc_object" ||
2322
identifier == CPROVER_PREFIX "dead_object" ||
2423
identifier == CPROVER_PREFIX "deallocated")
2524
{

‎src/ansi-c/ansi_c_internal_additions.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ void ansi_c_internal_additions(std::string &code)
178178
// malloc
179179
"const void *" CPROVER_PREFIX "deallocated=0;\n"
180180
"const void *" CPROVER_PREFIX "dead_object=0;\n"
181-
"const void *" CPROVER_PREFIX "malloc_object=0;\n"
181+
"const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
182182
CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
183183
"const void *" CPROVER_PREFIX "memory_leak=0;\n"
184184
"void *" CPROVER_PREFIX "allocate("

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
typedef __typeof__(sizeof(int)) __CPROVER_size_t;
1313
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
1414
extern const void *__CPROVER_deallocated;
15-
extern const void *__CPROVER_malloc_object;
15+
extern const void *__CPROVER_new_object;
1616
extern _Bool __CPROVER_malloc_is_new_array;
1717
extern const void *__CPROVER_memory_leak;
1818

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

+3-9
Original file line numberDiff line numberDiff line change
@@ -111,8 +111,6 @@ __CPROVER_HIDE:;
111111

112112
// record the object size for non-determistic bounds checking
113113
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
114-
__CPROVER_malloc_object =
115-
record_malloc ? malloc_res : __CPROVER_malloc_object;
116114
__CPROVER_malloc_is_new_array =
117115
record_malloc ? 0 : __CPROVER_malloc_is_new_array;
118116

@@ -175,8 +173,6 @@ __CPROVER_HIDE:;
175173

176174
// record the object size for non-determistic bounds checking
177175
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
178-
__CPROVER_malloc_object =
179-
record_malloc ? malloc_res : __CPROVER_malloc_object;
180176
__CPROVER_malloc_is_new_array =
181177
record_malloc ? 0 : __CPROVER_malloc_is_new_array;
182178

@@ -207,7 +203,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
207203

208204
// record the object size for non-determistic bounds checking
209205
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
210-
__CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
211206
__CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
212207

213208
// record alloca to detect invalid free
@@ -258,10 +253,9 @@ inline void free(void *ptr)
258253

259254
// catch people who try to use free(...) for stuff
260255
// allocated with new[]
261-
__CPROVER_precondition(ptr==0 ||
262-
__CPROVER_malloc_object!=ptr ||
263-
!__CPROVER_malloc_is_new_array,
264-
"free called for new[] object");
256+
__CPROVER_precondition(
257+
ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
258+
"free called for new[] object");
265259

266260
// catch people who try to use free(...) with alloca
267261
__CPROVER_precondition(

‎src/cpp/cpp_internal_additions.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ void cpp_internal_additions(std::ostream &out)
9090
// malloc
9191
out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
9292
out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
93-
out << "const void *" CPROVER_PREFIX "malloc_object = 0;" << '\n';
93+
out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n';
9494
out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
9595
<< '\n';
9696
out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';

‎src/cpp/library/cprover.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
typedef __typeof__(sizeof(int)) __CPROVER_size_t;
1414
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
1515
extern const void *__CPROVER_deallocated;
16-
extern const void *__CPROVER_malloc_object;
16+
extern const void *__CPROVER_new_object;
1717
extern _Bool __CPROVER_malloc_is_new_array;
1818
extern const void *__CPROVER_memory_leak;
1919

‎src/cpp/library/new.c

+10-12
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
1313
// ensure it's not recorded as deallocated
1414
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
1515

16-
// non-derministically record the object size for bounds checking
16+
// non-deterministically record the object for delete/delete[] checking
1717
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
18-
__CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
18+
__CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
1919
__CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
2020

2121
// detect memory leaks
@@ -40,9 +40,9 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
4040
// ensure it's not recorded as deallocated
4141
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
4242

43-
// non-deterministically record the object size for bounds checking
43+
// non-deterministically record the object for delete/delete[] checking
4444
__CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
45-
__CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
45+
__CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
4646
__CPROVER_malloc_is_new_array=record_malloc?1:__CPROVER_malloc_is_new_array;
4747

4848
// detect memory leaks
@@ -80,10 +80,9 @@ inline void __delete(void *ptr)
8080
__CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete");
8181

8282
// catch people who call delete for objects allocated with new[]
83-
__CPROVER_precondition(ptr==0 ||
84-
__CPROVER_malloc_object!=ptr ||
85-
!__CPROVER_malloc_is_new_array,
86-
"delete of array object");
83+
__CPROVER_precondition(
84+
ptr == 0 || __CPROVER_new_object != ptr || !__CPROVER_malloc_is_new_array,
85+
"delete of array object");
8786

8887
// If ptr is NULL, no operation is performed.
8988
// This is a requirement by the standard, not generosity!
@@ -120,10 +119,9 @@ inline void __delete_array(void *ptr)
120119
"double delete");
121120

122121
// catch people who call delete[] for objects allocated with new
123-
__CPROVER_precondition(ptr==0 ||
124-
__CPROVER_malloc_object!=ptr ||
125-
__CPROVER_malloc_is_new_array,
126-
"delete[] of non-array object");
122+
__CPROVER_precondition(
123+
ptr == 0 || __CPROVER_new_object != ptr || __CPROVER_malloc_is_new_array,
124+
"delete[] of non-array object");
127125

128126
if(ptr!=0)
129127
{

‎src/jsil/jsil_internal_additions.cpp

-16
Original file line numberDiff line numberDiff line change
@@ -39,22 +39,6 @@ void jsil_internal_additions(symbol_tablet &dest)
3939
dest.add(symbol);
4040
}
4141

42-
// add __CPROVER_malloc_object
43-
44-
{
45-
symbolt symbol;
46-
symbol.base_name = CPROVER_PREFIX "malloc_object";
47-
symbol.name=CPROVER_PREFIX "malloc_object";
48-
symbol.type=pointer_type(empty_typet());
49-
symbol.mode=ID_C;
50-
symbol.is_lvalue=true;
51-
symbol.is_state_var=true;
52-
symbol.is_thread_local=true;
53-
// mark as already typechecked
54-
symbol.is_extern=true;
55-
dest.add(symbol);
56-
}
57-
5842
// add eval
5943

6044
{

‎src/util/pointer_predicates.cpp

-8
Original file line numberDiff line numberDiff line change
@@ -40,14 +40,6 @@ exprt pointer_offset(const exprt &pointer)
4040
return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
4141
}
4242

43-
exprt malloc_object(const exprt &pointer, const namespacet &ns)
44-
{
45-
// we check __CPROVER_malloc_object!
46-
const symbolt &malloc_object_symbol=ns.lookup(CPROVER_PREFIX "malloc_object");
47-
48-
return same_object(pointer, malloc_object_symbol.symbol_expr());
49-
}
50-
5143
exprt deallocated(const exprt &pointer, const namespacet &ns)
5244
{
5345
// we check __CPROVER_deallocated!

‎src/util/pointer_predicates.h

-2
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,6 @@ exprt deallocated(const exprt &pointer, const namespacet &);
2222
exprt dead_object(const exprt &pointer, const namespacet &);
2323
exprt pointer_offset(const exprt &pointer);
2424
exprt pointer_object(const exprt &pointer);
25-
DEPRECATED(SINCE(2021, 5, 6, "Unnecessary, remove any use"))
26-
exprt malloc_object(const exprt &pointer, const namespacet &);
2725
exprt object_size(const exprt &pointer);
2826
DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
2927
exprt dynamic_object(const exprt &pointer);

0 commit comments

Comments
 (0)