Pull out the common logic for default step types

Previously the JSON and XML trace printing was duplicating the logic for
determing whether a trace step is a loop head

Author: Thomas Kiley

src/goto-programs/Makefile

@@ -64,6 +64,7 @@ SRC = adjust_float_expressions.cpp \
       slice_global_inits.cpp \
       string_abstraction.cpp \
       string_instrumentation.cpp \
+      structured_trace_util.cpp \
       system_library_symbols.cpp \
       validate_goto_model.cpp \
       vcd_goto_trace.cpp \

src/goto-programs/json_goto_trace.cpp

@@ -284,15 +284,17 @@ void convert_return(
 /// \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
 void convert_default(
   json_objectt &json_location_only,
   const conversion_dependenciest &conversion_dependencies,
-  const std::string &step_type)
+  const default_step_kindt &step_kind)
 {
   const goto_trace_stept &step = conversion_dependencies.step;
   const jsont &location = conversion_dependencies.location;
 
-  json_location_only["stepType"] = json_stringt(step_type);
+  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;

src/goto-programs/json_goto_trace.h

@@ -15,6 +15,7 @@ Date: November 2005
 #define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
 
 #include "goto_trace.h"
+#include "structured_trace_util.h"
 
 #include <algorithm>
 #include <util/invariant.h>
@@ -101,7 +102,7 @@ void convert_return(
 void convert_default(
   json_objectt &json_location_only,
   const conversion_dependenciest &conversion_dependencies,
-  const std::string &step_type);
+  const default_step_kindt &step_kind);
 
 /// Templated version of the conversion method.
 /// Works by dispatching to the more specialised
@@ -188,17 +189,14 @@ void convert(
     case goto_trace_stept::typet::SHARED_WRITE:
     case goto_trace_stept::typet::CONSTRAINT:
     case goto_trace_stept::typet::NONE:
-      const bool is_loophead = std::any_of(
-        step.pc->incoming_edges.begin(),
-        step.pc->incoming_edges.end(),
-        [](goto_programt::targett t) { return t->is_backwards_goto(); });
-      if(source_location != previous_source_location || is_loophead)
+      const auto default_step_kind = ::default_step_kind(*step.pc);
+      if(
+        source_location != previous_source_location ||
+        default_step_kind == default_step_kindt::LOOP_HEAD)
       {
         json_objectt &json_location_only = dest_array.push_back().make_object();
         convert_default(
-          json_location_only,
-          conversion_dependencies,
-          is_loophead ? "loop-head" : "location-only");
+          json_location_only, conversion_dependencies, default_step_kind);
       }
     }
 

src/goto-programs/structured_trace_util.cpp

@@ -0,0 +1,35 @@
+/*******************************************************************\
+
+Author: Diffblue
+
+\*******************************************************************/
+
+/// \file
+/// Utilities for printing location info steps in the trace in a format
+/// agnostic way
+
+#include "structured_trace_util.h"
+#include <algorithm>
+
+default_step_kindt
+default_step_kind(const goto_programt::instructiont &instruction)
+{
+  const bool is_loophead = std::any_of(
+    instruction.incoming_edges.begin(),
+    instruction.incoming_edges.end(),
+    [](goto_programt::targett t) { return t->is_backwards_goto(); });
+
+  return is_loophead ? default_step_kindt::LOOP_HEAD
+                     : default_step_kindt::LOCATION_ONLY;
+}
+std::string default_step_name(const default_step_kindt &step_type)
+{
+  switch(step_type)
+  {
+  case default_step_kindt::LOCATION_ONLY:
+    return "location-only";
+  case default_step_kindt::LOOP_HEAD:
+    return "loop-head";
+  }
+  UNREACHABLE;
+}

src/goto-programs/structured_trace_util.h

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Author: Diffblue
+
+\*******************************************************************/
+
+/// \file
+/// Utilities for printing location info steps in the trace in a format
+/// agnostic way
+
+#ifndef CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
+#define CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H
+
+#include "goto_program.h"
+#include <string>
+
+/// There are two kinds of step for location markers - location-only and
+/// loop-head (for locations associated with the first step of a loop).
+enum class default_step_kindt
+{
+  LOCATION_ONLY,
+  LOOP_HEAD
+};
+
+/// Identify for a given instruction whether it is a loophead or just a location
+///
+/// Loopheads are determined by whether there is backwards jump to them. This
+/// matches the loop detection used for loop IDs
+/// \param instruction: The instruction to inspect.
+/// \return LOOP_HEAD if this is a loop head, otherwise LOCATION_ONLY
+default_step_kindt
+default_step_kind(const goto_programt::instructiont &instruction);
+
+/// Turns a \ref default_step_kindt into a string that can be used in the trace
+/// \param step_type: The kind of step, deduced from \ref default_step_kind
+/// \return  Either "loop-head" or "location-only"
+std::string default_step_name(const default_step_kindt &step_type);
+
+#endif // CPROVER_GOTO_PROGRAMS_STRUCTURED_TRACE_UTIL_H

src/goto-programs/xml_goto_trace.cpp

@@ -18,11 +18,11 @@ Author: Daniel Kroening
 #include <util/symbol.h>
 #include <util/xml_irep.h>
 
-#include <algorithm>
 #include <langapi/language_util.h>
 #include <util/arith_tools.h>
 
 #include "printf_formatter.h"
+#include "structured_trace_util.h"
 #include "xml_expr.h"
 
 bool full_lhs_value_includes_binary(
@@ -245,16 +245,15 @@ void convert(
       // 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 bool is_loophead = std::any_of(
-        step.pc->incoming_edges.begin(),
-        step.pc->incoming_edges.end(),
-        [](goto_programt::targett t) { return t->is_backwards_goto(); });
-      if(source_location != previous_source_location || is_loophead)
+      const auto default_step_kind = ::default_step_kind(*step.pc);
+      if(
+        source_location != previous_source_location ||
+        default_step_kind == default_step_kindt::LOOP_HEAD)
       {
         if(!xml_location.name.empty())
         {
           xmlt &xml_location_only =
-            dest.new_element(is_loophead ? "loop-head" : "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(