support for base 256 bitvector representation

Author: Daniel Kroening

src/util/arith_tools.cpp

@@ -278,11 +278,23 @@ void mp_max(mp_integer &a, const mp_integer &b)
     a=b;
 }
 
+#define B256
+
 /// Get a bit with given index from bit-vector representation.
 /// \param src: the bitvector representation
 /// \param bit_index: index (0 is the least significant)
 bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
 {
+#ifdef B256
+  const auto byte_index = bit_index >> 3;
+
+  if(byte_index >= src.size())
+    return false;
+
+  unsigned char byte = src[src.size() - 1 - byte_index];
+
+  return ((byte >> (bit_index & 7)) & 1) != 0;
+#else
   // The representation is hex, most significant nibble first.
   const auto nibble_index = bit_index >> 2;
 
@@ -298,8 +310,10 @@ bool get_bitvector_bit(const irep_idt &src, std::size_t bit_index)
                     : islower(nibble) ? nibble - 'a' + 10 : nibble - 'A' + 10;
 
   return ((nibble_value >> (bit_index & 3)) & 1) != 0;
+#endif
 }
 
+#ifndef B256
 static char nibble2hex(unsigned nibble)
 {
   PRECONDITION(nibble <= 0xf);
@@ -309,6 +323,7 @@ static char nibble2hex(unsigned nibble)
   else
     return '0' + nibble;
 }
+#endif
 
 /// construct a bit-vector representation from a functor
 /// \param width: the width of the bit-vector
@@ -317,6 +332,35 @@ static char nibble2hex(unsigned nibble)
 irep_idt
 make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
 {
+#ifdef B256
+  std::string result;
+  result.reserve(width / 8 + 1);
+  unsigned byte = 0;
+
+  for(std::size_t i = 0; i < width; i++)
+  {
+    const auto bit_in_byte = i % 8;
+
+    byte |= ((unsigned)f(i)) << bit_in_byte;
+
+    if(bit_in_byte == 7)
+    {
+      result += (char)byte;
+      byte = 0;
+    }
+  }
+
+  if(byte != 0)
+    result += (char)byte;
+
+  // drop leading zeros
+  while(!result.empty() && result.back() == 0)
+    result.resize(result.size() - 1);
+
+  std::reverse(result.begin(), result.end());
+
+  return result;
+#else
   std::string result;
   result.reserve(width / 4 + 1);
   unsigned nibble = 0;
@@ -347,6 +391,7 @@ make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
     return ID_0;
   else
     return result;
+#endif
 }
 
 /// perform a binary bit-wise operation, given as a functor,

src/util/expr.cpp

@@ -165,6 +165,8 @@ bool exprt::is_boolean() const
   return type().id()==ID_bool;
 }
 
+#define B256
+
 /// Return whether the expression is a constant representing 0.
 /// Will consider the following types: ID_integer, ID_natural, ID_rational,
 /// ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv,
@@ -195,7 +197,11 @@ bool exprt::is_zero() const
       type_id == ID_unsignedbv || type_id == ID_signedbv ||
       type_id == ID_c_bool || type_id == ID_c_bit_field)
     {
+#ifdef B256
+      return constant.get_value().empty();
+#else
       return constant.value_is_zero_string();
+#endif
     }
     else if(type_id==ID_fixedbv)
     {

src/util/mp_arith.cpp

@@ -185,11 +185,47 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
   #endif
 }
 
+#define B256
+
+#ifdef B256
+std::string dump_integer(mp_integer src)
+{
+  std::size_t d = src.digits(256) + 1;
+  unsigned char *buf = new unsigned char[d], *p = buf;
+  src.dump(buf, d);
+  while(d > 0 && *p == 0)
+  {
+    d--;
+    p++;
+  }
+  return std::string((char *)p, d);
+}
+#endif
+
 /// 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)
 {
+#ifdef B256
+  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 dump_integer(tmp);
+  }
+  else
+  {
+    // we 'wrap around' if 'src' is too large
+    return dump_integer(src % p);
+  }
+#else
   const mp_integer p = power(2, width);
 
   if(src.is_negative())
@@ -207,12 +243,37 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)
     // we 'wrap around' if 'src' is too large
     return integer2string(src % p, 16);
   }
+#endif
 }
 
 /// convert a bit-vector representation (possibly signed) to integer
 const mp_integer
 bv2integer(const std::string &src, std::size_t width, bool is_signed)
 {
+#ifdef B256
+  if(is_signed)
+  {
+    PRECONDITION(width >= 1);
+    mp_integer tmp;
+    tmp.load((const unsigned char *)src.data(), src.size());
+    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
+  {
+    mp_integer result;
+    result.load((const unsigned char *)src.data(), src.size());
+    PRECONDITION(result < power(2, width));
+    return result;
+  }
+#else
   if(is_signed)
   {
     PRECONDITION(width >= 1);
@@ -233,6 +294,7 @@ bv2integer(const std::string &src, std::size_t width, bool is_signed)
     PRECONDITION(result < power(2, width));
     return result;
   }
+#endif
 }
 
 mp_integer::ullong_t integer2ulong(const mp_integer &n)