Skip to content

Commit b3ba2bd

Browse files
author
Daniel Kroening
authored
Merge pull request #3109 from diffblue/bv2integer_irep
switch bv2integer and integer2bv to irep_idt
2 parents c1065e0 + b2390e4 commit b3ba2bd

19 files changed

+77
-80
lines changed

‎src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1814,7 +1814,7 @@ std::string expr2ct::convert_constant(
18141814
const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
18151815
const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
18161816

1817-
mp_integer int_value = bv2integer(id2string(value), width, is_signed);
1817+
mp_integer int_value = bvrep2integer(value, width, is_signed);
18181818
mp_integer i=0;
18191819

18201820
irep_idt int_value_string=integer2string(int_value);
@@ -1853,7 +1853,7 @@ std::string expr2ct::convert_constant(
18531853
const auto width = to_bitvector_type(type).get_width();
18541854

18551855
mp_integer int_value =
1856-
bv2integer(id2string(value), width, type.id() == ID_signedbv);
1856+
bvrep2integer(value, width, type.id() == ID_signedbv);
18571857

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

‎src/ansi-c/literals/convert_float_literal.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <cassert>
1515

16-
#include <util/arith_tools.h>
1716
#include <util/c_types.h>
1817
#include <util/config.h>
1918
#include <util/ieee_float.h>
@@ -85,12 +84,13 @@ exprt convert_float_literal(const std::string &src)
8584
else
8685
UNREACHABLE;
8786

88-
constant_exprt result(integer2bv(a.pack(), a.spec.width()), type);
87+
const constant_exprt result = a.to_expr();
8988

9089
if(parsed_float.is_imaginary)
9190
{
9291
const complex_typet complex_type(type);
93-
return complex_exprt(from_integer(0, type), result, complex_type);
92+
return complex_exprt(
93+
ieee_floatt::zero(type).to_expr(), result, complex_type);
9494
}
9595

9696
return result;

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -566,7 +566,7 @@ int linker_script_merget::ls_data2instructions(
566566
symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
567567

568568
constant_exprt rhs(
569-
integer2bv(
569+
integer2bvrep(
570570
string2integer(id2string(symbol_value)),
571571
unsigned_int_type().get_width()),
572572
unsigned_int_type());
@@ -630,7 +630,7 @@ int linker_script_merget::ls_data2instructions(
630630
symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
631631
632632
constant_exprt rhs;
633-
rhs.set_value(integer2bv(
633+
rhs.set_value(integer2bvrep(
634634
string2integer(d["val"].value), unsigned_int_type().get_width()));
635635
rhs.type()=unsigned_int_type();
636636

‎src/goto-programs/goto_trace.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,8 @@ static std::string numeric_representation(
140140

141141
if(options.hex_representation)
142142
{
143-
mp_integer value_int = bv2integer(id2string(value), value.size(), false);
143+
const mp_integer value_int =
144+
bvrep2integer(to_constant_expr(expr).get_value(), value.size(), false);
144145
result = integer2string(value_int, 16);
145146
prefix = "0x";
146147
}

‎src/goto-programs/interpreter_evaluate.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -383,7 +383,7 @@ void interpretert::evaluate(
383383
{
384384
const irep_idt &value=to_constant_expr(expr).get_value();
385385
const auto width = to_c_bool_type(expr.type()).get_width();
386-
dest.push_back(bv2integer(id2string(value), width, false));
386+
dest.push_back(bvrep2integer(value, width, false));
387387
return;
388388
}
389389
else if(expr.type().id()==ID_bool)
@@ -985,15 +985,15 @@ void interpretert::evaluate(
985985
else if(expr.type().id()==ID_signedbv)
986986
{
987987
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));
988+
const auto s = integer2bvrep(value, width);
989+
dest.push_back(bvrep2integer(s, width, true));
990990
return;
991991
}
992992
else if(expr.type().id()==ID_unsignedbv)
993993
{
994994
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));
995+
const auto s = integer2bvrep(value, width);
996+
dest.push_back(bvrep2integer(s, width, false));
997997
return;
998998
}
999999
else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))

‎src/solvers/flattening/boolbv_constant.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
9191

9292
for(std::size_t i=0; i<width; i++)
9393
{
94-
const bool bit = get_bitvector_bit(value, width, i);
94+
const bool bit = get_bvrep_bit(value, width, i);
9595
bv[i]=const_literal(bit);
9696
}
9797

‎src/solvers/lowering/popcount.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
4848
for(std::size_t i = 0; i < new_width / (2 * shift); ++i)
4949
bitstring += std::string(shift, '0') + std::string(shift, '1');
5050
const mp_integer value = binary2integer(bitstring, false);
51-
constant_exprt bitmask(integer2bv(value, new_width), x.type());
51+
const constant_exprt bitmask(integer2bvrep(value, new_width), x.type());
5252
// build the expression
5353
x = plus_exprt(bitand_exprt(x, bitmask), bitand_exprt(shifted_x, bitmask));
5454
}

‎src/util/arith_tools.cpp

Lines changed: 32 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -44,19 +44,19 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
4444
else if(type_id==ID_unsignedbv)
4545
{
4646
const auto width = to_unsignedbv_type(type).get_width();
47-
int_value = bv2integer(id2string(value), width, false);
47+
int_value = bvrep2integer(value, width, false);
4848
return false;
4949
}
5050
else if(type_id==ID_signedbv)
5151
{
5252
const auto width = to_signedbv_type(type).get_width();
53-
int_value = bv2integer(id2string(value), width, true);
53+
int_value = bvrep2integer(value, width, true);
5454
return false;
5555
}
5656
else if(type_id==ID_c_bool)
5757
{
5858
const auto width = to_c_bool_type(type).get_width();
59-
int_value = bv2integer(id2string(value), width, false);
59+
int_value = bvrep2integer(value, width, false);
6060
return false;
6161
}
6262
else if(type_id==ID_c_enum)
@@ -65,13 +65,13 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
6565
if(subtype.id()==ID_signedbv)
6666
{
6767
const auto width = to_signedbv_type(type).get_width();
68-
int_value = bv2integer(id2string(value), width, true);
68+
int_value = bvrep2integer(value, width, true);
6969
return false;
7070
}
7171
else if(subtype.id()==ID_unsignedbv)
7272
{
7373
const auto width = to_unsignedbv_type(type).get_width();
74-
int_value = bv2integer(id2string(value), width, false);
74+
int_value = bvrep2integer(value, width, false);
7575
return false;
7676
}
7777
}
@@ -83,17 +83,17 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
8383

8484
if(subtype.id()==ID_signedbv)
8585
{
86-
int_value = bv2integer(id2string(value), width, true);
86+
int_value = bvrep2integer(value, width, true);
8787
return false;
8888
}
8989
else if(subtype.id()==ID_unsignedbv)
9090
{
91-
int_value = bv2integer(id2string(value), width, false);
91+
int_value = bvrep2integer(value, width, false);
9292
return false;
9393
}
9494
else if(subtype.id() == ID_c_bool)
9595
{
96-
int_value = bv2integer(id2string(value), width, false);
96+
int_value = bvrep2integer(value, width, false);
9797
return false;
9898
}
9999
}
@@ -136,28 +136,28 @@ constant_exprt from_integer(
136136
else if(type_id==ID_unsignedbv)
137137
{
138138
std::size_t width=to_unsignedbv_type(type).get_width();
139-
return constant_exprt(integer2bv(int_value, width), type);
139+
return constant_exprt(integer2bvrep(int_value, width), type);
140140
}
141141
else if(type_id==ID_bv)
142142
{
143143
std::size_t width=to_bv_type(type).get_width();
144-
return constant_exprt(integer2bv(int_value, width), type);
144+
return constant_exprt(integer2bvrep(int_value, width), type);
145145
}
146146
else if(type_id==ID_signedbv)
147147
{
148148
std::size_t width=to_signedbv_type(type).get_width();
149-
return constant_exprt(integer2bv(int_value, width), type);
149+
return constant_exprt(integer2bvrep(int_value, width), type);
150150
}
151151
else if(type_id==ID_c_enum)
152152
{
153153
const std::size_t width =
154154
to_c_enum_type(type).subtype().get_size_t(ID_width);
155-
return constant_exprt(integer2bv(int_value, width), type);
155+
return constant_exprt(integer2bvrep(int_value, width), type);
156156
}
157157
else if(type_id==ID_c_bool)
158158
{
159159
std::size_t width=to_c_bool_type(type).get_width();
160-
return constant_exprt(integer2bv(int_value, width), type);
160+
return constant_exprt(integer2bvrep(int_value, width), type);
161161
}
162162
else if(type_id==ID_bool)
163163
{
@@ -175,7 +175,7 @@ constant_exprt from_integer(
175175
else if(type_id==ID_c_bit_field)
176176
{
177177
std::size_t width=to_c_bit_field_type(type).get_width();
178-
return constant_exprt(integer2bv(int_value, width), type);
178+
return constant_exprt(integer2bvrep(int_value, width), type);
179179
}
180180
else if(type_id==ID_fixedbv)
181181
{
@@ -280,7 +280,7 @@ void mp_max(mp_integer &a, const mp_integer &b)
280280
/// \param src: the bitvector representation
281281
/// \param width: the number of bits in the bitvector
282282
/// \param bit_index: index (0 is the least significant)
283-
bool get_bitvector_bit(
283+
bool get_bvrep_bit(
284284
const irep_idt &src,
285285
std::size_t width,
286286
std::size_t bit_index)
@@ -314,14 +314,14 @@ make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f)
314314
/// \param width: the width of the bit-vector
315315
/// \param f: the functor
316316
/// \returns new bitvector representation
317-
irep_idt bitvector_bitwise_op(
317+
irep_idt bvrep_bitwise_op(
318318
const irep_idt &a,
319319
const irep_idt &b,
320320
const std::size_t width,
321321
const std::function<bool(bool, bool)> f)
322322
{
323323
return make_bvrep(width, [&a, &b, &width, f](std::size_t i) {
324-
return f(get_bitvector_bit(a, width, i), get_bitvector_bit(b, width, i));
324+
return f(get_bvrep_bit(a, width, i), get_bvrep_bit(b, width, i));
325325
});
326326
}
327327

@@ -331,12 +331,25 @@ irep_idt bitvector_bitwise_op(
331331
/// \param width: the width of the bit-vector
332332
/// \param f: the functor
333333
/// \returns new bitvector representation
334-
irep_idt bitvector_bitwise_op(
334+
irep_idt bvrep_bitwise_op(
335335
const irep_idt &a,
336336
const std::size_t width,
337337
const std::function<bool(bool)> f)
338338
{
339339
return make_bvrep(width, [&a, &width, f](std::size_t i) {
340-
return f(get_bitvector_bit(a, width, i));
340+
return f(get_bvrep_bit(a, width, i));
341341
});
342342
}
343+
344+
/// convert an integer to bit-vector representation with given width
345+
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
346+
{
347+
return integer2binary(src, width);
348+
}
349+
350+
/// convert a bit-vector representation (possibly signed) to integer
351+
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
352+
{
353+
PRECONDITION(src.size() == width);
354+
return binary2integer(id2string(src), is_signed);
355+
}

‎src/util/arith_tools.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,12 +164,15 @@ mp_integer power(const mp_integer &base, const mp_integer &exponent);
164164
void mp_min(mp_integer &a, const mp_integer &b);
165165
void mp_max(mp_integer &a, const mp_integer &b);
166166

167-
bool get_bitvector_bit(
167+
bool get_bvrep_bit(
168168
const irep_idt &src,
169169
std::size_t width,
170170
std::size_t bit_index);
171171

172172
irep_idt
173173
make_bvrep(const std::size_t width, const std::function<bool(std::size_t)> f);
174174

175+
irep_idt integer2bvrep(const mp_integer &, std::size_t width);
176+
mp_integer bvrep2integer(const irep_idt &, std::size_t width, bool is_signed);
177+
175178
#endif // CPROVER_UTIL_ARITH_TOOLS_H

‎src/util/bv_arithmetic.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ mp_integer bv_arithmetict::pack() const
8484

8585
exprt bv_arithmetict::to_expr() const
8686
{
87-
return constant_exprt(integer2bv(value, spec.width), spec.to_type());
87+
return constant_exprt(integer2bvrep(value, spec.width), spec.to_type());
8888
}
8989

9090
bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
@@ -184,5 +184,6 @@ 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.width, spec.is_signed);
187+
value = bvrep2integer(
188+
to_constant_expr(expr).get_value(), spec.width, spec.is_signed);
188189
}

‎src/util/expr.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,16 @@ Author: Daniel Kroening, [email protected]
1010
/// \file
1111
/// Expression Representation
1212

13+
// clang-format off
14+
#include "arith_tools.h"
1315
#include "expr.h"
1416
#include "expr_iterator.h"
1517
#include "fixedbv.h"
1618
#include "ieee_float.h"
1719
#include "rational.h"
1820
#include "rational_tools.h"
1921
#include "std_expr.h"
22+
// clang-format on
2023

2124
#include <stack>
2225

@@ -248,7 +251,7 @@ bool exprt::is_one() const
248251
{
249252
const auto width = to_bitvector_type(type()).get_width();
250253
mp_integer int_value =
251-
bv2integer(id2string(constant_expr.get_value()), width, false);
254+
bvrep2integer(id2string(constant_expr.get_value()), width, false);
252255
if(int_value==1)
253256
return true;
254257
}

‎src/util/fixedbv.cpp

Lines changed: 2 additions & 2 deletions
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()), spec.width, true);
29+
v = bvrep2integer(expr.get_value(), spec.width, true);
3030
}
3131

3232
void fixedbvt::from_integer(const mp_integer &i)
@@ -46,7 +46,7 @@ constant_exprt fixedbvt::to_expr() const
4646
type.set_width(spec.width);
4747
type.set_integer_bits(spec.integer_bits);
4848
PRECONDITION(spec.width != 0);
49-
return constant_exprt(integer2bv(v, spec.width), type);
49+
return constant_exprt(integer2bvrep(v, spec.width), type);
5050
}
5151

5252
void fixedbvt::round(const fixedbv_spect &dest_spec)

‎src/util/ieee_float.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -696,7 +696,7 @@ void ieee_floatt::divide_and_round(
696696

697697
constant_exprt ieee_floatt::to_expr() const
698698
{
699-
return constant_exprt(integer2bv(pack(), spec.width()), spec.to_type());
699+
return constant_exprt(integer2bvrep(pack(), spec.width()), spec.to_type());
700700
}
701701

702702
ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
@@ -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()), spec.width(), false));
1065+
unpack(bvrep2integer(expr.get_value(), spec.width(), false));
10661066
}
10671067

10681068
mp_integer ieee_floatt::to_integer() const

‎src/util/json_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ json_objectt json(
220220
static std::string binary(const constant_exprt &src)
221221
{
222222
const auto width = to_bitvector_type(src.type()).get_width();
223-
const auto int_val = bv2integer(id2string(src.get_value()), width, false);
223+
const auto int_val = bvrep2integer(src.get_value(), width, false);
224224
return integer2binary(int_val, width);
225225
}
226226

‎src/util/mp_arith.cpp

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -186,20 +186,6 @@ const mp_integer binary2integer(const std::string &n, bool is_signed)
186186
#endif
187187
}
188188

189-
/// convert an integer to bit-vector representation with given width
190-
const std::string integer2bv(const mp_integer &src, std::size_t width)
191-
{
192-
return integer2binary(src, width);
193-
}
194-
195-
/// convert a bit-vector representation (possibly signed) to integer
196-
const mp_integer
197-
bv2integer(const std::string &src, std::size_t width, bool is_signed)
198-
{
199-
PRECONDITION(src.size() == width);
200-
return binary2integer(src, is_signed);
201-
}
202-
203189
mp_integer::ullong_t integer2ulong(const mp_integer &n)
204190
{
205191
PRECONDITION(n.is_ulong());

0 commit comments

Comments
 (0)