Add array initialisation support in default goto-harness. #4234

NlightNFotis · 2019-02-20T16:22:02Z

Joint work by me and @hannes-steffenhagen-diffblue on adding support for statically and dynamically sized arrays non-deterministic initialisation on the function-call harness in the new goto-harness tool.

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.

hannes-steffenhagen-diffblue

We'll also need to update user documentation ideally with usage examples and current limitations (no support for globals and struct members for dynamic arrays atm)

src/goto-harness/function_call_harness_generator.cpp

hannes-steffenhagen-diffblue · 2019-02-20T16:45:59Z

src/goto-harness/function_call_harness_generator.cpp

@@ -42,6 +43,12 @@ struct function_call_harness_generatort::implt
  recursive_initialization_configt recursive_initialization_config;
  std::unique_ptr<recursive_initializationt> recursive_initialization;

+  std::set<irep_idt> function_parameters_to_treat_as_arrays;
+  std::set<irep_idt> function_arguments_to_treat_as_arrays;


I don't particularly enjoy the solution we have here - basically, we need to keep track of the names of function arguments as declared on the function, and their mapping to parameters, and which parameters the array initialisation applies to etc...

This is just a note, we don't need to do it right now.

src/goto-harness/function_call_harness_generator.cpp

hannes-steffenhagen-diffblue · 2019-02-20T16:48:03Z

src/goto-harness/recursive_initialization.cpp

@@ -37,7 +38,16 @@ void recursive_initializationt::initialize(
  }
  else if(type.id() == ID_pointer)
  {
-    initialize_pointer(lhs, depth, known_tags, body);
+    if(


This could have been solved more elegantly if we used a handler chain pattern as the test-gen team does for their harness generation. Didn't want to do this atm because this was mostly about porting existing functionality, but might be worth converting this at some point.

This is just a note, we don't need to do it right now.

xbauch

Looks good.

sonodtt · 2019-02-21T07:55:10Z

We'll also need to update user documentation ideally with usage examples and current limitations (no support for globals and struct members for dynamic arrays atm)

Superb. The less time anyone needs to spend 'reverse-engineering' context/boundary conditions/ edge case coverage - is all company time that can be used for other purposes. A huge win at little cost.
To some extent - the same applies to a PR - in general the less assumptions made about people knowing what is in/ "the purpose" / "edge conditions" of a PR the better. I recall also external contributors making the same point.

I am delighted to see that you're keeping this in mind (& I know Fotis also shares this perspective).

hannes-steffenhagen-diffblue · 2019-02-25T16:58:38Z

Note that some of the examples don’t quite work atm due to a bug that has a pending fix in another PR

#4277

tautschnig

A couple of comments, but also a rebase and making-CI-happy is required.

src/goto-harness/function_call_harness_generator.cpp

src/goto-harness/recursive_initialization.cpp

src/goto-harness/recursive_initialization.h

regression/goto-harness/pointer-to-array-function-parameters-min-size/test.desc

doc/cprover-manual/goto-harness.md

for the function we are calling in goto-harness. Before this we had a function called setup_parameters_and_call_entry_function, and now we have split it up into declare_arguments and call_function. This is so we can do some handling between declaring arguments and calling the function. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Add non-det initialization of statically sized arrays. This does element-wise initialisation. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 0ad43fd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102341655
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 151dfd2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102349568
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj

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

allredj

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

doc/cprover-manual/goto-harness.md

LAJW

Rough.

That random argument-dependent-static variable is VERY suspicious.

src/goto-harness/recursive_initialization.cpp

src/goto-harness/function_call_harness_generator.cpp

src/goto-harness/recursive_initialization.h

src/goto-harness/recursive_initialization.cpp

Small helper to convert a program argument to size_t and throw an exception if it doesn't work. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

allredj

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

Create and non-det initialise of pointers to arrays making sure that they actually point at arrays. Also allows binding function parameters to the size of the array parameter. Only works with function parameters at the moment, not with struct members or globals. Also adds tests. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Added a debugging helper function. It was worth keeping it around even after debugging. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

This adds some user documentation to goto-harness. Currently only includes documentation for the call-function harness, not the memory-snapshot harness

chrisr-diffblue · 2019-02-27T17:24:31Z

regression/goto-harness/chain.sh

@@ -23,5 +23,11 @@ if [ -e "${name}-mod.gb" ] ; then
  rm -f "${name}-mod.gb"
 fi

-$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} 
-$cbmc --function $entry_point "${name}-mod.gb" --unwind 20 --unwinding-assertions
+# `# some comment` is an inline comment - basically, cause bash to execute an empty command


chrisr-diffblue · 2019-02-27T17:28:53Z

src/goto-harness/recursive_initialization.h

@@ -31,6 +31,8 @@ struct recursive_initialization_configt
  std::set<irep_idt> pointers_to_treat_as_arrays;
  std::set<irep_idt> variables_that_hold_array_sizes;
  std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
+
+  std::string to_string() const; // for debugging purposes


If to_string() is only meant to be used for debugging purposes, is it worth wrapping it in #if DEBUG ?

chrisr-diffblue · 2019-02-27T17:29:44Z

doc/cprover-manual/goto-harness.md

+
+We have two types of harnesses we can generate for now:
+
+* The `memory-snapshot` harness. TODO: Daniel can document this.


There's more than one 'Daniel'....

Maybe explicitly reference the PR (#4261)?

allredj

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

NlightNFotis force-pushed the non_det_array_goto_harness branch from c3fed2e to 071a1f9 Compare February 20, 2019 16:37

hannes-steffenhagen-diffblue reviewed Feb 20, 2019

View reviewed changes

hannes-steffenhagen-diffblue self-assigned this Feb 20, 2019

xbauch approved these changes Feb 20, 2019

View reviewed changes

NlightNFotis force-pushed the non_det_array_goto_harness branch from 071a1f9 to 8f03071 Compare February 25, 2019 16:53

NlightNFotis marked this pull request as ready for review February 25, 2019 16:54

NlightNFotis requested review from chrisr-diffblue, danpoe, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners February 25, 2019 16:54

NlightNFotis force-pushed the non_det_array_goto_harness branch 2 times, most recently from 078f14b to 9b6a4b2 Compare February 25, 2019 17:23

tautschnig approved these changes Feb 26, 2019

View reviewed changes

NlightNFotis force-pushed the non_det_array_goto_harness branch from 9b6a4b2 to 0ad43fd Compare February 26, 2019 14:15

NlightNFotis and others added 2 commits February 26, 2019 15:00

Add initialization of static arrays

138c675

Add non-det initialization of statically sized arrays. This does element-wise initialisation. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

NlightNFotis force-pushed the non_det_array_goto_harness branch from 0ad43fd to 151dfd2 Compare February 26, 2019 15:00

allredj reviewed Feb 26, 2019

View reviewed changes

NlightNFotis force-pushed the non_det_array_goto_harness branch from 151dfd2 to 07c31d7 Compare February 26, 2019 15:20

allredj reviewed Feb 26, 2019

View reviewed changes

NlightNFotis force-pushed the non_det_array_goto_harness branch from 07c31d7 to 5904fec Compare February 27, 2019 10:44

allredj reviewed Feb 27, 2019

View reviewed changes

xbauch reviewed Feb 27, 2019

View reviewed changes

doc/cprover-manual/goto-harness.md Outdated Show resolved Hide resolved

xbauch reviewed Feb 27, 2019

View reviewed changes

doc/cprover-manual/goto-harness.md Outdated Show resolved Hide resolved

xbauch reviewed Feb 27, 2019

View reviewed changes

doc/cprover-manual/goto-harness.md Outdated Show resolved Hide resolved

xbauch reviewed Feb 27, 2019

View reviewed changes

doc/cprover-manual/goto-harness.md Show resolved Hide resolved

NlightNFotis added a commit to NlightNFotis/cbmc that referenced this pull request Feb 27, 2019

Non-det array init PR (diffblue#4234)

27934ef

NlightNFotis added a commit to NlightNFotis/cbmc that referenced this pull request Feb 27, 2019

DO NOT REVIEW - Non-det array init PR (diffblue#4234)

5598410

NlightNFotis force-pushed the non_det_array_goto_harness branch from 5904fec to 1be00d6 Compare February 27, 2019 14:45

LAJW reviewed Feb 27, 2019

View reviewed changes

Add helper to get exactly one size value

0f96839

Small helper to convert a program argument to size_t and throw an exception if it doesn't work. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

allredj reviewed Feb 27, 2019

View reviewed changes

NlightNFotis force-pushed the non_det_array_goto_harness branch 2 times, most recently from c248ef3 to 8b2d421 Compare February 27, 2019 16:46

NlightNFotis and others added 3 commits February 27, 2019 17:17

Add recursive_initialization_configt::to_string

bdcc2b1

Added a debugging helper function. It was worth keeping it around even after debugging. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Add goto-harness documentation to cprover-manual

0ea5c31

This adds some user documentation to goto-harness. Currently only includes documentation for the call-function harness, not the memory-snapshot harness

NlightNFotis force-pushed the non_det_array_goto_harness branch from 8b2d421 to 0ea5c31 Compare February 27, 2019 17:18

chrisr-diffblue reviewed Feb 27, 2019

View reviewed changes

chrisr-diffblue approved these changes Feb 27, 2019

View reviewed changes

allredj reviewed Feb 27, 2019

View reviewed changes

NlightNFotis merged commit b3cc3e9 into diffblue:develop Feb 28, 2019

NlightNFotis deleted the non_det_array_goto_harness branch February 28, 2019 10:49


		We have two types of harnesses we can generate for now:

		* The `memory-snapshot` harness. TODO: Daniel can document this.

Add array initialisation support in default goto-harness. #4234

Add array initialisation support in default goto-harness. #4234

Uh oh!

Conversation

NlightNFotis commented Feb 20, 2019

Uh oh!

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

xbauch left a comment

Choose a reason for hiding this comment

Uh oh!

sonodtt commented Feb 21, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue commented Feb 25, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

LAJW left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

allredj 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!

sonodtt commented Feb 21, 2019 •

edited

Loading

hannes-steffenhagen-diffblue commented Feb 25, 2019 •

edited

Loading