Skip to content

Commit 651f60d

Browse files
author
Daniel Kroening
authored
Merge pull request #3699 from tautschnig/width-use-api
Use proper APIs to get or set bitvector type width
2 parents 3d8d44c + f7eba4a commit 651f60d

19 files changed

+71
-60
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -974,7 +974,7 @@ static std::size_t get_bytecode_type_width(const typet &ty)
974974
{
975975
if(ty.id()==ID_pointer)
976976
return 32;
977-
return ty.get_size_t(ID_width);
977+
return to_bitvector_type(ty).get_width();
978978
}
979979

980980
code_blockt java_bytecode_convert_methodt::convert_instructions(
@@ -2646,7 +2646,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
26462646
{
26472647
const typet type = java_type_from_char(statement[0]);
26482648

2649-
const std::size_t width = type.get_size_t(ID_width);
2649+
const std::size_t width = get_bytecode_type_width(type);
26502650
typet target = unsignedbv_typet(width);
26512651

26522652
exprt lhs = op[0];

‎jbmc/src/java_bytecode/java_utils.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ unsigned java_local_variable_slots(const typet &t)
3333
if(t.id()==ID_pointer)
3434
return 1;
3535

36-
const std::size_t bitwidth = t.get_size_t(ID_width);
36+
const std::size_t bitwidth = to_bitvector_type(t).get_width();
3737
INVARIANT(
3838
bitwidth==8 ||
3939
bitwidth==16 ||

‎src/ansi-c/c_typecast.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -279,10 +279,10 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
279279
c_typecastt::c_typet c_typecastt::get_c_type(
280280
const typet &type) const
281281
{
282-
const std::size_t width = type.get_size_t(ID_width);
283-
284282
if(type.id()==ID_signedbv)
285283
{
284+
const std::size_t width = to_bitvector_type(type).get_width();
285+
286286
if(width<=config.ansi_c.char_width)
287287
return CHAR;
288288
else if(width<=config.ansi_c.short_int_width)
@@ -298,6 +298,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
298298
}
299299
else if(type.id()==ID_unsignedbv)
300300
{
301+
const std::size_t width = to_bitvector_type(type).get_width();
302+
301303
if(width<=config.ansi_c.char_width)
302304
return UCHAR;
303305
else if(width<=config.ansi_c.short_int_width)
@@ -317,6 +319,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
317319
return BOOL;
318320
else if(type.id()==ID_floatbv)
319321
{
322+
const std::size_t width = to_bitvector_type(type).get_width();
323+
320324
if(width<=config.ansi_c.single_width)
321325
return SINGLE;
322326
else if(width<=config.ansi_c.double_width)
@@ -591,8 +595,8 @@ void c_typecastt::implicit_typecast_arithmetic(
591595
if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
592596
{
593597
// get the biggest width of both
594-
std::size_t width1=type1.get_size_t(ID_width);
595-
std::size_t width2=type2.get_size_t(ID_width);
598+
std::size_t width1 = to_bitvector_type(type1).get_width();
599+
std::size_t width2 = to_bitvector_type(type2).get_width();
596600

597601
// produce type
598602
typet result_type;

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 19 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -69,12 +69,13 @@ exprt c_typecheck_baset::do_initializer_rec(
6969
if(value.id()==ID_initializer_list)
7070
return do_initializer_list(value, type, force_constant);
7171

72-
if(value.id()==ID_array &&
73-
value.get_bool(ID_C_string_constant) &&
74-
full_type.id()==ID_array &&
75-
(full_type.subtype().id()==ID_signedbv ||
76-
full_type.subtype().id()==ID_unsignedbv) &&
77-
full_type.subtype().get(ID_width)==value.type().subtype().get(ID_width))
72+
if(
73+
value.id() == ID_array && value.get_bool(ID_C_string_constant) &&
74+
full_type.id() == ID_array &&
75+
(full_type.subtype().id() == ID_signedbv ||
76+
full_type.subtype().id() == ID_unsignedbv) &&
77+
to_bitvector_type(full_type.subtype()).get_width() ==
78+
to_bitvector_type(value.type().subtype()).get_width())
7879
{
7980
exprt tmp=value;
8081

@@ -130,11 +131,12 @@ exprt c_typecheck_baset::do_initializer_rec(
130131
return tmp;
131132
}
132133

133-
if(value.id()==ID_string_constant &&
134-
full_type.id()==ID_array &&
135-
(full_type.subtype().id()==ID_signedbv ||
136-
full_type.subtype().id()==ID_unsignedbv) &&
137-
full_type.subtype().get(ID_width)==char_type().get(ID_width))
134+
if(
135+
value.id() == ID_string_constant && full_type.id() == ID_array &&
136+
(full_type.subtype().id() == ID_signedbv ||
137+
full_type.subtype().id() == ID_unsignedbv) &&
138+
to_bitvector_type(full_type.subtype()).get_width() ==
139+
char_type().get_width())
138140
{
139141
// will go away, to be replaced by the above block
140142

@@ -876,11 +878,12 @@ exprt c_typecheck_baset::do_initializer_list(
876878

877879
// 6.7.9, 14: An array of character type may be initialized by a character
878880
// string literal or UTF-8 string literal, optionally enclosed in braces.
879-
if(value.operands().size()>=1 &&
880-
value.op0().id()==ID_string_constant &&
881-
(full_type.subtype().id()==ID_signedbv ||
882-
full_type.subtype().id()==ID_unsignedbv) &&
883-
full_type.subtype().get(ID_width)==char_type().get(ID_width))
881+
if(
882+
value.operands().size() >= 1 && value.op0().id() == ID_string_constant &&
883+
(full_type.subtype().id() == ID_signedbv ||
884+
full_type.subtype().id() == ID_unsignedbv) &&
885+
to_bitvector_type(full_type.subtype()).get_width() ==
886+
char_type().get_width())
884887
{
885888
if(value.operands().size()>1)
886889
{

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,8 @@ void c_typecheck_baset::typecheck_type(typet &type)
7676
else if(type.id()==ID_pointer)
7777
{
7878
typecheck_type(type.subtype());
79-
INVARIANT(!type.get(ID_width).empty(), "pointers must have width");
79+
INVARIANT(
80+
to_bitvector_type(type).get_width() > 0, "pointers must have width");
8081
}
8182
else if(type.id()==ID_struct ||
8283
type.id()==ID_union)
@@ -1433,7 +1434,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
14331434
throw 0;
14341435
}
14351436

1436-
sub_width = c_enum_type.subtype().get_size_t(ID_width);
1437+
sub_width = to_bitvector_type(c_enum_type.subtype()).get_width();
14371438
}
14381439
else
14391440
{

‎src/ansi-c/expr2c.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,7 @@ std::string expr2ct::convert_rec(
244244
return q+"long double"+d;
245245
else
246246
{
247-
std::string swidth=src.get_string(ID_width);
247+
std::string swidth = std::to_string(width);
248248
std::string fwidth=src.get_string(ID_f);
249249
return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";
250250
}
@@ -282,7 +282,7 @@ std::string expr2ct::convert_rec(
282282

283283
// There is also wchar_t among the above, but this isn't a C type.
284284

285-
mp_integer width=string2integer(src.get_string(ID_width));
285+
const std::size_t width = to_bitvector_type(src).get_width();
286286

287287
bool is_signed=src.id()==ID_signedbv;
288288
std::string sign_str=is_signed?"signed ":"unsigned ";

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,8 @@ exprt convert_integer_literal(const std::string &src)
9090
else
9191
c_type=is_unsigned?ID_unsigned_long_long_int:ID_signed_long_long_int;
9292

93-
typet type=typet(is_unsigned?ID_unsignedbv:ID_signedbv);
94-
type.set(ID_width, width_suffix);
93+
bitvector_typet type(
94+
is_unsigned ? ID_unsignedbv : ID_signedbv, width_suffix);
9595
type.set(ID_C_c_type, c_type);
9696

9797
exprt result=from_integer(value, type);
@@ -166,9 +166,7 @@ exprt convert_integer_literal(const std::string &src)
166166
c_type=ID_signed_long_long_int;
167167
}
168168

169-
typet type=typet(is_signed?ID_signedbv:ID_unsignedbv);
170-
171-
type.set(ID_width, width);
169+
bitvector_typet type(is_signed ? ID_signedbv : ID_unsignedbv, width);
172170
type.set(ID_C_c_type, c_type);
173171

174172
exprt result;

‎src/ansi-c/padding.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ underlying_width(const c_bit_field_typet &type, const namespacet &ns)
123123
const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
124124

125125
if(c_enum_type.id() == ID_c_enum)
126-
return c_enum_type.subtype().get_size_t(ID_width);
126+
return to_bitvector_type(c_enum_type.subtype()).get_width();
127127
else
128128
return {};
129129
}

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -784,8 +784,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
784784
typecheck_expr(size);
785785

786786
bool size_is_unsigned=(size.type().id()==ID_unsignedbv);
787-
typet integer_type(size_is_unsigned?ID_unsignedbv:ID_signedbv);
788-
integer_type.set(ID_width, config.ansi_c.int_width);
787+
bitvector_typet integer_type(
788+
size_is_unsigned ? ID_unsignedbv : ID_signedbv, config.ansi_c.int_width);
789789
implicit_typecast(size, integer_type);
790790

791791
expr.set(ID_statement, ID_cpp_new_array);

‎src/cpp/expr2cpp.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -295,7 +295,8 @@ std::string expr2cppt::convert_rec(
295295
}
296296
else if(src.id()==ID_verilog_signedbv ||
297297
src.id()==ID_verilog_unsignedbv)
298-
return "sc_lv["+id2string(src.get(ID_width))+"]"+d;
298+
return "sc_lv[" + std::to_string(to_bitvector_type(src).get_width()) + "]" +
299+
d;
299300
else if(src.id()==ID_unassigned)
300301
return "?";
301302
else if(src.id()==ID_code)

‎src/goto-instrument/accelerate/overflow_instrumenter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -110,8 +110,8 @@ void overflow_instrumentert::overflow_expr(
110110
}
111111

112112
const typet &old_type=ns.follow(expr.op0().type());
113-
const std::size_t new_width = expr.type().get_size_t(ID_width);
114-
const std::size_t old_width = old_type.get_size_t(ID_width);
113+
const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
114+
const std::size_t old_width = to_bitvector_type(old_type).get_width();
115115

116116
if(type.id()==ID_signedbv)
117117
{

‎src/solvers/flattening/boolbv_not.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,10 @@ bvt boolbvt::convert_not(const not_exprt &expr)
1919
if(op_type.id()!=ID_verilog_signedbv ||
2020
op_type.id()!=ID_verilog_unsignedbv)
2121
{
22-
if((expr.type().id()==ID_verilog_signedbv ||
23-
expr.type().id()==ID_verilog_unsignedbv) &&
24-
expr.type().get_size_t(ID_width) == 1)
22+
if(
23+
(expr.type().id() == ID_verilog_signedbv ||
24+
expr.type().id() == ID_verilog_unsignedbv) &&
25+
to_bitvector_type(expr.type()).get_width() == 1)
2526
{
2627
literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
2728
literalt normal_bits_zero=

‎src/solvers/flattening/boolbv_reduction.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -76,9 +76,10 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
7676
if(op_type.id()!=ID_verilog_signedbv ||
7777
op_type.id()!=ID_verilog_unsignedbv)
7878
{
79-
if((expr.type().id()==ID_verilog_signedbv ||
80-
expr.type().id()==ID_verilog_unsignedbv) &&
81-
expr.type().get_size_t(ID_width) == 1)
79+
if(
80+
(expr.type().id() == ID_verilog_signedbv ||
81+
expr.type().id() == ID_verilog_unsignedbv) &&
82+
to_bitvector_type(expr.type()).get_width() == 1)
8283
{
8384
bvt bv;
8485
bv.resize(2);

‎src/solvers/flattening/boolbv_width.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
105105
type_id==ID_verilog_unsignedbv)
106106
{
107107
// we encode with two bits
108-
std::size_t size = type.get_size_t(ID_width);
108+
std::size_t size = to_bitvector_type(type).get_width();
109109
DATA_INVARIANT(
110110
size > 0, "verilog bitvector width shall be greater than zero");
111111
entry.total_width = size * 2;
@@ -175,7 +175,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
175175
else if(type_id==ID_c_enum)
176176
{
177177
// these have a subtype
178-
entry.total_width = type.subtype().get_size_t(ID_width);
178+
entry.total_width = to_bitvector_type(type.subtype()).get_width();
179179
CHECK_RETURN(entry.total_width > 0);
180180
}
181181
else if(type_id==ID_incomplete_c_enum)

‎src/util/arith_tools.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ constant_exprt from_integer(
153153
else if(type_id==ID_c_enum)
154154
{
155155
const std::size_t width =
156-
to_c_enum_type(type).subtype().get_size_t(ID_width);
156+
to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
157157
return constant_exprt(integer2bvrep(int_value, width), type);
158158
}
159159
else if(type_id==ID_c_bool)

‎src/util/bv_arithmetic.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ void bv_spect::from_type(const typet &type)
4343
else
4444
UNREACHABLE;
4545

46-
width=unsafe_string2unsigned(type.get_string(ID_width));
46+
width = to_bitvector_type(type).get_width();
4747
}
4848

4949
void bv_arithmetict::print(std::ostream &out) const

‎src/util/json_expr.cpp

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -283,8 +283,8 @@ json_objectt json(
283283
{
284284
result["name"]=json_stringt("integer");
285285
result["binary"] = json_stringt(binary(constant_expr));
286-
result["width"] =
287-
json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));
286+
result["width"] = json_numbert(std::to_string(
287+
to_bitvector_type(to_c_enum_type(type).subtype()).get_width()));
288288
result["type"]=json_stringt("enum");
289289
result["data"]=json_stringt(value_string);
290290
}
@@ -303,15 +303,17 @@ json_objectt json(
303303
else if(type.id()==ID_fixedbv)
304304
{
305305
result["name"]=json_stringt("fixed");
306-
result["width"]=json_numbert(type.get_string(ID_width));
306+
result["width"] =
307+
json_numbert(std::to_string(to_bitvector_type(type).get_width()));
307308
result["binary"] = json_stringt(binary(constant_expr));
308309
result["data"]=
309310
json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
310311
}
311312
else if(type.id()==ID_floatbv)
312313
{
313314
result["name"]=json_stringt("float");
314-
result["width"]=json_numbert(type.get_string(ID_width));
315+
result["width"] =
316+
json_numbert(std::to_string(to_bitvector_type(type).get_width()));
315317
result["binary"] = json_stringt(binary(constant_expr));
316318
result["data"]=
317319
json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
@@ -349,7 +351,8 @@ json_objectt json(
349351
else if(type.id()==ID_c_bool)
350352
{
351353
result["name"]=json_stringt("integer");
352-
result["width"]=json_numbert(type.get_string(ID_width));
354+
result["width"] =
355+
json_numbert(std::to_string(to_bitvector_type(type).get_width()));
353356
result["type"]=json_stringt(type_string);
354357
result["binary"]=json_stringt(expr.get_string(ID_value));
355358
result["data"]=json_stringt(value_string);

‎src/util/simplify_expr_int.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -913,7 +913,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
913913
});
914914

915915
to_constant_expr(opi).set_value(new_value);
916-
opi.type().set(ID_width, new_width);
916+
to_bitvector_type(opi.type()).set_width(new_width);
917917
// erase opn
918918
expr.operands().erase(expr.operands().begin()+i+1);
919919
result = false;
@@ -943,7 +943,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
943943
const std::string new_value=
944944
opi.get_string(ID_value)+opn.get_string(ID_value);
945945
opi.set(ID_value, new_value);
946-
opi.type().set(ID_width, new_value.size());
946+
to_bitvector_type(opi.type()).set_width(new_value.size());
947947
opi.type().id(ID_verilog_unsignedbv);
948948
// erase opn
949949
expr.operands().erase(expr.operands().begin()+i+1);
@@ -995,8 +995,7 @@ bool simplify_exprt::simplify_shifts(exprt &expr)
995995
if(expr.op0().type().id()==ID_unsignedbv ||
996996
expr.op0().type().id()==ID_signedbv)
997997
{
998-
mp_integer width=
999-
string2integer(id2string(expr.op0().type().get(ID_width)));
998+
const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
1000999

10011000
if(expr.id()==ID_lshr)
10021001
{

‎src/util/xml_expr.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -196,7 +196,7 @@ xmlt xml(
196196
result.name="integer";
197197
result.set_attribute("binary", expr.get_string(ID_value));
198198
result.set_attribute(
199-
"width", to_c_enum_type(type).subtype().get_string(ID_width));
199+
"width", to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
200200
result.set_attribute("c_type", "enum");
201201

202202
mp_integer i;
@@ -218,14 +218,14 @@ xmlt xml(
218218
else if(type.id()==ID_fixedbv)
219219
{
220220
result.name="fixed";
221-
result.set_attribute("width", type.get_string(ID_width));
221+
result.set_attribute("width", to_bitvector_type(type).get_width());
222222
result.set_attribute("binary", expr.get_string(ID_value));
223223
result.data=fixedbvt(to_constant_expr(expr)).to_ansi_c_string();
224224
}
225225
else if(type.id()==ID_floatbv)
226226
{
227227
result.name="float";
228-
result.set_attribute("width", type.get_string(ID_width));
228+
result.set_attribute("width", to_bitvector_type(type).get_width());
229229
result.set_attribute("binary", expr.get_string(ID_value));
230230
result.data=ieee_floatt(to_constant_expr(expr)).to_ansi_c_string();
231231
}

0 commit comments

Comments
 (0)