Skip to content

Commit ff4de42

Browse files
danpoedanpoe
committed
Simplify malloc models for allocation failures
1 parent 390b7c5 commit ff4de42

File tree

6 files changed

+33
-71
lines changed

6 files changed

+33
-71
lines changed

Diff for: ‎src/ansi-c/ansi_c_internal_additions.cpp

+4-8
Original file line numberDiff line numberDiff line change
@@ -186,17 +186,13 @@ void ansi_c_internal_additions(std::string &code)
186186
CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
187187
"const void *" CPROVER_PREFIX "alloca_object = 0;\n"
188188

189-
"int " CPROVER_PREFIX "malloc_failure_mode="+
190-
std::to_string(config.ansi_c.malloc_failure_mode)+";\n"
191-
"int " CPROVER_PREFIX "malloc_failure_mode_return_null="+
192-
std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n"
193-
"int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+
194-
std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n"
195189
CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
196190
integer2string(max_malloc_size(config.ansi_c.pointer_width, config
197191
.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"
192+
CPROVER_PREFIX "bool " CPROVER_PREFIX "allocate_may_fail = " +
193+
std::to_string(config.ansi_c.allocate_may_fail) + ";\n"
194+
CPROVER_PREFIX "bool " CPROVER_PREFIX "allocate_size_null = " +
195+
std::to_string(config.ansi_c.allocate_size_null) + ";\n"
200196

201197
// this is ANSI-C
202198
"extern " CPROVER_PREFIX "thread_local const char __func__["

Diff for: ‎src/ansi-c/library/stdlib.c

+10-40
Original file line numberDiff line numberDiff line change
@@ -75,29 +75,14 @@ __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)
78+
if(__CPROVER_allocate_size_null && alloc_size > __CPROVER_max_malloc_size)
7979
{
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-
}
80+
return (void *)0;
8781
}
88-
else if(
89-
__CPROVER_malloc_failure_mode ==
90-
__CPROVER_malloc_failure_mode_assert_then_assume)
82+
83+
if(__CPROVER_allocate_may_fail && __VERIFIER_nondet___CPROVER_bool())
9184
{
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);
85+
return (void *)0;
10186
}
10287

10388
void *malloc_res;
@@ -141,29 +126,14 @@ inline void *malloc(__CPROVER_size_t malloc_size)
141126
// but we only do so if `--malloc-may-fail` is set
142127
__CPROVER_HIDE:;
143128

144-
if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null)
129+
if(__CPROVER_allocate_size_null && malloc_size > __CPROVER_max_malloc_size)
145130
{
146-
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
147-
if(
148-
malloc_size > __CPROVER_max_malloc_size ||
149-
(__CPROVER_malloc_may_fail && should_malloc_fail))
150-
{
151-
return (void *)0;
152-
}
131+
return (void *)0;
153132
}
154-
else if(
155-
__CPROVER_malloc_failure_mode ==
156-
__CPROVER_malloc_failure_mode_assert_then_assume)
133+
134+
if(__CPROVER_allocate_may_fail && __VERIFIER_nondet___CPROVER_bool())
157135
{
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);
136+
return (void *)0;
167137
}
168138

169139
void *malloc_res;

Diff for: ‎src/cbmc/cbmc_parse_options.cpp

+6-5
Original file line numberDiff line numberDiff line change
@@ -1073,11 +1073,12 @@ void cbmc_parse_optionst::help()
10731073
" --error-label label check that label is unreachable\n"
10741074
" --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*)
10751075
" --mm MM memory consistency model for concurrent programs\n" // NOLINT(*)
1076-
// NOLINTNEXTLINE(whitespace/line_length)
1077-
" --malloc-fail-assert set malloc failure mode to assert-then-assume\n"
1078-
" --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"
1076+
<< help_entry(
1077+
"--overly-large-allocation-returns-null",
1078+
"memory allocation functions return null when more memory is allocated than can be addressed by cbmc") // NOLINT(*)
1079+
<< help_entry(
1080+
"--allocation-may-fail",
1081+
"allow memory allocation functions to return null") <<
10811082
HELP_REACHABILITY_SLICER
10821083
HELP_REACHABILITY_SLICER_FB
10831084
" --full-slice run full slicer (experimental)\n" // NOLINT(*)

Diff for: ‎src/cbmc/cbmc_parse_options.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,8 @@ class optionst;
5151
"(object-bits):" \
5252
OPT_GOTO_CHECK \
5353
"(no-assertions)(no-assumptions)" \
54-
"(malloc-fail-assert)(malloc-fail-null)" \
55-
"(malloc-may-fail)" \
54+
"(overly-large-allocation-returns-null)" \
55+
"(allocation-may-fail)" \
5656
OPT_XML_INTERFACE \
5757
OPT_JSON_INTERFACE \
5858
"(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \

Diff for: ‎src/util/config.cpp

+9-7
Original file line numberDiff line numberDiff line change
@@ -1093,17 +1093,19 @@ bool configt::set(const cmdlinet &cmdline)
10931093
bv_encoding.is_object_bits_default = false;
10941094
}
10951095

1096-
if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1096+
if(
1097+
cmdline.isset("overly-large-allocation-check") &&
1098+
cmdline.isset("overly-large-allocation-returns-null"))
10971099
{
10981100
throw invalid_command_line_argument_exceptiont{
1099-
"at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1101+
"only one of "
1102+
"--overly-large-allocation-check/--overly-large-allocation-returns-null "
1103+
"can be given at a time",
1104+
"--overly-large-allocation-check/--overly-large-allocation-returns-null"};
11001105
}
1101-
if(cmdline.isset("malloc-fail-null"))
1102-
ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null;
1103-
if(cmdline.isset("malloc-fail-assert"))
1104-
ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
11051106

1106-
ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
1107+
ansi_c.allocate_may_fail = cmdline.isset("allocation-may-fail");
1108+
ansi_c.allocate_size_null = cmdline.isset("overly-large-allocation-returns-null");
11071109

11081110
return false;
11091111
}

Diff for: ‎src/util/config.h

+2-9
Original file line numberDiff line numberDiff line change
@@ -129,16 +129,9 @@ class configt
129129
libt lib;
130130

131131
bool string_abstraction;
132-
bool malloc_may_fail = false;
133132

134-
enum malloc_failure_modet
135-
{
136-
malloc_failure_mode_none = 0,
137-
malloc_failure_mode_return_null = 1,
138-
malloc_failure_mode_assert_then_assume = 2
139-
};
140-
141-
malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
133+
bool allocate_may_fail = false;
134+
bool allocate_size_null = false;
142135

143136
static const std::size_t default_object_bits=8;
144137
} ansi_c;

0 commit comments

Comments
 (0)