Reflect the changes on individual generators

1: Config options are handled by the config's internal `handle_option`.
2: Options names are unified.
3: Memory-snapshot options are in a separate file.

Author: Petr Bauch

src/goto-harness/function_call_harness_generator.cpp

@@ -90,57 +90,19 @@ void function_call_harness_generatort::handle_option(
   const std::string &option,
   const std::list<std::string> &values)
 {
-  if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
-  {
-    p_impl->function = require_exactly_one_value(option, values);
-  }
-  else if(option == FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT)
-  {
-    p_impl->nondet_globals = true;
-  }
-  else if(option == FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT)
-  {
-    auto const value = require_exactly_one_value(option, values);
-    auto const min_null_tree_depth = string2optional<std::size_t>(value, 10);
-    if(min_null_tree_depth.has_value())
-    {
-      p_impl->recursive_initialization_config.min_null_tree_depth =
-        min_null_tree_depth.value();
-    }
-    else
-    {
-      throw invalid_command_line_argument_exceptiont{
-        "failed to convert `" + value + "' to integer",
-        "--" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT};
-    }
-  }
-  else if(option == FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT)
+  auto &require_exactly_one_value =
+    harness_options_parsert::require_exactly_one_value;
+
+  if(p_impl->recursive_initialization_config.handle_option(option, values))
   {
-    auto const value = require_exactly_one_value(option, values);
-    auto const max_nondet_tree_depth = string2optional<std::size_t>(value, 10);
-    if(max_nondet_tree_depth.has_value())
-    {
-      p_impl->recursive_initialization_config.max_nondet_tree_depth =
-        max_nondet_tree_depth.value();
-    }
-    else
-    {
-      throw invalid_command_line_argument_exceptiont{
-        "failed to convert `" + value + "' to integer",
-        "--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT};
-    }
   }
-  else if(option == FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT)
+  else if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
   {
-    p_impl->recursive_initialization_config.max_dynamic_array_size =
-      require_one_size_value(
-        FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values);
+    p_impl->function = require_exactly_one_value(option, values);
   }
-  else if(option == FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT)
+  else if(option == COMMON_HARNESS_GENERATOR_NONDET_GLOBALS_OPT)
   {
-    p_impl->recursive_initialization_config.min_dynamic_array_size =
-      require_one_size_value(
-        FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values);
+    p_impl->nondet_globals = true;
   }
   else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT)
   {
@@ -285,25 +247,8 @@ void function_call_harness_generatort::validate_options(
   {
     throw invalid_command_line_argument_exceptiont{
       "min dynamic array size cannot be greater than max dynamic array size",
-      "--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
-      " --" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
-  }
-}
-
-std::size_t function_call_harness_generatort::require_one_size_value(
-  const std::string &option,
-  const std::list<std::string> &values)
-{
-  auto const string_value = require_exactly_one_value(option, values);
-  auto value = string2optional<std::size_t>(string_value, 10);
-  if(value.has_value())
-  {
-    return value.value();
-  }
-  else
-  {
-    throw invalid_command_line_argument_exceptiont{
-      "failed to parse `" + string_value + "' as integer", "--" + option};
+      "--" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
+      " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
   }
 }
 

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -7,6 +7,8 @@ Author: Daniel Poetzl
 \******************************************************************/
 
 #include "memory_snapshot_harness_generator.h"
+#include "goto_harness_generator_factory.h"
+#include "memory_snapshot_harness_generator_options.h"
 
 #include <goto-programs/goto_convert.h>
 
@@ -23,18 +25,20 @@ 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,
   const std::list<std::string> &values)
 {
-  if(option == "memory-snapshot")
+  auto &require_exactly_one_value =
+    harness_options_parsert::require_exactly_one_value;
+  if(recursive_initialization_config.handle_option(option, values))
+  {
+  }
+  else if(option == MEMORY_SNAPSHOT_HARNESS_SNAPSHOT_OPT)
   {
     memory_snapshot_file = require_exactly_one_value(option, values);
   }
-  else if(option == "initial-location")
+  else if(option == MEMORY_SNAPSHOT_HARNESS_INITIAL_LOCATION_OPT)
   {
     const std::string initial_location =
       require_exactly_one_value(option, values);
@@ -57,7 +61,7 @@ void memory_snapshot_harness_generatort::handle_option(
       location_number = optionalt<unsigned>(safe_string2unsigned(start.back()));
     }
   }
-  else if(option == "havoc-variables")
+  else if(option == MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT)
   {
     variables_to_havoc.insert(values.begin(), values.end());
   }
@@ -222,7 +226,7 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
   goto_modelt &goto_model) const
 {
   recursive_initializationt recursive_initialization{
-    recursive_initialization_configt{}, goto_model};
+    recursive_initialization_config, goto_model};
 
   code_blockt code;
   for(const auto &pair : snapshot)

src/goto-harness/memory_snapshot_harness_generator.h

@@ -13,32 +13,13 @@ Author: Daniel Poetzl
 #include <string>
 
 #include "goto_harness_generator.h"
+#include "recursive_initialization.h"
 
 #include <goto-programs/goto_model.h>
 
 #include <util/message.h>
 #include <util/optional.h>
 
-// clang-format off
-#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS                              \
-  "(memory-snapshot):"                                                         \
-  "(initial-location):"                                                        \
-  "(havoc-variables):" // MEMORY_SNAPSHOT_HARNESS_GENERATOR_OPTIONS
-// clang-format on
-
-// clang-format off
-#define MEMORY_SNAPSHOT_HARNESS_GENERATOR_HELP                                 \
-  "memory snapshot harness generator (--harness-type\n"                        \
-  "  initialise-from-memory-snapshot)\n\n"                                     \
-  "--memory-snapshot <file>      initialise memory from JSON memory snapshot\n"\
-  "--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
-
 /// Generates a harness which first assigns global variables with values from
 /// a given memory snapshot and then calls a specified function. The called
 /// function is also modified such that it appears to start executing at the
@@ -164,6 +145,8 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   std::unordered_set<irep_idt> variables_to_havoc;
 
   message_handlert &message_handler;
+
+  recursive_initialization_configt recursive_initialization_config;
 };
 
 #endif // CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H