Trace loop heads

doc/assets/xml_spec.md

@@ -389,10 +389,18 @@ Function Return (element name: `function_return`)
 </xs:element>
 ```
 
-All Other Steps (element name: `location-only`)
+All Other Steps (element name: `location-only` and `loop-head`)
+
+A step that indicates where in the source program we are.
+
+A `location-only` step is emitted if the source location exists and
+differs from the previous one.
+
+A  `loop-head` step is emitted if the location relates to the start of a loop,
+even if the previous step is also the same start of the loop (to ensure
+that it is printed out for each loop iteration)
+
 
-Only included if the source location exists and differs from the
-previous one.\
 **Attributes**:
 
 -   `hidden`: boolean attribute
@@ -411,6 +419,9 @@ previous one.\
 <location-only hidden="false" step_nr="19" thread="0">
   <location .. />
 </location-only>
+<loop-head hidden="false" step_nr="19" thread="0">
+  <location .. />
+</loop-head>
 ```
 
 **XSD**:
@@ -424,6 +435,15 @@ previous one.\
     <xs:attributeGroup ref="traceStepAttrs">
   </xs:complexType>
 </xs:element>
+
+<xs:element name="loop-head">
+  <xs:complexType>
+    <xs:all>
+      <xs:element name="location" minOccurs="0"></xs:element>
+    </xs:all>
+    <xs:attributeGroup ref="traceStepAttrs">
+  </xs:complexType>
+</xs:element>
 ```
 
 Full Trace XSD
@@ -440,6 +460,7 @@ Full Trace XSD
       <xs:element ref="input"></xs:element>
       <xs:element ref="output"></xs:element>
       <xs:element ref="location-only"></xs:element>
+      <xs:element ref="loop-head"></xs:element>
     </xs:choice>
   </xs:complexType>
 </xs:element>

doc/assets/xml_spec.tex

@@ -373,10 +373,18 @@ \subsection{Trace Steps in XML}
 
 
 \begin{center}
-  {\Large All Other Steps} (element name: \texttt{location-only})
+  {\Large All Other Steps} (element name: \texttt{location-only} and
+\texttt{loop-head})
 \end{center}
 
-\noindent Only included if the source location exists and differs from the previous one.\\
+\noindent A step that indicates where in the source program we are.
+
+A \texttt{location-only} step is emitted if the source location exists and
+differs from the previous one.
+
+A  \texttt{loop-head} step is emitted if the location relates to the start of a loop,
+even if the previous step is also the same start of the loop (to ensure
+that it is printed out for each loop iteration) \\
 
 \noindent\textbf{Attributes}:
 \begin{itemize}
@@ -395,6 +403,9 @@ \subsection{Trace Steps in XML}
 <location-only hidden="false" step_nr="19" thread="0">
   <location .. />
 </location-only>
+<loop-head hidden="false" step_nr="19" thread="0">
+<location .. />
+</loop-head>
 \end{minted}
 
 \noindent\textbf{XSD}:
@@ -407,6 +418,14 @@ \subsection{Trace Steps in XML}
     <xs:attributeGroup ref="traceStepAttrs">
   </xs:complexType>
 </xs:element>
+<xs:element name="loop-head">
+  <xs:complexType>
+    <xs:all>
+      <xs:element name="location" minOccurs="0"></xs:element>
+    </xs:all>
+    <xs:attributeGroup ref="traceStepAttrs">
+  </xs:complexType>
+</xs:element>
 \end{minted}
 
 \subsection{Full Trace XSD}
@@ -422,6 +441,7 @@ \subsection{Full Trace XSD}
       <xs:element ref="input"></xs:element>
       <xs:element ref="output"></xs:element>
       <xs:element ref="location-only"></xs:element>
+      <xs:element ref="loop-head"></xs:element>
     </xs:choice>
   </xs:complexType>
 </xs:element>

doc/assets/xml_spec.xsd

@@ -138,6 +138,15 @@
   </xs:complexType>
 </xs:element>
 
+<xs:element name="loop-head">
+  <xs:complexType>
+    <xs:all>
+      <xs:element ref="location" minOccurs="0"/>
+    </xs:all>
+    <xs:attributeGroup ref="traceStepAttrs"/>
+  </xs:complexType>
+</xs:element>
+
 <xs:element name="goto_trace">
   <xs:complexType>
     <xs:choice minOccurs="0" maxOccurs="unbounded">
@@ -148,6 +157,7 @@
       <xs:element ref="input"></xs:element>
       <xs:element ref="output"></xs:element>
       <xs:element ref="location-only"></xs:element>
+      <xs:element ref="loop-head"></xs:element>
     </xs:choice>
   </xs:complexType>
 </xs:element>

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*\},

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

@@ -0,0 +1,22 @@
+CORE
+test.c
+--unwind 6 test.c --trace --xml-ui --partial-loops --slice-formula
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+\s*<loop-head .*>\n\s*  <location .* line="5" .*/>\n\s*</loop-head>\n\s*<loop-head .*>\n\s*  <location .* line="5".*/>\n\s*</loop-head>\n
+--
+--
+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 XML:(deleting the new lines
+after each \n to obtain the monster regex above).
+
+\s*<loop-head .*>
+\s*  <location .* line="5" .*/>
+\s*</loop-head>
+\s*<loop-head .*>
+\s*  <location .* line="5".*/>
+\s*</loop-head>
+

regression/cbmc/loophead-trace/test.c

@@ -0,0 +1,12 @@
+void main(void)
+{
+  int i = 0;
+
+  while(1)
+  {
+    i = 1;
+  }
+
+  // invalid assertion
+  assert(i == 0);
+}

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

@@ -276,22 +276,15 @@ void convert_return(
     json_call_return["sourceLocation"] = location;
 }
 
-/// Convert all other types of steps not already handled
-/// by the other conversion functions.
-/// \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.
 void convert_default(
   json_objectt &json_location_only,
-  const conversion_dependenciest &conversion_dependencies)
+  const conversion_dependenciest &conversion_dependencies,
+  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("location-only");
+  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,7 +15,9 @@ 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>
 #include <util/json.h>
 #include <util/json_irep.h>
@@ -97,9 +99,12 @@ 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 conversion_dependenciest &conversion_dependencies,
+  const default_step_kindt &step_kind);
 
 /// Templated version of the conversion method.
 /// Works by dispatching to the more specialised
@@ -186,10 +191,14 @@ 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 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);
+        convert_default(
+          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