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

@@ -24,6 +24,7 @@ Author: Daniel Poetzl
 #include <linking/static_lifetime_init.h>
 
 #include "goto_harness_generator_factory.h"
+#include "recursive_initialization.h"
 
 void memory_snapshot_harness_generatort::handle_option(
   const std::string &option,
@@ -56,6 +57,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(
@@ -196,17 +201,27 @@ void memory_snapshot_harness_generatort::add_init_section(
 }
 
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
-  const symbol_tablet &snapshot) const
+  const symbol_tablet &snapshot,
+  goto_modelt &goto_model) const
 {
+  recursive_initializationt recursive_initialization{
+    recursive_initialization_configt{}, goto_model};
+
   code_blockt code;
   for(const auto &pair : snapshot)
   {
     const symbolt &symbol = pair.second;
-
     if(!symbol.is_static_lifetime)
       continue;
 
-    code.add(code_assignt{symbol.symbol_expr(), symbol.value});
+    if(variables_to_havoc.count(symbol.base_name) == 0)
+    {
+      code.add(code_assignt{symbol.symbol_expr(), symbol.value});
+    }
+    else
+    {
+      recursive_initialization.initialize(symbol.symbol_expr(), 0, {}, code);
+    }
   }
   return code;
 }
@@ -312,7 +327,8 @@ void memory_snapshot_harness_generatort::generate(
 
   add_init_section(goto_model);
 
-  code_blockt harness_function_body = add_assignments_to_globals(snapshot);
+  code_blockt harness_function_body =
+    add_assignments_to_globals(snapshot, goto_model);
 
   add_call_with_nondet_arguments(
     *called_function_symbol, harness_function_body);

src/goto-harness/memory_snapshot_harness_generator.h

@@ -19,9 +19,12 @@ Author: Daniel Poetzl
 #include <util/message.h>
 #include <util/optional.h>
 
+// clang-format off
 #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 on
 
 // clang-format off
 #define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP                                 \
@@ -31,6 +34,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
 
@@ -61,8 +66,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
 
   void add_init_section(goto_modelt &goto_model) const;
 
-  code_blockt add_assignments_to_globals(const symbol_tablet &snapshot) const;
-
+  code_blockt add_assignments_to_globals(
+    const symbol_tablet &snapshot,
+    goto_modelt &goto_model) const;
   void add_call_with_nondet_arguments(
     const symbolt &called_function_symbol,
     code_blockt &code) const;
@@ -75,6 +81,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
 
   irep_idt entry_function_name;
   optionalt<unsigned> location_number;
+  std::unordered_set<irep_idt> variables_to_havoc;
 
   message_handlert &message_handler;
 };