diff --git a/doc/cprover-manual/properties.md b/doc/cprover-manual/properties.md index 3014bf2a412..86348cda8ee 100644 --- a/doc/cprover-manual/properties.md +++ b/doc/cprover-manual/properties.md @@ -319,3 +319,19 @@ example, replacing functions or setting global variables with the `__CPROVER` prefix might make analysis impossible. To avoid doing this by accident, negative lookahead can be used. For example, `(?!__).*` matches all names not starting with `__`. + +### Malloc failure mode + +|Flag | Check | +|------------------------|-------------------------------------------------| +| `--malloc-fail-null` | in case malloc fails return NULL | +| `--malloc-fail-assert` | in case malloc fails report as failed property | + +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 +failures to occur. The option `--malloc-fail-null` results in `malloc` returning +the NULL pointer when failing. The option `--malloc-fail-assert` places +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. diff --git a/regression/cbmc/Pointer_byte_extract5/main.i b/regression/cbmc/Pointer_byte_extract5/main.i index 023e2197a8d..1d05e271a94 100644 --- a/regression/cbmc/Pointer_byte_extract5/main.i +++ b/regression/cbmc/Pointer_byte_extract5/main.i @@ -11,13 +11,15 @@ typedef union typedef struct { int Count; - Union List[1]; + // flexible array member -- note that smt conversion does not yet support + // 0-sized arrays + Union List[0]; } Struct3; #pragma pack(pop) int main() { - Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union)); + Struct3 *p = malloc(sizeof(Struct3) + 2 * sizeof(Union)); p->Count = 3; int po=0; diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc index 36c5519b60c..c10bb5f3a43 100644 --- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -1,14 +1,15 @@ -CORE +CORE broken-smt-backend main.i --bounds-check --32 --no-simplify ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 14 failed +\*\* 1 of 15 failed -- ^warning: ignoring -- Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c. C90 did not have flexible arrays, and using arrays of size 1 was common -practice: http://c-faq.com/struct/structhack.html. We need to treat those as if -it were a zero-sized array. +practice: http://c-faq.com/struct/structhack.html. But past C90 using +non-flexible members for struct-hack is undefined, hence we changed the test to +use flexible member instead. diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index 48d0d5d9c53..012bef91e2b 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -4,11 +4,12 @@ main.i ^EXIT=10$ ^SIGNAL=0$ array\.List dynamic object upper bound in p->List\[2\]: FAILURE -\*\* 1 of 11 failed +\*\* 1 of 13 failed -- ^warning: ignoring -- Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c. C90 did not have flexible arrays, and using arrays of size 1 was common -practice: http://c-faq.com/struct/structhack.html. We need to treat those as if -it were a zero-sized array. +practice: http://c-faq.com/struct/structhack.html. But past C90 using +non-flexible members for struct-hack is undefined, hence we changed the test to +use flexible member instead. diff --git a/regression/cbmc/array_constraints1/test.desc b/regression/cbmc/array_constraints1/test.desc index 8040e5651bf..cf0c9168734 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 14 +^\*\* 2 of 15 -- ^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/largest_representable.c b/regression/cbmc/malloc-too-large/largest_representable.c new file mode 100644 index 00000000000..17dd78a4cd8 --- /dev/null +++ b/regression/cbmc/malloc-too-large/largest_representable.c @@ -0,0 +1,10 @@ +#include +#include +#include + +int main() +{ + int *p = malloc(__CPROVER_max_malloc_size); // try to allocate exactly the max + + return 0; +} diff --git a/regression/cbmc/malloc-too-large/largest_representable.desc b/regression/cbmc/malloc-too-large/largest_representable.desc new file mode 100644 index 00000000000..d6f9fd63d14 --- /dev/null +++ b/regression/cbmc/malloc-too-large/largest_representable.desc @@ -0,0 +1,9 @@ +CORE +largest_representable.c +--malloc-fail-assert +^EXIT=0$ +^SIGNAL=0$ +^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/max_size.c b/regression/cbmc/malloc-too-large/max_size.c new file mode 100644 index 00000000000..b8a938db857 --- /dev/null +++ b/regression/cbmc/malloc-too-large/max_size.c @@ -0,0 +1,10 @@ +#include +#include +#include + +int main() +{ + int *p = malloc(SIZE_MAX); + + return 0; +} diff --git a/regression/cbmc/malloc-too-large/max_size.desc b/regression/cbmc/malloc-too-large/max_size.desc new file mode 100644 index 00000000000..783470072e3 --- /dev/null +++ b/regression/cbmc/malloc-too-large/max_size.desc @@ -0,0 +1,9 @@ +CORE +max_size.c +--malloc-fail-assert +^EXIT=10$ +^SIGNAL=0$ +^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/malloc-too-large/one_byte_too_large.c b/regression/cbmc/malloc-too-large/one_byte_too_large.c new file mode 100644 index 00000000000..68b571cfe5b --- /dev/null +++ b/regression/cbmc/malloc-too-large/one_byte_too_large.c @@ -0,0 +1,12 @@ +#include +#include +#include + +int main() +{ + // try to allocate the smallest violating amount + int *p = malloc(__CPROVER_max_malloc_size + 1); + assert(p); + + return 0; +} diff --git a/regression/cbmc/malloc-too-large/one_byte_too_large.desc b/regression/cbmc/malloc-too-large/one_byte_too_large.desc new file mode 100644 index 00000000000..dbec5e98957 --- /dev/null +++ b/regression/cbmc/malloc-too-large/one_byte_too_large.desc @@ -0,0 +1,9 @@ +CORE +one_byte_too_large.c +--malloc-fail-null +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc index 2055355d938..101b9e5bff4 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 11 failed +^\*\* 8 of 12 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 e50051dc10b..a768254dffe 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 10 failed +^\*\* 2 of 11 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 f7de54ad46b..0459ac52e6e 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, 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 47aea19e28b..d11810ba33b 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: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, 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 47aea19e28b..d11810ba33b 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: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, 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 47aea19e28b..d11810ba33b 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: 7, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 8, 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 a791723bfd2..66d94a757da 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: 12, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 13, 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 c605898b19d..05dbfa5fd90 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: 6, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 16, function calls: 2$ -- ^warning: ignoring diff --git a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc index 3b50b0169c0..cb67debb7ff 100644 --- a/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc +++ b/regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc @@ -1,6 +1,6 @@ CORE main.c -first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5 +first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5 ^SIGNAL=0$ ^EXIT=0$ VERIFICATION SUCCESSFUL diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 2f758239409..5be02100d99 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -155,6 +155,15 @@ 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="+ + std::to_string(config.ansi_c.malloc_failure_mode_return_null)+";\n" + "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="+ + std::to_string(1 << (config.ansi_c.pointer_width - + config.bv_encoding.object_bits - 1))+";\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 a070ca1302c..770be402ca0 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -16,6 +16,12 @@ 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; + +// malloc failure modes +extern int __CPROVER_malloc_failure_mode_return_null; +extern int __CPROVER_malloc_failure_mode_assert_then_assume; void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); void __CPROVER_assert(__CPROVER_bool assertion, const char *description); diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index d80ecd1264a..65a0c664732 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -115,23 +115,47 @@ inline void *malloc(__CPROVER_size_t malloc_size) // realistically, malloc may return NULL, // and __CPROVER_allocate doesn't, but no one cares __CPROVER_HIDE:; - 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; + if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_return_null) + { + 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); + } - // 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; + void *malloc_res; + malloc_res = __CPROVER_allocate(malloc_size, 0); - // detect memory leaks - __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool(); - __CPROVER_memory_leak=record_may_leak?malloc_res:__CPROVER_memory_leak; + // make sure it's not recorded as deallocated + __CPROVER_deallocated = + (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated; - return malloc_res; + // 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; + + return malloc_res; } /* FUNCTION: __builtin_alloca */ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index ec7968b5c70..586f47947da 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1067,6 +1067,9 @@ void cbmc_parse_optionst::help() " --error-label label check that label is unreachable\n" " --cover CC create test-suite with coverage criterion CC\n" // NOLINT(*) " --mm MM memory consistency model for concurrent programs\n" // NOLINT(*) + // 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" 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 8d5fba3737f..32edb0ed4a4 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -50,6 +50,7 @@ class optionst; "(object-bits):" \ OPT_GOTO_CHECK \ "(no-assertions)(no-assumptions)" \ + "(malloc-fail-assert)(malloc-fail-null)" \ 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 cac312f4a97..421f1f65511 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1093,6 +1093,16 @@ bool configt::set(const cmdlinet &cmdline) bv_encoding.is_object_bits_default = false; } + if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null")) + { + throw invalid_command_line_argument_exceptiont{ + "at most one malloc failure mode is acceptable", "--malloc-fail-null"}; + } + if(cmdline.isset("malloc-fail-null")) + ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_return_null; + if(cmdline.isset("malloc-fail-assert")) + ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume; + return false; } diff --git a/src/util/config.h b/src/util/config.h index 608bbbeaf98..b2f2354689b 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -130,6 +130,15 @@ class configt bool string_abstraction; + enum malloc_failure_modet + { + malloc_failure_mode_none = 0, + malloc_failure_mode_return_null = 1, + malloc_failure_mode_assert_then_assume = 2 + }; + + malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none; + static const std::size_t default_object_bits=8; } ansi_c;