Skip to content

Commit 1f96e27

Browse files
author
Daniel Kroening
committed
bv2integer is now told the width
1 parent dca989c commit 1f96e27

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
@@ -674,7 +674,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
674674
expr_type_id==ID_signedbv ||
675675
expr_type_id==ID_floatbv)
676676
{
677-
mp_integer int_value = bv2integer(id2string(value), false);
677+
const auto width = to_bv_type(op_type).get_width();
678+
mp_integer int_value = bv2integer(id2string(value), width, false);
678679
expr=from_integer(int_value, expr_type);
679680
return false;
680681
}
@@ -816,71 +817,32 @@ bool simplify_exprt::simplify_if_implies(
816817
expr.op1().is_constant() &&
817818
cond.op1().type()==expr.op1().type())
818819
{
819-
const irep_idt &type_id=cond.op1().type().id();
820-
if(type_id==ID_integer || type_id==ID_natural)
821-
{
822-
if(string2integer(cond.op1().get_string(ID_value))>=
823-
string2integer(expr.op1().get_string(ID_value)))
824-
{
825-
new_truth = true;
826-
return false;
827-
}
828-
}
829-
else if(type_id==ID_unsignedbv)
830-
{
831-
const mp_integer i1, i2;
832-
if(
833-
bv2integer(cond.op1().get_string(ID_value), false) >=
834-
bv2integer(expr.op1().get_string(ID_value), false))
835-
{
836-
new_truth = true;
837-
return false;
838-
}
839-
}
840-
else if(type_id==ID_signedbv)
820+
mp_integer i1, i2;
821+
822+
if(
823+
!to_integer(to_constant_expr(cond.op1()), i1) &&
824+
!to_integer(to_constant_expr(expr.op1()), i2))
841825
{
842-
const mp_integer i1, i2;
843-
if(
844-
bv2integer(cond.op1().get_string(ID_value), true) >=
845-
bv2integer(expr.op1().get_string(ID_value), true))
826+
if(i1 >= i2)
846827
{
847828
new_truth = true;
848829
return false;
849830
}
850831
}
851832
}
833+
852834
if(cond.op1()==expr.op1() &&
853835
cond.op0().is_constant() &&
854836
expr.op0().is_constant() &&
855837
cond.op0().type()==expr.op0().type())
856838
{
857-
const irep_idt &type_id = cond.op1().type().id();
858-
if(type_id==ID_integer || type_id==ID_natural)
859-
{
860-
if(string2integer(cond.op1().get_string(ID_value))<=
861-
string2integer(expr.op1().get_string(ID_value)))
862-
{
863-
new_truth = true;
864-
return false;
865-
}
866-
}
867-
else if(type_id==ID_unsignedbv)
868-
{
869-
const mp_integer i1, i2;
870-
if(
871-
bv2integer(cond.op1().get_string(ID_value), false) <=
872-
bv2integer(expr.op1().get_string(ID_value), false))
873-
{
874-
new_truth = true;
875-
return false;
876-
}
877-
}
878-
else if(type_id==ID_signedbv)
839+
mp_integer i1, i2;
840+
841+
if(
842+
!to_integer(to_constant_expr(cond.op0()), i1) &&
843+
!to_integer(to_constant_expr(expr.op0()), i2))
879844
{
880-
const mp_integer i1, i2;
881-
if(
882-
bv2integer(cond.op1().get_string(ID_value), true) <=
883-
bv2integer(expr.op1().get_string(ID_value), true))
845+
if(i1 <= i2)
884846
{
885847
new_truth = true;
886848
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)