generate-function-body creates goto binaries that can't be analysed

[polgreen]

I want to generate a function body for any function that currently has no body, and I want that body to havoc all params that it can havoc. Essentially I want to do what this PR did: #1585

I am running the command

goto-instrument --generate-function-body '.*' --generate-function-body-options 'havoc,params:.*' input.binary output.binary

The input binary is available here:
https://drive.google.com/open?id=1SD9qIH9e8l4KPP0TQgvDAEZNUWNL9oXd

Once the output binary is generated, I would like to run CBMC on that:

cbmc --unwind 1 --stop-on-fail --object-bits 16 output.binary --trace

This gives the violated invariant:

Invariant check failed
File ../util/std_types.h function to_struct_union_type line 282
Reason: Precondition

In order to debug this violated invariant, I would like to view the goto functions, so I run

goto-instrument --show-goto-functions output.binary

This generates the violated invariant:

File mode.cpp function get_language_from_identifier line 93
Reason: symbol `gcc_builtin_va_arg' has unknown mode ''

I am using CBMC from Michael's xen-combined branch, which is up to date with develop at 6a10f1a

[polgreen]

Possibly of interest to @hannes-steffenhagen-diffblue ?

[kroening]

There are now two PRs, which fix the two issues identified here:
PR #2734 fixes the issue of the missing mode for gcc_builtin_va_arg.
PR #2735 fixes the problem of assigning to a void-typed nondeterministic object.

However, it the "havoc params" has further problems: in the case of arrays, it relies on the user to provide the array size, which must be constant, as part of the parameter type. This is not usually the case. This problem could be fixed using the 'havoc' instruction, as done in PR #1585.

[polgreen]

I don't follow the final comment, do you mean to insert a havoc instruction so that, at symex time, goto_symext::havoc_rec is used? Instead of havoc_generate_function_bodiest::havoc_expr_rec?

The latter function seems to duplicate a lot of the former functionality?

I'm also not sure what the intention is with the latter function as far as objects containing pointers go, if an object contains a pointer to an object, what should it's behaviour be?

[polgreen]

I think there might be something wrong with the goto_symext::havoc_rec function; I have reused the implementation from PR #1585 but I get errors saying things like " assignment to `symbol' not handled".

I have also tried using the generate function bodies stuff now with the 2 fixes described above, and just not havocing any arrays of unknown size. It doesn't throw any errors but analysis of the resulting binary is slow compared to PR #1585. On an example binary:

PR #1585 takes 3.5s to analyse and produce a trace, running the following command:

time cbmc input.binary --stop-on-fail --object-bits 16 --trace --trace-show-function-calls --trace-show-code --trace-hex --no-sat-preprocessor --unwind 0 --havoc-undefined-functions

Using generate-function-bodies takes 59.28s to generate the bodies and then 75s to produce a trace. That's 38x slower.

time goto-instrument --generate-function-body '.*' --generate-function-body-options 'havoc,params:.*' input.binary tmp.binary
time cbmc tmp.binary --stop-on-fail --object-bits 16 --trace --trace-show-function-calls --trace-show-code --trace-hex --no-sat-preprocessor --unwind 0

Could we re-open the discussion about the best method for doing things with functions without bodies?

[polgreen]

Also, this issue is still not fixed for all cases. I have a binary where it still produces the error

Invariant check failed
File: ../util/std_types.h:282 function: to_struct_union_type
Condition: type.id()==ID_struct || type.id()==ID_union
Reason: Precondition

Input and output binaries here:
https://s3.amazonaws.com/cbmc-public-bucket/in.binary
https://s3.amazonaws.com/cbmc-public-bucket/out.binary