Skip to content

Commit fb532e8

Browse files
tautschnigtautschnig
committed
Generalize ID_malloc to ID_allocate with optional zero-init
__CPROVER_allocate takes two arguments, where the second requests zero-initialization of the newly allocated object. Thus `calloc` can be implemented efficiently.
1 parent 3c47ccb commit fb532e8

32 files changed

+137
-72
lines changed

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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 9 additions & 0 deletions
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

Lines changed: 8 additions & 0 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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);

‎src/analyses/constant_propagator.cpp

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 4 additions & 4 deletions
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

Lines changed: 12 additions & 11 deletions
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 31 additions & 19 deletions
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

Lines changed: 2 additions & 1 deletion
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';

‎src/goto-programs/builtin_functions.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -580,8 +580,10 @@ void goto_convertt::do_java_new(
580580
CHECK_RETURN(object_size.is_not_nil());
581581

582582
// we produce a malloc side-effect, which stays
583-
side_effect_exprt malloc_expr(ID_malloc);
583+
side_effect_exprt malloc_expr(ID_allocate);
584584
malloc_expr.copy_to_operands(object_size);
585+
// could use true and get rid of the code below
586+
malloc_expr.copy_to_operands(false_exprt());
585587
malloc_expr.type()=rhs.type();
586588

587589
goto_programt::targett t_n=dest.add_instruction(ASSIGN);
@@ -618,8 +620,10 @@ void goto_convertt::do_java_new_array(
618620
CHECK_RETURN(!object_size.is_nil());
619621

620622
// we produce a malloc side-effect, which stays
621-
side_effect_exprt malloc_expr(ID_malloc);
623+
side_effect_exprt malloc_expr(ID_allocate);
622624
malloc_expr.copy_to_operands(object_size);
625+
// code use true and get rid of the code below
626+
malloc_expr.copy_to_operands(false_exprt());
623627
malloc_expr.type()=rhs.type();
624628

625629
goto_programt::targett t_n=dest.add_instruction(ASSIGN);

‎src/goto-programs/goto_convert.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -762,7 +762,7 @@ void goto_convertt::convert_assign(
762762
}
763763
else if(
764764
rhs.id() == ID_side_effect &&
765-
(rhs.get(ID_statement) == ID_malloc ||
765+
(rhs.get(ID_statement) == ID_allocate ||
766766
rhs.get(ID_statement) == ID_java_new_array_data))
767767
{
768768
// just preserve

‎src/goto-programs/goto_convert_side_effect.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -670,7 +670,7 @@ void goto_convertt::remove_side_effect(
670670
else if(statement==ID_cpp_delete ||
671671
statement==ID_cpp_delete_array)
672672
remove_cpp_delete(expr, dest, result_is_used);
673-
else if(statement==ID_malloc)
673+
else if(statement==ID_allocate)
674674
remove_malloc(expr, dest, result_is_used);
675675
else if(statement==ID_temporary_object)
676676
remove_temporary_object(expr, dest, result_is_used);

0 commit comments

Comments
 (0)