Skip to content

Commit 2db8c45

Browse files
author
Daniel Kroening
authored
Merge pull request #982 from tautschnig/pointer-handling
Fixes and improvements to dynamic memory handling
2 parents 0361c2a + fb532e8 commit 2db8c45

36 files changed

+218
-93
lines changed

‎regression/cbmc-with-incr/Malloc17/main.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ unsigned char* init1()
44
if (size!=1) return 0;
55

66
assert(sizeof(unsigned char)==1);
7-
unsigned char* buffer=__CPROVER_malloc(1);
7+
unsigned char* buffer=__CPROVER_allocate(1, 0);
88
assert(buffer!=0);
99

1010
buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
1818
if (size!=1) return 0;
1919

2020
assert(sizeof(unsigned char)==1);
21-
unsigned char* buffer=__CPROVER_malloc(1*sizeof(unsigned char));
21+
unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
2222
assert(buffer!=0);
2323

2424
buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
3232
if (size!=1) return 0;
3333

3434
assert(sizeof(unsigned char)==1);
35-
unsigned char* buffer=__CPROVER_malloc(sizeof(unsigned char)*1);
35+
unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
3636
assert(buffer!=0);
3737

3838
buffer[0]=0;

‎regression/cbmc-with-incr/Malloc18/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ unsigned char* init()
44
if (size!=1) return 0;
55

66
assert(sizeof(unsigned char)==1);
7-
unsigned char* buffer=__CPROVER_malloc(size);
7+
unsigned char* buffer=__CPROVER_allocate(size, 0);
88
assert(buffer!=0);
99

1010
buffer[0]=0;

‎regression/cbmc-with-incr/Malloc19/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ int main()
2222
{
2323
// Create node
2424
struct node *nd;
25-
nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
25+
nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
2626

2727
// Link node
2828
struct list_head *hd = &(nd->linkage);

‎regression/cbmc/Calloc1/main.c

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <stdlib.h>
2+
#include <assert.h>
3+
4+
int main()
5+
{
6+
int *x=calloc(sizeof(int), 1);
7+
assert(*x==0);
8+
return 0;
9+
}

‎regression/cbmc/Calloc1/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc/Malloc17/main.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ unsigned char* init1()
44
if (size!=1) return 0;
55

66
assert(sizeof(unsigned char)==1);
7-
unsigned char* buffer=__CPROVER_malloc(1);
7+
unsigned char* buffer=__CPROVER_allocate(1, 0);
88
assert(buffer!=0);
99

1010
buffer[0]=0;
@@ -18,7 +18,7 @@ unsigned char* init2()
1818
if (size!=1) return 0;
1919

2020
assert(sizeof(unsigned char)==1);
21-
unsigned char* buffer=__CPROVER_malloc(1*sizeof(unsigned char));
21+
unsigned char* buffer=__CPROVER_allocate(1*sizeof(unsigned char), 0);
2222
assert(buffer!=0);
2323

2424
buffer[0]=0;
@@ -32,7 +32,7 @@ unsigned char* init3()
3232
if (size!=1) return 0;
3333

3434
assert(sizeof(unsigned char)==1);
35-
unsigned char* buffer=__CPROVER_malloc(sizeof(unsigned char)*1);
35+
unsigned char* buffer=__CPROVER_allocate(sizeof(unsigned char)*1, 0);
3636
assert(buffer!=0);
3737

3838
buffer[0]=0;

‎regression/cbmc/Malloc18/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ unsigned char* init()
33
unsigned long buffer_size;
44
if(buffer_size!=1) return 0;
55

6-
unsigned char* buffer=__CPROVER_malloc(buffer_size);
6+
unsigned char* buffer=__CPROVER_allocate(buffer_size, 0);
77
__CPROVER_assert(buffer!=0, "malloc did not return NULL");
88

99
buffer[0]=10;

‎regression/cbmc/Malloc19/main.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ int main()
2222
{
2323
// Create node
2424
struct node *nd;
25-
nd = (struct node *)__CPROVER_malloc(sizeof(struct node));
25+
nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
2626

2727
// Link node
2828
struct list_head *hd = &(nd->linkage);

‎regression/cbmc/Malloc24/main.c

+47
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
#include <stdlib.h>
2+
3+
struct node
4+
{
5+
int value;
6+
struct node *next;
7+
};
8+
9+
struct list
10+
{
11+
int size;
12+
struct node *head;
13+
};
14+
15+
void removeLast(struct list * l)
16+
{
17+
int index = l->size - 1;
18+
struct node **current;
19+
for(current = &(l->head); index && *current; index--)
20+
current = &(*current)->next;
21+
*current = (*current)->next;
22+
l->size--;
23+
}
24+
25+
int main () {
26+
//build a 2-nodes list
27+
struct node *n0 = malloc(sizeof(struct node));
28+
struct node *n1 = malloc(sizeof(struct node));
29+
struct list *l = malloc(sizeof(struct list));
30+
l->size = 2;
31+
l->head = n0;
32+
33+
n0->next=n1;
34+
n1->next=NULL;
35+
36+
//remove last node from list
37+
38+
//this passes
39+
// struct node **current = &(l->head);
40+
// current = &(*current)->next;
41+
// *current = (*current)->next;
42+
// l->size--;
43+
//this doesn't
44+
removeLast(l);
45+
46+
__CPROVER_assert(n0->next == NULL , "not NULL");
47+
}

‎regression/cbmc/Malloc24/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--unwind 4 --pointer-check --unwinding-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎src/analyses/constant_propagator.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -277,7 +277,7 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
277277
return false;
278278

279279
if(expr.id()==ID_side_effect &&
280-
to_side_effect_expr(expr).get_statement()==ID_malloc)
280+
to_side_effect_expr(expr).get_statement()==ID_allocate)
281281
return false;
282282

283283
if(expr.id()==ID_symbol)

‎src/analyses/local_bitvector_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
232232
const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
233233
const irep_idt &statement=side_effect_expr.get_statement();
234234

235-
if(statement==ID_malloc)
235+
if(statement==ID_allocate)
236236
return flagst::mk_dynamic_heap();
237237
else
238238
return flagst::mk_unknown();

‎src/analyses/local_may_alias.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ void local_may_aliast::get_rec(
298298
const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
299299
const irep_idt &statement=side_effect_expr.get_statement();
300300

301-
if(statement==ID_malloc)
301+
if(statement==ID_allocate)
302302
{
303303
dest.insert(objects.number(exprt(ID_dynamic_object)));
304304
}

‎src/ansi-c/ansi_c_internal_additions.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ void ansi_c_internal_additions(std::string &code)
160160
"void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n"
161161

162162
// malloc
163-
"void *__CPROVER_malloc(__CPROVER_size_t size);\n"
163+
"void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);\n"
164164
"const void *__CPROVER_deallocated=0;\n"
165165
"const void *__CPROVER_dead_object=0;\n"
166166
"const void *__CPROVER_malloc_object=0;\n"

‎src/ansi-c/c_typecheck_expr.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -2271,16 +2271,16 @@ exprt c_typecheck_baset::do_special_functions(
22712271

22722272
return abs_expr;
22732273
}
2274-
else if(identifier==CPROVER_PREFIX "malloc")
2274+
else if(identifier==CPROVER_PREFIX "allocate")
22752275
{
2276-
if(expr.arguments().size()!=1)
2276+
if(expr.arguments().size()!=2)
22772277
{
22782278
err_location(f_op);
2279-
error() << "malloc expects one operand" << eom;
2279+
error() << "allocate expects two operands" << eom;
22802280
throw 0;
22812281
}
22822282

2283-
exprt malloc_expr=side_effect_exprt(ID_malloc);
2283+
exprt malloc_expr=side_effect_exprt(ID_allocate);
22842284
malloc_expr.type()=expr.type();
22852285
malloc_expr.add_source_location()=source_location;
22862286
malloc_expr.operands()=expr.arguments();

‎src/ansi-c/expr2c.cpp

+12-11
Original file line numberDiff line numberDiff line change
@@ -1115,18 +1115,19 @@ std::string expr2ct::convert_pointer_object_has_type(
11151115
return dest;
11161116
}
11171117

1118-
std::string expr2ct::convert_malloc(
1119-
const exprt &src,
1120-
unsigned &precedence)
1118+
std::string expr2ct::convert_allocate(const exprt &src, unsigned &precedence)
11211119
{
1122-
if(src.operands().size()!=1)
1120+
if(src.operands().size() != 2)
11231121
return convert_norep(src, precedence);
11241122

11251123
unsigned p0;
1126-
std::string op0=convert_with_precedence(src.op0(), p0);
1124+
std::string op0 = convert_with_precedence(src.op0(), p0);
11271125

1128-
std::string dest="MALLOC";
1129-
dest+='(';
1126+
unsigned p1;
1127+
std::string op1 = convert_with_precedence(src.op1(), p1);
1128+
1129+
std::string dest = "ALLOCATE";
1130+
dest += '(';
11301131

11311132
if(src.type().id()==ID_pointer &&
11321133
src.type().subtype().id()!=ID_empty)
@@ -1135,8 +1136,8 @@ std::string expr2ct::convert_malloc(
11351136
dest+=", ";
11361137
}
11371138

1138-
dest+=op0;
1139-
dest+=')';
1139+
dest += op0 + ", " + op1;
1140+
dest += ')';
11401141

11411142
return dest;
11421143
}
@@ -3656,8 +3657,8 @@ std::string expr2ct::convert_with_precedence(
36563657
return
36573658
convert_side_effect_expr_function_call(
36583659
to_side_effect_expr_function_call(src), precedence);
3659-
else if(statement==ID_malloc)
3660-
return convert_malloc(src, precedence=15);
3660+
else if(statement == ID_allocate)
3661+
return convert_allocate(src, precedence = 15);
36613662
else if(statement==ID_printf)
36623663
return convert_function(src, "printf", precedence=16);
36633664
else if(statement==ID_nondet)

‎src/ansi-c/expr2c_class.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -214,7 +214,7 @@ class expr2ct
214214
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
215215
// NOLINTNEXTLINE(whitespace/line_length)
216216
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
217-
std::string convert_malloc(const exprt &src, unsigned &precedence);
217+
std::string convert_allocate(const exprt &src, unsigned &precedence);
218218
std::string convert_nondet(const exprt &src, unsigned &precedence);
219219
std::string convert_prob_coin(const exprt &src, unsigned &precedence);
220220
std::string convert_prob_uniform(const exprt &src, unsigned &precedence);

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
1010
#define CPROVER_ANSI_C_LIBRARY_CPROVER_H
1111

1212
typedef __typeof__(sizeof(int)) __CPROVER_size_t;
13-
void *__CPROVER_malloc(__CPROVER_size_t size);
13+
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
1414
extern const void *__CPROVER_deallocated;
1515
extern const void *__CPROVER_malloc_object;
1616
extern __CPROVER_size_t __CPROVER_malloc_size;

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
88
// This just does memory allocation.
99
__CPROVER_HIDE:;
1010
void *res;
11-
res=__CPROVER_malloc(malloc_size);
11+
res = __CPROVER_allocate(malloc_size, 0);
1212

1313
// ensure it's not recorded as deallocated
1414
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -36,7 +36,7 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
3636
// This just does memory allocation.
3737
__CPROVER_HIDE:;
3838
void *res;
39-
res=__CPROVER_malloc(size*count);
39+
res = __CPROVER_allocate(size*count, 0);
4040

4141
// ensure it's not recorded as deallocated
4242
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;

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

+31-19
Original file line numberDiff line numberDiff line change
@@ -60,27 +60,39 @@ inline void abort(void)
6060
/* FUNCTION: calloc */
6161

6262
#undef calloc
63-
#undef malloc
6463

65-
inline void *malloc(__CPROVER_size_t malloc_size);
64+
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
6665

6766
inline void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
6867
{
68+
// realistically, calloc may return NULL,
69+
// and __CPROVER_allocate doesn't, but no one cares
6970
__CPROVER_HIDE:;
70-
void *res;
71-
res=malloc(nmemb*size);
72-
#ifdef __CPROVER_STRING_ABSTRACTION
73-
__CPROVER_is_zero_string(res)=1;
74-
__CPROVER_zero_string_length(res)=0;
75-
//for(int i=0; i<nmemb*size; i++) res[i]=0;
76-
#else
77-
if(nmemb>1)
78-
__CPROVER_array_set(res, 0);
79-
else if(nmemb==1)
80-
for(__CPROVER_size_t i=0; i<size; ++i)
81-
((char*)res)[i]=0;
82-
#endif
83-
return res;
71+
void *malloc_res;
72+
malloc_res = __CPROVER_allocate(nmemb * size, 1);
73+
74+
// make sure it's not recorded as deallocated
75+
__CPROVER_deallocated =
76+
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
77+
78+
// record the object size for non-determistic bounds checking
79+
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
80+
__CPROVER_malloc_object =
81+
record_malloc ? malloc_res : __CPROVER_malloc_object;
82+
__CPROVER_malloc_size = record_malloc ? nmemb * size : __CPROVER_malloc_size;
83+
__CPROVER_malloc_is_new_array =
84+
record_malloc ? 0 : __CPROVER_malloc_is_new_array;
85+
86+
// detect memory leaks
87+
__CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
88+
__CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
89+
90+
#ifdef __CPROVER_STRING_ABSTRACTION
91+
__CPROVER_is_zero_string(malloc_res) = 1;
92+
__CPROVER_zero_string_length(malloc_res) = 0;
93+
#endif
94+
95+
return malloc_res;
8496
}
8597

8698
/* FUNCTION: malloc */
@@ -92,10 +104,10 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
92104
inline void *malloc(__CPROVER_size_t malloc_size)
93105
{
94106
// realistically, malloc may return NULL,
95-
// and __CPROVER_malloc doesn't, but no one cares
107+
// and __CPROVER_allocate doesn't, but no one cares
96108
__CPROVER_HIDE:;
97109
void *malloc_res;
98-
malloc_res=__CPROVER_malloc(malloc_size);
110+
malloc_res = __CPROVER_allocate(malloc_size, 0);
99111

100112
// make sure it's not recorded as deallocated
101113
__CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
@@ -121,7 +133,7 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
121133
{
122134
__CPROVER_HIDE:;
123135
void *res;
124-
res=__CPROVER_malloc(alloca_size);
136+
res = __CPROVER_allocate(alloca_size, 0);
125137

126138
// make sure it's not recorded as deallocated
127139
__CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;

‎src/cpp/cpp_internal_additions.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,8 @@ void cpp_internal_additions(std::ostream &out)
9191
out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
9292

9393
// malloc
94-
out << "extern \"C\" void *__CPROVER_malloc(__CPROVER::size_t size);" << '\n';
94+
out << "extern \"C\" void *__CPROVER_allocate(__CPROVER_size_t size,"
95+
<< " __CPROVER_bool zero);" << '\n';
9596
out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n';
9697
out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n';
9798
out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n';

0 commit comments

Comments
 (0)