Cumulative commit

Will be squashed later.

Author: Petr Bauch

doc/cprover-manual/goto-harness.md

@@ -13,9 +13,10 @@ having to manually construct an appropriate environment.
 
 We have two types of harnesses we can generate for now:
 
-* The `memory-snapshot` harness. TODO: Daniel can document this.
 * The `function-call` harness, which automatically synthesises an environment
 without having any information about the program state.
+* The `memory-snapshot` harness, which loads an existing program state (in form
+of a JSON file) and selectively _havoc-ing_ some variables.
 
 It is used similarly to how `goto-instrument` is used by modifying an existing
 GOTO binary, as produced by `goto-cc`.
@@ -309,4 +310,57 @@ main.c function function
 
 ** 0 of 1 failed (1 iterations)
 VERIFICATION SUCCESSFUL
-```
+```
+
+### The memory snapshot harness
+
+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,
+we call the `memory-snapshot` harness instead.
+
+Furthermore, the program state of interest may be taken a particular location
+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>]`).
+
+Say we want to check the assertion in the following code:
+
+```C
+// main.c
+unsigned int x;
+unsigned int y;
+
+unsigned int complex_function_which_returns_one() {
+  unsinged int i = 0;
+  while (i < 1000000000) {
+    if (y)
+      break;
+  }
+  return i & 2;
+}
+
+int main() {
+  x = complex_function_which_returns_one();
+  assert(y + 2 > x);
+  return 0;
+}
+```
+
+But are not particularly interested in the analysing the complex function, since
+we trust that its implementation is correct. Hence we run the above program
+stopping after the assignment to `x` and storing the program state, e.g. using
+the `memory-analyzer`, in a JSON file `snapshot.json`. Then run the harness and
+verify the assertion with:
+
+```
+$ goto-cc -o main.gb main.c
+$ goto-harness \
+  --harness-function-name harness \
+  --harness-type initialise-with-memory-snapshot \
+  --memory-snapshot snapshot.json \
+  --initial-location main:1 \
+  --havoc-variables x \
+  main.gb main-mod.gb
+$ cbmc --function harness main-mod.gb
+```

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

@@ -0,0 +1,8 @@
+int x;
+
+int main()
+{
+  assert(x == 1);
+
+  return 0;
+}

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

@@ -0,0 +1,8 @@
+CORE
+main.c
+--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-1-snapshot.json --initial-location main:0 --havoc-variables x
+^EXIT=10$
+^SIGNAL=0$
+\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE
+--
+^warning: ignoring

src/goto-harness/memory_snapshot_harness_generator.h

@@ -53,17 +53,35 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
     override;
 
 protected:
+  /// Collect the memory-snapshot specific cmdline options (one at a time)
+  /// \param option: memory-snapshot | initial-location | havoc-variables
+  /// \param values: list of arguments related to a given option
   void handle_option(
     const std::string &option,
     const std::list<std::string> &values) override;
 
+  /// Check that user options make sense:
+  /// On their own, e.g. location number cannot be specified without a function.
+  /// In relation to the input program, e.g. function name must be known via
+  ///   the symbol table.
   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
   void
   get_memory_snapshot(const std::string &file, symbol_tablet &snapshot) const;
 
   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 \snapshot to the
+  ///    symbol
+  /// 2) recursively initialise the symbol to a non-deterministic value of the
+  ///    right type
+  /// \param snapshot: snapshot to load the symbols and their values from
+  /// \param goto_model: model to initialise the havoc-ing
+  /// \param code: block of code where the assignments are added
   void add_assignments_to_globals(
     const symbol_tablet &snapshot,
     goto_modelt &goto_model,