Skip to content

Commit 037e860

Browse files
danpoedanpoe
authored
Merge pull request #5212 from xbauch/feature/malloc-may-fail
Add malloc-may-fail option to goto-check
2 parents 7405bfb + d49cfdd commit 037e860

File tree

22 files changed

+120
-48
lines changed

22 files changed

+120
-48
lines changed

‎doc/cprover-manual/properties.md

+5
Original file line numberDiff line numberDiff line change
@@ -326,6 +326,7 @@ with `__`.
326326
|------------------------|-------------------------------------------------|
327327
| `--malloc-fail-null` | in case malloc fails return NULL |
328328
| `--malloc-fail-assert` | in case malloc fails report as failed property |
329+
| `--malloc-may-fail` | malloc may non-deterministically fail |
329330

330331
Calling `malloc` may fail for a number of reasons and the function may return a
331332
NULL pointer. The users can choose if and how they want the `malloc`-related
@@ -335,3 +336,7 @@ additional properties inside `malloc` that are checked and if failing the
335336
verification is terminated (by `assume(false)`). One such property is that the
336337
allocated size is not too large, i.e. internally representable. When neither of
337338
those two options are used, CBMC will assume that `malloc` does not fail.
339+
340+
Malloc may also fail for external reasons which are not modelled by CProver. If
341+
you want to replicate this behaviour use the option `--malloc-may-fail` in
342+
conjunction with one of the above modes of failure.

‎regression/cbmc/Pointer_byte_extract5/no-simplify.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.i
44
^EXIT=10$
55
^SIGNAL=0$
66
array\.List dynamic object upper bound in p->List\[2\]: FAILURE
7-
\*\* 1 of 15 failed
7+
\*\* 1 of 16 failed
88
--
99
^warning: ignoring
1010
--

‎regression/cbmc/Pointer_byte_extract5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ main.i
44
^EXIT=10$
55
^SIGNAL=0$
66
array\.List dynamic object upper bound in p->List\[2\]: FAILURE
7-
\*\* 1 of 13 failed
7+
\*\* 1 of 14 failed
88
--
99
^warning: ignoring
1010
--

‎regression/cbmc/array_constraints1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
^\*\* 2 of 15
7+
^\*\* 2 of 16
88
--
99
^warning: ignoring

‎regression/cbmc/malloc-may-fail/main.c

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <stdlib.h>
2+
3+
int main()
4+
{
5+
char *p = malloc(100);
6+
assert(p); // should fail, given the malloc-may-fail option
7+
}

‎regression/cbmc/malloc-may-fail/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--malloc-may-fail --malloc-fail-null
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring

‎regression/cbmc/malloc-may-fail/test_without_option.desc

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

‎regression/cbmc/pointer-overflow1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^SIGNAL=0$
66
^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS
77
^VERIFICATION FAILED$
8-
^\*\* 8 of 12 failed
8+
^\*\* 8 of 13 failed
99
--
1010
^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
1111
^warning: ignoring

‎regression/cbmc/r_w_ok1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33

44
__CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
5-
^\*\* 2 of 11 failed
5+
^\*\* 2 of 12 failed
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/goto-analyzer/constant_propagation_01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
77
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
77
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_03/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
77
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_04/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$
77
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_07/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$
6+
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 14, function calls: 0$
77
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
88
--
99
^warning: ignoring

‎regression/goto-analyzer/constant_propagation_12/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--constants --simplify out.gb
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
6+
^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
77
^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$
88
--
99
^warning: ignoring

‎src/ansi-c/ansi_c_internal_additions.cpp

+4-1
Original file line numberDiff line numberDiff line change
@@ -185,15 +185,18 @@ void ansi_c_internal_additions(std::string &code)
185185
"void *" CPROVER_PREFIX "allocate("
186186
CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
187187
"const void *" CPROVER_PREFIX "alloca_object = 0;\n"
188+
188189
"int " CPROVER_PREFIX "malloc_failure_mode="+
189190
std::to_string(config.ansi_c.malloc_failure_mode)+";\n"
190191
"int " CPROVER_PREFIX "malloc_failure_mode_return_null="+
191192
std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n"
192193
"int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+
193194
std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n"
194195
CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
195-
integer2string(max_malloc_size(config.ansi_c.pointer_width, config
196+
integer2string(max_malloc_size(config.ansi_c.pointer_width, config
196197
.bv_encoding.object_bits))+";\n"
198+
CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " +
199+
std::to_string(config.ansi_c.malloc_may_fail) + ";\n"
197200

198201
// this is ANSI-C
199202
"extern " CPROVER_PREFIX "thread_local const char __func__["

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

+2
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,10 @@ extern const void *__CPROVER_malloc_object;
1616
extern __CPROVER_size_t __CPROVER_malloc_size;
1717
extern _Bool __CPROVER_malloc_is_new_array;
1818
extern const void *__CPROVER_memory_leak;
19+
1920
extern int __CPROVER_malloc_failure_mode;
2021
extern __CPROVER_size_t __CPROVER_max_malloc_size;
22+
extern _Bool __CPROVER_malloc_may_fail;
2123

2224
// malloc failure modes
2325
extern int __CPROVER_malloc_failure_mode_return_null;

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

+67-36
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,31 @@ __CPROVER_HIDE:;
7575
__CPROVER_size_t alloc_size = nmemb * size;
7676
#pragma CPROVER check pop
7777

78+
if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
79+
{
80+
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
81+
if(
82+
alloc_size > __CPROVER_max_malloc_size ||
83+
(__CPROVER_malloc_may_fail && should_malloc_fail))
84+
{
85+
return (void *)0;
86+
}
87+
}
88+
else if(
89+
__CPROVER_malloc_failure_mode ==
90+
__CPROVER_malloc_failure_mode_assert_then_assume)
91+
{
92+
__CPROVER_assert(
93+
alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
94+
__CPROVER_assume(alloc_size <= __CPROVER_max_malloc_size);
95+
96+
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
97+
__CPROVER_assert(
98+
!__CPROVER_malloc_may_fail || !should_malloc_fail,
99+
"max allocation may fail");
100+
__CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
101+
}
102+
78103
void *malloc_res;
79104
// realistically, calloc may return NULL,
80105
// and __CPROVER_allocate doesn't, but no one cares
@@ -112,50 +137,55 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
112137

113138
inline void *malloc(__CPROVER_size_t malloc_size)
114139
{
115-
// realistically, malloc may return NULL,
116-
// and __CPROVER_allocate doesn't, but no one cares
117-
__CPROVER_HIDE:;
140+
// realistically, malloc may return NULL,
141+
// but we only do so if `--malloc-may-fail` is set
142+
__CPROVER_HIDE:;
118143

144+
if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
145+
{
146+
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
119147
if(
120-
__CPROVER_malloc_failure_mode ==
121-
__CPROVER_malloc_failure_mode_return_null)
148+
malloc_size > __CPROVER_max_malloc_size ||
149+
(__CPROVER_malloc_may_fail && should_malloc_fail))
122150
{
123-
if(malloc_size > __CPROVER_max_malloc_size)
124-
{
125-
return (void *)0;
126-
}
127-
}
128-
else if(
129-
__CPROVER_malloc_failure_mode ==
130-
__CPROVER_malloc_failure_mode_assert_then_assume)
131-
{
132-
__CPROVER_assert(
133-
malloc_size <= __CPROVER_max_malloc_size,
134-
"max allocation size exceeded");
135-
__CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
151+
return (void *)0;
136152
}
153+
}
154+
else if(
155+
__CPROVER_malloc_failure_mode ==
156+
__CPROVER_malloc_failure_mode_assert_then_assume)
157+
{
158+
__CPROVER_assert(
159+
malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded");
160+
__CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size);
161+
162+
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
163+
__CPROVER_assert(
164+
!__CPROVER_malloc_may_fail || !should_malloc_fail,
165+
"max allocation may fail");
166+
__CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail);
167+
}
137168

138-
void *malloc_res;
139-
malloc_res = __CPROVER_allocate(malloc_size, 0);
169+
void *malloc_res;
170+
malloc_res = __CPROVER_allocate(malloc_size, 0);
140171

141-
// make sure it's not recorded as deallocated
142-
__CPROVER_deallocated =
143-
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
172+
// make sure it's not recorded as deallocated
173+
__CPROVER_deallocated =
174+
(malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
144175

145-
// record the object size for non-determistic bounds checking
146-
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
147-
__CPROVER_malloc_object =
148-
record_malloc ? malloc_res : __CPROVER_malloc_object;
149-
__CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size;
150-
__CPROVER_malloc_is_new_array =
151-
record_malloc ? 0 : __CPROVER_malloc_is_new_array;
176+
// record the object size for non-determistic bounds checking
177+
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
178+
__CPROVER_malloc_object =
179+
record_malloc ? malloc_res : __CPROVER_malloc_object;
180+
__CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size;
181+
__CPROVER_malloc_is_new_array =
182+
record_malloc ? 0 : __CPROVER_malloc_is_new_array;
152183

153-
// detect memory leaks
154-
__CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
155-
__CPROVER_memory_leak =
156-
record_may_leak ? malloc_res : __CPROVER_memory_leak;
184+
// detect memory leaks
185+
__CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
186+
__CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
157187

158-
return malloc_res;
188+
return malloc_res;
159189
}
160190

161191
/* FUNCTION: __builtin_alloca */
@@ -446,7 +476,8 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
446476
// this shouldn't move if the new size isn't bigger
447477
void *res;
448478
res=malloc(malloc_size);
449-
__CPROVER_array_copy(res, ptr);
479+
if(res != (void *)0)
480+
__CPROVER_array_copy(res, ptr);
450481
free(ptr);
451482

452483
return res;

‎src/cbmc/cbmc_parse_options.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -1076,6 +1076,8 @@ void cbmc_parse_optionst::help()
10761076
// NOLINTNEXTLINE(whitespace/line_length)
10771077
" --malloc-fail-assert set malloc failure mode to assert-then-assume\n"
10781078
" --malloc-fail-null set malloc failure mode to return null\n"
1079+
// NOLINTNEXTLINE(whitespace/line_length)
1080+
" --malloc-may-fail allow malloc calls to return a null pointer\n"
10791081
HELP_REACHABILITY_SLICER
10801082
HELP_REACHABILITY_SLICER_FB
10811083
" --full-slice run full slicer (experimental)\n" // NOLINT(*)

‎src/cbmc/cbmc_parse_options.h

+1
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ class optionst;
5252
OPT_GOTO_CHECK \
5353
"(no-assertions)(no-assumptions)" \
5454
"(malloc-fail-assert)(malloc-fail-null)" \
55+
"(malloc-may-fail)" \
5556
OPT_XML_INTERFACE \
5657
OPT_JSON_INTERFACE \
5758
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \

‎src/util/config.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -1103,6 +1103,8 @@ bool configt::set(const cmdlinet &cmdline)
11031103
if(cmdline.isset("malloc-fail-assert"))
11041104
ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
11051105

1106+
ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
1107+
11061108
return false;
11071109
}
11081110

‎src/util/config.h

+1
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,7 @@ class configt
129129
libt lib;
130130

131131
bool string_abstraction;
132+
bool malloc_may_fail = false;
132133

133134
enum malloc_failure_modet
134135
{

0 commit comments

Comments
 (0)