Reflect the existence of wrappers

Most of the sanity checks are in the wrappers and the `get_target` function is
now redundant.

Author: petr-bauch

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -66,106 +66,51 @@ void memory_snapshot_harness_generatort::validate_options(
       "--harness-type initialise-from-memory-snapshot");
   }
 
-  if(entry_function_name.empty())
+  if(initial_source_location_line.empty() == initial_goto_location_line.empty())
   {
-    INVARIANT(
-      !location_number.has_value(),
-      "when `function` is empty then the option --initial-location was not "
-      "given and thus `location_number` was not set");
-
     throw invalid_command_line_argument_exceptiont(
-      "option --initial-location is required",
-      "--harness-type initialise-from-memory-snapshot");
+      "choose either source or goto location to specify the entry point",
+      "--initial-source/goto-location");
   }
 
-  const auto &goto_functions = goto_model.goto_functions;
-  const auto &goto_function =
-    goto_functions.function_map.find(entry_function_name);
-  if(goto_function == goto_functions.function_map.end())
+  if(!initial_source_location_line.empty())
   {
-    throw invalid_command_line_argument_exceptiont(
-      "unknown initial location specification", "--initial-location");
+    entry_location = initialize_entry_via_source(
+      parse_source_location(initial_source_location_line),
+      goto_model.goto_functions);
   }
-
-  if(!goto_function->second.body_available())
-  {
-    throw invalid_command_line_argument_exceptiont(
-      "given function `" + id2string(entry_function_name) +
-        "` does not have a body",
-      "--initial-location");
-  }
-
-  if(location_number.has_value())
-  {
-    const auto &goto_program = goto_function->second.body;
-    const auto opt_it = goto_program.get_target(*location_number);
-
-    if(!opt_it.has_value())
-    {
-      throw invalid_command_line_argument_exceptiont(
-        "no instruction with location number " +
-          std::to_string(*location_number) + " in function " +
-          id2string(entry_function_name),
-        "--initial-location");
-    }
-  }
-
-  if(goto_functions.function_map.count(INITIALIZE_FUNCTION) == 0)
+  else
   {
-    throw invalid_command_line_argument_exceptiont(
-      "invalid input program: " + std::string(INITIALIZE_FUNCTION) +
-        " not found",
-      "<in>");
+    entry_location = initialize_entry_via_goto(
+      parse_goto_location(initial_goto_location_line),
+      goto_model.goto_functions);
   }
 
   const symbol_tablet &symbol_table = goto_model.symbol_table;
+
   const symbolt *called_function_symbol =
-    symbol_table.lookup(entry_function_name);
+    symbol_table.lookup(entry_location.function_name);
 
   if(called_function_symbol == nullptr)
   {
     throw invalid_command_line_argument_exceptiont(
-      "function `" + id2string(entry_function_name) +
+      "function `" + id2string(entry_location.function_name) +
         "` not found in the symbol table",
       "--initial-location");
   }
 }
 
 void memory_snapshot_harness_generatort::add_init_section(
+  const symbol_exprt &func_init_done_var,
   goto_modelt &goto_model) const
 {
   goto_functionst &goto_functions = goto_model.goto_functions;
-  symbol_tablet &symbol_table = goto_model.symbol_table;
 
   goto_functiont &goto_function =
-    goto_functions.function_map[entry_function_name];
-  const symbolt &function_symbol = symbol_table.lookup_ref(entry_function_name);
+    goto_functions.function_map[entry_location.function_name];
 
   goto_programt &goto_program = goto_function.body;
 
-  // introduce a symbol for a Boolean variable to indicate the point at which
-  // the function initialisation is completed
-  symbolt &func_init_done_symbol = get_fresh_aux_symbol(
-    bool_typet(),
-    id2string(entry_function_name),
-    "func_init_done",
-    function_symbol.location,
-    function_symbol.mode,
-    symbol_table);
-  func_init_done_symbol.is_static_lifetime = true;
-  func_init_done_symbol.value = false_exprt();
-
-  const symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
-
-  // initialise func_init_done_var in __CPROVER_initialize if it is present
-  // so that it's FALSE value is visible before the harnessed function is called
-  goto_programt &cprover_initialize =
-    goto_functions.function_map.find(INITIALIZE_FUNCTION)->second.body;
-  cprover_initialize.insert_before(
-    std::prev(cprover_initialize.instructions.end()),
-    goto_programt::make_assignment(
-      code_assignt(func_init_done_var, false_exprt())));
-
   const goto_programt::const_targett start_it =
     goto_program.instructions.begin();
 
@@ -182,9 +127,8 @@ void memory_snapshot_harness_generatort::add_init_section(
   goto_program.compute_location_numbers();
   goto_program.insert_after(
     ins_it2,
-    goto_programt::make_goto(goto_program.const_cast_target(
-      location_number.has_value() ? *goto_program.get_target(*location_number)
-                                  : start_it)));
+    goto_programt::make_goto(
+      goto_program.const_cast_target(entry_location.start_instruction)));
 }
 
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
@@ -310,13 +254,28 @@ void memory_snapshot_harness_generatort::generate(
   goto_functionst &goto_functions = goto_model.goto_functions;
 
   const symbolt *called_function_symbol =
-    symbol_table.lookup(entry_function_name);
+    symbol_table.lookup(entry_location.function_name);
+
+  // introduce a symbol for a Boolean variable to indicate the point at which
+  // the function initialisation is completed
+  auto &func_init_done_symbol = get_fresh_aux_symbol(
+    bool_typet(),
+    id2string(entry_location.function_name),
+    "func_init_done",
+    source_locationt::nil(),
+    called_function_symbol->mode,
+    symbol_table);
+  func_init_done_symbol.is_static_lifetime = true;
+  func_init_done_symbol.value = false_exprt();
+  symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
 
-  add_init_section(goto_model);
+  add_init_section(func_init_done_var, goto_model);
 
   code_blockt harness_function_body =
     add_assignments_to_globals(snapshot, goto_model);
 
+  harness_function_body.add(code_assignt{func_init_done_var, false_exprt{}});
+
   add_call_with_nondet_arguments(
     *called_function_symbol, harness_function_body);
 

src/goto-harness/memory_snapshot_harness_generator.h

@@ -99,7 +99,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
 
   /// Parse a command line option to extract the user specified entry goto
   ///   location
-  /// \param cmdl_option: a string of the format <func[:<n>]>
+  /// \param cmdl_option: a string of the format `name:number`
   /// \return correctly constructed entry goto location
   entry_goto_locationt parse_goto_location(const std::string &cmdl_option);
 
@@ -126,7 +126,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
 
   /// Parse a command line option to extract the user specified entry source
   ///   location
-  /// \param cmdl_option: a string of the format <file:n>
+  /// \param cmdl_option: a string of the format `name:number`
   /// \return correctly constructed entry source location
   entry_source_locationt parse_source_location(const std::string &cmdl_option);
 
@@ -214,8 +214,12 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   ///     ..second_part..
   ///   }
   ///
+  /// \param func_init_done_var: symbol expression for the `func_init_done`
+  ///   variable
   /// \param goto_model: Model where the modification takes place
-  void add_init_section(goto_modelt &goto_model) const;
+  void add_init_section(
+    const symbol_exprt &func_init_done_var,
+    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 \p snapshot to the

src/goto-programs/goto_program.h

@@ -588,28 +588,6 @@ class goto_programt
     return t;
   }
 
-  optionalt<const_targett> get_target(const unsigned location_number) const
-  {
-    PRECONDITION(!instructions.empty());
-
-    const unsigned start_location_number = instructions.front().location_number;
-
-    if(
-      location_number < start_location_number ||
-      location_number > instructions.back().location_number)
-    {
-      return nullopt;
-    }
-
-    auto location_target =
-      std::next(instructions.begin(), location_number - start_location_number);
-
-    // location numbers are contiguous unless new instructions are inserted
-    // here we check that nobody inserted any instruction into our function
-    CHECK_RETURN(location_target->location_number == location_number);
-    return location_target;
-  }
-
   template <typename Target>
   std::list<Target> get_successors(Target target) const;