Skip to content

Commit c4124b6

Browse files
author
Daniel Kroening
committed
bv2integer is now told the width
1 parent ee4edcb commit c4124b6

12 files changed

+67
-81
lines changed

‎src/ansi-c/expr2c.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1811,9 +1811,10 @@ std::string expr2ct::convert_constant(
18111811
if(c_enum_type.id()!=ID_c_enum)
18121812
return convert_norep(src, precedence);
18131813

1814-
bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
1814+
const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
1815+
const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
18151816

1816-
mp_integer int_value = bv2integer(id2string(value), is_signed);
1817+
mp_integer int_value = bv2integer(id2string(value), width, is_signed);
18171818
mp_integer i=0;
18181819

18191820
irep_idt int_value_string=integer2string(int_value);
@@ -1849,8 +1850,10 @@ std::string expr2ct::convert_constant(
18491850
type.id()==ID_c_bit_field ||
18501851
type.id()==ID_c_bool)
18511852
{
1853+
const auto width = to_bitvector_type(type).get_width();
1854+
18521855
mp_integer int_value =
1853-
bv2integer(id2string(value), type.id() == ID_signedbv);
1856+
bv2integer(id2string(value), width, type.id() == ID_signedbv);
18541857

18551858
const irep_idt &c_type=
18561859
type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):

‎src/goto-programs/goto_trace.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -136,17 +136,18 @@ static std::string numeric_representation(
136136
std::string result;
137137
std::string prefix;
138138

139+
const irep_idt &value = expr.get_value();
140+
139141
if(options.hex_representation)
140142
{
141-
mp_integer value_int =
142-
bv2integer(id2string(expr.get_value()), false);
143+
mp_integer value_int = bv2integer(id2string(value), value.size(), false);
143144
result = integer2string(value_int, 16);
144145
prefix = "0x";
145146
}
146147
else
147148
{
148149
prefix = "0b";
149-
result = id2string(expr.get_value());
150+
result = id2string(value);
150151
}
151152

152153
std::ostringstream oss;

‎src/goto-programs/interpreter_evaluate.cpp

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -382,7 +382,8 @@ void interpretert::evaluate(
382382
else if(expr.type().id()==ID_c_bool)
383383
{
384384
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));
386387
return;
387388
}
388389
else if(expr.type().id()==ID_bool)
@@ -981,16 +982,16 @@ void interpretert::evaluate(
981982
}
982983
else if(expr.type().id()==ID_signedbv)
983984
{
984-
const std::string s =
985-
integer2bv(value, to_signedbv_type(expr.type()).get_width());
986-
dest.push_back(bv2integer(s, true));
985+
const auto width = to_signedbv_type(expr.type()).get_width();
986+
const std::string s = integer2bv(value, width);
987+
dest.push_back(bv2integer(s, width, true));
987988
return;
988989
}
989990
else if(expr.type().id()==ID_unsignedbv)
990991
{
991-
const std::string s =
992-
integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
993-
dest.push_back(bv2integer(s, false));
992+
const auto width = to_unsignedbv_type(expr.type()).get_width();
993+
const std::string s = integer2bv(value, width);
994+
dest.push_back(bv2integer(s, width, false));
994995
return;
995996
}
996997
else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))

‎src/util/arith_tools.cpp

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -43,44 +43,57 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
4343
}
4444
else if(type_id==ID_unsignedbv)
4545
{
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);
4748
return false;
4849
}
4950
else if(type_id==ID_signedbv)
5051
{
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);
5254
return false;
5355
}
5456
else if(type_id==ID_c_bool)
5557
{
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);
5760
return false;
5861
}
5962
else if(type_id==ID_c_enum)
6063
{
6164
const typet &subtype=to_c_enum_type(type).subtype();
6265
if(subtype.id()==ID_signedbv)
6366
{
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);
6569
return false;
6670
}
6771
else if(subtype.id()==ID_unsignedbv)
6872
{
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);
7075
return false;
7176
}
7277
}
7378
else if(type_id==ID_c_bit_field)
7479
{
75-
const typet &subtype=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+
7684
if(subtype.id()==ID_signedbv)
7785
{
78-
int_value = bv2integer(id2string(value), true);
86+
int_value = bv2integer(id2string(value), width, true);
7987
return false;
8088
}
8189
else if(subtype.id()==ID_unsignedbv)
8290
{
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);
8497
return false;
8598
}
8699
}

‎src/util/bv_arithmetic.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)
184184
{
185185
PRECONDITION(expr.is_constant());
186186
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);
188188
}

‎src/util/expr.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -245,7 +245,8 @@ bool exprt::is_one() const
245245
}
246246
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
247247
{
248-
mp_integer int_value = bv2integer(value, false);
248+
const auto width = to_bitvector_type(type()).get_width();
249+
mp_integer int_value = bv2integer(value, width, false);
249250
if(int_value==1)
250251
return true;
251252
}

‎src/util/fixedbv.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)
2626
void fixedbvt::from_expr(const constant_exprt &expr)
2727
{
2828
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);
3030
}
3131

3232
void fixedbvt::from_integer(const mp_integer &i)

‎src/util/ieee_float.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
10621062
void ieee_floatt::from_expr(const constant_exprt &expr)
10631063
{
10641064
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));
10661066
}
10671067

10681068
mp_integer ieee_floatt::to_integer() const

‎src/util/mp_arith.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,10 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)
192192
}
193193

194194
/// 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)
196197
{
198+
PRECONDITION(src.size() == width);
197199
return binary2integer(src, is_signed);
198200
}
199201

‎src/util/mp_arith.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,8 @@ const mp_integer binary2integer(const std::string &, bool is_signed);
5656
const std::string integer2bv(const mp_integer &, std::size_t width);
5757

5858
/// convert a bit-vector representation (possibly signed) to integer
59-
const mp_integer bv2integer(const std::string &, bool is_signed);
59+
const mp_integer
60+
bv2integer(const std::string &, std::size_t width, bool is_signed);
6061

6162
/// \deprecated use numeric_cast_v<unsigned long long> instead
6263
DEPRECATED("Use numeric_cast_v<unsigned long long> instead")

‎src/util/simplify_expr.cpp

Lines changed: 15 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -677,7 +677,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
677677
expr_type_id==ID_signedbv ||
678678
expr_type_id==ID_floatbv)
679679
{
680-
mp_integer int_value = bv2integer(id2string(value), false);
680+
const auto width = to_bv_type(op_type).get_width();
681+
mp_integer int_value = bv2integer(id2string(value), width, false);
681682
expr=from_integer(int_value, expr_type);
682683
return false;
683684
}
@@ -819,71 +820,32 @@ bool simplify_exprt::simplify_if_implies(
819820
expr.op1().is_constant() &&
820821
cond.op1().type()==expr.op1().type())
821822
{
822-
const irep_idt &type_id=cond.op1().type().id();
823-
if(type_id==ID_integer || type_id==ID_natural)
824-
{
825-
if(string2integer(cond.op1().get_string(ID_value))>=
826-
string2integer(expr.op1().get_string(ID_value)))
827-
{
828-
new_truth = true;
829-
return false;
830-
}
831-
}
832-
else if(type_id==ID_unsignedbv)
833-
{
834-
const mp_integer i1, i2;
835-
if(
836-
bv2integer(cond.op1().get_string(ID_value), false) >=
837-
bv2integer(expr.op1().get_string(ID_value), false))
838-
{
839-
new_truth = true;
840-
return false;
841-
}
842-
}
843-
else if(type_id==ID_signedbv)
823+
mp_integer i1, i2;
824+
825+
if(
826+
!to_integer(to_constant_expr(cond.op1()), i1) &&
827+
!to_integer(to_constant_expr(expr.op1()), i2))
844828
{
845-
const mp_integer i1, i2;
846-
if(
847-
bv2integer(cond.op1().get_string(ID_value), true) >=
848-
bv2integer(expr.op1().get_string(ID_value), true))
829+
if(i1 >= i2)
849830
{
850831
new_truth = true;
851832
return false;
852833
}
853834
}
854835
}
836+
855837
if(cond.op1()==expr.op1() &&
856838
cond.op0().is_constant() &&
857839
expr.op0().is_constant() &&
858840
cond.op0().type()==expr.op0().type())
859841
{
860-
const irep_idt &type_id = cond.op1().type().id();
861-
if(type_id==ID_integer || type_id==ID_natural)
862-
{
863-
if(string2integer(cond.op1().get_string(ID_value))<=
864-
string2integer(expr.op1().get_string(ID_value)))
865-
{
866-
new_truth = true;
867-
return false;
868-
}
869-
}
870-
else if(type_id==ID_unsignedbv)
871-
{
872-
const mp_integer i1, i2;
873-
if(
874-
bv2integer(cond.op1().get_string(ID_value), false) <=
875-
bv2integer(expr.op1().get_string(ID_value), false))
876-
{
877-
new_truth = true;
878-
return false;
879-
}
880-
}
881-
else if(type_id==ID_signedbv)
842+
mp_integer i1, i2;
843+
844+
if(
845+
!to_integer(to_constant_expr(cond.op0()), i1) &&
846+
!to_integer(to_constant_expr(expr.op0()), i2))
882847
{
883-
const mp_integer i1, i2;
884-
if(
885-
bv2integer(cond.op1().get_string(ID_value), true) <=
886-
bv2integer(expr.op1().get_string(ID_value), true))
848+
if(i1 <= i2)
887849
{
888850
new_truth = true;
889851
return false;

‎src/util/simplify_expr_pointer.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,9 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
387387
else
388388
{
389389
// this is a pointer, we can't use to_integer
390-
mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
390+
const auto width = to_pointer_type(ptr.type()).get_width();
391+
mp_integer number =
392+
bv2integer(id2string(c_ptr.get_value()), width, false);
391393
// a null pointer would have been caught above, return value 0
392394
// will indicate that conversion failed
393395
if(number==0)

0 commit comments

Comments
 (0)