Memory snapshot harness havoc #4351

xbauch · 2019-03-08T11:14:05Z

This PR adds the option to selectively initialise global variables from a snapshot to a non-deterministic value rather than the value they had in the snapshot.

The scope of this PR are global variables of primitive types but since we use the recursive_initialization for the havoc-ing, the scope is inherited from the goto-harness general. At this moment, struct_tag, pointer, and array have dedicated treatment. On the other hand it is not within the scope of this PR to modify the configuration of the recursive initialization, i.e. the default values are used.

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.

xbauch · 2019-03-08T11:15:31Z

Only the actual havoc-ing commit (for early feedback), documentation and tests are coming.

sonodtt · 2019-03-11T14:44:55Z

doc/cprover-manual/goto-harness.md

+function to work in arbitrary environment. If we want a more restricted
+environment or if we have the program in which our function will only be called,
+we call the `memory-snapshot` harness instead.


we call -> we can call

sonodtt · 2019-03-11T14:45:19Z

doc/cprover-manual/goto-harness.md

+### The memory snapshot harness
+
+The `function-call` harness is used in situations when we want the analysed


situations when -> situations in which

sonodtt · 2019-03-11T14:45:41Z

doc/cprover-manual/goto-harness.md

+The `function-call` harness is used in situations when we want the analysed
+function to work in arbitrary environment. If we want a more restricted
+environment or if we have the program in which our function will only be called,


remove 'only' function will only be called

I wanted "only" there somewhere. What about:
..or if we have the only program in which our function will be called..
?

sonodtt · 2019-03-11T14:47:33Z

doc/cprover-manual/goto-harness.md

+we call the `memory-snapshot` harness instead.
+
+Furthermore, the program state of interest may be taken a particular location


remove 'taken' ? might be clear enough. Alternatively - 'taken from'

What about "taken at a particular location"?

sonodtt · 2019-03-11T14:49:44Z

doc/cprover-manual/goto-harness.md

+```
+
+But are not particularly interested in the analysing the complex function, since


'interested in the' -> 'interested in analysing'

pps sorry about all the minor fixes. 100% aware english is not your 1st language - and you're doing great.

Done. And no reason to apologise, the language is important especially in the manual.

NlightNFotis

This looks good to me overall.

NlightNFotis · 2019-03-12T15:27:09Z

doc/cprover-manual/goto-harness.md

+we trust that its implementation is correct. Hence we run the above program
+stopping after the assignments to `x` and `x` and storing the program state,
+e.g. using the `memory-analyzer`, in a JSON file `snapshot.json`. Then run the


Do we have any documentation for the memory-analyzer? I recall seeing some around, but I can't seem to be able to find it now? If we don't, would it be a good idea to write some separate documentation for that as well?

xbauch#3 I intent to make it part of #4261 once review-able.

allredj

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

tautschnig · 2019-03-14T21:50:30Z

regression/goto-harness/havoc-global-int-01/test.desc

+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE
+--
+^warning: ignoring


I think it would be helpful to document how the JSON snapshots were generated. There will be a day where we need to change them in some way.

That documentation was intended to be a part of #4261 (as we used the memory-analyzer to generate the JSON). Do you think it should be documented here as well?

tautschnig · 2019-03-14T21:51:57Z

src/goto-harness/memory_snapshot_harness_generator.cpp

+    if(variables_to_havoc.count(symbol.base_name) == 0)
+    {
+      code_assignt code_assign(symbol.symbol_expr(), symbol.value);
+      code.add(code_assign);


Nit picking: I don't think the code_assign temporary adds value, you might just do code.add(code_assignt{...});. If you do prefer to keep it I'd suggest to use code.add(std::move(code_assign));

tautschnig · 2019-03-14T21:53:19Z

src/goto-harness/memory_snapshot_harness_generator.h

@@ -48,30 +49,92 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
  {
  }

+  /// 1. load memory table from the snapshot


I'd start this documentation with a one-sentence summary. Otherwise I'd suspect this to render awkwardly.

tautschnig · 2019-03-14T21:54:00Z

src/goto-harness/memory_snapshot_harness_generator.h

@@ -48,30 +49,92 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
  {
  }

+  /// 1. load memory table from the snapshot
+  /// 2. add initial section to the initial location


Also I think it would be nice to make these proper sentences, starting with an uppercase letter and terminated with a full stop.

tautschnig · 2019-03-14T21:54:43Z

src/goto-harness/memory_snapshot_harness_generator.h

  void validate_options() override;

+  /// Parse the snapshot JSON file and initialise the symbol table
+  /// \param file: the snapshot JSON file
+  /// \param snapshot: the resulting symbol table build from the snapshot


s/build/built/

tautschnig · 2019-03-14T21:55:13Z

src/goto-harness/memory_snapshot_harness_generator.h

  void
  get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const;

+  /// Turn this:


I'd start with a one-sentence summary. Otherwise this likely renders awkwardly.

tautschnig · 2019-03-14T21:55:42Z

src/goto-harness/memory_snapshot_harness_generator.h

  void add_init_section(goto_modelt &goto_model) const;

+  /// For each global symbol in the \p snapshot symbol table either:
+  /// 1) add \ref code_assignt assigning a value from the \p snapshot to the
+  ///    symbol


tautschnig · 2019-03-14T21:57:03Z

doc/cprover-manual/goto-harness.md

+The `function-call` harness is used in situations in which we want the analysed
+function to work in arbitrary environment. If we want a more restricted
+environment or if we have the program in which our function will be called,


or if we have an executable program in which

tautschnig · 2019-03-14T21:57:43Z

doc/cprover-manual/goto-harness.md

+initial location does not have to be the first instruction of a function: we can
+also specify the _location number_ `n` to set the initial location inside our
+function. The _location numbers_ do not have to co-relate with the lines of the


s/co-relate/correlate/ (or maybe "coincide")

hannes-steffenhagen-diffblue · 2019-03-11T14:55:05Z

src/goto-harness/memory_snapshot_harness_generator.h

@@ -21,7 +21,8 @@ Author: Daniel Poetzl

 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS                              \
  "(memory-snapshot):"                                                         \
-  "(initial-location):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS
+  "(initial-location):"                                                        \
+  "(havoc-variables):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS


This section should have // clang-format off and // clang-format on options to prevent clang-format from messing up the formatting here

hannes-steffenhagen-diffblue · 2019-03-11T14:56:41Z

src/goto-harness/memory_snapshot_harness_generator.cpp

  code_blockt &code) const
 {
+  recursive_initialization_configt recursive_initialization_config;
+  auto recursive_initialization = util_make_unique<recursive_initializationt>(


If you're just using this in-place here there's no need for dynamic allocation... we only had that in the other harness generator because it was a stateful mess

hannes-steffenhagen-diffblue · 2019-03-11T14:57:55Z

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -54,6 +56,10 @@ void memory_snapshot_harness_generatort::handle_option(
      location_number = optionalt<unsigned>(safe_string2unsigned(start.back()));
    }
  }
+  else if (option == "havoc-variables")


s/variables/globals?

hannes-steffenhagen-diffblue · 2019-03-11T14:59:29Z

doc/cprover-manual/goto-harness.md

+### The memory snapshot harness
+
+The `function-call` harness is used in situations when we want the analysed


I find this sentence to be a bit awkward. The point of the snapshot harness is to analyse a function starting from a "real" program state (or a subset thereof)

hannes-steffenhagen-diffblue · 2019-03-11T15:01:00Z

doc/cprover-manual/goto-harness.md

+within a function. In that case we do not want the harness to instrument the
+whole function but rather to allow starting the execution from a specific
+initial location (specified via `--initial-location func[:<n>]`).


Might be worth noting here that the --initial-location here should match the program location at the original breakpoint location

hannes-steffenhagen-diffblue · 2019-03-18T11:33:54Z

regression/goto-harness/havoc-global-int-01/main.c

+
+int main()
+{
+  assert(x == 1);


what exactly is this test testing? Presumably this assertion would still fail if the snapshot harness didn't work?

hannes-steffenhagen-diffblue · 2019-03-18T11:36:04Z

regression/goto-harness/havoc-global-int-02/main.c

+  fill_array(large_array, array_size);
+  y = array_sum(large_array, array_size);
+  checkpoint();
+  assert(y + 2 > x);


can you have an assert(false) after checkpoint just to check that the generated code actually makes this part still reachable?

hannes-steffenhagen-diffblue

I think this looks reasonable, but I'd take another look at the regression tests

Basically just grabs a list of var-names from command line and calls recursive initialize on them instead of assigning their value.

Code level documentation for the class methods.

Covering memory-snapshot harness, but not the memory analyzer.

For global int, global struct, multiple snapshot-ed symbols, multiple havoc-ed symbols.

xbauch changed the title ~~Feature/memory snapshot harness havoc~~ Memory snapshot harness havoc Mar 8, 2019

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch 2 times, most recently from 3ee09ca to eeb1139 Compare March 11, 2019 11:11

sonodtt reviewed Mar 11, 2019

View reviewed changes

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from 175f325 to 3208756 Compare March 11, 2019 14:52

NlightNFotis reviewed Mar 12, 2019

View reviewed changes

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from 7d6dc91 to 11c311b Compare March 13, 2019 08:35

xbauch marked this pull request as ready for review March 13, 2019 08:46

xbauch requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli, smowton and tautschnig as code owners March 13, 2019 08:46

xbauch changed the title ~~Memory snapshot harness havoc~~ Memory snapshot harness havoc [depends: #4150] Mar 13, 2019

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from 11c311b to e207cfe Compare March 13, 2019 11:39

allredj reviewed Mar 13, 2019

View reviewed changes

tautschnig added the dependent - do not merge label Mar 14, 2019

tautschnig approved these changes Mar 14, 2019

View reviewed changes

tautschnig assigned xbauch Mar 14, 2019

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from aeff777 to 2240eb9 Compare March 18, 2019 09:14

xbauch changed the title ~~Memory snapshot harness havoc [depends: #4150]~~ Memory snapshot harness havoc Mar 18, 2019

xbauch removed the dependent - do not merge label Mar 18, 2019

hannes-steffenhagen-diffblue reviewed Mar 18, 2019

View reviewed changes

hannes-steffenhagen-diffblue approved these changes Mar 18, 2019

View reviewed changes

xbauch added the do not merge label Mar 18, 2019

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from 2240eb9 to 0074f5e Compare March 18, 2019 12:41

xbauch removed the do not merge label Mar 18, 2019

Petr Bauch added 3 commits March 18, 2019 13:08

Havoc global variables in memory snapshot harness

7eaf157

Basically just grabs a list of var-names from command line and calls recursive initialize on them instead of assigning their value.

Add documentation to memory snapshot harness

6ca35c2

Code level documentation for the class methods.

Add cprover manual entry

fce288d

Covering memory-snapshot harness, but not the memory analyzer.

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from 0074f5e to 1425e3a Compare March 18, 2019 13:10

Add regression tests

ceaafdf

For global int, global struct, multiple snapshot-ed symbols, multiple havoc-ed symbols.

xbauch force-pushed the feature/memory-snapshot-harness-havoc branch from 1425e3a to ceaafdf Compare March 18, 2019 13:23

xbauch merged commit a504983 into diffblue:develop Mar 18, 2019

xbauch deleted the feature/memory-snapshot-harness-havoc branch March 20, 2019 09:14

		### The memory snapshot harness

		The `function-call` harness is used in situations when we want the analysed

		we call the `memory-snapshot` harness instead.

		Furthermore, the program state of interest may be taken a particular location

		```

		But are not particularly interested in the analysing the complex function, since

Memory snapshot harness havoc #4351

Memory snapshot harness havoc #4351

Uh oh!

Conversation

xbauch commented Mar 8, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

xbauch commented Mar 8, 2019

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!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

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!

Choose a reason for hiding this comment

Uh oh!

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

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!

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!

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!

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!

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

xbauch commented Mar 8, 2019 •

edited

Loading

sonodtt Mar 11, 2019 •

edited

Loading

sonodtt Mar 11, 2019 •

edited

Loading

hannes-steffenhagen-diffblue left a comment •

edited

Loading