Skip to content

Commit 5d379b0

Browse files
author
Daniel Kroening
committed
introduce integer2bv and bv2integer
The representation of bitvectors is now hard-wired to binary with leading zeros and fixed width. These two new functions provide a wrapper around any future representation.
1 parent 251245e commit 5d379b0

16 files changed

+70
-52
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: 2 additions & 2 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);
@@ -1850,7 +1850,7 @@ std::string expr2ct::convert_constant(
18501850
type.id()==ID_c_bool)
18511851
{
18521852
mp_integer int_value=
1853-
binary2integer(id2string(value), type.id()==ID_signedbv);
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: 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-
integer2binary(
569+
integer2bv(
570570
string2integer(id2string(symbol_value)),
571571
unsigned_int_type().get_width()),
572572
unsigned_int_type());
@@ -632,7 +632,7 @@ 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),
635+
rhs.set_value(integer2bv(string2integer(d["val"].value),
636636
unsigned_int_type().get_width()));
637637
rhs.type()=unsigned_int_type();
638638

‎src/goto-programs/goto_convert.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1835,7 +1835,7 @@ bool goto_convertt::get_string_constant(
18351835
if(it->is_constant())
18361836
{
18371837
unsigned long i=integer2ulong(
1838-
binary2integer(id2string(to_constant_expr(*it).get_value()), true));
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
@@ -138,7 +138,7 @@ numeric_representation(const exprt &expr, const trace_optionst &options)
138138
if(options.hex_representation)
139139
{
140140
mp_integer value_int =
141-
binary2integer(id2string(to_constant_expr(expr).get_value()), false);
141+
bv2integer(id2string(to_constant_expr(expr).get_value()), false);
142142
result = integer2string(value_int, 16);
143143
prefix = "0x";
144144
}

‎src/goto-programs/interpreter_evaluate.cpp

Lines changed: 5 additions & 5 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)
@@ -982,15 +982,15 @@ void interpretert::evaluate(
982982
else if(expr.type().id()==ID_signedbv)
983983
{
984984
const std::string s=
985-
integer2binary(value, to_signedbv_type(expr.type()).get_width());
986-
dest.push_back(binary2integer(s, true));
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
{
991991
const std::string s=
992-
integer2binary(value, to_unsignedbv_type(expr.type()).get_width());
993-
dest.push_back(binary2integer(s, false));
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: 9 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,8 @@ 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(bv2integer(cond.op1().get_string(ID_value), false)>=
836+
bv2integer(expr.op1().get_string(ID_value), false))
837837
{
838838
new_truth = true;
839839
return false;
@@ -842,8 +842,8 @@ bool simplify_exprt::simplify_if_implies(
842842
else if(type_id==ID_signedbv)
843843
{
844844
const mp_integer i1, i2;
845-
if(binary2integer(cond.op1().get_string(ID_value), true)>=
846-
binary2integer(expr.op1().get_string(ID_value), true))
845+
if(bv2integer(cond.op1().get_string(ID_value), true)>=
846+
bv2integer(expr.op1().get_string(ID_value), true))
847847
{
848848
new_truth = true;
849849
return false;
@@ -868,8 +868,8 @@ bool simplify_exprt::simplify_if_implies(
868868
else if(type_id==ID_unsignedbv)
869869
{
870870
const mp_integer i1, i2;
871-
if(binary2integer(cond.op1().get_string(ID_value), false)<=
872-
binary2integer(expr.op1().get_string(ID_value), false))
871+
if(bv2integer(cond.op1().get_string(ID_value), false)<=
872+
bv2integer(expr.op1().get_string(ID_value), false))
873873
{
874874
new_truth = true;
875875
return false;
@@ -878,8 +878,8 @@ bool simplify_exprt::simplify_if_implies(
878878
else if(type_id==ID_signedbv)
879879
{
880880
const mp_integer i1, i2;
881-
if(binary2integer(cond.op1().get_string(ID_value), true)<=
882-
binary2integer(expr.op1().get_string(ID_value), true))
881+
if(bv2integer(cond.op1().get_string(ID_value), true)<=
882+
bv2integer(expr.op1().get_string(ID_value), true))
883883
{
884884
new_truth = true;
885885
return false;

‎src/util/simplify_expr_int.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -88,17 +88,17 @@ static bool sum_expr(
8888
}
8989
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
9090
{
91-
dest.set_value(integer2binary(
92-
binary2integer(id2string(dest.get_value()), false)+
93-
binary2integer(id2string(expr.get_value()), false),
91+
dest.set_value(integer2bv(
92+
bv2integer(id2string(dest.get_value()), false)+
93+
bv2integer(id2string(expr.get_value()), false),
9494
to_bitvector_type(dest.type()).get_width()));
9595
return false;
9696
}
9797
else if(type_id==ID_fixedbv)
9898
{
99-
dest.set_value(integer2binary(
100-
binary2integer(id2string(dest.get_value()), false)+
101-
binary2integer(id2string(expr.get_value()), false),
99+
dest.set_value(integer2bv(
100+
bv2integer(id2string(dest.get_value()), false)+
101+
bv2integer(id2string(expr.get_value()), false),
102102
to_bitvector_type(dest.type()).get_width()));
103103
return false;
104104
}
@@ -143,9 +143,9 @@ static bool mul_expr(
143143
else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
144144
{
145145
// the following works for signed and unsigned integers
146-
dest.set_value(integer2binary(
147-
binary2integer(id2string(dest.get_value()), false)*
148-
binary2integer(id2string(expr.get_value()), false),
146+
dest.set_value(integer2bv(
147+
bv2integer(id2string(dest.get_value()), false)*
148+
bv2integer(id2string(expr.get_value()), false),
149149
to_bitvector_type(dest.type()).get_width()));
150150
return false;
151151
}
@@ -831,7 +831,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
831831
}
832832
else if(expr.id()==ID_bitxor)
833833
{
834-
constant_exprt new_op(integer2binary(0, width), expr.type());
834+
constant_exprt new_op(integer2bv(0, width), expr.type());
835835
expr.swap(new_op);
836836
return false;
837837
}

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