Add loopheads to the JSON output

Author: Thomas Kiley

regression/cbmc/loophead-trace/test-json.desc

@@ -0,0 +1,37 @@
+CORE
+test.c
+--unwind 6 test.c --trace --json-ui --partial-loops --slice-formula
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+\s*\{\n\s*  .*\n\s*  "sourceLocation": \{\n\s*    .*,\n\s*    .*,\n\s*    "line": "5",\n\s*    .*\n\s*  \},\n\s*  "stepType": "loop-head",\n\s*  .*\n\s*\},\n\s*\{\n\s*  .*\n\s*  "sourceLocation": \{\n\s*    .*,\n\s*    .*,\n\s*    "line": "5",\n\s*    .*\n\s*  \},\n\s*  "stepType": "loop-head",\n\s*  .*\n\s*\},
+--
+--
+Ensure even with sliced formulas, we get a location only step for
+each iteration of the loop (called loop-heads) when using partial loops.
+
+This test is checking the following json:(deleting the new lines after each \n to obtain
+monster regex above).
+
+\s*\{\n
+\s*  .*\n
+\s*  "sourceLocation": \{\n
+\s*    .*,\n
+\s*    .*,\n
+\s*    "line": "5",\n
+\s*    .*\n
+\s*  \},\n
+\s*  "stepType": "loop-head",\n
+\s*  .*\n
+\s*\},\n
+\s*\{\n
+\s*  .*\n
+\s*  "sourceLocation": \{\n
+\s*    .*,\n
+\s*    .*,\n
+\s*    "line": "5",\n
+\s*    .*\n
+\s*  \},\n
+\s*  "stepType": "loop-head",\n
+\s*  .*\n
+\s*\},

src/goto-programs/json_goto_trace.cpp

@@ -286,12 +286,13 @@ void convert_return(
 ///   needs.
 void convert_default(
   json_objectt &json_location_only,
-  const conversion_dependenciest &conversion_dependencies)
+  const conversion_dependenciest &conversion_dependencies,
+  const std::string &step_type)
 {
   const goto_trace_stept &step = conversion_dependencies.step;
   const jsont &location = conversion_dependencies.location;
 
-  json_location_only["stepType"] = json_stringt("location-only");
+  json_location_only["stepType"] = json_stringt(step_type);
   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

@@ -16,6 +16,7 @@ Date: November 2005
 
 #include "goto_trace.h"
 
+#include <algorithm>
 #include <util/invariant.h>
 #include <util/json.h>
 #include <util/json_irep.h>
@@ -99,7 +100,8 @@ void convert_return(
 ///   needs.
 void convert_default(
   json_objectt &json_location_only,
-  const conversion_dependenciest &conversion_dependencies);
+  const conversion_dependenciest &conversion_dependencies,
+  const std::string &step_type);
 
 /// Templated version of the conversion method.
 /// Works by dispatching to the more specialised
@@ -186,10 +188,17 @@ void convert(
     case goto_trace_stept::typet::SHARED_WRITE:
     case goto_trace_stept::typet::CONSTRAINT:
     case goto_trace_stept::typet::NONE:
-      if(source_location != previous_source_location)
+      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)
       {
         json_objectt &json_location_only = dest_array.push_back().make_object();
-        convert_default(json_location_only, conversion_dependencies);
+        convert_default(
+          json_location_only,
+          conversion_dependencies,
+          is_loophead ? "loop-head" : "location-only");
       }
     }