Havoc global variables in memory snapshot harness

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

Author: Petr Bauch

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -22,6 +22,8 @@ Author: Daniel Poetzl
 #include <util/symbol_table.h>
 
 #include "goto_harness_generator_factory.h"
+#include "recursive_initialization.h"
+
 
 void memory_snapshot_harness_generatort::handle_option(
   const std::string &option,
@@ -54,6 +56,10 @@ void memory_snapshot_harness_generatort::handle_option(
       location_number = optionalt<unsigned>(safe_string2unsigned(start.back()));
     }
   }
+  else if (option == "havoc-variables")
+  {
+    variables_to_havoc.insert(values.begin(), values.end());
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont(
@@ -157,18 +163,29 @@ void memory_snapshot_harness_generatort::add_init_section(
 
 void memory_snapshot_harness_generatort::add_assignments_to_globals(
   const symbol_tablet &snapshot,
+  goto_modelt &goto_model,
   code_blockt &code) const
 {
+  recursive_initialization_configt recursive_initialization_config;
+  auto recursive_initialization = util_make_unique<recursive_initializationt>(
+    recursive_initialization_config, goto_model);
+
   for(const auto &pair : snapshot)
   {
     const symbolt &symbol = pair.second;
 
     if(!symbol.is_static_lifetime)
       continue;
 
-    code_assignt code_assign(symbol.symbol_expr(), symbol.value);
-
-    code.add(code_assign);
+    if(variables_to_havoc.count(symbol.base_name) == 0)
+    {
+      code_assignt code_assign(symbol.symbol_expr(), symbol.value);
+      code.add(code_assign);
+    }
+    else
+    {
+      recursive_initialization->initialize(symbol.symbol_expr(), 0, {}, code);
+    }
   }
 }
 
@@ -282,7 +299,7 @@ void memory_snapshot_harness_generatort::generate(
 
   code_blockt harness_function_body;
 
-  add_assignments_to_globals(snapshot, harness_function_body);
+  add_assignments_to_globals(snapshot, goto_model, harness_function_body);
 
   add_call_with_nondet_arguments(
     *called_function_symbol, harness_function_body);

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
 
 // clang-format off
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP                                 \
@@ -31,6 +32,8 @@ Author: Daniel Poetzl
   "--initial-location <func[:<n>]>\n"                                          \
   "                              use given function and location number as "   \
   "entry\n                              point\n"                               \
+  "--havoc-variables vars        initialise variables from vars to\n"          \
+  "                              non-deterministic values"                     \
   // MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP
 // clang-format on
 
@@ -63,6 +66,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
 
   void add_assignments_to_globals(
     const symbol_tablet &snapshot,
+    goto_modelt &goto_model,
     code_blockt &code) const;
 
   void add_call_with_nondet_arguments(
@@ -75,6 +79,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
 
   irep_idt function;
   optionalt<unsigned> location_number;
+  std::unordered_set<irep_idt> variables_to_havoc;
 
   message_handlert &message_handler;
 };