Fix property sort

src/goto-checker/report_util.cpp

@@ -181,69 +181,80 @@ static void output_single_property_plain(
                << messaget::eom;
 }
 
+using propertyt = std::pair<irep_idt, property_infot>;
+/// 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 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 &property1, const propertyt &property2)
+{
+  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())
+    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<std::string, std::size_t> {
+    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(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(property2.first);
+  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;
+  else
+    return left_id_number < right_id_number;
+}
+
 static std::vector<propertiest::const_iterator>
 get_sorted_properties(const propertiest &properties)
 {
   std::vector<propertiest::const_iterator> 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<std::string, std::size_t> {
-        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;
 }

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 \

unit/goto-checker/report_util/is_property_less_than.cpp

@@ -0,0 +1,102 @@
+// Copyright 2016-2020 Diffblue Limited. All Rights Reserved.
+
+#include <goto-checker/report_util.cpp>
+#include <testing-utils/use_catch.h>
+
+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));
+      }
+    }
+  }
+  SECTION("Compare property ids")
+  {
+    goto_programt::instructionst instructions;
+    instructions.push_back(instruction_for_location("fileA", "funcA", 1));
+
+    std::vector<irep_idt> 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));
+      }
+    }
+  }
+}

unit/goto-checker/report_util/module_dependencies.txt

@@ -0,0 +1,2 @@
+goto-checker
+testing-utils