introduce integer2bv and bv2integer

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

@@ -86,7 +86,7 @@ static const std::string get_thread_block_identifier(
 {
   PRECONDITION(f_code.arguments().size() == 1);
   const exprt &expr = f_code.arguments()[0];
-  mp_integer lbl_id = binary2integer(expr.op0().get_string(ID_value), false);
+  mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
   return integer2string(lbl_id);
 }
 

src/ansi-c/expr2c.cpp

@@ -1813,7 +1813,7 @@ std::string expr2ct::convert_constant(
 
     bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
 
-    mp_integer int_value=binary2integer(id2string(value), is_signed);
+    mp_integer int_value = bv2integer(id2string(value), is_signed);
     mp_integer i=0;
 
     irep_idt int_value_string=integer2string(int_value);
@@ -1849,8 +1849,8 @@ std::string expr2ct::convert_constant(
           type.id()==ID_c_bit_field ||
           type.id()==ID_c_bool)
   {
-    mp_integer int_value=
-      binary2integer(id2string(value), type.id()==ID_signedbv);
+    mp_integer int_value =
+      bv2integer(id2string(value), type.id() == ID_signedbv);
 
     const irep_idt &c_type=
       type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):

src/goto-cc/linker_script_merge.cpp

@@ -566,7 +566,7 @@ int linker_script_merget::ls_data2instructions(
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
     constant_exprt rhs(
-      integer2binary(
+      integer2bv(
         string2integer(id2string(symbol_value)),
         unsigned_int_type().get_width()),
       unsigned_int_type());
@@ -632,8 +632,8 @@ int linker_script_merget::ls_data2instructions(
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
     constant_exprt rhs;
-    rhs.set_value(integer2binary(string2integer(d["val"].value),
-          unsigned_int_type().get_width()));
+    rhs.set_value(integer2bv(
+      string2integer(d["val"].value), unsigned_int_type().get_width()));
     rhs.type()=unsigned_int_type();
 
     exprt rhs_tc(rhs);

src/goto-programs/goto_convert.cpp

@@ -1834,8 +1834,8 @@ bool goto_convertt::get_string_constant(
       forall_operands(it, index_op)
         if(it->is_constant())
         {
-          unsigned long i=integer2ulong(
-            binary2integer(id2string(to_constant_expr(*it).get_value()), true));
+          unsigned long i = integer2ulong(
+            bv2integer(id2string(to_constant_expr(*it).get_value()), true));
 
           if(i!=0) // to skip terminating 0
             result+=static_cast<char>(i);

src/goto-programs/goto_trace.cpp

@@ -137,7 +137,7 @@ numeric_representation(const exprt &expr, const trace_optionst &options)
   if(options.hex_representation)
   {
     mp_integer value_int =
-      binary2integer(id2string(to_constant_expr(expr).get_value()), false);
+      bv2integer(id2string(to_constant_expr(expr).get_value()), false);
     result = integer2string(value_int, 16);
     prefix = "0x";
   }

src/goto-programs/interpreter_evaluate.cpp

@@ -382,7 +382,7 @@ void interpretert::evaluate(
     else if(expr.type().id()==ID_c_bool)
     {
       const irep_idt &value=to_constant_expr(expr).get_value();
-      dest.push_back(binary2integer(id2string(value), false));
+      dest.push_back(bv2integer(id2string(value), false));
       return;
     }
     else if(expr.type().id()==ID_bool)
@@ -981,16 +981,16 @@ void interpretert::evaluate(
       }
       else if(expr.type().id()==ID_signedbv)
       {
-        const std::string s=
-          integer2binary(value, to_signedbv_type(expr.type()).get_width());
-        dest.push_back(binary2integer(s, true));
+        const std::string s =
+          integer2bv(value, to_signedbv_type(expr.type()).get_width());
+        dest.push_back(bv2integer(s, true));
         return;
       }
       else if(expr.type().id()==ID_unsignedbv)
       {
-        const std::string s=
-          integer2binary(value, to_unsignedbv_type(expr.type()).get_width());
-        dest.push_back(binary2integer(s, false));
+        const std::string s =
+          integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
+        dest.push_back(bv2integer(s, false));
         return;
       }
       else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))

src/util/arith_tools.cpp

@@ -43,30 +43,30 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   }
   else if(type_id==ID_unsignedbv)
   {
-    int_value=binary2integer(id2string(value), false);
+    int_value = bv2integer(id2string(value), false);
     return false;
   }
   else if(type_id==ID_signedbv)
   {
-    int_value=binary2integer(id2string(value), true);
+    int_value = bv2integer(id2string(value), true);
     return false;
   }
   else if(type_id==ID_c_bool)
   {
-    int_value=binary2integer(id2string(value), false);
+    int_value = bv2integer(id2string(value), false);
     return false;
   }
   else if(type_id==ID_c_enum)
   {
     const typet &subtype=to_c_enum_type(type).subtype();
     if(subtype.id()==ID_signedbv)
     {
-      int_value=binary2integer(id2string(value), true);
+      int_value = bv2integer(id2string(value), true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value=binary2integer(id2string(value), false);
+      int_value = bv2integer(id2string(value), false);
       return false;
     }
   }
@@ -75,12 +75,12 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
     const typet &subtype=type.subtype();
     if(subtype.id()==ID_signedbv)
     {
-      int_value=binary2integer(id2string(value), true);
+      int_value = bv2integer(id2string(value), true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value=binary2integer(id2string(value), false);
+      int_value = bv2integer(id2string(value), false);
       return false;
     }
   }
@@ -123,28 +123,28 @@ constant_exprt from_integer(
   else if(type_id==ID_unsignedbv)
   {
     std::size_t width=to_unsignedbv_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_bv)
   {
     std::size_t width=to_bv_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_signedbv)
   {
     std::size_t width=to_signedbv_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_c_enum)
   {
     const std::size_t width =
       to_c_enum_type(type).subtype().get_size_t(ID_width);
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_c_bool)
   {
     std::size_t width=to_c_bool_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_bool)
   {
@@ -162,7 +162,7 @@ constant_exprt from_integer(
   else if(type_id==ID_c_bit_field)
   {
     std::size_t width=to_c_bit_field_type(type).get_width();
-    return constant_exprt(integer2binary(int_value, width), type);
+    return constant_exprt(integer2bv(int_value, width), type);
   }
   else if(type_id==ID_fixedbv)
   {

src/util/bv_arithmetic.cpp

@@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const
 
 exprt bv_arithmetict::to_expr() const
 {
-  return constant_exprt(integer2binary(value, spec.width), spec.to_type());
+  return constant_exprt(integer2bv(value, spec.width), spec.to_type());
 }
 
 bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)
 {
   PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value=binary2integer(expr.get_string(ID_value), spec.is_signed);
+  value = bv2integer(expr.get_string(ID_value), spec.is_signed);
 }

src/util/expr.cpp

@@ -245,7 +245,7 @@ bool exprt::is_one() const
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
     {
-      mp_integer int_value=binary2integer(value, false);
+      mp_integer int_value = bv2integer(value, false);
       if(int_value==1)
         return true;
     }

src/util/fixedbv.cpp

@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)
 void fixedbvt::from_expr(const constant_exprt &expr)
 {
   spec=fixedbv_spect(to_fixedbv_type(expr.type()));
-  v=binary2integer(id2string(expr.get_value()), true);
+  v = bv2integer(id2string(expr.get_value()), true);
 }
 
 void fixedbvt::from_integer(const mp_integer &i)
@@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const
   type.set_width(spec.width);
   type.set_integer_bits(spec.integer_bits);
   PRECONDITION(spec.width != 0);
-  return constant_exprt(integer2binary(v, spec.width), type);
+  return constant_exprt(integer2bv(v, spec.width), type);
 }
 
 void fixedbvt::round(const fixedbv_spect &dest_spec)

src/util/ieee_float.cpp

@@ -696,7 +696,7 @@ void ieee_floatt::divide_and_round(
 
 constant_exprt ieee_floatt::to_expr() const
 {
-  return constant_exprt(integer2binary(pack(), spec.width()), spec.to_type());
+  return constant_exprt(integer2bv(pack(), spec.width()), spec.to_type());
 }
 
 ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
 void ieee_floatt::from_expr(const constant_exprt &expr)
 {
   spec=ieee_float_spect(to_floatbv_type(expr.type()));
-  unpack(binary2integer(id2string(expr.get_value()), false));
+  unpack(bv2integer(id2string(expr.get_value()), false));
 }
 
 mp_integer ieee_floatt::to_integer() const

src/util/mp_arith.cpp

@@ -185,6 +185,18 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
   #endif
 }
 
+/// convert an integer to bit-vector representation with given width
+const std::string integer2bv(const mp_integer &src, std::size_t width)
+{
+  return integer2binary(src, width);
+}
+
+/// convert a bit-vector representation (possibly signed) to integer
+const mp_integer bv2integer(const std::string &src, bool is_signed)
+{
+  return binary2integer(src, is_signed);
+}
+
 mp_integer::ullong_t integer2ulong(const mp_integer &n)
 {
   PRECONDITION(n.is_ulong());

src/util/mp_arith.h

@@ -52,6 +52,12 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
 const std::string integer2binary(const mp_integer &, std::size_t width);
 const mp_integer binary2integer(const std::string &, bool is_signed);
 
+/// convert an integer to bit-vector representation with given width
+const std::string integer2bv(const mp_integer &, std::size_t width);
+
+/// convert a bit-vector representation (possibly signed) to integer
+const mp_integer bv2integer(const std::string &, bool is_signed);
+
 /// \deprecated use numeric_cast_v<unsigned long long> instead
 DEPRECATED("Use numeric_cast_v<unsigned long long> instead")
 mp_integer::ullong_t integer2ulong(const mp_integer &);

src/util/simplify_expr.cpp

@@ -677,7 +677,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
          expr_type_id==ID_signedbv ||
          expr_type_id==ID_floatbv)
       {
-        mp_integer int_value=binary2integer(id2string(value), false);
+        mp_integer int_value = bv2integer(id2string(value), false);
         expr=from_integer(int_value, expr_type);
         return false;
       }
@@ -832,8 +832,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_unsignedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), false)>=
-           binary2integer(expr.op1().get_string(ID_value), false))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), false) >=
+          bv2integer(expr.op1().get_string(ID_value), false))
         {
           new_truth = true;
           return false;
@@ -842,8 +843,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_signedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), true)>=
-           binary2integer(expr.op1().get_string(ID_value), true))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), true) >=
+          bv2integer(expr.op1().get_string(ID_value), true))
         {
           new_truth = true;
           return false;
@@ -868,8 +870,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_unsignedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), false)<=
-           binary2integer(expr.op1().get_string(ID_value), false))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), false) <=
+          bv2integer(expr.op1().get_string(ID_value), false))
         {
           new_truth = true;
           return false;
@@ -878,8 +881,9 @@ bool simplify_exprt::simplify_if_implies(
       else if(type_id==ID_signedbv)
       {
         const mp_integer i1, i2;
-        if(binary2integer(cond.op1().get_string(ID_value), true)<=
-           binary2integer(expr.op1().get_string(ID_value), true))
+        if(
+          bv2integer(cond.op1().get_string(ID_value), true) <=
+          bv2integer(expr.op1().get_string(ID_value), true))
         {
           new_truth = true;
           return false;

src/util/simplify_expr_int.cpp

@@ -821,7 +821,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     }
     else if(expr.id()==ID_bitxor)
     {
-      constant_exprt new_op(integer2binary(0, width), expr.type());
+      constant_exprt new_op(integer2bv(0, width), expr.type());
       expr.swap(new_op);
       return false;
     }

src/util/simplify_expr_pointer.cpp

@@ -387,7 +387,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     else
     {
       // this is a pointer, we can't use to_integer
-      mp_integer number=binary2integer(id2string(c_ptr.get_value()), false);
+      mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
       // a null pointer would have been caught above, return value 0
       // will indicate that conversion failed
       if(number==0)