Skip to content

Commit 954faed

Browse files
author
Daniel Kroening
authored
Merge pull request #3100 from diffblue/hex-bitvectors3
bv2integer is now told the width
2 parents 7b2d061 + 92f2621 commit 954faed

14 files changed

+79
-89
lines changed

‎jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ static const std::string get_thread_block_identifier(
8686
{
8787
PRECONDITION(f_code.arguments().size() == 1);
8888
const exprt &expr = f_code.arguments()[0];
89-
mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
89+
const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
9090
return integer2string(lbl_id);
9191
}
9292

‎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_convert.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1830,11 +1830,12 @@ bool goto_convertt::get_string_constant(
18301830
forall_operands(it, index_op)
18311831
if(it->is_constant())
18321832
{
1833-
unsigned long i = integer2ulong(
1834-
bv2integer(id2string(to_constant_expr(*it).get_value()), true));
1833+
const auto i = numeric_cast<std::size_t>(*it);
1834+
if(!i.has_value())
1835+
return true;
18351836

1836-
if(i!=0) // to skip terminating 0
1837-
result+=static_cast<char>(i);
1837+
if(i.value() != 0) // to skip terminating 0
1838+
result += static_cast<char>(i.value());
18381839
}
18391840

18401841
return value=result, false;

‎src/goto-programs/goto_trace.cpp

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -129,22 +129,25 @@ void goto_trace_stept::output(
129129
/// \param expr: expression to get numeric representation from
130130
/// \param options: configuration options
131131
/// \return a string with the numeric representation
132-
static std::string
133-
numeric_representation(const exprt &expr, const trace_optionst &options)
132+
static std::string numeric_representation(
133+
const constant_exprt &expr,
134+
const trace_optionst &options)
134135
{
135136
std::string result;
136137
std::string prefix;
138+
139+
const irep_idt &value = expr.get_value();
140+
137141
if(options.hex_representation)
138142
{
139-
mp_integer value_int =
140-
bv2integer(id2string(to_constant_expr(expr).get_value()), false);
143+
mp_integer value_int = bv2integer(id2string(value), value.size(), false);
141144
result = integer2string(value_int, 16);
142145
prefix = "0x";
143146
}
144147
else
145148
{
146149
prefix = "0b";
147-
result = expr.get_string(ID_value);
150+
result = id2string(value);
148151
}
149152

150153
std::ostringstream oss;
@@ -181,7 +184,8 @@ std::string trace_numeric_value(
181184
type.id()==ID_c_enum ||
182185
type.id()==ID_c_enum_tag)
183186
{
184-
const std::string &str = numeric_representation(expr, options);
187+
const std::string &str =
188+
numeric_representation(to_constant_expr(expr), options);
185189
return str;
186190
}
187191
else if(type.id()==ID_bool)

‎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
@@ -193,8 +193,10 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)
193193
}
194194

195195
/// convert a bit-vector representation (possibly signed) to integer
196-
const mp_integer bv2integer(const std::string &src, bool is_signed)
196+
const mp_integer
197+
bv2integer(const std::string &src, std::size_t width, bool is_signed)
197198
{
199+
PRECONDITION(src.size() == width);
198200
return binary2integer(src, is_signed);
199201
}
200202

‎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)