From 96c8aa49bbb1c5c38c5ded899a5e7567717149b3 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 18 Jun 2020 15:13:22 +0100 Subject: [PATCH 1/3] 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 --- src/goto-programs/json_goto_trace.cpp | 16 +++++------ src/goto-programs/json_goto_trace.h | 20 +++++-------- src/goto-programs/structured_trace_util.cpp | 32 +++++++++++++++++++++ src/goto-programs/structured_trace_util.h | 14 +++++++++ src/goto-programs/xml_goto_trace.cpp | 32 +++++++-------------- 5 files changed, 71 insertions(+), 43 deletions(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 2bfb04ee9d7..262a9d621fe 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/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); } diff --git a/src/goto-programs/json_goto_trace.h b/src/goto-programs/json_goto_trace.h index 9c98fac09e7..ac692de8e9e 100644 --- a/src/goto-programs/json_goto_trace.h +++ b/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()) diff --git a/src/goto-programs/structured_trace_util.cpp b/src/goto-programs/structured_trace_util.cpp index 7aecf8726c4..244c655e5e3 100644 --- a/src/goto-programs/structured_trace_util.cpp +++ b/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 default_step_kindt @@ -33,3 +35,33 @@ std::string default_step_name(const default_step_kindt &step_type) } UNREACHABLE; } + +optionalt 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}; +} diff --git a/src/goto-programs/structured_trace_util.h b/src/goto-programs/structured_trace_util.h index 67dd1d5395a..e8bbbf32b16 100644 --- a/src/goto-programs/structured_trace_util.h +++ b/src/goto-programs/structured_trace_util.h @@ -13,6 +13,7 @@ Author: Diffblue #include "goto_program.h" #include +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_step( + const goto_trace_stept &step, + const source_locationt &previous_source_location); + #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 964545c26be..bab0dfed78f 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/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; } } From 4a2341170838664acbcce2552df76e61eb566749 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 18 Jun 2020 15:48:27 +0100 Subject: [PATCH 2/3] Add unit test for the restructured normal step printing --- unit/Makefile | 1 + unit/goto-programs/structured_trace_util.cpp | 161 +++++++++++++++++++ 2 files changed, 162 insertions(+) create mode 100644 unit/goto-programs/structured_trace_util.cpp diff --git a/unit/Makefile b/unit/Makefile index e30aaf506f9..2b85801f809 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -35,6 +35,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/label_function_pointer_call_sites.cpp \ goto-programs/osx_fat_reader.cpp \ goto-programs/restrict_function_pointers.cpp \ + goto-programs/structured_trace_util.cpp \ goto-programs/remove_returns.cpp \ goto-programs/xml_expr.cpp \ goto-symex/apply_condition.cpp \ diff --git a/unit/goto-programs/structured_trace_util.cpp b/unit/goto-programs/structured_trace_util.cpp new file mode 100644 index 00000000000..07490f88f4e --- /dev/null +++ b/unit/goto-programs/structured_trace_util.cpp @@ -0,0 +1,161 @@ +/*******************************************************************\ + +Module: structured_trace_util + +Author: Diffblue + +\*******************************************************************/ +#include + +#include +#include + +void link_edges(goto_programt::targett source, goto_programt::targett target) +{ + source->targets.push_back(target); + target->incoming_edges.insert(source); +} + +TEST_CASE("structured_trace_util", "[core][util][trace]") +{ + goto_programt::instructionst instructions; + + source_locationt nil_location; + + source_locationt unrelated_location; + unrelated_location.set_file("foo.c"); + unrelated_location.set_line(1); + + source_locationt no_file_location; + unrelated_location.set_line(1); + + source_locationt basic_location; + basic_location.set_file("test.c"); + basic_location.set_line(1); + + source_locationt loop_head_location; + loop_head_location.set_file("test.c"); + loop_head_location.set_line(2); + + source_locationt back_edge_location; + back_edge_location.set_file("test.c"); + back_edge_location.set_line(3); + + // 0 # normal_location + // 1 # loop_head + // 2: goto 1 # back_edge + // 3: no_location + // 4: no_file + goto_programt::instructiont normal_instruction; + normal_instruction.location_number = 0; + normal_instruction.source_location = basic_location; + instructions.push_back(normal_instruction); + + goto_programt::instructiont loop_head; + loop_head.location_number = 1; + loop_head.source_location = loop_head_location; + instructions.push_back(loop_head); + + goto_programt::instructiont back_edge; + back_edge.source_location = back_edge_location; + back_edge.location_number = 2; + back_edge.type = GOTO; + instructions.push_back(back_edge); + + goto_programt::instructiont no_location; + no_location.location_number = 3; + instructions.push_back(no_location); + + goto_programt::instructiont no_file; + no_file.location_number = 4; + no_file.source_location = no_file_location; + instructions.push_back(no_file); + + link_edges( + std::next(instructions.begin(), 2), std::next(instructions.begin(), 1)); + + SECTION("location-only steps") + { + goto_trace_stept step; + step.step_nr = 1; + step.thread_nr = 2; + step.hidden = true; + SECTION("Simple step") + { + step.pc = instructions.begin(); + + const auto parsed_step = default_step(step, unrelated_location); + + REQUIRE(parsed_step); + REQUIRE(parsed_step->step_number == 1); + REQUIRE(parsed_step->thread_number == 2); + REQUIRE(parsed_step->hidden); + REQUIRE(parsed_step->kind == default_step_kindt::LOCATION_ONLY); + REQUIRE(parsed_step->location == basic_location); + } + SECTION("Invalid previous step") + { + step.pc = instructions.begin(); + + const auto parsed_step = default_step(step, nil_location); + + REQUIRE(parsed_step); + REQUIRE(parsed_step->step_number == 1); + REQUIRE(parsed_step->thread_number == 2); + REQUIRE(parsed_step->hidden); + REQUIRE(parsed_step->kind == default_step_kindt::LOCATION_ONLY); + REQUIRE(parsed_step->location == basic_location); + } + + SECTION("Duplicate step") + { + step.pc = instructions.begin(); + const auto parsed_step = default_step(step, basic_location); + REQUIRE_FALSE(parsed_step); + } + SECTION("No source location") + { + step.pc = std::next(instructions.begin(), 3); + + const auto parsed_step = default_step(step, unrelated_location); + REQUIRE_FALSE(parsed_step); + } + SECTION("No file") + { + step.pc = std::next(instructions.begin(), 4); + + const auto parsed_step = default_step(step, unrelated_location); + REQUIRE_FALSE(parsed_step); + } + } + SECTION("Loop head steps") + { + goto_trace_stept step; + step.step_nr = 1; + step.thread_nr = 2; + step.hidden = true; + step.pc = std::next(instructions.begin(), 1); + SECTION("Simple step") + { + const auto parsed_step = default_step(step, unrelated_location); + + REQUIRE(parsed_step); + REQUIRE(parsed_step->step_number == 1); + REQUIRE(parsed_step->thread_number == 2); + REQUIRE(parsed_step->hidden); + REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD); + REQUIRE(parsed_step->location == loop_head_location); + } + + SECTION("Duplicate step") + { + const auto parsed_step = default_step(step, loop_head_location); + REQUIRE(parsed_step); + REQUIRE(parsed_step->step_number == 1); + REQUIRE(parsed_step->thread_number == 2); + REQUIRE(parsed_step->hidden); + REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD); + REQUIRE(parsed_step->location == loop_head_location); + } + } +} From f639b89e34b9601b1b938aa5fe186ecd79b882b9 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 18 Jun 2020 15:55:52 +0100 Subject: [PATCH 3/3] Tidy up the unit test so easier to see intent --- unit/goto-programs/structured_trace_util.cpp | 73 +++++++++----------- 1 file changed, 33 insertions(+), 40 deletions(-) diff --git a/unit/goto-programs/structured_trace_util.cpp b/unit/goto-programs/structured_trace_util.cpp index 07490f88f4e..072fbb4fd45 100644 --- a/unit/goto-programs/structured_trace_util.cpp +++ b/unit/goto-programs/structured_trace_util.cpp @@ -16,60 +16,53 @@ void link_edges(goto_programt::targett source, goto_programt::targett target) target->incoming_edges.insert(source); } +source_locationt simple_location(const std::string &file, unsigned line) +{ + source_locationt location; + location.set_file(file); + location.set_line(line); + return location; +} + +goto_programt::targett add_instruction( + const source_locationt &location, + goto_programt::instructionst &instructions) +{ + goto_programt::instructiont instruction; + instruction.location_number = instructions.size(); + instruction.source_location = location; + instructions.push_back(instruction); + return std::next(instructions.begin(), instruction.location_number); +} + TEST_CASE("structured_trace_util", "[core][util][trace]") { goto_programt::instructionst instructions; source_locationt nil_location; - source_locationt unrelated_location; - unrelated_location.set_file("foo.c"); - unrelated_location.set_line(1); + const source_locationt unrelated_location = simple_location("foo.c", 1); source_locationt no_file_location; - unrelated_location.set_line(1); - - source_locationt basic_location; - basic_location.set_file("test.c"); - basic_location.set_line(1); - - source_locationt loop_head_location; - loop_head_location.set_file("test.c"); - loop_head_location.set_line(2); + no_file_location.set_line(1); - source_locationt back_edge_location; - back_edge_location.set_file("test.c"); - back_edge_location.set_line(3); + const source_locationt basic_location = simple_location("test.c", 1); + const source_locationt loop_head_location = simple_location("test.c", 2); + const source_locationt back_edge_location = simple_location("test.c", 3); // 0 # normal_location + add_instruction(basic_location, instructions); // 1 # loop_head + add_instruction(loop_head_location, instructions); // 2: goto 1 # back_edge + const auto back_edge = add_instruction(back_edge_location, instructions); + back_edge->type = GOTO; // 3: no_location - // 4: no_file - goto_programt::instructiont normal_instruction; - normal_instruction.location_number = 0; - normal_instruction.source_location = basic_location; - instructions.push_back(normal_instruction); - - goto_programt::instructiont loop_head; - loop_head.location_number = 1; - loop_head.source_location = loop_head_location; - instructions.push_back(loop_head); - - goto_programt::instructiont back_edge; - back_edge.source_location = back_edge_location; - back_edge.location_number = 2; - back_edge.type = GOTO; - instructions.push_back(back_edge); - goto_programt::instructiont no_location; no_location.location_number = 3; instructions.push_back(no_location); - - goto_programt::instructiont no_file; - no_file.location_number = 4; - no_file.source_location = no_file_location; - instructions.push_back(no_file); + // 4: no_file + add_instruction(no_file_location, instructions); link_edges( std::next(instructions.begin(), 2), std::next(instructions.begin(), 1)); @@ -133,7 +126,7 @@ TEST_CASE("structured_trace_util", "[core][util][trace]") goto_trace_stept step; step.step_nr = 1; step.thread_nr = 2; - step.hidden = true; + step.hidden = false; step.pc = std::next(instructions.begin(), 1); SECTION("Simple step") { @@ -142,7 +135,7 @@ TEST_CASE("structured_trace_util", "[core][util][trace]") REQUIRE(parsed_step); REQUIRE(parsed_step->step_number == 1); REQUIRE(parsed_step->thread_number == 2); - REQUIRE(parsed_step->hidden); + REQUIRE_FALSE(parsed_step->hidden); REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD); REQUIRE(parsed_step->location == loop_head_location); } @@ -153,7 +146,7 @@ TEST_CASE("structured_trace_util", "[core][util][trace]") REQUIRE(parsed_step); REQUIRE(parsed_step->step_number == 1); REQUIRE(parsed_step->thread_number == 2); - REQUIRE(parsed_step->hidden); + REQUIRE_FALSE(parsed_step->hidden); REQUIRE(parsed_step->kind == default_step_kindt::LOOP_HEAD); REQUIRE(parsed_step->location == loop_head_location); }