Merge pull request #3199 from diffblue/bvirep-cleanup

bitvector representation cleanup

Author: kroening

src/solvers/flattening/boolbv_get.cpp

@@ -215,6 +215,7 @@ exprt boolbvt::bv_get_rec(
     }
   }
 
+  // most significant bit first
   std::string value;
 
   for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
@@ -261,7 +262,11 @@ exprt boolbvt::bv_get_rec(
 
   default:
   case bvtypet::IS_C_ENUM:
-    return constant_exprt(value, type);
+  {
+    const irep_idt bvrep = make_bvrep(
+      width, [&value](size_t i) { return value[value.size() - i - 1] == '1'; });
+    return constant_exprt(bvrep, type);
+  }
   }
 
   return nil_exprt();

src/solvers/flattening/bv_pointers.cpp

@@ -633,7 +633,11 @@ exprt bv_pointerst::bv_get_rec(
   // we treat these like bit-vector constants, but with
   // some additional annotation
 
-  constant_exprt result(value, type);
+  const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
+    return value[value.size() - 1 - i] == '1';
+  });
+
+  constant_exprt result(bvrep, type);
 
   pointer_logict::pointert pointer;
   pointer.object=integer2size_t(binary2integer(value_addr, false));

src/solvers/lowering/popcount.cpp

@@ -47,7 +47,8 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
     bitstring.reserve(new_width);
     for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
       bitstring += std::string(shift, '0') + std::string(shift, '1');
-    constant_exprt bitmask(bitstring, x.type());
+    const mp_integer value = binary2integer(bitstring, false);
+    constant_exprt bitmask(integer2bv(value, new_width), x.type());
     // build the expression
     x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
   }

src/solvers/refinement/string_refinement.cpp

@@ -1449,8 +1449,8 @@ static exprt sum_over_map(
     int second=negated?(-term.second):term.second;
     if(t.id()==ID_constant)
     {
-      std::string value(to_constant_expr(t).get_value().c_str());
-      constants+=binary2integer(value, true)*second;
+      const auto int_value = numeric_cast_v<mp_integer>(to_constant_expr(t));
+      constants += int_value * second;
     }
     else
     {

src/util/json_expr.cpp

@@ -217,6 +217,13 @@ json_objectt json(
   return result;
 }
 
+static std::string binary(const constant_exprt &src)
+{
+  const auto width = to_bitvector_type(src.type()).get_width();
+  const auto int_val = bv2integer(id2string(src.get_value()), width, false);
+  return integer2binary(int_val, width);
+}
+
 /// Output a CBMC expression in json.
 /// The mode is used to correctly report types.
 /// \param expr: an expression
@@ -263,15 +270,15 @@ json_objectt json(
       std::size_t width=to_bitvector_type(type).get_width();
 
       result["name"]=json_stringt("integer");
-      result["binary"] = json_stringt(constant_expr.get_value());
+      result["binary"] = json_stringt(binary(constant_expr));
       result["width"]=json_numbert(std::to_string(width));
       result["type"]=json_stringt(type_string);
       result["data"]=json_stringt(value_string);
     }
     else if(type.id()==ID_c_enum)
     {
       result["name"]=json_stringt("integer");
-      result["binary"] = json_stringt(constant_expr.get_value());
+      result["binary"] = json_stringt(binary(constant_expr));
       result["width"] =
         json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));
       result["type"]=json_stringt("enum");
@@ -287,21 +294,21 @@ json_objectt json(
     else if(type.id()==ID_bv)
     {
       result["name"]=json_stringt("bitvector");
-      result["binary"] = json_stringt(constant_expr.get_value());
+      result["binary"] = json_stringt(binary(constant_expr));
     }
     else if(type.id()==ID_fixedbv)
     {
       result["name"]=json_stringt("fixed");
       result["width"]=json_numbert(type.get_string(ID_width));
-      result["binary"] = json_stringt(constant_expr.get_value());
+      result["binary"] = json_stringt(binary(constant_expr));
       result["data"]=
         json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
     }
     else if(type.id()==ID_floatbv)
     {
       result["name"]=json_stringt("float");
       result["width"]=json_numbert(type.get_string(ID_width));
-      result["binary"] = json_stringt(constant_expr.get_value());
+      result["binary"] = json_stringt(binary(constant_expr));
       result["data"]=
         json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
     }

src/util/simplify_expr.cpp

@@ -1458,7 +1458,9 @@ exprt simplify_exprt::bits2expr(
       tmp[i]=bits[map.map_bit(i)];
 
     std::reverse(tmp.begin(), tmp.end());
-    return constant_exprt(tmp, type);
+
+    mp_integer i = binary2integer(tmp, false);
+    return constant_exprt(integer2bv(i, bits.size()), type);
   }
   else if(type.id()==ID_c_enum)
   {
@@ -1567,14 +1569,15 @@ optionalt<std::string> simplify_exprt::expr2bits(
        type.id()==ID_floatbv ||
        type.id()==ID_fixedbv)
     {
-      std::string nat=id2string(to_constant_expr(expr).get_value());
-      std::reverse(nat.begin(), nat.end());
+      const auto width = to_bitvector_type(type).get_width();
+      const auto &bvrep = to_constant_expr(expr).get_value();
 
       endianness_mapt map(type, little_endian, ns);
 
-      std::string result=nat;
-      for(std::string::size_type i=0; i<nat.size(); ++i)
-        result[map.map_bit(i)]=nat[i];
+      std::string result(width, ' ');
+
+      for(std::string::size_type i = 0; i < width; ++i)
+        result[map.map_bit(i)] = get_bitvector_bit(bvrep, width, i) ? '1' : '0';
 
       return result;
     }

src/util/simplify_expr_int.cpp

@@ -787,10 +787,12 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
         it!=expr.operands().end();
         ) // no it++
     {
-      if(it->is_constant() &&
-         id2string(to_constant_expr(*it).get_value()).find('0')==
-           std::string::npos &&
-         expr.operands().size()>1)
+      if(
+        it->is_constant() &&
+        bv2integer(
+          id2string(to_constant_expr(*it).get_value()), width, false) ==
+          power(2, width) - 1 &&
+        expr.operands().size() > 1)
       {
         it=expr.operands().erase(it);
         result=false;
@@ -885,8 +887,9 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
       exprt &op=*it;
       if(op.is_true() || op.is_false())
       {
-        bool value=op.is_true();
-        op=constant_exprt(value?ID_1:ID_0, unsignedbv_typet(1));
+        const bool value = op.is_true();
+        op = from_integer(value, unsignedbv_typet(1));
+        result = false;
       }
     }
 
@@ -904,13 +907,24 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
          is_bitvector_type(opn.type()))
       {
         // merge!
-        const std::string new_value=
-          opi.get_string(ID_value)+opn.get_string(ID_value);
-        opi.set(ID_value, new_value);
-        opi.type().set(ID_width, new_value.size());
+        const auto &value_i = to_constant_expr(opi).get_value();
+        const auto &value_n = to_constant_expr(opn).get_value();
+        const auto width_i = to_bitvector_type(opi.type()).get_width();
+        const auto width_n = to_bitvector_type(opn.type()).get_width();
+        const auto new_width = width_i + width_n;
+
+        const auto new_value = make_bvrep(
+          new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
+            return x < width_n
+                     ? get_bitvector_bit(value_n, width_n, x)
+                     : get_bitvector_bit(value_i, width_i, x - width_n);
+          });
+
+        to_constant_expr(opi).set_value(new_value);
+        opi.type().set(ID_width, new_width);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
-        result=true;
+        result = false;
       }
       else
         i++;
@@ -941,7 +955,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
         opi.type().id(ID_verilog_unsignedbv);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
-        result=true;
+        result = false;
       }
       else
         i++;
@@ -1269,13 +1283,15 @@ bool simplify_exprt::simplify_bitnot(exprt &expr)
 
   exprt &op=operands.front();
 
-  if(expr.type().id()==ID_bv ||
-     expr.type().id()==ID_unsignedbv ||
-     expr.type().id()==ID_signedbv)
+  const auto &type = expr.type();
+
+  if(
+    type.id() == ID_bv || type.id() == ID_unsignedbv ||
+    type.id() == ID_signedbv)
   {
-    const auto width = to_bitvector_type(expr.type()).get_width();
+    const auto width = to_bitvector_type(type).get_width();
 
-    if(op.type()==expr.type())
+    if(op.type() == type)
     {
       if(op.id()==ID_constant)
       {