diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index 86348cda8ee..ba4e3110ee8 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -326,6 +326,7 @@ with `__`. |------------------------|-------------------------------------------------| | `--malloc-fail-null` | in case malloc fails return NULL | | `--malloc-fail-assert` | in case malloc fails report as failed property | +| `--malloc-may-fail` | malloc may non-deterministically fail | Calling `malloc` may fail for a number of reasons and the function may return a 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 verification is terminated (by `assume(false)`). One such property is that the allocated size is not too large, i.e. internally representable. When neither of those two options are used, CBMC will assume that `malloc` does not fail. + +Malloc may also fail for external reasons which are not modelled by CProver. If +you want to replicate this behaviour use the option `--malloc-may-fail` in +conjunction with one of the above modes of failure. diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index c10bb5f3a43..a0cd2a4ed2e 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 15 failed +\*\* 1 of 16 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 012bef91e2b..9416192f053 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -4,7 +4,7 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 13 failed +\*\* 1 of 14 failed -- ^warning: ignoring -- diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index cf0c9168734..9d4f5476bc3 100644 --- a/regression/cbmc/array_constraints1/test.desc +++ b/regression/cbmc/array_constraints1/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\*\* 2 of 15 +^\*\* 2 of 16 -- ^warning: ignoring diff --git a/regression/cbmc/malloc-may-fail/main.c b/regression/cbmc/malloc-may-fail/main.c new file mode 100644 index 00000000000..7c7de3e6ff6 --- /dev/null +++ b/regression/cbmc/malloc-may-fail/main.c @@ -0,0 +1,7 @@ +#include + +int main() +{ + char *p = malloc(100); + assert(p); // should fail, given the malloc-may-fail option +} diff --git a/regression/cbmc/malloc-may-fail/test.desc b/regression/cbmc/malloc-may-fail/test.desc new file mode 100644 index 00000000000..fb64c203397 --- /dev/null +++ b/regression/cbmc/malloc-may-fail/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--malloc-may-fail --malloc-fail-null +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/malloc-may-fail/test_without_option.desc b/regression/cbmc/malloc-may-fail/test_without_option.desc new file mode 100644 index 00000000000..f0c5e3ae1ef --- /dev/null +++ b/regression/cbmc/malloc-may-fail/test_without_option.desc @@ -0,0 +1,9 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ assertion p: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index 101b9e5bff4..c0f0033f690 100644 --- a/regression/cbmc/pointer-overflow1/test.desc +++ b/regression/cbmc/pointer-overflow1/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS ^VERIFICATION FAILED$ -^\*\* 8 of 12 failed +^\*\* 8 of 13 failed -- ^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE ^warning: ignoring diff --git a/regression/cbmc/r_w_ok1/test.desc b/regression/cbmc/r_w_ok1/test.desc index a768254dffe..6a461a6a137 100644 --- a/regression/cbmc/r_w_ok1/test.desc +++ b/regression/cbmc/r_w_ok1/test.desc @@ -2,7 +2,7 @@ CORE main.c __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$ -^\*\* 2 of 11 failed +^\*\* 2 of 12 failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 0459ac52e6e..04d1b4716c0 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 18, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index d11810ba33b..e315b641f52 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index d11810ba33b..e315b641f52 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index d11810ba33b..e315b641f52 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 9, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 17, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 66d94a757da..9d08d672a02 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 13, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 14, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index 05dbfa5fd90..ae3f57fbdf2 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$ ^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$ -- ^warning: ignoring diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 68486e49a23..cc6e04020ec 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -185,6 +185,7 @@ void ansi_c_internal_additions(std::string &code) "void *" CPROVER_PREFIX "allocate(" CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n" "const void *" CPROVER_PREFIX "alloca_object = 0;\n" + "int " CPROVER_PREFIX "malloc_failure_mode="+ std::to_string(config.ansi_c.malloc_failure_mode)+";\n" "int " CPROVER_PREFIX "malloc_failure_mode_return_null="+ @@ -192,8 +193,10 @@ void ansi_c_internal_additions(std::string &code) "int " CPROVER_PREFIX "malloc_failure_mode_assert_then_assume="+ std::to_string(config.ansi_c.malloc_failure_mode_assert_then_assume)+";\n" CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ - integer2string(max_malloc_size(config.ansi_c.pointer_width, config + integer2string(max_malloc_size(config.ansi_c.pointer_width, config .bv_encoding.object_bits))+";\n" + CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_may_fail = " + + std::to_string(config.ansi_c.malloc_may_fail) + ";\n" // this is ANSI-C "extern " CPROVER_PREFIX "thread_local const char __func__[" diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 770be402ca0..a0016e42ef9 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -16,8 +16,10 @@ extern const void *__CPROVER_malloc_object; extern __CPROVER_size_t __CPROVER_malloc_size; extern _Bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; + extern int __CPROVER_malloc_failure_mode; extern __CPROVER_size_t __CPROVER_max_malloc_size; +extern _Bool __CPROVER_malloc_may_fail; // malloc failure modes extern int __CPROVER_malloc_failure_mode_return_null; diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 65a0c664732..2bf24fdc654 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -75,6 +75,31 @@ __CPROVER_HIDE:; __CPROVER_size_t alloc_size = nmemb * size; #pragma CPROVER check pop + if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null) + { + __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); + if( + alloc_size > __CPROVER_max_malloc_size || + (__CPROVER_malloc_may_fail && should_malloc_fail)) + { + return (void *)0; + } + } + else if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_assert_then_assume) + { + __CPROVER_assert( + alloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded"); + __CPROVER_assume(alloc_size <= __CPROVER_max_malloc_size); + + __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_assert( + !__CPROVER_malloc_may_fail || !should_malloc_fail, + "max allocation may fail"); + __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail); + } + void *malloc_res; // realistically, calloc may return NULL, // and __CPROVER_allocate doesn't, but no one cares @@ -112,50 +137,55 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); inline void *malloc(__CPROVER_size_t malloc_size) { - // realistically, malloc may return NULL, - // and __CPROVER_allocate doesn't, but no one cares - __CPROVER_HIDE:; +// realistically, malloc may return NULL, +// but we only do so if `--malloc-may-fail` is set +__CPROVER_HIDE:; + if(__CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null) + { + __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); if( - __CPROVER_malloc_failure_mode == - __CPROVER_malloc_failure_mode_return_null) + malloc_size > __CPROVER_max_malloc_size || + (__CPROVER_malloc_may_fail && should_malloc_fail)) { - if(malloc_size > __CPROVER_max_malloc_size) - { - return (void *)0; - } - } - else if( - __CPROVER_malloc_failure_mode == - __CPROVER_malloc_failure_mode_assert_then_assume) - { - __CPROVER_assert( - malloc_size <= __CPROVER_max_malloc_size, - "max allocation size exceeded"); - __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size); + return (void *)0; } + } + else if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_assert_then_assume) + { + __CPROVER_assert( + malloc_size <= __CPROVER_max_malloc_size, "max allocation size exceeded"); + __CPROVER_assume(malloc_size <= __CPROVER_max_malloc_size); + + __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_assert( + !__CPROVER_malloc_may_fail || !should_malloc_fail, + "max allocation may fail"); + __CPROVER_assume(!__CPROVER_malloc_may_fail || !should_malloc_fail); + } - void *malloc_res; - malloc_res = __CPROVER_allocate(malloc_size, 0); + void *malloc_res; + malloc_res = __CPROVER_allocate(malloc_size, 0); - // make sure it's not recorded as deallocated - __CPROVER_deallocated = - (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated; + // make sure it's not recorded as deallocated + __CPROVER_deallocated = + (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated; - // record the object size for non-determistic bounds checking - __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); - __CPROVER_malloc_object = - record_malloc ? malloc_res : __CPROVER_malloc_object; - __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size; - __CPROVER_malloc_is_new_array = - record_malloc ? 0 : __CPROVER_malloc_is_new_array; + // record the object size for non-determistic bounds checking + __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_malloc_object = + record_malloc ? malloc_res : __CPROVER_malloc_object; + __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size; + __CPROVER_malloc_is_new_array = + record_malloc ? 0 : __CPROVER_malloc_is_new_array; - // detect memory leaks - __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); - __CPROVER_memory_leak = - record_may_leak ? malloc_res : __CPROVER_memory_leak; + // detect memory leaks + __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool(); + __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak; - return malloc_res; + return malloc_res; } /* FUNCTION: __builtin_alloca */ @@ -446,7 +476,8 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size) // this shouldn't move if the new size isn't bigger void *res; res=malloc(malloc_size); - __CPROVER_array_copy(res, ptr); + if(res != (void *)0) + __CPROVER_array_copy(res, ptr); free(ptr); return res; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7c6d23449d6..b547bd66214 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1076,6 +1076,8 @@ void cbmc_parse_optionst::help() // NOLINTNEXTLINE(whitespace/line_length) " --malloc-fail-assert set malloc failure mode to assert-then-assume\n" " --malloc-fail-null set malloc failure mode to return null\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --malloc-may-fail allow malloc calls to return a null pointer\n" HELP_REACHABILITY_SLICER HELP_REACHABILITY_SLICER_FB " --full-slice run full slicer (experimental)\n" // NOLINT(*) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index e16b68ba686..d5cc76e332e 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -52,6 +52,7 @@ class optionst; OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ "(malloc-fail-assert)(malloc-fail-null)" \ + "(malloc-may-fail)" \ OPT_XML_INTERFACE \ OPT_JSON_INTERFACE \ "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ diff --git a/src/util/config.cpp b/src/util/config.cpp index 421f1f65511..889b48b984e 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1103,6 +1103,8 @@ bool configt::set(const cmdlinet &cmdline) if(cmdline.isset("malloc-fail-assert")) ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume; + ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail"); + return false; } diff --git a/src/util/config.h b/src/util/config.h index b2f2354689b..19290cd3dbb 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -129,6 +129,7 @@ class configt libt lib; bool string_abstraction; + bool malloc_may_fail = false; enum malloc_failure_modet {