goto-cc incompatible with cbmc's --malloc-may-fail and --malloc-fail-null

[SaswatPadhi]

CBMC version: 5.13.0
Operating system: Linux 64-bit

Minimal example:

#include <assert.h>
#include <stdlib.h>

int main (void) {
  int*p = malloc(sizeof(*p));
  assert(p);
  return 0;
}

cbmc --malloc-may-fail --malloc-fail-null test.c correctly detects a bug in this .c file.
When we run goto-cc test.c -o test.goto, and then run cbmc --malloc-may-fail --malloc-fail-null test.goto, cbmc incorrectly reports successful verification.

Currently, goto-cc does not accept these two malloc flags, so we cannot add them to the goto-cc invocation.

What behaviour did you expect:

$ cbmc --malloc-may-fail --malloc-fail-null test.c
CBMC version 5.13.0 (cbmc-5.13.1) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 89 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
324 variables, 48 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.0016344s

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

test.c function main
[main.assertion.1] line 6 assertion p: FAILURE

** 1 of 3 failed (2 iterations)
VERIFICATION FAILED

What happened instead:

$ goto-cc test.c -o test.goto; cbmc --malloc-may-fail --malloc-fail-null test.goto
CBMC version 5.13.0 (cbmc-5.13.1) 64-bit x86_64 linux
Reading GOTO program from file
Reading: test.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
file <built-in-additions> line 21: warning: conflicting initializers for variable "__CPROVER_malloc_failure_mode"
using old value in module test file <built-in-additions> line 21
0
ignoring new value in module <built-in-library> file <built-in-additions> line 21
1
file <built-in-additions> line 25: warning: conflicting initializers for variable "__CPROVER_malloc_may_fail"
using old value in module test file <built-in-additions> line 25
FALSE
ignoring new value in module <built-in-library> file <built-in-additions> line 25
TRUE
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
size of program expression: 76 steps
simple slicing removed 0 assignments
Generated 1 VCC(s), 0 remaining after simplification

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

test.c function main
[main.assertion.1] line 6 assertion p: SUCCESS

** 0 of 3 failed (1 iterations)
VERIFICATION SUCCESSFUL

[SaswatPadhi]

cc: @danielsn @markrtuttle

[martin-cs]

FWIW I would not expect --malloc-may-fail and --malloc-fail-null to be supported by goto-cc. They are analysis flags and goto-cc's job should just be compilation.

Also paging @danpoe re: #5401

[martin-cs]

I'm not sure how this effects the "implemented as a transform" vs. "implemented as a library" debate.

[hannes-steffenhagen-diffblue]

I am not sure why this is needed given you can just pass these flags to cbmc, since they only affect how the internal library works there should be no reason to want these at goto-cc time. As Martin said @danpoe had an idea of how to do these in a different way (or at least he did for the size checks, not sure if there's really much else we can do for the null case except for instrumenting the code elsewhere like martin suggests).

[SaswatPadhi]

We generate the .goto file, do some transformations on it, and run the transformed file on cbmc.

Is there any way we could capture the intermediate .goto file generated by cbmc instead of calling goto-cc (so we can apply our transformations on it and rerun it on cbmc)?

[martin-cs]

goto-cc is C front-end and conversion to goto-programs.
goto-instrument is transforms to and from goto-programs.
cbmc is C front-end, conversion to goto-programs, some of the simple transforms and the the BMC back-end.

goto-cc is how you capture the intermediate goto program and goto-instrument is how you transform it. All of the transforms that cbmc supports should also be in goto-instrument. How is the goto program generated by cbmc different to the one generated by goto-cc?

[SaswatPadhi]

Thanks @martin-cs.
In this case, the goto program generated by goto-cc does not have the right instrumentation for --malloc-may-fail and --malloc-fail-null.

So I was wondering if we could capture the goto program after cbmc has performed the standard transforms as per the given flags, then we could apply our transforms on the goto program and rerun cbmc.

[hannes-steffenhagen-diffblue]

What kind of instrumentation are you doing? Off the top of my head I'd say it's probably not a good idea to modify the function bodies of the internal C library, which is really the only sort of instrumentation I can think of that wouldn't be possible this way.

[martin-cs]

@SaswatPadhi In which case, this incompatibility is what needs to be fixed, not changing the workflow.

@hannes-steffenhagen-diffblue / @danpoe who implemented --malloc-may-fail and --malloc-fail-null ? I can't see why these can't be part of the model for malloc and why they need separate instrumentation.

[hannes-steffenhagen-diffblue]

@martin-cs they're part of the model for malloc. All these flags are doing is setting __CPROVER_malloc_failure_mode to different values in __CPROVER_initialise, and malloc just contains code like

if(__CPROVER_malloc_failure_mode == {something}) {
  // blah
} else if(...) {
...
}

(There's currently also __CPROVER_malloc_failure_mode_assert_then_assume, which from what I can tell is essentially doing nonsense, this is the thing @danpoe wanted to fix but he's currently not actively working on cbmc anymore).

[martin-cs]

@hannes-steffenhagen-diffblue Thanks; please forgive my misunderstanding. That is, IMHO, the right way to do things.

In which case is it just that the initialisation code that goto-cc generates when linking is missing the right globals?

[danielsn]

@martin-cs: I think the issue is related to the one that occurred here #5272 - goto-cc sets default values for the globals, which cbmc doesn't override.

[martin-cs]

That would sound believable. Regenerating the initialisation code should be sufficient to fix this.