Refactor trace loop heads

src/goto-programs/json_goto_trace.cpp

@@ -278,14 +278,12 @@ void convert_return(
 
 void convert_default(
   json_objectt &json_location_only,
-  const conversion_dependenciest &conversion_dependencies,
-  const default_step_kindt &step_kind)
+  const default_trace_stept &default_step)
 {
-  const goto_trace_stept &step = conversion_dependencies.step;
-  const jsont &location = conversion_dependencies.location;
-
-  json_location_only["stepType"] = json_stringt(default_step_name(step_kind));
-  json_location_only["hidden"] = jsont::json_boolean(step.hidden);
-  json_location_only["thread"] = json_numbert(std::to_string(step.thread_nr));
-  json_location_only["sourceLocation"] = location;
+  json_location_only["stepType"] =
+    json_stringt(default_step_name(default_step.kind));
+  json_location_only["hidden"] = jsont::json_boolean(default_step.hidden);
+  json_location_only["thread"] =
+    json_numbert(std::to_string(default_step.thread_number));
+  json_location_only["sourceLocation"] = json(default_step.location);
 }

src/goto-programs/json_goto_trace.h

@@ -96,15 +96,11 @@ void convert_return(
 /// \param [out] json_location_only: The JSON object that
 ///   will contain the information about the step
 ///   after this function has run.
-/// \param conversion_dependencies: A structure
-///   that contains information the conversion function
-///   needs.
-/// \param step_kind: The kind of default step we are printing.
-///   See \ref default_step_kind
+/// \param default_step: The procesed details about this step, see \ref
+///   default_step_kind
 void convert_default(
   json_objectt &json_location_only,
-  const conversion_dependenciest &conversion_dependencies,
-  const default_step_kindt &step_kind);
+  const default_trace_stept &default_step);
 
 /// Templated version of the conversion method.
 /// Works by dispatching to the more specialised
@@ -191,15 +187,13 @@ void convert(
     case goto_trace_stept::typet::SHARED_WRITE:
     case goto_trace_stept::typet::CONSTRAINT:
     case goto_trace_stept::typet::NONE:
-      const auto default_step_kind = ::default_step_kind(*step.pc);
-      if(
-        source_location != previous_source_location ||
-        default_step_kind == default_step_kindt::LOOP_HEAD)
+      const auto default_step = ::default_step(step, previous_source_location);
+      if(default_step)
       {
         json_objectt &json_location_only = dest_array.push_back().make_object();
-        convert_default(
-          json_location_only, conversion_dependencies, default_step_kind);
+        convert_default(json_location_only, *default_step);
       }
+      break;
     }
 
     if(source_location.is_not_nil() && !source_location.get_file().empty())

src/goto-programs/structured_trace_util.cpp

@@ -9,6 +9,8 @@ Author: Diffblue
 /// agnostic way
 
 #include "structured_trace_util.h"
+#include "goto_trace.h"
+
 #include <algorithm>
 
 default_step_kindt
@@ -33,3 +35,33 @@ std::string default_step_name(const default_step_kindt &step_type)
   }
   UNREACHABLE;
 }
+
+optionalt<default_trace_stept> default_step(
+  const goto_trace_stept &step,
+  const source_locationt &previous_source_location)
+{
+  const source_locationt &source_location = step.pc->source_location;
+  if(source_location.is_nil() || source_location.get_file().empty())
+    return {};
+
+  const auto default_step_kind = ::default_step_kind(*step.pc);
+
+  // If this is just a source location then we output only the first
+  // location of a sequence of same locations.
+  // However, we don't want to suppress loop head locations because
+  // they might come from different loop iterations. If we suppressed
+  // them it would be impossible to know which loop iteration
+  // we are in.
+  if(
+    source_location == previous_source_location &&
+    default_step_kind == default_step_kindt::LOCATION_ONLY)
+  {
+    return {};
+  }
+
+  return default_trace_stept{default_step_kind,
+                             step.hidden,
+                             step.thread_nr,
+                             step.step_nr,
+                             source_location};
+}

src/goto-programs/structured_trace_util.h

@@ -13,6 +13,7 @@ Author: Diffblue
 
 #include "goto_program.h"
 #include <string>
+class goto_trace_stept;
 
 /// There are two kinds of step for location markers - location-only and
 /// loop-head (for locations associated with the first step of a loop).
@@ -36,4 +37,17 @@ default_step_kind(const goto_programt::instructiont &instruction);
 /// \return  Either "loop-head" or "location-only"
 std::string default_step_name(const default_step_kindt &step_type);
 
+struct default_trace_stept
+{
+  default_step_kindt kind;
+  bool hidden;
+  unsigned thread_number;
+  std::size_t step_number;
+  source_locationt location;
+};
+
+optionalt<default_trace_stept> default_step(
+  const goto_trace_stept &step,
+  const source_locationt &previous_source_location);
+
 #endif // CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H

src/goto-programs/xml_goto_trace.cpp

@@ -239,31 +239,21 @@ void convert(
     case goto_trace_stept::typet::ASSUME:
     case goto_trace_stept::typet::NONE:
     {
-      // If this is just a source location then we output only the first
-      // location of a sequence of same locations.
-      // However, we don't want to suppress loop head locations because
-      // they might come from different loop iterations. If we suppressed
-      // them it would be impossible to know in which loop iteration
-      // we are in.
-      const auto default_step_kind = ::default_step_kind(*step.pc);
-      if(
-        source_location != previous_source_location ||
-        default_step_kind == default_step_kindt::LOOP_HEAD)
+      const auto default_step = ::default_step(step, previous_source_location);
+      if(default_step)
       {
-        if(!xml_location.name.empty())
-        {
-          xmlt &xml_location_only =
-            dest.new_element(default_step_name(default_step_kind));
+        xmlt &xml_location_only =
+          dest.new_element(default_step_name(default_step->kind));
 
-          xml_location_only.set_attribute_bool("hidden", step.hidden);
-          xml_location_only.set_attribute(
-            "thread", std::to_string(step.thread_nr));
-          xml_location_only.set_attribute(
-            "step_nr", std::to_string(step.step_nr));
+        xml_location_only.set_attribute_bool("hidden", default_step->hidden);
+        xml_location_only.set_attribute(
+          "thread", std::to_string(default_step->thread_number));
+        xml_location_only.set_attribute(
+          "step_nr", std::to_string(default_step->step_number));
 
-          xml_location_only.new_element().swap(xml_location);
-        }
+        xml_location_only.new_element(xml(default_step->location));
       }
+
       break;
     }
     }

unit/Makefile

@@ -35,6 +35,7 @@ SRC += analyses/ai/ai.cpp \
        goto-programs/label_function_pointer_call_sites.cpp \
        goto-programs/osx_fat_reader.cpp \
        goto-programs/restrict_function_pointers.cpp \
+       goto-programs/structured_trace_util.cpp \
        goto-programs/remove_returns.cpp \
        goto-programs/xml_expr.cpp \
        goto-symex/apply_condition.cpp \

unit/goto-programs/structured_trace_util.cpp

@@ -0,0 +1,154 @@
+/*******************************************************************\
+
+Module: structured_trace_util
+
+Author: Diffblue
+
+\*******************************************************************/
+#include <testing-utils/use_catch.h>
+
+#include <goto-programs/goto_trace.h>
+#include <goto-programs/structured_trace_util.h>
+
+void link_edges(goto_programt::targett source, goto_programt::targett target)
+{
+  source->targets.push_back(target);
+  target->incoming_edges.insert(source);
+}
+
+source_locationt simple_location(const std::string &file, unsigned line)
+{
+  source_locationt location;
+  location.set_file(file);
+  location.set_line(line);
+  return location;
+}
+
+goto_programt::targett add_instruction(
+  const source_locationt &location,
+  goto_programt::instructionst &instructions)
+{
+  goto_programt::instructiont instruction;
+  instruction.location_number = instructions.size();
+  instruction.source_location = location;
+  instructions.push_back(instruction);
+  return std::next(instructions.begin(), instruction.location_number);
+}
+
+TEST_CASE("structured_trace_util", "[core][util][trace]")
+{
+  goto_programt::instructionst instructions;
+
+  source_locationt nil_location;
+
+  const source_locationt unrelated_location = simple_location("foo.c", 1);
+
+  source_locationt no_file_location;
+  no_file_location.set_line(1);
+
+  const source_locationt basic_location = simple_location("test.c", 1);
+  const source_locationt loop_head_location = simple_location("test.c", 2);
+  const source_locationt back_edge_location = simple_location("test.c", 3);
+
+  // 0 # normal_location
+  add_instruction(basic_location, instructions);
+  // 1 # loop_head
+  add_instruction(loop_head_location, instructions);
+  // 2: goto 1 # back_edge
+  const auto back_edge = add_instruction(back_edge_location, instructions);
+  back_edge->type = GOTO;
+  // 3: no_location
+  goto_programt::instructiont no_location;
+  no_location.location_number = 3;
+  instructions.push_back(no_location);
+  // 4: no_file
+  add_instruction(no_file_location, instructions);
+
+  link_edges(
+    std::next(instructions.begin(), 2), std::next(instructions.begin(), 1));
+
+  SECTION("location-only steps")
+  {
+    goto_trace_stept step;
+    step.step_nr = 1;
+    step.thread_nr = 2;
+    step.hidden = true;
+    SECTION("Simple step")
+    {
+      step.pc = instructions.begin();
+
+      const auto parsed_step = default_step(step, unrelated_location);
+
+      REQUIRE(parsed_step);
+      REQUIRE(parsed_step->step_number == 1);
+      REQUIRE(parsed_step->thread_number == 2);
+      REQUIRE(parsed_step->hidden);
+      REQUIRE(parsed_step->kind == default_step_kindt::LOCATION_ONLY);
+      REQUIRE(parsed_step->location == basic_location);
+    }
+    SECTION("Invalid previous step")
+    {
+      step.pc = instructions.begin();
+
+      const auto parsed_step = default_step(step, nil_location);
+
+      REQUIRE(parsed_step);
+      REQUIRE(parsed_step->step_number == 1);
+      REQUIRE(parsed_step->thread_number == 2);
+      REQUIRE(parsed_step->hidden);
+      REQUIRE(parsed_step->kind == default_step_kindt::LOCATION_ONLY);
+      REQUIRE(parsed_step->location == basic_location);
+    }
+
+    SECTION("Duplicate step")
+    {
+      step.pc = instructions.begin();
+      const auto parsed_step = default_step(step, basic_location);
+      REQUIRE_FALSE(parsed_step);
+    }
+    SECTION("No source location")
+    {
+      step.pc = std::next(instructions.begin(), 3);
+
+      const auto parsed_step = default_step(step, unrelated_location);
+      REQUIRE_FALSE(parsed_step);
+    }
+    SECTION("No file")
+    {
+      step.pc = std::next(instructions.begin(), 4);
+
+      const auto parsed_step = default_step(step, unrelated_location);
+      REQUIRE_FALSE(parsed_step);
+    }
+  }
+  SECTION("Loop head steps")
+  {
+    goto_trace_stept step;
+    step.step_nr = 1;
+    step.thread_nr = 2;
+    step.hidden = false;
+    step.pc = std::next(instructions.begin(), 1);
+    SECTION("Simple step")
+    {
+      const auto parsed_step = default_step(step, unrelated_location);
+
+      REQUIRE(parsed_step);
+      REQUIRE(parsed_step->step_number == 1);
+      REQUIRE(parsed_step->thread_number == 2);
+      REQUIRE_FALSE(parsed_step->hidden);
+      REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD);
+      REQUIRE(parsed_step->location == loop_head_location);
+    }
+
+    SECTION("Duplicate step")
+    {
+      const auto parsed_step = default_step(step, loop_head_location);
+      REQUIRE(parsed_step);
+      REQUIRE(parsed_step->step_number == 1);
+      REQUIRE(parsed_step->thread_number == 2);
+      REQUIRE_FALSE(parsed_step->hidden);
+      REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD);
+      REQUIRE(parsed_step->location == loop_head_location);
+    }
+  }
+}