Add option to non-det globals to goto-harness

Add ability to non-deterministically initialise
globals in the function call harness generator.

Co-authored-by: Fotis Koutoulakis <[email protected]>
Co-authored-by: Hannes Steffenhagen <[email protected]>

Author: NlightNFotis

regression/goto-harness/do_not_nondet_globals_by_default/main.c

@@ -0,0 +1,6 @@
+int a_global;
+
+void entry_function(void)
+{
+  assert(a_global == 0);
+}

regression/goto-harness/do_not_nondet_globals_by_default/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function entry_function
+^\[entry_function.assertion.1\] line \d+ assertion a_global == 0: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

regression/goto-harness/non_det_globals_option/main.c

@@ -0,0 +1,6 @@
+int a_global;
+
+void entry_function(void)
+{
+  assert(a_global == 0);
+}

regression/goto-harness/non_det_globals_option/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--harness-type call-function --function entry_function --nondet-globals
+^\[entry_function.assertion.1\] line \d+ assertion a_global == 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$

src/goto-harness/function_call_harness_generator.cpp

@@ -30,9 +30,13 @@ struct function_call_harness_generatort::implt
   irep_idt harness_function_name;
   symbol_tablet *symbol_table;
   goto_functionst *goto_functions;
+  bool nondet_globals = false;
 
   /// \see goto_harness_generatort::generate
   void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
+  /// Iterate over the symbol table and generate initialisation code for
+  /// globals into the function body.
+  void generate_nondet_globals(code_blockt &function_body);
   /// Non-deterministically initialise the parameters of the entry function
   /// and insert function call to the passed code block.
   void setup_parameters_and_call_entry_function(code_blockt &function_body);
@@ -63,6 +67,10 @@ void function_call_harness_generatort::handle_option(
   {
     p_impl->function = require_exactly_one_value(option, values);
   }
+  else if(option == FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT)
+  {
+    p_impl->nondet_globals = true;
+  }
   else
   {
     throw invalid_command_line_argument_exceptiont{
@@ -120,10 +128,29 @@ void function_call_harness_generatort::implt::generate(
   // create body for the function
   code_blockt function_body{};
 
+  generate_nondet_globals(function_body);
   setup_parameters_and_call_entry_function(function_body);
   add_harness_function_to_goto_model(std::move(function_body));
 }
 
+void function_call_harness_generatort::implt::generate_nondet_globals(
+  code_blockt &function_body)
+{
+  if(nondet_globals)
+  {
+    for(const auto &symbol_table_entry : *symbol_table)
+    {
+      const auto &symbol = symbol_table_entry.second;
+      if(
+        symbol.is_static_lifetime && symbol.is_lvalue &&
+        !has_prefix(id2string(symbol.name), "__CPROVER_"))
+      {
+        generate_initialisation_code_for(function_body, symbol.symbol_expr());
+      }
+    }
+  }
+}
+
 void function_call_harness_generatort::implt::generate_initialisation_code_for(
   code_blockt &block,
   const exprt &lhs)

src/goto-harness/function_harness_generator_options.h

@@ -10,10 +10,13 @@ Author: Diffblue Ltd.
 #define CPROVER_GOTO_HARNESS_FUNCTION_HARNESS_GENERATOR_OPTIONS_H
 
 #define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "function"
+#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT "nondet-globals"
 
 // clang-format off
 #define FUNCTION_HARNESS_GENERATOR_OPTIONS                                     \
   "(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):"                             \
+  "(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")"                        \
+// FUNCTION_HARNESS_GENERATOR_OPTIONS
 
 // clang-format on
 
@@ -22,6 +25,8 @@ Author: Diffblue Ltd.
   "function harness generator (--harness-type call-function)\n\n"              \
   "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT                                 \
   "      the function the harness should call\n"                               \
+  "--" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT                           \
+  "      set global variables to non-deterministic values in harness\n"        \
   // FUNCTION_HARNESS_GENERATOR_HELP
 
 // clang-format on