Skip to content

Commit 35ee875

Browse files
author
Daniel Kroening
authored
Merge pull request #3096 from diffblue/hex-bitvectors
introduce integer2bv and bv2integer
2 parents b9b40ed + 935f4d2 commit 35ee875

16 files changed

+70
-48
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 = binary2integer(expr.op0().get_string(ID_value), false);
89+
mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
9090
return integer2string(lbl_id);
9191
}
9292

‎src/ansi-c/expr2c.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1813,7 +1813,7 @@ std::string expr2ct::convert_constant(
18131813

18141814
bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
18151815

1816-
mp_integer int_value=binary2integer(id2string(value), is_signed);
1816+
mp_integer int_value = bv2integer(id2string(value), is_signed);
18171817
mp_integer i=0;
18181818

18191819
irep_idt int_value_string=integer2string(int_value);
@@ -1849,8 +1849,8 @@ std::string expr2ct::convert_constant(
18491849
type.id()==ID_c_bit_field ||
18501850
type.id()==ID_c_bool)
18511851
{
1852-
mp_integer int_value=
1853-
binary2integer(id2string(value), type.id()==ID_signedbv);
1852+
mp_integer int_value =
1853+
bv2integer(id2string(value), type.id() == ID_signedbv);
18541854

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

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 3 additions & 3 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-
integer2binary(
569+
integer2bv(
570570
string2integer(id2string(symbol_value)),
571571
unsigned_int_type().get_width()),
572572
unsigned_int_type());
@@ -632,8 +632,8 @@ int linker_script_merget::ls_data2instructions(
632632
symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
633633
634634
constant_exprt rhs;
635-
rhs.set_value(integer2binary(string2integer(d["val"].value),
636-
unsigned_int_type().get_width()));
635+
rhs.set_value(integer2bv(
636+
string2integer(d["val"].value), unsigned_int_type().get_width()));
637637
rhs.type()=unsigned_int_type();
638638
639639
exprt rhs_tc(rhs);

‎src/goto-programs/goto_convert.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1834,8 +1834,8 @@ bool goto_convertt::get_string_constant(
18341834
forall_operands(it, index_op)
18351835
if(it->is_constant())
18361836
{
1837-
unsigned long i=integer2ulong(
1838-
binary2integer(id2string(to_constant_expr(*it).get_value()), true));
1837+
unsigned long i = integer2ulong(
1838+
bv2integer(id2string(to_constant_expr(*it).get_value()), true));
18391839

18401840
if(i!=0) // to skip terminating 0
18411841
result+=static_cast<char>(i);

‎src/goto-programs/goto_trace.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ numeric_representation(const exprt &expr, const trace_optionst &options)
137137
if(options.hex_representation)
138138
{
139139
mp_integer value_int =
140-
binary2integer(id2string(to_constant_expr(expr).get_value()), false);
140+
bv2integer(id2string(to_constant_expr(expr).get_value()), false);
141141
result = integer2string(value_int, 16);
142142
prefix = "0x";
143143
}

‎src/goto-programs/interpreter_evaluate.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -382,7 +382,7 @@ 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(binary2integer(id2string(value), false));
385+
dest.push_back(bv2integer(id2string(value), false));
386386
return;
387387
}
388388
else if(expr.type().id()==ID_bool)
@@ -981,16 +981,16 @@ void interpretert::evaluate(
981981
}
982982
else if(expr.type().id()==ID_signedbv)
983983
{
984-
const std::string s=
985-
integer2binary(value, to_signedbv_type(expr.type()).get_width());
986-
dest.push_back(binary2integer(s, true));
984+
const std::string s =
985+
integer2bv(value, to_signedbv_type(expr.type()).get_width());
986+
dest.push_back(bv2integer(s, true));
987987
return;
988988
}
989989
else if(expr.type().id()==ID_unsignedbv)
990990
{
991-
const std::string s=
992-
integer2binary(value, to_unsignedbv_type(expr.type()).get_width());
993-
dest.push_back(binary2integer(s, false));
991+
const std::string s =
992+
integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
993+
dest.push_back(bv2integer(s, false));
994994
return;
995995
}
996996
else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))

‎src/util/arith_tools.cpp

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -43,30 +43,30 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
4343
}
4444
else if(type_id==ID_unsignedbv)
4545
{
46-
int_value=binary2integer(id2string(value), false);
46+
int_value = bv2integer(id2string(value), false);
4747
return false;
4848
}
4949
else if(type_id==ID_signedbv)
5050
{
51-
int_value=binary2integer(id2string(value), true);
51+
int_value = bv2integer(id2string(value), true);
5252
return false;
5353
}
5454
else if(type_id==ID_c_bool)
5555
{
56-
int_value=binary2integer(id2string(value), false);
56+
int_value = bv2integer(id2string(value), false);
5757
return false;
5858
}
5959
else if(type_id==ID_c_enum)
6060
{
6161
const typet &subtype=to_c_enum_type(type).subtype();
6262
if(subtype.id()==ID_signedbv)
6363
{
64-
int_value=binary2integer(id2string(value), true);
64+
int_value = bv2integer(id2string(value), true);
6565
return false;
6666
}
6767
else if(subtype.id()==ID_unsignedbv)
6868
{
69-
int_value=binary2integer(id2string(value), false);
69+
int_value = bv2integer(id2string(value), false);
7070
return false;
7171
}
7272
}
@@ -75,12 +75,12 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
7575
const typet &subtype=type.subtype();
7676
if(subtype.id()==ID_signedbv)
7777
{
78-
int_value=binary2integer(id2string(value), true);
78+
int_value = bv2integer(id2string(value), true);
7979
return false;
8080
}
8181
else if(subtype.id()==ID_unsignedbv)
8282
{
83-
int_value=binary2integer(id2string(value), false);
83+
int_value = bv2integer(id2string(value), false);
8484
return false;
8585
}
8686
}
@@ -123,28 +123,28 @@ constant_exprt from_integer(
123123
else if(type_id==ID_unsignedbv)
124124
{
125125
std::size_t width=to_unsignedbv_type(type).get_width();
126-
return constant_exprt(integer2binary(int_value, width), type);
126+
return constant_exprt(integer2bv(int_value, width), type);
127127
}
128128
else if(type_id==ID_bv)
129129
{
130130
std::size_t width=to_bv_type(type).get_width();
131-
return constant_exprt(integer2binary(int_value, width), type);
131+
return constant_exprt(integer2bv(int_value, width), type);
132132
}
133133
else if(type_id==ID_signedbv)
134134
{
135135
std::size_t width=to_signedbv_type(type).get_width();
136-
return constant_exprt(integer2binary(int_value, width), type);
136+
return constant_exprt(integer2bv(int_value, width), type);
137137
}
138138
else if(type_id==ID_c_enum)
139139
{
140140
const std::size_t width =
141141
to_c_enum_type(type).subtype().get_size_t(ID_width);
142-
return constant_exprt(integer2binary(int_value, width), type);
142+
return constant_exprt(integer2bv(int_value, width), type);
143143
}
144144
else if(type_id==ID_c_bool)
145145
{
146146
std::size_t width=to_c_bool_type(type).get_width();
147-
return constant_exprt(integer2binary(int_value, width), type);
147+
return constant_exprt(integer2bv(int_value, width), type);
148148
}
149149
else if(type_id==ID_bool)
150150
{
@@ -162,7 +162,7 @@ constant_exprt from_integer(
162162
else if(type_id==ID_c_bit_field)
163163
{
164164
std::size_t width=to_c_bit_field_type(type).get_width();
165-
return constant_exprt(integer2binary(int_value, width), type);
165+
return constant_exprt(integer2bv(int_value, width), type);
166166
}
167167
else if(type_id==ID_fixedbv)
168168
{

‎src/util/bv_arithmetic.cpp

Lines changed: 2 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(integer2binary(value, spec.width), spec.to_type());
87+
return constant_exprt(integer2bv(value, spec.width), spec.to_type());
8888
}
8989

9090
bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)
@@ -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=binary2integer(expr.get_string(ID_value), spec.is_signed);
187+
value = bv2integer(expr.get_string(ID_value), spec.is_signed);
188188
}

‎src/util/expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -245,7 +245,7 @@ bool exprt::is_one() const
245245
}
246246
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
247247
{
248-
mp_integer int_value=binary2integer(value, false);
248+
mp_integer int_value = bv2integer(value, false);
249249
if(int_value==1)
250250
return true;
251251
}

‎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=binary2integer(id2string(expr.get_value()), true);
29+
v = bv2integer(id2string(expr.get_value()), 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(integer2binary(v, spec.width), type);
49+
return constant_exprt(integer2bv(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(integer2binary(pack(), spec.width()), spec.to_type());
699+
return constant_exprt(integer2bv(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(binary2integer(id2string(expr.get_value()), false));
1065+
unpack(bv2integer(id2string(expr.get_value()), false));
10661066
}
10671067

10681068
mp_integer ieee_floatt::to_integer() const

‎src/util/mp_arith.cpp

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

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

‎src/util/mp_arith.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,12 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
5252
const std::string integer2binary(const mp_integer &, std::size_t width);
5353
const mp_integer binary2integer(const std::string &, bool is_signed);
5454

55+
/// convert an integer to bit-vector representation with given width
56+
const std::string integer2bv(const mp_integer &, std::size_t width);
57+
58+
/// convert a bit-vector representation (possibly signed) to integer
59+
const mp_integer bv2integer(const std::string &, bool is_signed);
60+
5561
/// \deprecated use numeric_cast_v<unsigned long long> instead
5662
DEPRECATED("Use numeric_cast_v<unsigned long long> instead")
5763
mp_integer::ullong_t integer2ulong(const mp_integer &);

‎src/util/simplify_expr.cpp

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -677,7 +677,7 @@ 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=binary2integer(id2string(value), false);
680+
mp_integer int_value = bv2integer(id2string(value), false);
681681
expr=from_integer(int_value, expr_type);
682682
return false;
683683
}
@@ -832,8 +832,9 @@ bool simplify_exprt::simplify_if_implies(
832832
else if(type_id==ID_unsignedbv)
833833
{
834834
const mp_integer i1, i2;
835-
if(binary2integer(cond.op1().get_string(ID_value), false)>=
836-
binary2integer(expr.op1().get_string(ID_value), false))
835+
if(
836+
bv2integer(cond.op1().get_string(ID_value), false) >=
837+
bv2integer(expr.op1().get_string(ID_value), false))
837838
{
838839
new_truth = true;
839840
return false;
@@ -842,8 +843,9 @@ bool simplify_exprt::simplify_if_implies(
842843
else if(type_id==ID_signedbv)
843844
{
844845
const mp_integer i1, i2;
845-
if(binary2integer(cond.op1().get_string(ID_value), true)>=
846-
binary2integer(expr.op1().get_string(ID_value), true))
846+
if(
847+
bv2integer(cond.op1().get_string(ID_value), true) >=
848+
bv2integer(expr.op1().get_string(ID_value), true))
847849
{
848850
new_truth = true;
849851
return false;
@@ -868,8 +870,9 @@ bool simplify_exprt::simplify_if_implies(
868870
else if(type_id==ID_unsignedbv)
869871
{
870872
const mp_integer i1, i2;
871-
if(binary2integer(cond.op1().get_string(ID_value), false)<=
872-
binary2integer(expr.op1().get_string(ID_value), false))
873+
if(
874+
bv2integer(cond.op1().get_string(ID_value), false) <=
875+
bv2integer(expr.op1().get_string(ID_value), false))
873876
{
874877
new_truth = true;
875878
return false;
@@ -878,8 +881,9 @@ bool simplify_exprt::simplify_if_implies(
878881
else if(type_id==ID_signedbv)
879882
{
880883
const mp_integer i1, i2;
881-
if(binary2integer(cond.op1().get_string(ID_value), true)<=
882-
binary2integer(expr.op1().get_string(ID_value), true))
884+
if(
885+
bv2integer(cond.op1().get_string(ID_value), true) <=
886+
bv2integer(expr.op1().get_string(ID_value), true))
883887
{
884888
new_truth = true;
885889
return false;

‎src/util/simplify_expr_int.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -821,7 +821,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
821821
}
822822
else if(expr.id()==ID_bitxor)
823823
{
824-
constant_exprt new_op(integer2binary(0, width), expr.type());
824+
constant_exprt new_op(integer2bv(0, width), expr.type());
825825
expr.swap(new_op);
826826
return false;
827827
}

‎src/util/simplify_expr_pointer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -387,7 +387,7 @@ 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=binary2integer(id2string(c_ptr.get_value()), false);
390+
mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
391391
// a null pointer would have been caught above, return value 0
392392
// will indicate that conversion failed
393393
if(number==0)

0 commit comments

Comments
 (0)