Introduce wrappers for entry location

Two kinds of user specification: either via goto location or via source line. We
wrap these in entry_goto/source_locationt and build the production of the final
entry_locationt.

Author: Petr Bauch

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -6,6 +6,8 @@ Author: Daniel Poetzl
 
 \******************************************************************/
 
+#include <algorithm>
+
 #include "memory_snapshot_harness_generator.h"
 
 #include <goto-programs/goto_convert.h>
@@ -350,3 +352,133 @@ void memory_snapshot_harness_generatort::generate(
 
   goto_functions.update();
 }
+
+memory_snapshot_harness_generatort::entry_goto_locationt
+memory_snapshot_harness_generatort::parse_goto_location(
+  const std::string &cmdl_option)
+{
+  std::vector<std::string> start;
+  split_string(cmdl_option, ':', start, true);
+
+  if(
+    start.empty() || start.front().empty() ||
+    (start.size() == 2 && start.back().empty()) || start.size() > 2)
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "invalid initial location specification", "--initial-location");
+  }
+
+  if(start.size() == 2)
+  {
+    const auto location_number = string2optional_unsigned(start.back());
+    CHECK_RETURN(location_number.has_value());
+    return entry_goto_locationt{start.front(), *location_number};
+  }
+  else
+  {
+    return entry_goto_locationt{start.front()};
+  }
+}
+
+memory_snapshot_harness_generatort::entry_source_locationt
+memory_snapshot_harness_generatort::parse_source_location(
+  const std::string &cmdl_option)
+{
+  std::string initial_file_string;
+  std::string initial_line_string;
+  split_string(
+    cmdl_option, ':', initial_file_string, initial_line_string, true);
+
+  if(initial_file_string.empty() || initial_line_string.empty())
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "invalid initial location specification", "--initial-file-line");
+  }
+
+  const auto line_number = string2optional_unsigned(initial_line_string);
+  CHECK_RETURN(line_number.has_value());
+  return entry_source_locationt{initial_file_string, *line_number};
+}
+
+memory_snapshot_harness_generatort::entry_locationt
+memory_snapshot_harness_generatort::initialize_entry_via_goto(
+  const entry_goto_locationt &entry_goto_location,
+  const goto_functionst &goto_functions)
+{
+  PRECONDITION(!entry_goto_location.function_name.empty());
+  const irep_idt &function_name = entry_goto_location.function_name;
+
+  // by function(+location): search for the function then jump to n-th
+  // location, then check the number
+  const auto &goto_function =
+    goto_functions.function_map.find(entry_goto_location.function_name);
+  if(
+    goto_function != goto_functions.function_map.end() &&
+    goto_function->second.body_available())
+  {
+    const auto &goto_program = goto_function->second.body;
+
+    const auto corresponding_instruction =
+      entry_goto_location.find_first_corresponding_instruction(
+        goto_program.instructions);
+
+    if(corresponding_instruction != goto_program.instructions.end())
+      return entry_locationt{function_name, corresponding_instruction};
+  }
+  throw invalid_command_line_argument_exceptiont(
+    "could not find the specified entry point", "--initial-goto-location");
+}
+
+memory_snapshot_harness_generatort::entry_locationt
+memory_snapshot_harness_generatort::initialize_entry_via_source(
+  const entry_source_locationt &entry_source_location,
+  const goto_functionst &goto_functions)
+{
+  PRECONDITION(!entry_source_location.file_name.empty());
+
+  // by line: iterate over all instructions until source location match
+  for(const auto &entry : goto_functions.function_map)
+  {
+    const auto &goto_function = entry.second;
+    // if !body_available() then body.instruction.empty() and that's fine
+    const auto &goto_program = goto_function.body;
+
+    const auto corresponding_instruction =
+      entry_source_location.find_first_corresponding_instruction(
+        goto_program.instructions);
+
+    if(corresponding_instruction != goto_program.instructions.end())
+      return entry_locationt{entry.first, corresponding_instruction};
+  }
+  throw invalid_command_line_argument_exceptiont(
+    "could not find the specified entry point", "--initial-source-location");
+}
+
+goto_programt::const_targett memory_snapshot_harness_generatort::
+  entry_goto_locationt::find_first_corresponding_instruction(
+    const goto_programt::instructionst &instructions) const
+{
+  if(!location_number.has_value())
+    return instructions.begin();
+
+  return std::find_if(
+    instructions.begin(),
+    instructions.end(),
+    [this](const goto_programt::instructiont &instruction) {
+      return *location_number == instruction.location_number;
+    });
+}
+
+goto_programt::const_targett memory_snapshot_harness_generatort::
+  entry_source_locationt::find_first_corresponding_instruction(
+    const goto_programt::instructionst &instructions) const
+{
+  return std::find_if(
+    instructions.begin(),
+    instructions.end(),
+    [this](const goto_programt::instructiont &instruction) {
+      return instruction.source_location.get_file() == file_name &&
+             safe_string2unsigned(id2string(
+               instruction.source_location.get_line())) >= line_number;
+    });
+}

src/goto-harness/memory_snapshot_harness_generator.h

@@ -69,6 +69,103 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
     override;
 
 protected:
+  /// User provided goto location: function name and (maybe) location number;
+  /// the structure wraps this option with a parser
+  struct entry_goto_locationt
+  {
+    irep_idt function_name;
+    optionalt<unsigned> location_number;
+
+    entry_goto_locationt() = delete;
+    explicit entry_goto_locationt(irep_idt function_name)
+      : function_name(function_name)
+    {
+    }
+    explicit entry_goto_locationt(
+      irep_idt function_name,
+      unsigned location_number)
+      : function_name(function_name), location_number(location_number)
+    {
+    }
+
+    /// Returns the first \ref goto_programt::instructiont represented by this
+    ///   goto location, i.e. if there is no location number then the first
+    ///   instruction, otherwise the one with the right location number
+    /// \param instructions: list of instructions to be searched
+    /// \return iterator to the right instruction (or `end()`)
+    goto_programt::const_targett find_first_corresponding_instruction(
+      const goto_programt::instructionst &instructions) const;
+  };
+
+  /// Parse a command line option to extract the user specified entry goto
+  ///   location
+  /// \param cmdl_option: a string of the format <func[:<n>]>
+  /// \return correctly constructed entry goto location
+  entry_goto_locationt parse_goto_location(const std::string &cmdl_option);
+
+  /// User provided source location: file name and line number; the structure
+  /// wraps this option with a parser
+  struct entry_source_locationt
+  {
+    irep_idt file_name;
+    unsigned line_number;
+
+    entry_source_locationt() = delete;
+    explicit entry_source_locationt(irep_idt file_name, unsigned line_number)
+      : file_name(file_name), line_number(line_number)
+    {
+    }
+
+    /// Returns the first \ref goto_programt::instructiont represented by this
+    ///   source location, i.e. one with the same file name and line number
+    /// \param instructions: list of instructions to be searched
+    /// \return iterator to the right instruction (or `end()`)
+    goto_programt::const_targett find_first_corresponding_instruction(
+      const goto_programt::instructionst &instructions) const;
+  };
+
+  /// Parse a command line option to extract the user specified entry source
+  ///   location
+  /// \param cmdl_option: a string of the format <file:n>
+  /// \return correctly constructed entry source location
+  entry_source_locationt parse_source_location(const std::string &cmdl_option);
+
+  /// Wraps the information needed to identify the entry point. Initializes via
+  /// either \ref entry_goto_locationt or \ref entry_source_locationt
+  struct entry_locationt
+  {
+    irep_idt function_name;
+    goto_programt::const_targett start_instruction;
+
+    entry_locationt() = default;
+    explicit entry_locationt(
+      irep_idt function_name,
+      goto_programt::const_targett start_instruction)
+      : function_name(function_name), start_instruction(start_instruction)
+    {
+    }
+  };
+
+  /// Find and return the entry instruction (requested by the user as goto
+  ///   location: function name + location number)
+  /// \param entry_goto_location: user specified goto location
+  /// \param goto_functions: goto functions to be searched for the entry
+  ///   instruction
+  /// \return the correctly constructed entry location
+  entry_locationt initialize_entry_via_goto(
+    const entry_goto_locationt &entry_goto_location,
+    const goto_functionst &goto_functions);
+
+  /// Find and return the entry instruction (requested by the user as source
+  ///   location: file name + line number)
+  /// \param entry_source_location: user specified goto location
+  /// \param goto_functions: goto functions to be searched for the entry
+  ///   instruction
+  /// \return the correctly constructed entry location
+  entry_locationt initialize_entry_via_source(
+    const entry_source_locationt &entry_source_location,
+    const goto_functionst &goto_functions);
+
   /// Collect the memory-snapshot specific cmdline options (one at a time)
   /// \param option: memory-snapshot | initial-location | havoc-variables
   /// \param values: list of arguments related to a given option
@@ -155,6 +252,9 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   optionalt<unsigned> location_number;
   std::unordered_set<irep_idt> variables_to_havoc;
 
+  /// data to initialize the entry function
+  entry_locationt entry_location;
+
   message_handlert &message_handler;
 };