switch representation of bit-vectors to hex

Simultaneously leading zeros are dropped.  This reduces the memory
consumption of bit-vectors by 4x or more.

Author: Daniel Kroening

src/goto-programs/goto_trace.cpp

@@ -131,23 +131,34 @@ void goto_trace_stept::output(
 /// \return a string with the numeric representation
 static std::string numeric_representation(
   const constant_exprt &expr,
+  const namespacet &ns,
   const trace_optionst &options)
 {
   std::string result;
   std::string prefix;
 
+  const typet &expr_type = expr.type();
+
+  const typet &underlying_type =
+    expr_type.id() == ID_c_enum_tag
+      ? ns.follow_tag(to_c_enum_tag_type(expr_type)).subtype()
+      : expr_type;
+
   const irep_idt &value = expr.get_value();
 
+  const auto width = to_bitvector_type(underlying_type).get_width();
+
+  const mp_integer value_int = bv2integer(id2string(value), width, false);
+
   if(options.hex_representation)
   {
-    mp_integer value_int = bv2integer(id2string(value), value.size(), false);
     result = integer2string(value_int, 16);
     prefix = "0x";
   }
   else
   {
+    result = integer2binary(value_int, width);
     prefix = "0b";
-    result = id2string(value);
   }
 
   std::ostringstream oss;
@@ -184,9 +195,7 @@ std::string trace_numeric_value(
        type.id()==ID_c_enum ||
        type.id()==ID_c_enum_tag)
     {
-      const std::string &str =
-        numeric_representation(to_constant_expr(expr), options);
-      return str;
+      return numeric_representation(to_constant_expr(expr), ns, options);
     }
     else if(type.id()==ID_bool)
     {

src/solvers/flattening/boolbv_constant.cpp

@@ -81,14 +81,6 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
   {
     const auto &value = expr.get_value();
 
-    if(value.size() != width)
-    {
-      error().source_location=expr.find_source_location();
-      error() << "wrong value length in constant: "
-              << expr.pretty() << eom;
-      throw 0;
-    }
-
     for(std::size_t i=0; i<width; i++)
     {
       const bool bit = get_bitvector_bit(value, i);

src/util/arith_tools.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 #include "std_types.h"
 #include "std_expr.h"
 
+#include <algorithm>
+
 bool to_integer(const exprt &expr, mp_integer &int_value)
 {
   if(!expr.is_constant())
@@ -281,10 +283,31 @@ void mp_max(mp_integer &a, const mp_integer &b)
 /// \param bit_index: index (0 is the least significant)
 bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
 {
-  // The representation is binary, using '0'/'1',
-  // most significant bit first.
-  PRECONDITION(bit_index < src.size());
-  return src[src.size() - 1 - bit_index] == '1';
+  // The representation is hex, most significant nibble first.
+  const auto nibble_index = bit_index >> 2;
+
+  if(nibble_index >= src.size())
+    return false;
+
+  char nibble = src[src.size() - 1 - nibble_index];
+
+  DATA_INVARIANT(isxdigit(nibble), "");
+
+  unsigned nibble_value =
+    isdigit(nibble) ? nibble - '0'
+                    : islower(nibble) ? nibble - 'a' + 10 : nibble - 'A' + 10;
+
+  return ((nibble_value >> (bit_index & 3)) & 1) != 0;
+}
+
+static char nibble2hex(unsigned nibble)
+{
+  PRECONDITION(nibble <= 0xf);
+
+  if(nibble >= 10)
+    return 'A' + nibble - 10;
+  else
+    return '0' + nibble;
 }
 
 /// construct a bit-vector representation from a functor
@@ -294,12 +317,36 @@ bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
 irep_idt
 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
 {
-  std::string result(width, ' ');
+  std::string result;
+  result.reserve(width / 4 + 1);
+  unsigned nibble = 0;
 
   for(std::size_t i = 0; i < width; i++)
-    result[width - 1 - i] = f(i) ? '1' : '0';
+  {
+    const auto bit_in_nibble = i % 4;
 
-  return result;
+    nibble |= ((unsigned)f(i)) << bit_in_nibble;
+
+    if(bit_in_nibble == 3)
+    {
+      result += nibble2hex(nibble);
+      nibble = 0;
+    }
+  }
+
+  if(nibble != 0)
+    result += nibble2hex(nibble);
+
+  // drop leading zeros
+  while(!result.empty() && result.back() == '0')
+    result.resize(result.size() - 1);
+
+  std::reverse(result.begin(), result.end());
+
+  if(result.empty())
+    return ID_0;
+  else
+    return result;
 }
 
 /// perform a binary bit-wise operation, given as a functor,

src/util/mp_arith.cpp

@@ -186,17 +186,53 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
 }
 
 /// convert an integer to bit-vector representation with given width
+/// This uses two's complement for negative numbers.
+/// If the value is out of range, it is 'wrapped around'.
 const std::string integer2bv(const mp_integer &src, std::size_t width)
 {
-  return integer2binary(src, width);
+  const mp_integer p = power(2, width);
+
+  if(src.is_negative())
+  {
+    // do two's complement encoding of negative numbers
+    mp_integer tmp = src;
+    tmp.negate();
+    tmp %= p;
+    if(tmp != 0)
+      tmp = p - tmp;
+    return integer2string(tmp, 16);
+  }
+  else
+  {
+    // we 'wrap around' if 'src' is too large
+    return integer2string(src % p, 16);
+  }
 }
 
 /// convert a bit-vector representation (possibly signed) to integer
 const mp_integer
 bv2integer(const std::string &src, std::size_t width, bool is_signed)
 {
-  PRECONDITION(src.size() == width);
-  return binary2integer(src, is_signed);
+  if(is_signed)
+  {
+    PRECONDITION(width >= 1);
+    const auto tmp = string2integer(src, 16);
+    const auto p = power(2, width - 1);
+    if(tmp >= p)
+    {
+      const auto result = tmp - 2 * p;
+      PRECONDITION(result >= -p);
+      return result;
+    }
+    else
+      return tmp;
+  }
+  else
+  {
+    const auto result = string2integer(src, 16);
+    PRECONDITION(result < power(2, width));
+    return result;
+  }
 }
 
 mp_integer::ullong_t integer2ulong(const mp_integer &n)