Pull out function for processing the default trace step

This models the logic for whether a trace step should be included away
from whether the format is json or XML

Author: Thomas Kiley

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;
     }
     }