bv2integer is now told the width

kroening · kroening · commit 3487bbe7cb0a · 2018-10-18T10:22:45.000+01:00
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1811,9 +1811,10 @@ std::string expr2ct::convert_constant(
     if(c_enum_type.id()!=ID_c_enum)
       return convert_norep(src, precedence);
 
-    bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
+    const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
+    const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
 
-    mp_integer int_value = bv2integer(id2string(value), is_signed);
+    mp_integer int_value = bv2integer(id2string(value), width, is_signed);
     mp_integer i=0;
 
     irep_idt int_value_string=integer2string(int_value);
@@ -1849,8 +1850,10 @@ std::string expr2ct::convert_constant(
           type.id()==ID_c_bit_field ||
           type.id()==ID_c_bool)
   {
+    const auto width = to_bitvector_type(type).get_width();
+
     mp_integer int_value =
-      bv2integer(id2string(value), type.id() == ID_signedbv);
+      bv2integer(id2string(value), width, type.id() == ID_signedbv);
 
     const irep_idt &c_type=
       type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
@@ -136,17 +136,18 @@ static std::string numeric_representation(
   std::string result;
   std::string prefix;
 
+  const irep_idt &value = expr.get_value();
+
   if(options.hex_representation)
   {
-    mp_integer value_int =
-      bv2integer(id2string(expr.get_value()), false);
+    mp_integer value_int = bv2integer(id2string(value), value.size(), false);
     result = integer2string(value_int, 16);
     prefix = "0x";
   }
   else
   {
     prefix = "0b";
-    result = id2string(expr.get_value());
+    result = id2string(value);
   }
 
   std::ostringstream oss;
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -382,7 +382,8 @@ void interpretert::evaluate(
     else if(expr.type().id()==ID_c_bool)
     {
       const irep_idt &value=to_constant_expr(expr).get_value();
-      dest.push_back(bv2integer(id2string(value), false));
+      const auto width = to_c_bool_type(expr.type()).get_width();
+      dest.push_back(bv2integer(id2string(value), width, false));
       return;
     }
     else if(expr.type().id()==ID_bool)
@@ -983,16 +984,16 @@ void interpretert::evaluate(
       }
       else if(expr.type().id()==ID_signedbv)
       {
-        const std::string s =
-          integer2bv(value, to_signedbv_type(expr.type()).get_width());
-        dest.push_back(bv2integer(s, true));
+        const auto width = to_signedbv_type(expr.type()).get_width();
+        const std::string s = integer2bv(value, width);
+        dest.push_back(bv2integer(s, width, true));
         return;
       }
       else if(expr.type().id()==ID_unsignedbv)
       {
-        const std::string s =
-          integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
-        dest.push_back(bv2integer(s, false));
+        const auto width = to_unsignedbv_type(expr.type()).get_width();
+        const std::string s = integer2bv(value, width);
+        dest.push_back(bv2integer(s, width, false));
         return;
       }
       else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -43,44 +43,57 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   }
   else if(type_id==ID_unsignedbv)
   {
-    int_value = bv2integer(id2string(value), false);
+    const auto width = to_unsignedbv_type(type).get_width();
+    int_value = bv2integer(id2string(value), width, false);
     return false;
   }
   else if(type_id==ID_signedbv)
   {
-    int_value = bv2integer(id2string(value), true);
+    const auto width = to_signedbv_type(type).get_width();
+    int_value = bv2integer(id2string(value), width, true);
     return false;
   }
   else if(type_id==ID_c_bool)
   {
-    int_value = bv2integer(id2string(value), false);
+    const auto width = to_c_bool_type(type).get_width();
+    int_value = bv2integer(id2string(value), width, 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 = bv2integer(id2string(value), true);
+      const auto width = to_signedbv_type(type).get_width();
+      int_value = bv2integer(id2string(value), width, true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value = bv2integer(id2string(value), false);
+      const auto width = to_unsignedbv_type(type).get_width();
+      int_value = bv2integer(id2string(value), width, false);
       return false;
     }
   }
   else if(type_id==ID_c_bit_field)
   {
-    const typet &subtype = to_c_bit_field_type(type).subtype();
+    const auto &c_bit_field_type = to_c_bit_field_type(type);
+    const auto width = c_bit_field_type.get_width();
+    const typet &subtype = c_bit_field_type.subtype();
+
     if(subtype.id()==ID_signedbv)
     {
-      int_value = bv2integer(id2string(value), true);
+      int_value = bv2integer(id2string(value), width, true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value = bv2integer(id2string(value), false);
+      int_value = bv2integer(id2string(value), width, false);
+      return false;
+    }
+    else if(subtype.id()==ID_c_bool)
+    {
+      int_value = bv2integer(id2string(value), width, false);
       return false;
     }
   }
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)
 {
   PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value = bv2integer(expr.get_string(ID_value), spec.is_signed);
+  value = bv2integer(expr.get_string(ID_value), spec.width, spec.is_signed);
 }
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -246,8 +246,9 @@ bool exprt::is_one() const
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
     {
+      const auto width = to_bitvector_type(type()).get_width();
       mp_integer int_value =
-        bv2integer(id2string(constant_expr.get_value()), false);
+        bv2integer(id2string(constant_expr.get_value()), width, false);
       if(int_value==1)
         return true;
     }
diff --git a/src/util/fixedbv.cpp b/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 = bv2integer(id2string(expr.get_value()), true);
+  v = bv2integer(id2string(expr.get_value()), spec.width, true);
 }
 
 void fixedbvt::from_integer(const mp_integer &i)
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
@@ -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(bv2integer(id2string(expr.get_value()), false));
+  unpack(bv2integer(id2string(expr.get_value()), spec.width(), false));
 }
 
 mp_integer ieee_floatt::to_integer() const
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
@@ -192,8 +192,10 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)
 }
 
 /// convert a bit-vector representation (possibly signed) to integer
-const mp_integer bv2integer(const std::string &src, bool is_signed)
+const mp_integer
+bv2integer(const std::string &src, std::size_t width, bool is_signed)
 {
+  PRECONDITION(src.size() == width);
   return binary2integer(src, is_signed);
 }
 
diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h
@@ -55,7 +55,8 @@ const mp_integer binary2integer(const std::string &, bool is_signed);
 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);
+const mp_integer
+bv2integer(const std::string &, std::size_t width, bool is_signed);
 
 /// \deprecated use numeric_cast_v<unsigned long long> instead
 DEPRECATED("Use numeric_cast_v<unsigned long long> instead")
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -669,7 +669,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
          expr_type_id==ID_signedbv ||
          expr_type_id==ID_floatbv)
       {
-        mp_integer int_value = bv2integer(id2string(value), false);
+        const auto width = to_bv_type(op_type).get_width();
+        mp_integer int_value = bv2integer(id2string(value), width, false);
         expr=from_integer(int_value, expr_type);
         return false;
       }
@@ -811,71 +812,32 @@ bool simplify_exprt::simplify_if_implies(
        expr.op1().is_constant() &&
        cond.op1().type()==expr.op1().type())
     {
-      const irep_idt &type_id=cond.op1().type().id();
-      if(type_id==ID_integer || type_id==ID_natural)
-      {
-        if(string2integer(cond.op1().get_string(ID_value))>=
-           string2integer(expr.op1().get_string(ID_value)))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_unsignedbv)
-      {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), false) >=
-          bv2integer(expr.op1().get_string(ID_value), false))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_signedbv)
+      mp_integer i1, i2;
+
+      if(
+        !to_integer(to_constant_expr(cond.op1()), i1) &&
+        !to_integer(to_constant_expr(expr.op1()), i2))
       {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), true) >=
-          bv2integer(expr.op1().get_string(ID_value), true))
+        if(i1 >= i2)
         {
           new_truth = true;
           return false;
         }
       }
     }
+
     if(cond.op1()==expr.op1() &&
        cond.op0().is_constant() &&
        expr.op0().is_constant() &&
        cond.op0().type()==expr.op0().type())
     {
-      const irep_idt &type_id = cond.op1().type().id();
-      if(type_id==ID_integer || type_id==ID_natural)
-      {
-        if(string2integer(cond.op1().get_string(ID_value))<=
-           string2integer(expr.op1().get_string(ID_value)))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_unsignedbv)
-      {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), false) <=
-          bv2integer(expr.op1().get_string(ID_value), false))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_signedbv)
+      mp_integer i1, i2;
+
+      if(
+        !to_integer(to_constant_expr(cond.op0()), i1) &&
+        !to_integer(to_constant_expr(expr.op0()), i2))
       {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), true) <=
-          bv2integer(expr.op1().get_string(ID_value), true))
+        if(i1 <= i2)
         {
           new_truth = true;
           return false;
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
@@ -387,7 +387,9 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     else
     {
       // this is a pointer, we can't use to_integer
-      mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
+      const auto width = to_pointer_type(ptr.type()).get_width();
+      mp_integer number =
+        bv2integer(id2string(c_ptr.get_value()), width, false);
       // a null pointer would have been caught above, return value 0
       // will indicate that conversion failed
       if(number==0)

Original file line number	Diff line number	Diff line change
`@@ -136,17 +136,18 @@ static std::string numeric_representation(`
`136`	`136`	`std::string result;`
`137`	`137`	`std::string prefix;`
`138`	`138`
	`139`	`+ const irep_idt &value = expr.get_value();`
	`140`	`+`
`139`	`141`	`if(options.hex_representation)`
`140`	`142`	`{`
`141`		`- mp_integer value_int =`
`142`		`- bv2integer(id2string(expr.get_value()), false);`
	`143`	`+ mp_integer value_int = bv2integer(id2string(value), value.size(), false);`
`143`	`144`	`result = integer2string(value_int, 16);`
`144`	`145`	`prefix = "0x";`
`145`	`146`	`}`
`146`	`147`	`else`
`147`	`148`	`{`
`148`	`149`	`prefix = "0b";`
`149`		`- result = id2string(expr.get_value());`
	`150`	`+ result = id2string(value);`
`150`	`151`	`}`
`151`	`152`
`152`	`153`	`std::ostringstream oss;`
Original file line number	Diff line number	Diff line change
`@@ -382,7 +382,8 @@ void interpretert::evaluate(`
`382`	`382`	`else if(expr.type().id()==ID_c_bool)`
`383`	`383`	`{`
`384`	`384`	`const irep_idt &value=to_constant_expr(expr).get_value();`
`385`		`- dest.push_back(bv2integer(id2string(value), false));`
	`385`	`+ const auto width = to_c_bool_type(expr.type()).get_width();`
	`386`	`+ dest.push_back(bv2integer(id2string(value), width, false));`
`386`	`387`	`return;`
`387`	`388`	`}`
`388`	`389`	`else if(expr.type().id()==ID_bool)`
`@@ -983,16 +984,16 @@ void interpretert::evaluate(`
`983`	`984`	`}`
`984`	`985`	`else if(expr.type().id()==ID_signedbv)`
`985`	`986`	`{`
`986`		`- const std::string s =`
`987`		`- integer2bv(value, to_signedbv_type(expr.type()).get_width());`
`988`		`- dest.push_back(bv2integer(s, true));`
	`987`	`+ const auto width = to_signedbv_type(expr.type()).get_width();`
	`988`	`+ const std::string s = integer2bv(value, width);`
	`989`	`+ dest.push_back(bv2integer(s, width, true));`
`989`	`990`	`return;`
`990`	`991`	`}`
`991`	`992`	`else if(expr.type().id()==ID_unsignedbv)`
`992`	`993`	`{`
`993`		`- const std::string s =`
`994`		`- integer2bv(value, to_unsignedbv_type(expr.type()).get_width());`
`995`		`- dest.push_back(bv2integer(s, false));`
	`994`	`+ const auto width = to_unsignedbv_type(expr.type()).get_width();`
	`995`	`+ const std::string s = integer2bv(value, width);`
	`996`	`+ dest.push_back(bv2integer(s, width, false));`
`996`	`997`	`return;`
`997`	`998`	`}`
`998`	`999`	`else if((expr.type().id()==ID_bool) \|\| (expr.type().id()==ID_c_bool))`
Original file line number	Diff line number	Diff line change
`@@ -43,44 +43,57 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`43`	`43`	`}`
`44`	`44`	`else if(type_id==ID_unsignedbv)`
`45`	`45`	`{`
`46`		`- int_value = bv2integer(id2string(value), false);`
	`46`	`+ const auto width = to_unsignedbv_type(type).get_width();`
	`47`	`+ int_value = bv2integer(id2string(value), width, false);`
`47`	`48`	`return false;`
`48`	`49`	`}`
`49`	`50`	`else if(type_id==ID_signedbv)`
`50`	`51`	`{`
`51`		`- int_value = bv2integer(id2string(value), true);`
	`52`	`+ const auto width = to_signedbv_type(type).get_width();`
	`53`	`+ int_value = bv2integer(id2string(value), width, true);`
`52`	`54`	`return false;`
`53`	`55`	`}`
`54`	`56`	`else if(type_id==ID_c_bool)`
`55`	`57`	`{`
`56`		`- int_value = bv2integer(id2string(value), false);`
	`58`	`+ const auto width = to_c_bool_type(type).get_width();`
	`59`	`+ int_value = bv2integer(id2string(value), width, false);`
`57`	`60`	`return false;`
`58`	`61`	`}`
`59`	`62`	`else if(type_id==ID_c_enum)`
`60`	`63`	`{`
`61`	`64`	`const typet &subtype=to_c_enum_type(type).subtype();`
`62`	`65`	`if(subtype.id()==ID_signedbv)`
`63`	`66`	`{`
`64`		`- int_value = bv2integer(id2string(value), true);`
	`67`	`+ const auto width = to_signedbv_type(type).get_width();`
	`68`	`+ int_value = bv2integer(id2string(value), width, true);`
`65`	`69`	`return false;`
`66`	`70`	`}`
`67`	`71`	`else if(subtype.id()==ID_unsignedbv)`
`68`	`72`	`{`
`69`		`- int_value = bv2integer(id2string(value), false);`
	`73`	`+ const auto width = to_unsignedbv_type(type).get_width();`
	`74`	`+ int_value = bv2integer(id2string(value), width, false);`
`70`	`75`	`return false;`
`71`	`76`	`}`
`72`	`77`	`}`
`73`	`78`	`else if(type_id==ID_c_bit_field)`
`74`	`79`	`{`
`75`		`- const typet &subtype = to_c_bit_field_type(type).subtype();`
	`80`	`+ const auto &c_bit_field_type = to_c_bit_field_type(type);`
	`81`	`+ const auto width = c_bit_field_type.get_width();`
	`82`	`+ const typet &subtype = c_bit_field_type.subtype();`
	`83`	`+`
`76`	`84`	`if(subtype.id()==ID_signedbv)`
`77`	`85`	`{`
`78`		`- int_value = bv2integer(id2string(value), true);`
	`86`	`+ int_value = bv2integer(id2string(value), width, true);`
`79`	`87`	`return false;`
`80`	`88`	`}`
`81`	`89`	`else if(subtype.id()==ID_unsignedbv)`
`82`	`90`	`{`
`83`		`- int_value = bv2integer(id2string(value), false);`
	`91`	`+ int_value = bv2integer(id2string(value), width, false);`
	`92`	`+ return false;`
	`93`	`+ }`
	`94`	`+ else if(subtype.id()==ID_c_bool)`
	`95`	`+ {`
	`96`	`+ int_value = bv2integer(id2string(value), width, false);`
`84`	`97`	`return false;`
`85`	`98`	`}`
`86`	`99`	`}`
Original file line number	Diff line number	Diff line change
`@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)`
`184`	`184`	`{`
`185`	`185`	`PRECONDITION(expr.is_constant());`
`186`	`186`	`spec=bv_spect(expr.type());`
`187`		`- value = bv2integer(expr.get_string(ID_value), spec.is_signed);`
	`187`	`+ value = bv2integer(expr.get_string(ID_value), spec.width, spec.is_signed);`
`188`	`188`	`}`
Original file line number	Diff line number	Diff line change
`@@ -246,8 +246,9 @@ bool exprt::is_one() const`
`246`	`246`	`}`
`247`	`247`	`else if(type_id==ID_unsignedbv \|\| type_id==ID_signedbv)`
`248`	`248`	`{`
	`249`	`+ const auto width = to_bitvector_type(type()).get_width();`
`249`	`250`	`mp_integer int_value =`
`250`		`- bv2integer(id2string(constant_expr.get_value()), false);`
	`251`	`+ bv2integer(id2string(constant_expr.get_value()), width, false);`
`251`	`252`	`if(int_value==1)`
`252`	`253`	`return true;`
`253`	`254`	`}`
Original file line number	Diff line number	Diff line change
`@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)`
`26`	`26`	`void fixedbvt::from_expr(const constant_exprt &expr)`
`27`	`27`	`{`
`28`	`28`	`spec=fixedbv_spect(to_fixedbv_type(expr.type()));`
`29`		`- v = bv2integer(id2string(expr.get_value()), true);`
	`29`	`+ v = bv2integer(id2string(expr.get_value()), spec.width, true);`
`30`	`30`	`}`
`31`	`31`
`32`	`32`	`void fixedbvt::from_integer(const mp_integer &i)`
Original file line number	Diff line number	Diff line change
`@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)`
`1062`	`1062`	`void ieee_floatt::from_expr(const constant_exprt &expr)`
`1063`	`1063`	`{`
`1064`	`1064`	`spec=ieee_float_spect(to_floatbv_type(expr.type()));`
`1065`		`- unpack(bv2integer(id2string(expr.get_value()), false));`
	`1065`	`+ unpack(bv2integer(id2string(expr.get_value()), spec.width(), false));`
`1066`	`1066`	`}`
`1067`	`1067`
`1068`	`1068`	`mp_integer ieee_floatt::to_integer() const`
Original file line number	Diff line number	Diff line change
`@@ -192,8 +192,10 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)`
`192`	`192`	`}`
`193`	`193`
`194`	`194`	`/// convert a bit-vector representation (possibly signed) to integer`
`195`		`-const mp_integer bv2integer(const std::string &src, bool is_signed)`
	`195`	`+const mp_integer`
	`196`	`+bv2integer(const std::string &src, std::size_t width, bool is_signed)`
`196`	`197`	`{`
	`198`	`+ PRECONDITION(src.size() == width);`
`197`	`199`	`return binary2integer(src, is_signed);`
`198`	`200`	`}`
`199`	`201`