Add malloc-may-fail option to goto-check #5212

xbauch · 2020-01-07T10:08:24Z

And append an assert(false) property to every malloc call.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

xbauch · 2020-01-07T10:13:33Z

This may fix #4605.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: effdd30).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/143378007

codecov-io · 2020-01-07T11:21:58Z

Codecov Report

Merging #5212 into develop will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #5212   +/-   ##
========================================
  Coverage    68.19%   68.19%           
========================================
  Files         1176     1176           
  Lines        97516    97520    +4     
========================================
+ Hits         66501    66504    +3     
- Misses       31015    31016    +1

Flag	Coverage Δ
#cproversmt2	`42.73% <100.00%> (+<0.01%)`	⬆️
#regression	`65.37% <100.00%> (+<0.01%)`	⬆️
#unit	`32.24% <100.00%> (+<0.01%)`	⬆️

Impacted Files	Coverage Δ
src/cbmc/cbmc_parse_options.cpp	`76.99% <ø> (ø)`
src/cbmc/cbmc_parse_options.h	`100.00% <ø> (ø)`
src/util/config.h	`72.72% <ø> (ø)`
src/ansi-c/ansi_c_internal_additions.cpp	`94.36% <100.00%> (+0.16%)`	⬆️
src/util/config.cpp	`56.81% <100.00%> (+0.15%)`	⬆️
src/util/graph.h	`80.26% <0.00%> (-0.44%)`	⬇️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 7405bfb...d49cfdd. Read the comment docs.

martin-cs

Why not just change the model of what malloc does? That seems to keep all of the functionality in one place?

https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/stdlib.c#L113

Maybe it is time to change https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/stdlib.c#L115 specifically.

xbauch · 2020-01-13T15:41:29Z

Why not just change the model of what malloc does?

I think the reasoning here is to avoid "false-positive" alarms with every malloc call by default, and only to be correctly reporting the potential of malloc to fail if requested.

martin-cs · 2020-01-13T16:04:06Z

I think the reasoning here is to avoid "false-positive" alarms with every `malloc` call by default, and only to be correctly reporting the potential of malloc to fail if requested.

Then have a global as part of the model that allows it to be turned on / off / linked to a symbolic value during analysis. It doesn't have to be, and shouldn't be, hard-coded to one way or the other.

hannes-steffenhagen-diffblue · 2020-01-24T16:54:41Z

src/ansi-c/library/stdlib.c

-  // make sure it's not recorded as deallocated
-  __CPROVER_deallocated=(malloc_res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
+    __CPROVER_assert(
+      __CPROVER_malloc_may_fail == (__CPROVER_bool)0, "malloc may fail");


? Why is there an assert that this is false? I thought this would be more like if (__CPROVER_malloc_may_fail && __VERIFIER_nondet___CPROVER_bool()) return NULL;

Because conditionally returning NULL breaks too many things down the line in CBMC.

I take it back. Returning NULL seems to work here just fine.

src/ansi-c/library/stdlib.c

thk123 · 2020-01-29T10:37:47Z

regression/cbmc/Pointer_byte_extract5/main.i

@@ -11,13 +11,13 @@ typedef union
 typedef struct
 {
  int Count;
-  Union List[1];
+  Union List[0];


❓ Why does this change? The change should go in a separate commit with a why

This was undefined behaviour (and the changed in malloc exposed that CBMC does not really support that). It now has separate commit with explanation.

I find it rather surprising that the changes in this PR expose the lack of support for this C90-hack. What exactly was going wrong here?

Why this particular PR exposes the problem is a bit more complicated. But the problem itself can be easily reproduced, e.g. (CMBC reports the assertion as failing):

#include <malloc.h> #include <assert.h> struct Foo { int i; char data[1]; }; int main() { struct Foo* foo = malloc(sizeof(struct Foo) + sizeof(char)); foo->data[1]='b'; // set data[1] assert(foo->data[1]=='b'); // check data[1] -- should succeed return 0; }

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

regression/cbmc/Pointer_byte_extract5/test.desc

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

regression/goto-analyzer/constant_propagation_02/test.desc

src/cbmc/cbmc_parse_options.cpp

thk123 · 2020-01-29T10:42:13Z

src/cbmc/cbmc_parse_options.h

@@ -48,6 +48,7 @@ class optionst;
  "(document-subgoals)(outfile):(test-preprocessor)" \
  "D:I:(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
  "(object-bits):" \
+  "(malloc-may-fail)" \


❔ should this option be available in other C based tools, like goto-analyzer, or does that not really make sense?

Ambivalent.

thk123 · 2020-01-29T10:43:14Z

src/util/config.cpp

@@ -1093,6 +1093,11 @@ bool configt::set(const cmdlinet &cmdline)
    bv_encoding.is_object_bits_default = false;
  }

+  if(cmdline.isset("malloc-may-fail"))


⛏️ ?

Suggested change

if(cmdline.isset("malloc-may-fail"))

ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");

thk123 · 2020-01-29T16:27:31Z

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

+^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


⛏️ in future, we've found it helpful in test-gen to include a description explaining the purpose of the test below the line. for all tests. It helps when a test fails to understand why does it even exist. E.g

-- ^warning: ignoring -- Test that if --malloc-may-fail is enabled, that assert can return a null pointer

tautschnig

The changes to extend support to calloc, realloc need to happen before this can be merged. The modified regression test I'd not insist as much on, but still I'd like to see clarification.

tautschnig · 2020-02-04T22:10:51Z

src/ansi-c/library/stdlib.c

+  if(__CPROVER_malloc_may_fail && __VERIFIER_nondet___CPROVER_bool())
+    return (void *)0;


It may be more consistent to just declare a local, uninitialised variable of type __CPROVER_bool to avoid the side-effect of a function call.

The non-determinism also needs to be introduced in calloc.

realloc now needs to handle the case of a failing malloc.

Add 1. No can do: using uninitialised variables doesn't even compile with the current flag set. I can initialise it to nondet_bool.

2,3 are done.

tautschnig · 2020-02-04T22:14:04Z

regression/cbmc/Pointer_byte_extract5/main.i

@@ -11,13 +11,13 @@ typedef union
 typedef struct
 {
  int Count;
-  Union List[1];
+  Union List[0];


I find it rather surprising that the changes in this PR expose the lack of support for this C90-hack. What exactly was going wrong here?

tautschnig · 2020-02-04T22:14:52Z

src/cbmc/cbmc_parse_options.cpp

@@ -1041,6 +1041,7 @@ void cbmc_parse_optionst::help()
    "\n"
    "Backend options:\n"
    " --object-bits n              number of bits used for object addresses\n"
+    // NOLINTNEXTLINE(whitespace/line_length)


The commit message says "will be squashed" so presumably that should happen ;-)

martin-cs · 2020-02-06T13:48:08Z

There seems to be some duplication w.r.t. #5210 which is preferred?

chrisr-diffblue · 2020-02-19T14:40:50Z

@martin-cs I believe the difference between this PR and #5210 is around the behaviour they are modelling. #5210 is modelling the very specific case of what happens if the user code attempts to alloc a chunk of memory that is larger than CBMC can represent. Where as this PR is modelling the case where "the system" (e.g. OS) cannot satisfy a malloc request because of insufficient memory availability. This is a non-deterministic situation, so this PR models the situation where malloc may non-deterministically fail.

chrisr-diffblue

Looks pretty good, but would also be super nice if you could extend the user docs at the same time ;-)

chrisr-diffblue · 2020-02-19T14:44:25Z

src/cbmc/cbmc_parse_options.cpp

@@ -1041,6 +1041,8 @@ void cbmc_parse_optionst::help()
    "\n"
    "Backend options:\n"
    " --object-bits n              number of bits used for object addresses\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --malloc-may-fail            allow malloc calls to return a null pointer\n"


Similar to #5210, should this help message move up into the "Program instrumentation options" section?

Moved to the instrumentation section + the documentation was also added.

hannes-steffenhagen-diffblue

This should have an implementation for realloc as well, also I don’t think we should mix up the cases where malloc fails due to some nondeterministic condition and when it fails because we reach cprover internal limits.

hannes-steffenhagen-diffblue · 2020-03-02T14:57:01Z

src/ansi-c/library/stdlib.c

+
+    __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_assert(
+      !__CPROVER_malloc_may_fail || !should_malloc_fail,


I don’t think it makes a lot of sense to have the assertion here in this form, this will always fail the way it is written.

martin-cs

I like this approach a lot more than the previous one.

and hard-code appropriate check inside our `stdlib.c`. Plus some documentation and test.

using the same code as for malloc.

More assignments due to the `__CPROVER_malloc_may_fail` instantiations.

adding one more for the malloc failing.

allredj reviewed Jan 7, 2020

View reviewed changes

peterschrammel changed the title ~~Add malloc-may-fail option to goto-checker~~ Add malloc-may-fail option to goto-check Jan 7, 2020

martin-cs reviewed Jan 13, 2020

View reviewed changes

xbauch force-pushed the feature/malloc-may-fail branch 2 times, most recently from d97765e to 06ead45 Compare January 24, 2020 16:29

hannes-steffenhagen-diffblue reviewed Jan 24, 2020

View reviewed changes

xbauch force-pushed the feature/malloc-may-fail branch from 06ead45 to 993b47b Compare January 24, 2020 17:04

xbauch marked this pull request as ready for review January 24, 2020 20:31

xbauch requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners January 24, 2020 20:31

xbauch force-pushed the feature/malloc-may-fail branch 3 times, most recently from 4b6ce6d to 059cbc9 Compare January 28, 2020 08:05

thk123 reviewed Jan 29, 2020

View reviewed changes

xbauch force-pushed the feature/malloc-may-fail branch 3 times, most recently from b8f6035 to 043f0e0 Compare January 29, 2020 14:20

thk123 approved these changes Jan 29, 2020

View reviewed changes

smowton approved these changes Feb 4, 2020

View reviewed changes

tautschnig reviewed Feb 4, 2020

View reviewed changes

xbauch force-pushed the feature/malloc-may-fail branch from 6ea384f to f999d2f Compare February 5, 2020 10:50

xbauch requested a review from chrisr-diffblue as a code owner February 5, 2020 10:50

xbauch force-pushed the feature/malloc-may-fail branch from f999d2f to 241b666 Compare February 6, 2020 08:33

chrisr-diffblue reviewed Feb 19, 2020

View reviewed changes

xbauch force-pushed the feature/malloc-may-fail branch 3 times, most recently from 03cff3d to fec2e3a Compare February 27, 2020 13:36

xbauch added the do not merge label Feb 28, 2020

xbauch force-pushed the feature/malloc-may-fail branch 2 times, most recently from fec2e3a to 0f2f62f Compare February 28, 2020 09:21

hannes-steffenhagen-diffblue reviewed Mar 2, 2020

View reviewed changes

chrisr-diffblue approved these changes Jun 29, 2020

View reviewed changes

martin-cs approved these changes Jun 29, 2020

View reviewed changes

petr-bauch added 4 commits June 29, 2020 17:09

Add malloc-may-fail option to cbmc

bdd8b8a

and hard-code appropriate check inside our `stdlib.c`. Plus some documentation and test.

Calloc may fail

2b08c66

using the same code as for malloc.

Update the constant propagation tests

fbdd1ba

More assignments due to the `__CPROVER_malloc_may_fail` instantiations.

Update the number of test assertions

d49cfdd

adding one more for the malloc failing.

danpoe force-pushed the feature/malloc-may-fail branch from bc7894a to d49cfdd Compare June 29, 2020 16:10

danpoe merged commit 037e860 into diffblue:develop Jun 29, 2020

danpoe mentioned this pull request Jul 1, 2020

Rework memory allocation failure checks and options #5401

Open

5 tasks

	if(cmdline.isset("malloc-may-fail"))
	ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");

		if(__CPROVER_malloc_may_fail && __VERIFIER_nondet___CPROVER_bool())
		return (void *)0;

Add malloc-may-fail option to goto-check #5212

Add malloc-may-fail option to goto-check #5212

Uh oh!

Conversation

xbauch commented Jan 7, 2020

Uh oh!

xbauch commented Jan 7, 2020

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jan 7, 2020 • edited by codecov bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

xbauch commented Jan 13, 2020

Uh oh!

martin-cs commented Jan 13, 2020 via email

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs commented Feb 6, 2020

Uh oh!

chrisr-diffblue commented Feb 19, 2020

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

codecov-io commented Jan 7, 2020 •

edited by codecov bot

Loading