Merge pull request #4946 from xbauch/fix/snapshot-source-location

Fix snapshot harness source location initialisation

Author: tautschnig

regression/snapshot-harness/simple-source-location/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+int global_var;
+
+void initialize()
+{
+  global_var = 1;
+}
+
+void checkpoint()
+{
+}
+
+int foo()
+{
+  initialize();
+  checkpoint();
+
+  assert(global_var == 0);
+  //line to be used for init (20)
+  assert(global_var == 0);
+
+  return 0;
+}
+
+int main()
+{
+  foo();
+
+  return 0;
+}

regression/snapshot-harness/simple-source-location/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+global_var --harness-type initialise-with-memory-snapshot --initial-source-location main.c:20
+^EXIT=10$
+^SIGNAL=0$
+^\[foo.assertion.1\] line [0-9]+ assertion global_var == 0: SUCCESS$
+^\[foo.assertion.2\] line [0-9]+ assertion global_var == 0: FAILURE$
+VERIFICATION FAILED
+--
+^warning: ignoring
+--
+The first assertion is succeeding because unreachable.

regression/snapshot-harness/structs_02/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+
+struct S
+{
+  int c1;
+  int c2;
+} st;
+
+int *p;
+
+void initialize()
+{
+  st.c1 = 1;
+  st.c2 = 3;
+  p = &(st.c2);
+}
+
+void checkpoint()
+{
+}
+
+int foo()
+{
+  initialize();
+  checkpoint();
+
+  assert(st.c1 + 2 == st.c2);
+  assert(st.c1 + 2 == *p);
+  assert(*p == st.c2);
+  *p = st.c2 + 1;
+  assert(*p == st.c2);
+
+  return 0;
+}
+
+int main()
+{
+  foo();
+
+  return 0;
+}

regression/snapshot-harness/structs_02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+st,p --harness-type initialise-with-memory-snapshot --initial-source-location main.c:27
+^EXIT=0$
+^SIGNAL=0$
+\[foo.assertion.1\] line [0-9]+ assertion st.c1 \+ 2 == st.c2: SUCCESS
+\[foo.assertion.2\] line [0-9]+ assertion st.c1 \+ 2 == \*p: SUCCESS
+\[foo.assertion.3\] line [0-9]+ assertion \*p == st.c2: SUCCESS
+\[foo.assertion.4\] line [0-9]+ assertion \*p == st.c2: SUCCESS
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -504,22 +504,30 @@ memory_snapshot_harness_generatort::initialize_entry_via_source(
 {
   PRECONDITION(!entry_source_location.file_name.empty());
 
+  source_location_matcht best_match;
   // 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 =
+    const auto candidate_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};
+    if(candidate_instruction.first != goto_program.instructions.end())
+    {
+      best_match.match_up(
+        candidate_instruction.second, entry.first, candidate_instruction.first);
+    }
   }
-  throw invalid_command_line_argument_exceptiont(
-    "could not find the specified entry point", "--initial-source-location");
+
+  if(best_match.match_found)
+    return entry_locationt{best_match.function_name, best_match.instruction};
+  else
+    throw invalid_command_line_argument_exceptiont(
+      "could not find the specified entry point", "--initial-source-location");
 }
 
 goto_programt::const_targett memory_snapshot_harness_generatort::
@@ -537,16 +545,24 @@ goto_programt::const_targett memory_snapshot_harness_generatort::
     });
 }
 
-goto_programt::const_targett memory_snapshot_harness_generatort::
-  entry_source_locationt::find_first_corresponding_instruction(
+std::pair<goto_programt::const_targett, size_t>
+memory_snapshot_harness_generatort::entry_source_locationt::
+  find_first_corresponding_instruction(
     const goto_programt::instructionst &instructions) const
 {
-  return std::find_if(
+  auto it = 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;
     });
+
+  if(it == instructions.end())
+    return {it, 0};
+  else
+    return {it,
+            safe_string2unsigned(id2string(it->source_location.get_line())) -
+              line_number};
 }

src/goto-harness/memory_snapshot_harness_generator.h

@@ -97,8 +97,10 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
     /// 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(
+    /// \return <iterator to the right instruction (or `end()`), distance to
+    ///   `line_number`>
+    std::pair<goto_programt::const_targett, size_t>
+    find_first_corresponding_instruction(
       const goto_programt::instructionst &instructions) const;
   };
 
@@ -124,6 +126,35 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
     }
   };
 
+  /// Wraps the information for source location match candidates. Keeps track of
+  /// the distance between user specified source code line and goto-program
+  /// instruction line.
+  struct source_location_matcht
+  {
+    size_t distance;
+    irep_idt function_name;
+    goto_programt::const_targett instruction;
+    bool match_found;
+
+    source_location_matcht() : distance(0), match_found(false)
+    {
+    }
+
+    void match_up(
+      const size_t &candidate_distance,
+      const irep_idt &candidate_function_name,
+      const goto_programt::const_targett &candidate_instruction)
+    {
+      if(match_found && distance <= candidate_distance)
+        return;
+
+      match_found = true;
+      distance = candidate_distance;
+      function_name = candidate_function_name;
+      instruction = candidate_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