From 8ddbbb712a92e365cf94b15c16f52e1c54cf7919 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 22 Jan 2020 10:08:14 +0000 Subject: [PATCH 1/4] Pull out the compare function --- src/goto-checker/report_util.cpp | 116 +++++++++++++++++-------------- 1 file changed, 63 insertions(+), 53 deletions(-) diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 368a8b9687b..ce9b3d44459 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -181,69 +181,79 @@ static void output_single_property_plain( << messaget::eom; } +using propertyt = std::pair; +/// Compare two properties according to the following sort: +/// 1. alphabetical ordering of file name +/// 2. alphabetical ordering of function name +/// 3. numerical ordering of line number +/// 4. alphabetical ordering of goal ID +/// 5. number ordering of the goal ID number +/// \param pit1: The first property. +/// \param pit2: The second propery. +/// \return True if the first property is less than the second property +static bool is_property_less_than(const propertyt &pit1, const propertyt &pit2) +{ + const auto &p1 = pit1.second.pc->source_location; + const auto &p2 = pit2.second.pc->source_location; + if(p1.get_file() != p2.get_file()) + return id2string(p1.get_file()) < id2string(p2.get_file()); + if(p1.get_function() != p2.get_function()) + return id2string(p1.get_function()) < id2string(p2.get_function()); + else if( + !p1.get_line().empty() && !p2.get_line().empty() && + p1.get_line() != p2.get_line()) + return std::stoul(id2string(p1.get_line())) < + std::stoul(id2string(p2.get_line())); + + const auto split_property_id = + [](const irep_idt &property_id) -> std::pair { + const auto property_string = id2string(property_id); + const auto last_dot = property_string.rfind('.'); + std::string property_name; + std::string property_number; + if(last_dot == std::string::npos) + { + property_name = ""; + property_number = property_string; + } + else + { + property_name = property_string.substr(0, last_dot); + property_number = property_string.substr(last_dot + 1); + } + const auto maybe_number = string2optional_size_t(property_number); + if(maybe_number.has_value()) + return std::make_pair(property_name, *maybe_number); + else + return std::make_pair(property_name, 0); + }; + + const auto left_split = split_property_id(pit1.first); + const auto left_id_name = left_split.first; + const auto left_id_number = left_split.second; + + const auto right_split = split_property_id(pit2.first); + const auto right_id_name = left_split.first; + const auto right_id_number = left_split.second; + + if(left_id_name != right_id_name) + return left_id_name < right_id_name; + else + return left_id_number < right_id_number; +} + static std::vector get_sorted_properties(const propertiest &properties) { std::vector sorted_properties; for(auto p_it = properties.begin(); p_it != properties.end(); p_it++) sorted_properties.push_back(p_it); - // now determine an ordering for those goals: - // 1. alphabetical ordering of file name - // 2. alphabetical ordering of function name - // 3. numerical ordering of line number - // 4. alphabetical ordering of goal ID - // 5. number ordering of the goal ID number + std::sort( sorted_properties.begin(), sorted_properties.end(), [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) { - const auto &p1 = pit1->second.pc->source_location; - const auto &p2 = pit2->second.pc->source_location; - if(p1.get_file() != p2.get_file()) - return id2string(p1.get_file()) < id2string(p2.get_file()); - if(p1.get_function() != p2.get_function()) - return id2string(p1.get_function()) < id2string(p2.get_function()); - else if( - !p1.get_line().empty() && !p2.get_line().empty() && - p1.get_line() != p2.get_line()) - return std::stoul(id2string(p1.get_line())) < - std::stoul(id2string(p2.get_line())); - - const auto split_property_id = - [](const irep_idt &property_id) -> std::pair { - const auto property_string = id2string(property_id); - const auto last_dot = property_string.rfind('.'); - std::string property_name; - std::string property_number; - if(last_dot == std::string::npos) - { - property_name = ""; - property_number = property_string; - } - else - { - property_name = property_string.substr(0, last_dot); - property_number = property_string.substr(last_dot + 1); - } - const auto maybe_number = string2optional_size_t(property_number); - if(maybe_number.has_value()) - return std::make_pair(property_name, *maybe_number); - else - return std::make_pair(property_name, 0); - }; - - const auto left_split = split_property_id(pit1->first); - const auto left_id_name = left_split.first; - const auto left_id_number = left_split.second; - - const auto right_split = split_property_id(pit2->first); - const auto right_id_name = left_split.first; - const auto right_id_number = left_split.second; - - if(left_id_name != right_id_name) - return left_id_name < right_id_name; - else - return left_id_number < right_id_number; + return is_property_less_than(*pit1, *pit2); }); return sorted_properties; } From 8e06fb29302d4194459d8a96c48f67a9dfe81b2d Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 22 Jan 2020 10:09:26 +0000 Subject: [PATCH 2/4] Rename to use full names for properties --- src/goto-checker/report_util.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index ce9b3d44459..4b6c971c2fe 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -188,13 +188,14 @@ using propertyt = std::pair; /// 3. numerical ordering of line number /// 4. alphabetical ordering of goal ID /// 5. number ordering of the goal ID number -/// \param pit1: The first property. -/// \param pit2: The second propery. +/// \param property1: The first property. +/// \param property2: The second propery. /// \return True if the first property is less than the second property -static bool is_property_less_than(const propertyt &pit1, const propertyt &pit2) +static bool +is_property_less_than(const propertyt &property1, const propertyt &property2) { - const auto &p1 = pit1.second.pc->source_location; - const auto &p2 = pit2.second.pc->source_location; + const auto &p1 = property1.second.pc->source_location; + const auto &p2 = property2.second.pc->source_location; if(p1.get_file() != p2.get_file()) return id2string(p1.get_file()) < id2string(p2.get_file()); if(p1.get_function() != p2.get_function()) @@ -228,11 +229,11 @@ static bool is_property_less_than(const propertyt &pit1, const propertyt &pit2) return std::make_pair(property_name, 0); }; - const auto left_split = split_property_id(pit1.first); + const auto left_split = split_property_id(property1.first); const auto left_id_name = left_split.first; const auto left_id_number = left_split.second; - const auto right_split = split_property_id(pit2.first); + const auto right_split = split_property_id(property2.first); const auto right_id_name = left_split.first; const auto right_id_number = left_split.second; From 7b173490bb9bc0c80c1dd9d50d003896e9384b2f Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 22 Jan 2020 11:08:53 +0000 Subject: [PATCH 3/4] Add a unit test for checking the ordering by instruction --- unit/Makefile | 1 + .../report_util/is_property_less_than.cpp | 72 +++++++++++++++++++ .../report_util/module_dependencies.txt | 2 + 3 files changed, 75 insertions(+) create mode 100644 unit/goto-checker/report_util/is_property_less_than.cpp create mode 100644 unit/goto-checker/report_util/module_dependencies.txt diff --git a/unit/Makefile b/unit/Makefile index ed549005358..ccbe365b11f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ big-int/big-int.cpp \ compound_block_locations.cpp \ + goto-checker/report_util/is_property_less_than.cpp \ goto-instrument/cover_instrument.cpp \ goto-instrument/cover/cover_only.cpp \ goto-programs/goto_model_function_type_consistency.cpp \ diff --git a/unit/goto-checker/report_util/is_property_less_than.cpp b/unit/goto-checker/report_util/is_property_less_than.cpp new file mode 100644 index 00000000000..b6e2a221575 --- /dev/null +++ b/unit/goto-checker/report_util/is_property_less_than.cpp @@ -0,0 +1,72 @@ +// Copyright 2016-2020 Diffblue Limited. All Rights Reserved. + +#include +#include + +static goto_programt::instructiont instruction_for_location( + const irep_idt &file, + const irep_idt &function, + size_t line_no) +{ + source_locationt location; + location.set_file(file); + location.set_function(function); + location.set_line(line_no); + goto_programt::instructiont instruction; + instruction.source_location = location; + return instruction; +} + +static property_infot test_info(const goto_programt::const_targett &target) +{ + return property_infot(target, "ignored", property_statust::UNKNOWN); +} + +static propertyt +property(const irep_idt &identifier, const property_infot &info) +{ + return std::make_pair(identifier, info); +} + +std::ostream &operator<<(std::ostream &os, const propertyt &value) +{ + os << "{ property_id=" << value.first << ", " + << " property_location={ " + << " file=" << value.second.pc->source_location.get_file() << ", " + << " function=" << value.second.pc->source_location.get_function() << ", " + << " line=" << value.second.pc->source_location.get_line() << "}}"; + return os; +} + +TEST_CASE("Comparing two properties", "[core][goto-checker][report_util]") +{ + SECTION("Compare locations") + { + goto_programt::instructionst instructions; + instructions.push_back(instruction_for_location("fileA", "funcA", 1)); + instructions.push_back(instruction_for_location("fileA", "funcA", 2)); + instructions.push_back(instruction_for_location("fileA", "funcB", 1)); + instructions.push_back(instruction_for_location("fileA", "funcB", 2)); + instructions.push_back(instruction_for_location("fileB", "funcA", 1)); + instructions.push_back(instruction_for_location("fileB", "funcA", 2)); + instructions.push_back(instruction_for_location("fileB", "funcB", 1)); + instructions.push_back(instruction_for_location("fileB", "funcB", 2)); + + for(auto first_location = instructions.begin(); + first_location != instructions.end(); + ++first_location) + { + for(auto second_location = std::next(first_location); + second_location != instructions.end(); + ++second_location) + { + const propertyt p1 = property("ignored", test_info(first_location)); + const propertyt p2 = property("ignored", test_info(second_location)); + INFO(p1); + INFO(p2); + REQUIRE(is_property_less_than(p1, p2)); + REQUIRE_FALSE(is_property_less_than(p2, p1)); + } + } + } +} diff --git a/unit/goto-checker/report_util/module_dependencies.txt b/unit/goto-checker/report_util/module_dependencies.txt new file mode 100644 index 00000000000..9c63129fd0a --- /dev/null +++ b/unit/goto-checker/report_util/module_dependencies.txt @@ -0,0 +1,2 @@ +goto-checker +testing-utils From ac888bbd45e81b2721b0db0386bc4829c71f3fb9 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 22 Jan 2020 11:20:09 +0000 Subject: [PATCH 4/4] Fix error in sorting properties that differ by property name Add unit tests demonstrating the fix. --- src/goto-checker/report_util.cpp | 4 +-- .../report_util/is_property_less_than.cpp | 30 +++++++++++++++++++ 2 files changed, 32 insertions(+), 2 deletions(-) diff --git a/src/goto-checker/report_util.cpp b/src/goto-checker/report_util.cpp index 4b6c971c2fe..8174b682ede 100644 --- a/src/goto-checker/report_util.cpp +++ b/src/goto-checker/report_util.cpp @@ -234,8 +234,8 @@ is_property_less_than(const propertyt &property1, const propertyt &property2) const auto left_id_number = left_split.second; const auto right_split = split_property_id(property2.first); - const auto right_id_name = left_split.first; - const auto right_id_number = left_split.second; + const auto right_id_name = right_split.first; + const auto right_id_number = right_split.second; if(left_id_name != right_id_name) return left_id_name < right_id_name; diff --git a/unit/goto-checker/report_util/is_property_less_than.cpp b/unit/goto-checker/report_util/is_property_less_than.cpp index b6e2a221575..d74748cb5b6 100644 --- a/unit/goto-checker/report_util/is_property_less_than.cpp +++ b/unit/goto-checker/report_util/is_property_less_than.cpp @@ -69,4 +69,34 @@ TEST_CASE("Comparing two properties", "[core][goto-checker][report_util]") } } } + SECTION("Compare property ids") + { + goto_programt::instructionst instructions; + instructions.push_back(instruction_for_location("fileA", "funcA", 1)); + + std::vector properties; + properties.push_back("A.1"); + properties.push_back("A.2"); + properties.push_back("B.1"); + properties.push_back("B.2"); + + for(auto first_property = properties.begin(); + first_property != properties.end(); + ++first_property) + { + for(auto second_property = std::next(first_property); + second_property != properties.end(); + ++second_property) + { + const propertyt p1 = + property(*first_property, test_info(instructions.begin())); + const propertyt p2 = + property(*second_property, test_info(instructions.begin())); + INFO(p1); + INFO(p2); + REQUIRE(is_property_less_than(p1, p2)); + REQUIRE_FALSE(is_property_less_than(p2, p1)); + } + } + } }