Skip to content

Commit 9b96fd1

Browse files
author
Daniel Kroening
committed
bv2integer is now told the width
1 parent 2f080ef commit 9b96fd1

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)
@@ -983,16 +984,16 @@ void interpretert::evaluate(
983984
}
984985
else if(expr.type().id()==ID_signedbv)
985986
{
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));
989990
return;
990991
}
991992
else if(expr.type().id()==ID_unsignedbv)
992993
{
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));
996997
return;
997998
}
998999
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 = 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+
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
@@ -246,8 +246,9 @@ bool exprt::is_one() const
246246
}
247247
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
248248
{
249+
const auto width = to_bitvector_type(type()).get_width();
249250
mp_integer int_value =
250-
bv2integer(id2string(constant_expr.get_value()), false);
251+
bv2integer(id2string(constant_expr.get_value()), width, false);
251252
if(int_value==1)
252253
return true;
253254
}

‎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
@@ -55,7 +55,8 @@ const mp_integer binary2integer(const std::string &, bool is_signed);
5555
const std::string integer2bv(const mp_integer &, std::size_t width);
5656

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

6061
/// \deprecated use numeric_cast_v<unsigned long long> instead
6162
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
@@ -669,7 +669,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
669669
expr_type_id==ID_signedbv ||
670670
expr_type_id==ID_floatbv)
671671
{
672-
mp_integer int_value = bv2integer(id2string(value), false);
672+
const auto width = to_bv_type(op_type).get_width();
673+
mp_integer int_value = bv2integer(id2string(value), width, false);
673674
expr=from_integer(int_value, expr_type);
674675
return false;
675676
}
@@ -811,71 +812,32 @@ bool simplify_exprt::simplify_if_implies(
811812
expr.op1().is_constant() &&
812813
cond.op1().type()==expr.op1().type())
813814
{
814-
const irep_idt &type_id=cond.op1().type().id();
815-
if(type_id==ID_integer || type_id==ID_natural)
816-
{
817-
if(string2integer(cond.op1().get_string(ID_value))>=
818-
string2integer(expr.op1().get_string(ID_value)))
819-
{
820-
new_truth = true;
821-
return false;
822-
}
823-
}
824-
else if(type_id==ID_unsignedbv)
825-
{
826-
const mp_integer i1, i2;
827-
if(
828-
bv2integer(cond.op1().get_string(ID_value), false) >=
829-
bv2integer(expr.op1().get_string(ID_value), false))
830-
{
831-
new_truth = true;
832-
return false;
833-
}
834-
}
835-
else if(type_id==ID_signedbv)
815+
mp_integer i1, i2;
816+
817+
if(
818+
!to_integer(to_constant_expr(cond.op1()), i1) &&
819+
!to_integer(to_constant_expr(expr.op1()), i2))
836820
{
837-
const mp_integer i1, i2;
838-
if(
839-
bv2integer(cond.op1().get_string(ID_value), true) >=
840-
bv2integer(expr.op1().get_string(ID_value), true))
821+
if(i1 >= i2)
841822
{
842823
new_truth = true;
843824
return false;
844825
}
845826
}
846827
}
828+
847829
if(cond.op1()==expr.op1() &&
848830
cond.op0().is_constant() &&
849831
expr.op0().is_constant() &&
850832
cond.op0().type()==expr.op0().type())
851833
{
852-
const irep_idt &type_id = cond.op1().type().id();
853-
if(type_id==ID_integer || type_id==ID_natural)
854-
{
855-
if(string2integer(cond.op1().get_string(ID_value))<=
856-
string2integer(expr.op1().get_string(ID_value)))
857-
{
858-
new_truth = true;
859-
return false;
860-
}
861-
}
862-
else if(type_id==ID_unsignedbv)
863-
{
864-
const mp_integer i1, i2;
865-
if(
866-
bv2integer(cond.op1().get_string(ID_value), false) <=
867-
bv2integer(expr.op1().get_string(ID_value), false))
868-
{
869-
new_truth = true;
870-
return false;
871-
}
872-
}
873-
else if(type_id==ID_signedbv)
834+
mp_integer i1, i2;
835+
836+
if(
837+
!to_integer(to_constant_expr(cond.op0()), i1) &&
838+
!to_integer(to_constant_expr(expr.op0()), i2))
874839
{
875-
const mp_integer i1, i2;
876-
if(
877-
bv2integer(cond.op1().get_string(ID_value), true) <=
878-
bv2integer(expr.op1().get_string(ID_value), true))
840+
if(i1 <= i2)
879841
{
880842
new_truth = true;
881843
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)