Generate function bodies that nondet havoc the function arguments [blocks: #3457] #3455

danpoe · 2018-11-22T14:17:28Z

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).
n/a 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.

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: a9ba6ac).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92410007
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

chrisr-diffblue · 2018-11-29T17:20:58Z

Needs a rebase on top of #3443 by the looks of it - 3443 has 4 commits, only the top 5 commits of this branch should be reviewed according to the description of this PR - yet this PR has 23 commits :-)

allredj

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

…ation-from-object-factories Factor out object allocation from object factories [blocks: #3455]

allredj

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 19e3122).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95290559
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

tautschnig

My main technical issue is the dependency on ansi-c being introduced, which seems wrong. Otherwise I found reviewing pretty hard, because the commit messages didn't really provide sufficient information. Could both of these please be fixed?

tautschnig · 2018-12-21T10:54:38Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1185,6 +1185,19 @@ void goto_instrument_parse_optionst::instrument_goto_program()
    remove_skip(goto_model);
  }

+  if(cmdline.isset("generate-function-body"))


Could you please explain the "Why?" in the commit message?

regression/goto-instrument/generate-function-body-havoc-params-simple/test.desc

tautschnig · 2018-12-21T10:56:42Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <memory>

+#include <ansi-c/c_object_factory_parameters.h>


Please move this a few lines down, with the other ansi-c include.

tautschnig · 2018-12-21T10:57:59Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1187,8 +1189,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()

  if(cmdline.isset("generate-function-body"))
  {
+    optionst options;


Please use a different name, this shadows the existing options object in this method.

tautschnig · 2018-12-21T10:58:27Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1187,8 +1189,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()

  if(cmdline.isset("generate-function-body"))
  {
+    optionst options;
+    parse_c_object_factory_options(cmdline, options);
+    c_object_factory_parameterst object_factory_parameters(options);


Do we know for sure that the "C" object factory is the right one?

The function body generation is currently hardcoded to use the c_nondet_symbol_factory. I'm not sure at this point how difficult it would be to also make it work with the java object factory. I'd rather have this PR only include the C feature for now.

tautschnig · 2018-12-21T10:59:04Z

src/goto-instrument/goto_instrument_parse_options.h

@@ -104,6 +104,8 @@ Author: Daniel Kroening, [email protected]
  OPT_REPLACE_CALLS \
  "(validate-goto-binary)" \
  OPT_VALIDATE \
+  "(max-nondet-tree-depth):" \
+  "(min-null-tree-depth):" \


Don't we have/shouldn't we have some OPT_... for those?

src/goto-programs/generate_function_bodies.cpp

tautschnig · 2018-12-21T11:01:56Z

src/ansi-c/ansi_c_entry_point.cpp

@@ -42,7 +42,8 @@ exprt::operandst build_function_environment(
      base_name,
      p.type(),
      p.source_location(),
-      object_factory_parameters);
+      object_factory_parameters,
+      lifetimet::AUTOMATIC_LOCAL);


Random place for comment: it would be nice if the commit message could explain why the existing symbol factory wasn't usable as-is.

tautschnig · 2018-12-21T11:02:39Z

src/goto-programs/generate_function_bodies.cpp

+    symbol_factory.declare_created_symbols(init_code);
+    init_code.append(assignments);
+
+    null_message_handlert nmh;


I'm not sure that's a good idea.

Ok, I'm using a real one now.

danpoe · 2019-01-14T17:55:34Z

@tautschnig I've now addressed all the comments.

This is because we want to use the c nondet symbol factory from the ansi-c directory, and code in goto-programs should not depend on code in ansi-c.

This is so we can use the goto_check() features (such as --pointer-check) in the regression tests for the function body generation feature (e.g., to ensure that the generated code for a function does not dereference a null pointer passed to the function, by using --pointer-check). A potential drawback is that goto check instrumentation code is also added to the code generated by the function body generation feature, which could affect performance.

Parse the c object factory command line parameters when the function body generation is enabled, and pass the resulting c_object_factory_parameterst object along to an appropriate subclass of generate_function_bodiest.

We essentially make two changes to the c nondet symbol factory: - A parameter assign_const is added to gen_nondet_init(). When false, an object of const type is not nondet assigned. This will be used in the function body generation feature to not havoc const arguments (e.g., the targets of pointers to const int) - A parameter lifetime (an enum of type lifetimet) is added to the constructor of symbol_factoryt. It indicates whether it uses lifetimet::AUTOMATIC_LOCAL, lifetimet::STATIC_GLOBAL, or lifetimet::DYNAMIC when allocating new objects with allocate_object(). Previously this was hardcoded to behave like lifetime::AUTOMATIC_LOCAL. However, in the function body generation we need to add code to a function to allocate dynamic objects. This is because the function may be called multiple times, hence using local or global variables does not work.

This removes the existing code in the function body generation for havoc-ing objects (in havoc_expr_rec()) and replaces it with calls to the c nondet symbol factory (gen_nondet_init()).

allredj

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

danpoe requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, NathanJPhillips, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners November 22, 2018 14:17

danpoe force-pushed the feature/nondet-function-argument-targets branch from 44c1de2 to f4e7c0c Compare November 23, 2018 13:03

danpoe requested a review from forejtv as a code owner November 23, 2018 15:10

danpoe added the do not merge label Nov 23, 2018

danpoe force-pushed the feature/nondet-function-argument-targets branch 2 times, most recently from 6066ba1 to 71185a1 Compare November 23, 2018 16:11

danpoe removed the do not merge label Nov 23, 2018

danpoe force-pushed the feature/nondet-function-argument-targets branch from 7e828df to a9ba6ac Compare November 23, 2018 16:51

allredj reviewed Nov 23, 2018

View reviewed changes

danpoe mentioned this pull request Nov 24, 2018

Generate function bodies with nondet return values #3457

Merged

6 tasks

tautschnig changed the title ~~Generate function bodies that nondet havoc the function arguments~~ Generate function bodies that nondet havoc the function arguments [blocks: #3457] Nov 24, 2018

tautschnig assigned danpoe Nov 24, 2018

tautschnig added the blocker label Nov 24, 2018

danpoe added the dependent - do not merge label Nov 29, 2018

danpoe changed the title ~~Generate function bodies that nondet havoc the function arguments [blocks: #3457]~~ Generate function bodies that nondet havoc the function arguments [blocks: #3457, depends-on: #3443] Nov 29, 2018

danpoe force-pushed the feature/nondet-function-argument-targets branch from a9ba6ac to c3076a7 Compare November 29, 2018 17:49

allredj reviewed Nov 29, 2018

View reviewed changes

danpoe force-pushed the feature/nondet-function-argument-targets branch from c3076a7 to e66793d Compare December 19, 2018 11:45

danpoe added a commit that referenced this pull request Dec 19, 2018

Merge pull request #3443 from danpoe/refactor/factor-out-object-alloc…

5594db6

…ation-from-object-factories Factor out object allocation from object factories [blocks: #3455]

danpoe force-pushed the feature/nondet-function-argument-targets branch 2 times, most recently from fe3bcb3 to 19e3122 Compare December 19, 2018 16:01

allredj reviewed Dec 19, 2018

View reviewed changes

tautschnig self-assigned this Dec 19, 2018

danpoe force-pushed the feature/nondet-function-argument-targets branch from 19e3122 to 3257165 Compare December 20, 2018 11:11

allredj reviewed Dec 20, 2018

View reviewed changes

tautschnig reviewed Dec 21, 2018

View reviewed changes

tautschnig assigned danpoe and unassigned tautschnig Dec 21, 2018

danpoe force-pushed the feature/nondet-function-argument-targets branch from 3257165 to a0c1701 Compare January 14, 2019 17:53

danpoe assigned tautschnig and unassigned danpoe Jan 14, 2019

tautschnig approved these changes Jan 14, 2019

View reviewed changes

tautschnig assigned peterschrammel, martin-cs and chrisr-diffblue and unassigned tautschnig Jan 14, 2019

danpoe force-pushed the feature/nondet-function-argument-targets branch 2 times, most recently from 136f584 to ade4e66 Compare January 15, 2019 10:38

danpoe added 6 commits January 15, 2019 10:38

Move function body generation to goto instrument directory

2c90986

This is because we want to use the c nondet symbol factory from the ansi-c directory, and code in goto-programs should not depend on code in ansi-c.

Add regression tests for havoc-ing of function arguments

15e34b6

Pass c object factory parameters to function body generation

6cf7982

Parse the c object factory command line parameters when the function body generation is enabled, and pass the resulting c_object_factory_parameterst object along to an appropriate subclass of generate_function_bodiest.

Use c nondet object factory in function body generation

ade4e66

This removes the existing code in the function body generation for havoc-ing objects (in havoc_expr_rec()) and replaces it with calls to the c nondet symbol factory (gen_nondet_init()).

allredj reviewed Jan 15, 2019

View reviewed changes

chrisr-diffblue approved these changes Jan 22, 2019

View reviewed changes

danpoe merged commit 81d8eb1 into diffblue:develop Jan 22, 2019

danpoe deleted the feature/nondet-function-argument-targets branch June 2, 2020 17:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Generate function bodies that nondet havoc the function arguments [blocks: #3457] #3455

Generate function bodies that nondet havoc the function arguments [blocks: #3457] #3455

danpoe commented Nov 22, 2018 •

edited

Loading

allredj left a comment

chrisr-diffblue commented Nov 29, 2018

allredj left a comment

allredj left a comment

allredj left a comment

tautschnig left a comment

tautschnig Dec 21, 2018

tautschnig Dec 21, 2018

tautschnig Dec 21, 2018

tautschnig Dec 21, 2018

danpoe Jan 14, 2019

tautschnig Jan 14, 2019

tautschnig Dec 21, 2018

tautschnig Dec 21, 2018

tautschnig Dec 21, 2018

danpoe Jan 14, 2019

danpoe commented Jan 14, 2019

allredj left a comment

Generate function bodies that nondet havoc the function arguments [blocks: #3457] #3455

Generate function bodies that nondet havoc the function arguments [blocks: #3457] #3455

Conversation

danpoe commented Nov 22, 2018 • edited Loading

allredj left a comment

Choose a reason for hiding this comment

chrisr-diffblue commented Nov 29, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe commented Jan 14, 2019

allredj left a comment

Choose a reason for hiding this comment

danpoe commented Nov 22, 2018 •

edited

Loading