From 38fd0039bc8bf8863b5be549c1acc19fadee61ac Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 30 May 2020 00:04:21 +0100 Subject: [PATCH 1/6] Do not suppress loop head locations in the trace In the trace, we only output 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. --- src/goto-programs/xml_goto_trace.cpp | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index caf41b1c83d..3cd1dc48255 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening #include #include +#include #include #include @@ -237,12 +238,23 @@ void convert( case goto_trace_stept::typet::GOTO: case goto_trace_stept::typet::ASSUME: case goto_trace_stept::typet::NONE: - if(source_location!=previous_source_location) + { + // 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 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) { - // just the source location if(!xml_location.name.empty()) { - xmlt &xml_location_only=dest.new_element("location-only"); + xmlt &xml_location_only = + dest.new_element(is_loophead ? "loop-head" : "location-only"); xml_location_only.set_attribute_bool("hidden", step.hidden); xml_location_only.set_attribute( @@ -253,6 +265,8 @@ void convert( xml_location_only.new_element().swap(xml_location); } } + break; + } } if(source_location.is_not_nil() && !source_location.get_file().empty()) From 65c8fe2bc0d2e73766c965ec082c66ab370d6023 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 12 Jun 2020 18:28:07 +0100 Subject: [PATCH 2/6] Add tests for checking loop heads Even though the slicing removes all the assignments, the loop heads are maintained in the test --- regression/cbmc/loophead-trace/test-xml.desc | 22 ++++++++++++++++++++ regression/cbmc/loophead-trace/test.c | 12 +++++++++++ 2 files changed, 34 insertions(+) create mode 100644 regression/cbmc/loophead-trace/test-xml.desc create mode 100644 regression/cbmc/loophead-trace/test.c diff --git a/regression/cbmc/loophead-trace/test-xml.desc b/regression/cbmc/loophead-trace/test-xml.desc new file mode 100644 index 00000000000..b039701d87d --- /dev/null +++ b/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*\n\s* \n\s*\n\s*\n\s* \n\s*\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* +\s* +\s* +\s* +\s* +\s* + diff --git a/regression/cbmc/loophead-trace/test.c b/regression/cbmc/loophead-trace/test.c new file mode 100644 index 00000000000..906178e30c0 --- /dev/null +++ b/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); +} From 4ee5f2d5dd2fb348cd743e1435f3ccb30104661b Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 12 Jun 2020 18:42:29 +0100 Subject: [PATCH 3/6] Add loopheads to the JSON output --- regression/cbmc/loophead-trace/test-json.desc | 37 +++++++++++++++++++ src/goto-programs/json_goto_trace.cpp | 5 ++- src/goto-programs/json_goto_trace.h | 15 ++++++-- 3 files changed, 52 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc/loophead-trace/test-json.desc diff --git a/regression/cbmc/loophead-trace/test-json.desc b/regression/cbmc/loophead-trace/test-json.desc new file mode 100644 index 00000000000..9754b659021 --- /dev/null +++ b/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*\}, diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index ca9267f84b5..a25cc64be2e 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/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; diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 3bdc67c6f77..d28a05d5774 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -16,6 +16,7 @@ Date: November 2005 #include "goto_trace.h" +#include #include #include #include @@ -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"); } } From 20f964f5d3ab6f6cd096c35d540b842ab12f7356 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 18 Jun 2020 11:31:43 +0100 Subject: [PATCH 4/6] Update trace docs and spec for the loop-head element Extend the documentation to cover the new version of location-only called loop-head. --- doc/assets/xml_spec.md | 27 ++++++++++++++++++++++++--- doc/assets/xml_spec.tex | 24 ++++++++++++++++++++++-- doc/assets/xml_spec.xsd | 10 ++++++++++ 3 files changed, 56 insertions(+), 5 deletions(-) diff --git a/doc/assets/xml_spec.md b/doc/assets/xml_spec.md index fe3ca41020e..142ef548c4e 100644 --- a/doc/assets/xml_spec.md +++ b/doc/assets/xml_spec.md @@ -389,10 +389,18 @@ Function Return (element name: `function_return`) ``` -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.\ + ``` **XSD**: @@ -424,6 +435,15 @@ previous one.\ + + + + + + + + + ``` Full Trace XSD @@ -440,6 +460,7 @@ Full Trace XSD + diff --git a/doc/assets/xml_spec.tex b/doc/assets/xml_spec.tex index ea78a67e99c..015b8e53dd3 100644 --- a/doc/assets/xml_spec.tex +++ b/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} + \end{minted} \noindent\textbf{XSD}: @@ -407,6 +418,14 @@ \subsection{Trace Steps in XML} + + + + + + + + \end{minted} \subsection{Full Trace XSD} @@ -422,6 +441,7 @@ \subsection{Full Trace XSD} + diff --git a/doc/assets/xml_spec.xsd b/doc/assets/xml_spec.xsd index dd3c4b7f11b..40f7c078ea4 100644 --- a/doc/assets/xml_spec.xsd +++ b/doc/assets/xml_spec.xsd @@ -138,6 +138,15 @@ + + + + + + + + + @@ -148,6 +157,7 @@ + From a8c5f575efc17edd4eeb40364698708dda010019 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 18 Jun 2020 12:28:43 +0100 Subject: [PATCH 5/6] 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 --- src/goto-programs/Makefile | 1 + src/goto-programs/json_goto_trace.cpp | 6 ++-- src/goto-programs/json_goto_trace.h | 16 ++++----- src/goto-programs/structured_trace_util.cpp | 35 ++++++++++++++++++ src/goto-programs/structured_trace_util.h | 39 +++++++++++++++++++++ src/goto-programs/xml_goto_trace.cpp | 13 ++++--- 6 files changed, 92 insertions(+), 18 deletions(-) create mode 100644 src/goto-programs/structured_trace_util.cpp create mode 100644 src/goto-programs/structured_trace_util.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 429bbc046c3..ac22aa41a86 100644 --- a/src/goto-programs/Makefile +++ b/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 \ diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index a25cc64be2e..f519582c400 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/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; diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index d28a05d5774..5fbe31f932a 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/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 #include @@ -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); } } diff --git a/src/goto-programs/structured_trace_util.cpp b/src/goto-programs/structured_trace_util.cpp new file mode 100644 index 00000000000..7aecf8726c4 --- /dev/null +++ b/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 + +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; +} diff --git a/src/goto-programs/structured_trace_util.h b/src/goto-programs/structured_trace_util.h new file mode 100644 index 00000000000..67dd1d5395a --- /dev/null +++ b/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 + +/// 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 diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 3cd1dc48255..964545c26be 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -18,11 +18,11 @@ Author: Daniel Kroening #include #include -#include #include #include #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( From 657c1a667749fedd4044c823eb069c30bd6bc5d7 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 18 Jun 2020 16:29:57 +0100 Subject: [PATCH 6/6] Fix the documentation for convert_default Consolidate the documentation - deleting the duplicated doxygen that was attached to the implementation as well as the declaration --- src/goto-programs/json_goto_trace.cpp | 10 ---------- src/goto-programs/json_goto_trace.h | 2 ++ 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index f519582c400..2bfb04ee9d7 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -276,16 +276,6 @@ 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. -/// \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, diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 5fbe31f932a..9c98fac09e7 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/src/goto-programs/json_goto_trace.h @@ -99,6 +99,8 @@ 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,