Add nondet initialisation of strings in goto-harness. #4285

NlightNFotis · 2019-02-27T12:24:22Z

Add the capability to non-deterministically initialise strings in goto-harness call-function harness generator.

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 · 2019-02-27T14:16:13Z

src/goto-harness/function_call_harness_generator.cpp

@@ -48,6 +48,9 @@ struct function_call_harness_generatort::implt
  std::set<irep_idt> function_parameters_to_treat_as_arrays;
  std::set<irep_idt> function_arguments_to_treat_as_arrays;

+  std::set<irep_idt> function_parameters_to_treat_as_cstrings;


FWIW I think we need to start more cleanly separating between what we get for command-line options and what things we generate as intermediates based on that.

⛏ unordered_set!

❓ Also, given how this is used, I don't understand why aren't you using a map (param -> value)? It seems to me, keeping them as separate maps forces you to add more manual checks, while you could be relying on the type system to do that for you.

src/goto-harness/recursive_initialization.cpp

xbauch

Looks good.

src/goto-harness/recursive_initialization.cpp

tautschnig

There is nothing that alarms me about the changes compared to the array init work, but I do note that a lot of the comments that were made on that PR (in particular those by @LAJW) apply here as well and should be carefully considered.

doc/cprover-manual/goto-harness.md

sonodtt · 2019-02-28T09:28:47Z

Great work on the documentation. That's a significant amount of effort in terms of both structure and examples - and I appreciate how hard that can be. Marvellous.
I think it will pay off handsomely in the medium to long term, and deducing all this from the code... unreliable at best.

sonodtt

Just some minor checks on the documentation.

Unintended blocker review

LAJW · 2019-02-28T15:53:31Z

src/goto-harness/function_call_harness_generator.cpp

@@ -48,6 +48,9 @@ struct function_call_harness_generatort::implt
  std::set<irep_idt> function_parameters_to_treat_as_arrays;
  std::set<irep_idt> function_arguments_to_treat_as_arrays;

+  std::set<irep_idt> function_parameters_to_treat_as_cstrings;


⛏ unordered_set!

LAJW · 2019-02-28T15:57:38Z

src/goto-harness/function_call_harness_generator.cpp

@@ -48,6 +48,9 @@ struct function_call_harness_generatort::implt
  std::set<irep_idt> function_parameters_to_treat_as_arrays;
  std::set<irep_idt> function_arguments_to_treat_as_arrays;

+  std::set<irep_idt> function_parameters_to_treat_as_cstrings;


❓ Also, given how this is used, I don't understand why aren't you using a map (param -> value)? It seems to me, keeping them as separate maps forces you to add more manual checks, while you could be relying on the type system to do that for you.

src/goto-harness/function_call_harness_generator.cpp

regression/goto-harness/nondet_strings/main.c

regression/goto-harness/nondet_strings/test.desc

src/goto-harness/function_call_harness_generator.cpp

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: fdab393).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102682997
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.

Add support for nondet-initialisation of strings in the function-call goto-harness leveraging pointer nondet initialisation. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

allredj

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

romainbrenguier · 2019-03-04T08:04:30Z

src/goto-harness/recursive_initialization.cpp

+  for(const auto &pointer_to_treat_as_string_name :
+      pointers_to_treat_as_cstrings)
+  {
+    out << "\n    " << pointer_to_treat_as_string_name << std::endl;


This should use join_strings

hannes-steffenhagen-diffblue reviewed Feb 27, 2019

View reviewed changes

NlightNFotis force-pushed the nondet-strings branch 2 times, most recently from f178c76 to 7d57a85 Compare February 27, 2019 14:17

xbauch reviewed Feb 27, 2019

View reviewed changes

src/goto-harness/recursive_initialization.cpp Show resolved Hide resolved

xbauch approved these changes Feb 27, 2019

View reviewed changes

hannes-steffenhagen-diffblue reviewed Feb 27, 2019

View reviewed changes

src/goto-harness/recursive_initialization.cpp Outdated Show resolved Hide resolved

src/goto-harness/recursive_initialization.cpp Outdated Show resolved Hide resolved

NlightNFotis force-pushed the nondet-strings branch from 7d57a85 to 763b8d1 Compare February 27, 2019 14:43

NlightNFotis marked this pull request as ready for review February 27, 2019 17:21

NlightNFotis requested review from chrisr-diffblue, danpoe, kroening, martin-cs, peterschrammel, smowton and tautschnig as code owners February 27, 2019 17:21

tautschnig approved these changes Feb 27, 2019

View reviewed changes

sonodtt reviewed Feb 28, 2019

View reviewed changes

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

sonodtt reviewed Feb 28, 2019

View reviewed changes

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

NlightNFotis force-pushed the nondet-strings branch from 24785d4 to 73575b3 Compare February 28, 2019 15:11

sonodtt self-requested a review February 28, 2019 15:14

sonodtt previously requested changes Feb 28, 2019

View reviewed changes

sonodtt self-requested a review February 28, 2019 15:28

NlightNFotis force-pushed the nondet-strings branch from 73575b3 to fdab393 Compare February 28, 2019 15:29

LAJW reviewed Feb 28, 2019

View reviewed changes

romainbrenguier reviewed Feb 28, 2019

View reviewed changes

src/goto-harness/function_call_harness_generator.cpp Show resolved Hide resolved

allredj reviewed Feb 28, 2019

View reviewed changes

NlightNFotis force-pushed the nondet-strings branch from fdab393 to 4fc128c Compare February 28, 2019 17:15

NlightNFotis and others added 2 commits March 1, 2019 10:58

Add support for nondet initialisation of strings.

e00ac3f

Add support for nondet-initialisation of strings in the function-call goto-harness leveraging pointer nondet initialisation. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>

Add documentation for nondet init of cstrings

ac740d6

NlightNFotis force-pushed the nondet-strings branch from 4fc128c to ac740d6 Compare March 1, 2019 10:58

allredj reviewed Mar 1, 2019

View reviewed changes

chrisr-diffblue approved these changes Mar 1, 2019

View reviewed changes

romainbrenguier reviewed Mar 4, 2019

View reviewed changes

NlightNFotis merged commit f3300d6 into diffblue:develop Mar 4, 2019

NlightNFotis deleted the nondet-strings branch March 4, 2019 10:21

Add nondet initialisation of strings in goto-harness. #4285

Add nondet initialisation of strings in goto-harness. #4285

Uh oh!

Conversation

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

Uh oh!

Uh oh!

hannes-steffenhagen-diffblue Feb 27, 2019

Choose a reason for hiding this comment

Uh oh!

LAJW Feb 28, 2019

Choose a reason for hiding this comment

Uh oh!

LAJW Feb 28, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

xbauch left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

sonodtt left a comment

Choose a reason for hiding this comment

Uh oh!

LAJW Feb 28, 2019

Choose a reason for hiding this comment

Uh oh!

LAJW Feb 28, 2019

Choose a reason for hiding this comment

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!

romainbrenguier Mar 4, 2019

Choose a reason for hiding this comment

Uh oh!

Uh oh!

NlightNFotis commented Feb 27, 2019 •

edited

Loading

sonodtt commented Feb 28, 2019 •

edited

Loading