Havoc non det functions #1585

polgreen · 2017-11-13T18:56:53Z

CBMC currently assumes that functions with no body can return a non-deterministic value. This pull request extends that, to assume that functions with no body can also write a non-deterministic value to any non-const function arguments.

polgreen · 2017-11-23T15:16:30Z

Could this be reviewed please, again preferably by @kroening or @peterschrammel, because Michael has already reviewed this internally. Thanks

If function body does not exist, we assume that any pointers passed to function may be written to with a non-deterministic value, but only with something the size of the pointer type. regression test for havoc_undefined_functions

smowton

Should this also mess with reachable pointers? For example, if I passed a struct A { B* b }; could it mess with param->b->x, or just param->b? In the latter case this needs extra tests. Suggest also adding tests that exercise the things it should not do -- string constants, for example, I imagine should not be changed even if cast to (char*)?

polgreen · 2017-11-24T15:42:04Z

havoc-undefined-functions is really just a command line argument that applies an existing CBMC feature during analysis instead of it needing to be written into the source code of the program we are analysing before hand. The feature is: __CPROVER_havoc_object, which was introduced here, with regression testing:
beac327

I need to add another test to --havoc-undefined-functions that tests that we don't call havoc_rec() if the subtype is const.

The other questions are really questions about the behaviour of __CPROVER_havoc_object, so I'll try to speak to @kroening and when i'm sure what the semantics should be, extend the regression test in cbmc/ havoc_object1.

(although the answers from my quick testing are that (char*) string constant is not havoc'd and reachable pointers are not havoc'd, which matches what I think would be expected)

smowton · 2017-11-24T15:45:12Z

That sounds expected. I'd extend the test a little to check that behaviour -- the test will document what happens, if not necessarily what the original author intended :)

thk123

Looks very useful - I do wonder if there is some way of combining the code for havoc_rec (which I've not seen) and the code for generating nondet pointers for input, but almost certainly out of scope for this PR.

It would be good to add some tests for:

pointers to structs
pointers to structs that contain pointers
pointers to const values (to ensure they are not havoc'd)
const pointers to non-const values (to ensure they are)

thk123 · 2017-11-28T10:56:18Z

regression/cbmc/havoc_undefined_functions/test.desc

+--havoc-undefined-functions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$


Nit: missing empty line

thk123 · 2017-11-28T10:56:28Z

regression/cbmc/havoc_undefined_functions/main.c

+  function(&a);
+  __CPROVER_assert(a==0,"");
+  return 0;
+}


Nit: missing empty line

thk123 · 2017-11-28T10:57:38Z

src/cbmc/cbmc_parse_options.h

@@ -52,6 +52,7 @@ class optionst;
  "(show-symbol-table)(show-parse-tree)(show-vcc)" \
  "(show-claims)(claim):(show-properties)" \
  "(drop-unused-functions)" \
+  "(havoc-undefined-functions)" \


This seems like a super useful option in other binaries (such as goto-cc/goto-analzyer/goto-instrument), if you have time it'd be great to add it to them as well

This is done during symexing rather than by changing the goto-functions, so I can't very easily move this into goto-instrument, but it can be used for any binary that cbmc can analyse.

I don't really know what you would expect to be inserted into binaries, if it was to be part of goto-instrument, goto-analyze or goto-cc? It could replace the function body with __CPROVER_havoc(whatever the return values and pointer arguments are), but that is only meaningful if you are going to analyze the binary with cbmc afterwards.

smowton · 2017-12-03T12:48:30Z

One thing we should get an opinion on, probably from @kroening or @peterschrammel: CBMC currently produces interesting stub side effects by giving the GOTO functions bodies (for example, for Java they allocate a fresh object tree and optionally mess with parameters), and test gen does the same, while this uses an intrinsic that symex then interprets. It seems to me we should settle on one method or the other.

polgreen · 2017-12-03T13:02:51Z

Yes, although CBMC does already assign, during symexing, non-deterministic values to returns from undefined functions, so we already have two different methods without this PR. This is an extension of the existing behaviour during symexing, which is why I implemented it where it is

peterschrammel · 2017-12-03T13:37:45Z

There are at least four different things what to do with functions without bodies:

assume(false)
nondeterministic return value only, no side-effects (current default behaviour)
nondeterministic return value and side-effects
use summary

There should be a unified mechanism for choosing between these. Doing it through a goto-program transformation is the obvious candidate.

I suggest creating stub bodies for functions without bodies and filling the bodies with the required goto instructions dependent on the chosen function-without-body-replacement-action 1-4.
This would also seamlessly integrate with lazy loading, I think (replacement-action 0 "load/use actual body if available").

martin-cs · 2017-12-15T23:47:04Z

Although it is potentially quite a bit more work ... I agree with @peterschrammel on this one. There are similar issues with goto-analyze and I've been thinking that we need to tidy up the various different options and patches being used there. A properly unified solution would be even better. However I think there are more options than he outlined:

A. Effects on globals (ignore / non-det).
B. assert(false) (finding when the missing function actually matters).
C. Creating new objects (if returning (or modifying) pointers).
D. Ignore completely (assume(true))

polgreen · 2018-08-21T14:38:13Z

Can we reopen the discussion about the best way of dealing with functions without bodies? @peterschrammel @martin-cs

I appreciate the neatness of having a single solution that uses the goto program transformations, but it's just not quick enough for what I want to do, which is to use the aggressive slicer on Xen.

I have tried running the generate-function-bodies solution on the code that I am analysing, and the workflow is an order of magnitude slower (see issue #2663)

chrisr-diffblue · 2018-08-21T14:42:23Z

@hannes-steffenhagen-diffblue might want to be involved in the discussion too

polgreen · 2018-08-21T15:04:43Z

Good point. Although I assume he's being spammed by the issue thread anyway..!

TGWDB · 2021-08-05T10:49:23Z

Closing this PR on the basis that although there may have been ideas/discussion three years ago, there has been no action/progress since. Please reopen if you believe this is erroneous of will update this PR with new development.

polgreen requested review from kroening, peterschrammel and tautschnig as code owners November 13, 2017 18:56

polgreen mentioned this pull request Nov 14, 2017

Aggressive slicer #1587

Closed

polgreen force-pushed the havoc_non_det_functions branch from 88409fa to e1734af Compare November 24, 2017 12:17

polgreen requested review from cesaro, chrisr-diffblue, martin-cs, mgudemann, smowton and thk123 as code owners November 24, 2017 12:17

introduces --havoc-undefined-function

b9a5096

If function body does not exist, we assume that any pointers passed to function may be written to with a non-deterministic value, but only with something the size of the pointer type. regression test for havoc_undefined_functions

polgreen force-pushed the havoc_non_det_functions branch from e1734af to b9a5096 Compare November 24, 2017 12:19

smowton reviewed Nov 24, 2017

View reviewed changes

thk123 reviewed Nov 28, 2017

View reviewed changes

tautschnig assigned kroening, peterschrammel and polgreen Nov 30, 2017

martin-cs mentioned this pull request Dec 15, 2017

Block function command line option #1566

Closed

peterschrammel mentioned this pull request Jan 16, 2018

JBMC: Remove-returns per function #1730

Merged

tautschnig mentioned this pull request Feb 27, 2018

Add option to generate function body to goto-instrument #1889

Merged

tautschnig mentioned this pull request Apr 27, 2018

Lazy methods: allow driver program to provide stubs #2124

Merged

polgreen closed this Jun 20, 2018

polgreen mentioned this pull request Aug 2, 2018

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

Open

polgreen reopened this Aug 21, 2018

TGWDB closed this Aug 5, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Havoc non det functions #1585

Havoc non det functions #1585

polgreen commented Nov 13, 2017 •

edited

Loading

polgreen commented Nov 23, 2017

smowton left a comment

polgreen commented Nov 24, 2017

smowton commented Nov 24, 2017

thk123 left a comment

thk123 Nov 28, 2017

thk123 Nov 28, 2017

thk123 Nov 28, 2017

polgreen Dec 3, 2017

smowton commented Dec 3, 2017

polgreen commented Dec 3, 2017

peterschrammel commented Dec 3, 2017 •

edited

Loading

martin-cs commented Dec 15, 2017

polgreen commented Aug 21, 2018 •

edited

Loading

chrisr-diffblue commented Aug 21, 2018

polgreen commented Aug 21, 2018

TGWDB commented Aug 5, 2021

Havoc non det functions #1585

Havoc non det functions #1585

Conversation

polgreen commented Nov 13, 2017 • edited Loading

polgreen commented Nov 23, 2017

smowton left a comment

Choose a reason for hiding this comment

polgreen commented Nov 24, 2017

smowton commented Nov 24, 2017

thk123 left a comment

Choose a reason for hiding this comment

thk123 Nov 28, 2017

Choose a reason for hiding this comment

thk123 Nov 28, 2017

Choose a reason for hiding this comment

thk123 Nov 28, 2017

Choose a reason for hiding this comment

polgreen Dec 3, 2017

Choose a reason for hiding this comment

smowton commented Dec 3, 2017

polgreen commented Dec 3, 2017

peterschrammel commented Dec 3, 2017 • edited Loading

martin-cs commented Dec 15, 2017

polgreen commented Aug 21, 2018 • edited Loading

chrisr-diffblue commented Aug 21, 2018

polgreen commented Aug 21, 2018

TGWDB commented Aug 5, 2021

polgreen commented Nov 13, 2017 •

edited

Loading

peterschrammel commented Dec 3, 2017 •

edited

Loading

polgreen commented Aug 21, 2018 •

edited

Loading