source_linest: use platform-independent mp_integer

An input binary could have been produced on a platform that has a larger
size_t width than the one used during analysis. This requires making
format_number_range not use bounded integer type, which is an
improvement for using mp_integer enables use with all kinds of input
ranges rather than hard-coding "unsigned" as the type.

Author: tautschnig

src/goto-instrument/source_lines.cpp

@@ -14,7 +14,6 @@ Author: Mark R. Tuttle
 #include <util/format_number_range.h>
 #include <util/range.h>
 #include <util/source_location.h>
-#include <util/string2int.h>
 #include <util/string_utils.h>
 
 #include <sstream>
@@ -30,7 +29,7 @@ void source_linest::insert(const source_locationt &loc)
 
   if(loc.get_line().empty())
     return;
-  std::size_t line = safe_string2size_t(id2string(loc.get_line()));
+  mp_integer line = string2integer(id2string(loc.get_line()));
 
   block_lines[file][func].insert(line);
 }
@@ -44,7 +43,7 @@ std::string source_linest::to_string() const
         std::stringstream ss;
         const auto map = make_range(file_entry.second)
                            .map([&](const function_linest::value_type &pair) {
-                             std::vector<unsigned> line_numbers(
+                             std::vector<mp_integer> line_numbers(
                                pair.second.begin(), pair.second.end());
                              return file_entry.first + ':' + pair.first + ':' +
                                     format_number_range(line_numbers);
@@ -65,7 +64,7 @@ irept source_linest::to_irep() const
     irept file_result;
     for(const auto &lines_entry : file_entry.second)
     {
-      std::vector<unsigned> line_numbers(
+      std::vector<mp_integer> line_numbers(
         lines_entry.second.begin(), lines_entry.second.end());
       file_result.set(lines_entry.first, format_number_range(line_numbers));
     }

src/goto-instrument/source_lines.h

@@ -21,6 +21,7 @@ Author: Mark R. Tuttle
 #define CPROVER_GOTO_INSTRUMENT_SOURCE_LINES_H
 
 #include <util/irep.h>
+#include <util/mp_arith.h>
 
 #include <map>
 #include <set>
@@ -45,10 +46,10 @@ class source_linest
   /// Construct a string representing the set of lines
   ///
   /// \return The set of lines represented as string of the form
-  ///   set1;set2;set3 where each seti is a string of the form
+  ///   set1;set2;set3 where each set is a string of the form
   ///   file:function:n1,n2,n3,n4 where n1, n2, n3, n4 are line
-  ///   numbers from the given function in the given file listed in
-  ///   ascending order.
+  ///   numbers (or ranges thereof) from the given function in the given file
+  ///   listed in ascending order.
   std::string to_string() const;
 
   /// Construct an irept representing the set of lines
@@ -60,7 +61,7 @@ class source_linest
 
 private:
   /// A set of lines from a single function
-  typedef std::set<std::size_t> linest;
+  using linest = std::set<mp_integer>;
   /// A set of lines from multiple function
   using function_linest = std::map<std::string, linest>;
   /// A set of lines from multiple files

src/util/format_number_range.cpp

@@ -22,21 +22,20 @@ Author: Daniel Kroening, [email protected]
 /// create shorter representation for output
 /// \param input_numbers: vector of numbers
 /// \return string of compressed number range representation
-std::string format_number_range(const std::vector<unsigned> &input_numbers)
+std::string format_number_range(const std::vector<mp_integer> &input_numbers)
 {
   PRECONDITION(!input_numbers.empty());
 
-  std::vector<unsigned> numbers(input_numbers);
+  std::vector<mp_integer> numbers(input_numbers);
   std::sort(numbers.begin(), numbers.end());
-  unsigned end_number=numbers.back();
-  if(numbers.front()==end_number)
-    return std::to_string(end_number); // only single number
+  if(numbers.front() == numbers.back())
+    return integer2string(numbers.back()); // only single number
 
   std::stringstream number_range;
 
   auto start_number = numbers.front();
 
-  for(std::vector<unsigned>::const_iterator it = numbers.begin();
+  for(std::vector<mp_integer>::const_iterator it = numbers.begin();
       it != numbers.end();
       ++it)
   {
@@ -75,14 +74,14 @@ std::string format_number_range(const std::vector<unsigned> &input_numbers)
 /// Appends \p number resp. numbers \p begin_range ... \p number to \p numbers
 static void append_numbers(
   const std::string &number_range,
-  std::vector<unsigned> &numbers,
+  std::vector<mp_integer> &numbers,
   bool last_number_is_set,
   bool is_range)
 {
   if(!last_number_is_set && is_range)
   {
     throw deserialization_exceptiont(
-      "unterminated number range '" + std::to_string(*(++numbers.rbegin())) +
+      "unterminated number range '" + integer2string(*(++numbers.rbegin())) +
       "-'");
   }
 
@@ -94,27 +93,27 @@ static void append_numbers(
 
   if(is_range)
   {
-    unsigned end_range = numbers.back();
+    mp_integer end_range = numbers.back();
     numbers.pop_back();
-    unsigned begin_range = numbers.back();
+    mp_integer begin_range = numbers.back();
     numbers.pop_back();
     if(begin_range > end_range)
     {
       throw deserialization_exceptiont(
         "lower bound must not be larger than upper bound '" +
-        std::to_string(begin_range) + "-" + std::to_string(end_range) + "'");
+        integer2string(begin_range) + "-" + integer2string(end_range) + "'");
     }
-    for(unsigned i = begin_range; i < end_range; ++i)
+    for(mp_integer i = begin_range; i < end_range; ++i)
       numbers.push_back(i);
     // add upper bound separately to avoid
     // potential overflow issues in the loop above
     numbers.push_back(end_range);
   }
 }
 
-std::vector<unsigned> parse_number_range(const std::string &number_range)
+std::vector<mp_integer> parse_number_range(const std::string &number_range)
 {
-  std::vector<unsigned> numbers(1, 0);
+  std::vector<mp_integer> numbers(1, 0);
   bool last_number_is_set = false;
   bool is_range = false;
 

src/util/format_number_range.h

@@ -12,13 +12,15 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_FORMAT_NUMBER_RANGE_H
 #define CPROVER_UTIL_FORMAT_NUMBER_RANGE_H
 
+#include "mp_arith.h"
+
 #include <string>
 #include <vector>
 
-std::string format_number_range(const std::vector<unsigned> &);
+std::string format_number_range(const std::vector<mp_integer> &);
 
 /// Parse a compressed range into a vector of numbers,
 /// e.g. "2,4-6" -> [2,4,5,6]
-std::vector<unsigned> parse_number_range(const std::string &);
+std::vector<mp_integer> parse_number_range(const std::string &);
 
 #endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H

unit/util/format_number_range.cpp

@@ -15,51 +15,51 @@ TEST_CASE(
   "Format a range of unsigned numbers",
   "[core][util][format_number_range]")
 {
-  const std::vector<unsigned> singleton = {1u};
+  const std::vector<mp_integer> singleton = {1};
   REQUIRE(format_number_range(singleton) == "1");
 
-  const std::vector<unsigned> r1 = {0u, 42u};
+  const std::vector<mp_integer> r1 = {0, 42};
   REQUIRE(format_number_range(r1) == "0,42");
 
-  const std::vector<unsigned> r2 = {0u, 1u};
+  const std::vector<mp_integer> r2 = {0, 1};
   REQUIRE(format_number_range(r2) == "0,1");
 
-  const std::vector<unsigned> r3 = {1u, 2u, 3u};
+  const std::vector<mp_integer> r3 = {1, 2, 3};
   REQUIRE(format_number_range(r3) == "1-3");
 
-  const std::vector<unsigned> r4 = {1u, 3u, 4u, 5u};
+  const std::vector<mp_integer> r4 = {1, 3, 4, 5};
   REQUIRE(format_number_range(r4) == "1,3-5");
 
-  const std::vector<unsigned> r5 = {1u, 10u, 11u, 12u, 42u};
+  const std::vector<mp_integer> r5 = {1, 10, 11, 12, 42};
   REQUIRE(format_number_range(r5) == "1,10-12,42");
 
-  const std::vector<unsigned> r6 = {1u, 10u, 11u, 12u, 42u, 43u, 44u};
+  const std::vector<mp_integer> r6 = {1, 10, 11, 12, 42, 43, 44};
   REQUIRE(format_number_range(r6) == "1,10-12,42-44");
 }
 
 TEST_CASE(
   "Parse a range of unsigned numbers",
   "[core][util][format_number_range]")
 {
-  const std::vector<unsigned> singleton = {1u};
+  const std::vector<mp_integer> singleton = {1};
   REQUIRE(parse_number_range("1") == singleton);
 
-  const std::vector<unsigned> r1 = {0u, 42u};
+  const std::vector<mp_integer> r1 = {0, 42};
   REQUIRE(parse_number_range("0,42") == r1);
 
-  const std::vector<unsigned> r2 = {0u, 1u};
+  const std::vector<mp_integer> r2 = {0, 1};
   REQUIRE(parse_number_range("0,1") == r2);
 
-  const std::vector<unsigned> r3 = {1u, 2u, 3u};
+  const std::vector<mp_integer> r3 = {1, 2, 3};
   REQUIRE(parse_number_range("1-3") == r3);
 
-  const std::vector<unsigned> r4 = {1u, 3u, 4u, 5u};
+  const std::vector<mp_integer> r4 = {1, 3, 4, 5};
   REQUIRE(parse_number_range("1,3-5") == r4);
 
-  const std::vector<unsigned> r5 = {1u, 10u, 11u, 12u, 42u};
+  const std::vector<mp_integer> r5 = {1, 10, 11, 12, 42};
   REQUIRE(parse_number_range("1,10-12,42") == r5);
 
-  const std::vector<unsigned> r6 = {1u, 10u, 11u, 12u, 42u, 43u, 44u};
+  const std::vector<mp_integer> r6 = {1, 10, 11, 12, 42, 43, 44};
   REQUIRE(parse_number_range("1,10-12,42-44") == r6);
 
   REQUIRE_THROWS_AS(parse_number_range(""), deserialization_exceptiont);