Skip to content

Commit 37a2a8e

Browse files
tautschnigtautschnig
authored
Merge pull request #8230 from tautschnig/cleanup/no-follow-goto-programs
goto-programs: Replace uses of namespacet::follow
2 parents 03f604e + 60dc466 commit 37a2a8e

12 files changed

+88
-103
lines changed

‎src/goto-programs/class_identifier.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,8 @@ static exprt build_class_identifier(
2828

2929
while(1)
3030
{
31-
const typet &type=ns.follow(e.type());
32-
const struct_typet &struct_type=to_struct_type(type);
31+
const struct_typet &struct_type =
32+
ns.follow_tag(to_struct_tag_type(e.type()));
3333
const struct_typet::componentst &components=struct_type.components();
3434
INVARIANT(!components.empty(), "class structs cannot be empty");
3535

@@ -85,7 +85,8 @@ void set_class_identifier(
8585
const namespacet &ns,
8686
const struct_tag_typet &class_type)
8787
{
88-
const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
88+
const struct_typet &struct_type =
89+
ns.follow_tag(to_struct_tag_type(expr.type()));
8990
const struct_typet::componentst &components=struct_type.components();
9091

9192
if(components.empty())

‎src/goto-programs/destructor.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,13 @@ code_function_callt get_destructor(
3838
{
3939
const typet &arg_type=code_type.parameters().front().type();
4040

41+
if(arg_type.id() != ID_pointer)
42+
continue;
43+
44+
const typet &base_type = to_pointer_type(arg_type).base_type();
4145
if(
42-
arg_type.id() == ID_pointer &&
43-
ns.follow(to_pointer_type(arg_type).base_type()) == type)
46+
base_type.id() == ID_struct_tag &&
47+
ns.follow_tag(to_struct_tag_type(base_type)) == type)
4448
{
4549
const symbol_exprt symbol_expr(op.get(ID_name), op.type());
4650
return code_function_callt(symbol_expr);

‎src/goto-programs/graphml_witness.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -132,10 +132,11 @@ std::string graphml_witnesst::convert_assign_rec(
132132
return convert_assign_rec(identifier, tmp);
133133
}
134134

135-
const struct_union_typet &type=
136-
to_struct_union_type(ns.follow(assign.lhs().type()));
137-
const struct_union_typet::componentst &components=
138-
type.components();
135+
const typet &lhs_type = assign.lhs().type();
136+
const struct_union_typet::componentst &components =
137+
(lhs_type.id() == ID_struct_tag || lhs_type.id() == ID_union_tag)
138+
? ns.follow_tag(to_struct_or_union_tag_type(lhs_type)).components()
139+
: to_struct_union_type(lhs_type).components();
139140

140141
exprt::operandst::const_iterator it=
141142
assign.rhs().operands().begin();

‎src/goto-programs/interpreter.cpp

Lines changed: 21 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -424,11 +424,11 @@ void interpretert::execute_decl()
424424
struct_typet::componentt
425425
interpretert::get_component(const typet &object_type, const mp_integer &offset)
426426
{
427-
const typet real_type = ns.follow(object_type);
428-
if(real_type.id()!=ID_struct)
427+
if(object_type.id() != ID_struct_tag)
429428
throw "request for member of non-struct";
430429

431-
const struct_typet &struct_type=to_struct_type(real_type);
430+
const struct_typet &struct_type =
431+
ns.follow_tag(to_struct_tag_type(object_type));
432432
const struct_typet::componentst &components=struct_type.components();
433433

434434
mp_integer tmp_offset=offset;
@@ -460,11 +460,10 @@ exprt interpretert::get_value(
460460
const mp_integer &offset,
461461
bool use_non_det)
462462
{
463-
const typet real_type=ns.follow(type);
464-
if(real_type.id()==ID_struct)
463+
if(type.id() == ID_struct_tag)
465464
{
466-
struct_exprt result({}, real_type);
467-
const struct_typet &struct_type=to_struct_type(real_type);
465+
struct_exprt result({}, type);
466+
const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));
468467
const struct_typet::componentst &components=struct_type.components();
469468

470469
// Retrieve the values for the individual members
@@ -482,10 +481,10 @@ exprt interpretert::get_value(
482481

483482
return std::move(result);
484483
}
485-
else if(real_type.id()==ID_array)
484+
else if(type.id() == ID_array)
486485
{
487486
// Get size of array
488-
array_exprt result({}, to_array_type(real_type));
487+
array_exprt result({}, to_array_type(type));
489488
const exprt &size_expr = to_array_type(type).size();
490489
mp_integer subtype_size = get_size(to_array_type(type).element_type());
491490
mp_integer count;
@@ -526,13 +525,12 @@ exprt interpretert::get_value(
526525
mp_vectort &rhs,
527526
const mp_integer &offset)
528527
{
529-
const typet real_type=ns.follow(type);
530528
PRECONDITION(!rhs.empty());
531529

532-
if(real_type.id()==ID_struct)
530+
if(type.id() == ID_struct_tag)
533531
{
534-
struct_exprt result({}, real_type);
535-
const struct_typet &struct_type=to_struct_type(real_type);
532+
struct_exprt result({}, type);
533+
const struct_typet &struct_type = ns.follow_tag(to_struct_tag_type(type));
536534
const struct_typet::componentst &components=struct_type.components();
537535

538536
// Retrieve the values for the individual members
@@ -548,10 +546,10 @@ exprt interpretert::get_value(
548546
}
549547
return std::move(result);
550548
}
551-
else if(real_type.id()==ID_array)
549+
else if(type.id() == ID_array)
552550
{
553-
array_exprt result({}, to_array_type(real_type));
554-
const exprt &size_expr = to_array_type(real_type).size();
551+
array_exprt result({}, to_array_type(type));
552+
const exprt &size_expr = to_array_type(type).size();
555553

556554
// Get size of array
557555
mp_integer subtype_size = get_size(to_array_type(type).element_type());
@@ -576,34 +574,34 @@ exprt interpretert::get_value(
576574
}
577575
return std::move(result);
578576
}
579-
else if(real_type.id()==ID_floatbv)
577+
else if(type.id() == ID_floatbv)
580578
{
581579
ieee_floatt f(to_floatbv_type(type));
582580
f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
583581
return f.to_expr();
584582
}
585-
else if(real_type.id()==ID_fixedbv)
583+
else if(type.id() == ID_fixedbv)
586584
{
587585
fixedbvt f;
588586
f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
589587
return f.to_expr();
590588
}
591-
else if(real_type.id()==ID_bool)
589+
else if(type.id() == ID_bool)
592590
{
593591
if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
594592
return true_exprt();
595593
else
596594
false_exprt();
597595
}
598-
else if(real_type.id()==ID_c_bool)
596+
else if(type.id() == ID_c_bool)
599597
{
600598
return from_integer(
601599
rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
602600
}
603-
else if(real_type.id() == ID_pointer)
601+
else if(type.id() == ID_pointer)
604602
{
605603
if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
606-
return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
604+
return null_pointer_exprt(to_pointer_type(type)); // NULL pointer
607605

608606
if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
609607
{
@@ -634,7 +632,7 @@ exprt interpretert::get_value(
634632

635633
throw "interpreter: reading from invalid pointer";
636634
}
637-
else if(real_type.id()==ID_string)
635+
else if(type.id() == ID_string)
638636
{
639637
// Strings are currently encoded by their irep_idt ID.
640638
return constant_exprt(

‎src/goto-programs/interpreter_evaluate.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1042,7 +1042,7 @@ mp_integer interpretert::evaluate_address(
10421042
else if(expr.id()==ID_member)
10431043
{
10441044
const struct_typet &struct_type =
1045-
to_struct_type(ns.follow(to_member_expr(expr).compound().type()));
1045+
ns.follow_tag(to_struct_tag_type(to_member_expr(expr).compound().type()));
10461046

10471047
const irep_idt &component_name=
10481048
to_member_expr(expr).get_component_name();

‎src/goto-programs/json_expr.cpp

Lines changed: 14 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -361,24 +361,22 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
361361
{
362362
result["name"] = json_stringt("struct");
363363

364-
const typet &type = ns.follow(expr.type());
364+
const struct_typet &struct_type =
365+
expr.type().id() == ID_struct_tag
366+
? ns.follow_tag(to_struct_tag_type(expr.type()))
367+
: to_struct_type(expr.type());
368+
const struct_typet::componentst &components = struct_type.components();
369+
DATA_INVARIANT(
370+
components.size() == expr.operands().size(),
371+
"number of struct components should match with its type");
365372

366-
// these are expected to have a struct type
367-
if(type.id() == ID_struct)
373+
json_arrayt &members = result["members"].make_array();
374+
for(std::size_t m = 0; m < expr.operands().size(); m++)
368375
{
369-
const struct_typet &struct_type = to_struct_type(type);
370-
const struct_typet::componentst &components = struct_type.components();
371-
DATA_INVARIANT(
372-
components.size() == expr.operands().size(),
373-
"number of struct components should match with its type");
374-
375-
json_arrayt &members = result["members"].make_array();
376-
for(std::size_t m = 0; m < expr.operands().size(); m++)
377-
{
378-
json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
379-
{"name", json_stringt(components[m].get_name())}};
380-
members.push_back(std::move(e));
381-
}
376+
json_objectt e{
377+
{"value", json(expr.operands()[m], ns, mode)},
378+
{"name", json_stringt(components[m].get_name())}};
379+
members.push_back(std::move(e));
382380
}
383381
}
384382
else if(expr.id() == ID_union)

‎src/goto-programs/remove_const_function_pointers.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -800,7 +800,8 @@ bool remove_const_function_pointerst::is_const_type(const typet &type) const
800800
exprt remove_const_function_pointerst::get_component_value(
801801
const struct_exprt &struct_expr, const member_exprt &member_expr)
802802
{
803-
const struct_typet &struct_type=to_struct_type(ns.follow(struct_expr.type()));
803+
const struct_typet &struct_type =
804+
ns.follow_tag(to_struct_tag_type(struct_expr.type()));
804805
size_t component_number=
805806
struct_type.component_number(member_expr.get_component_name());
806807

‎src/goto-programs/rewrite_union.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,10 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns)
139139
byte_extract_exprt &be = to_byte_extract_expr(expr);
140140
if(be.op().type().id() == ID_union || be.op().type().id() == ID_union_tag)
141141
{
142-
const union_typet &union_type = to_union_type(ns.follow(be.op().type()));
142+
const union_typet &union_type =
143+
be.op().type().id() == ID_union_tag
144+
? ns.follow_tag(to_union_tag_type(be.op().type()))
145+
: to_union_type(be.op().type());
143146

144147
for(const auto &comp : union_type.components())
145148
{

‎src/goto-programs/string_abstraction.cpp

Lines changed: 20 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -353,14 +353,10 @@ exprt string_abstractiont::make_val_or_dummy_rec(goto_programt &dest,
353353
symbol.type.id() == ID_union_tag ||
354354
(symbol.type.id() == ID_struct_tag && symbol.type != string_struct))
355355
{
356-
const struct_union_typet &su_source =
357-
to_struct_union_type(ns.follow(source_type));
358-
const struct_union_typet::componentst &s_components=
359-
su_source.components();
360-
const struct_union_typet &struct_union_type =
361-
to_struct_union_type(ns.follow(symbol.type));
362-
const struct_union_typet::componentst &components=
363-
struct_union_type.components();
356+
const struct_union_typet::componentst &s_components =
357+
ns.follow_tag(to_struct_or_union_tag_type(source_type)).components();
358+
const struct_union_typet::componentst &components =
359+
ns.follow_tag(to_struct_or_union_tag_type(symbol.type)).components();
364360
unsigned seen=0;
365361

366362
struct_union_typet::componentst::const_iterator it2=components.begin();
@@ -442,10 +438,9 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
442438
build_unknown(whatt::LENGTH, false),
443439
to_array_type(source_type).size().id() == ID_infinity
444440
? build_unknown(whatt::SIZE, false)
445-
: to_array_type(source_type).size()},
441+
: typecast_exprt::conditional_cast(
442+
to_array_type(source_type).size(), build_type(whatt::SIZE))},
446443
string_struct);
447-
448-
make_type(to_struct_expr(new_symbol.value).op2(), build_type(whatt::SIZE));
449444
}
450445
else
451446
new_symbol.value=
@@ -733,7 +728,10 @@ const typet &string_abstractiont::build_abstraction_type_rec(const typet &type,
733728
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
734729
{
735730
const struct_union_typet &struct_union_type =
736-
to_struct_union_type(ns.follow(type));
731+
type.id() == ID_struct_tag ? static_cast<const struct_union_typet &>(
732+
ns.follow_tag(to_struct_tag_type(type)))
733+
: static_cast<const struct_union_typet &>(
734+
ns.follow_tag(to_union_tag_type(type)));
737735

738736
struct_union_typet::componentst new_comp;
739737
for(const auto &comp : struct_union_type.components())
@@ -1212,8 +1210,8 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
12121210
i2.is_not_nil(),
12131211
"failed to create length-component for the left-hand-side");
12141212

1215-
exprt new_length=i_lhs.index();
1216-
make_type(new_length, i2.type());
1213+
exprt new_length =
1214+
typecast_exprt::conditional_cast(i_lhs.index(), i2.type());
12171215

12181216
if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
12191217
new_length, i2);
@@ -1232,16 +1230,14 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
12321230
i2.is_not_nil(),
12331231
"failed to create length-component for the left-hand-side");
12341232

1235-
make_type(ptr.offset, build_type(whatt::LENGTH));
1236-
return
1237-
char_assign(
1238-
dest,
1239-
target,
1240-
new_lhs,
1241-
i2,
1242-
ptr.offset.is_nil()?
1243-
from_integer(0, build_type(whatt::LENGTH)):
1244-
ptr.offset);
1233+
return char_assign(
1234+
dest,
1235+
target,
1236+
new_lhs,
1237+
i2,
1238+
ptr.offset.is_nil() ? from_integer(0, build_type(whatt::LENGTH))
1239+
: typecast_exprt::conditional_cast(
1240+
ptr.offset, build_type(whatt::LENGTH)));
12451241
}
12461242
}
12471243

‎src/goto-programs/string_abstraction.h

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -73,13 +73,6 @@ class string_abstractiont
7373

7474
bool is_ptr_string_struct(const typet &type) const;
7575

76-
void make_type(exprt &dest, const typet &type)
77-
{
78-
if(dest.is_not_nil() &&
79-
ns.follow(dest.type())!=ns.follow(type))
80-
dest = typecast_exprt(dest, type);
81-
}
82-
8376
goto_programt::targett abstract(
8477
goto_programt &dest, goto_programt::targett it);
8578
goto_programt::targett abstract_assign(

‎src/goto-programs/string_instrumentation.cpp

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -64,12 +64,6 @@ class string_instrumentationt
6464
symbol_table_baset &symbol_table;
6565
namespacet ns;
6666

67-
void make_type(exprt &dest, const typet &type)
68-
{
69-
if(ns.follow(dest.type())!=ns.follow(type))
70-
dest = typecast_exprt(dest, type);
71-
}
72-
7367
void instrument(goto_programt &dest, goto_programt::targett it);
7468
void do_function_call(goto_programt &dest, goto_programt::targett target);
7569

@@ -785,8 +779,7 @@ void string_instrumentationt::do_strerror(
785779

786780
// assign address
787781
{
788-
exprt rhs=ptr;
789-
make_type(rhs, lhs.type());
782+
exprt rhs = typecast_exprt::conditional_cast(ptr, lhs.type());
790783
tmp.add(goto_programt::make_assignment(
791784
code_assignt(lhs, rhs), it->source_location()));
792785
}

‎src/goto-programs/xml_expr.cpp

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -253,21 +253,18 @@ xmlt xml(const exprt &expr, const namespacet &ns)
253253
{
254254
result.name = "struct";
255255

256-
const typet &type = ns.follow(expr.type());
256+
const struct_typet &struct_type =
257+
expr.type().id() == ID_struct_tag
258+
? ns.follow_tag(to_struct_tag_type(expr.type()))
259+
: to_struct_type(expr.type());
260+
const struct_typet::componentst &components = struct_type.components();
261+
PRECONDITION(components.size() == expr.operands().size());
257262

258-
// these are expected to have a struct type
259-
if(type.id() == ID_struct)
263+
for(unsigned m = 0; m < expr.operands().size(); m++)
260264
{
261-
const struct_typet &struct_type = to_struct_type(type);
262-
const struct_typet::componentst &components = struct_type.components();
263-
PRECONDITION(components.size() == expr.operands().size());
264-
265-
for(unsigned m = 0; m < expr.operands().size(); m++)
266-
{
267-
xmlt &e = result.new_element("member");
268-
e.new_element() = xml(expr.operands()[m], ns);
269-
e.set_attribute("name", id2string(components[m].get_name()));
270-
}
265+
xmlt &e = result.new_element("member");
266+
e.new_element() = xml(expr.operands()[m], ns);
267+
e.set_attribute("name", id2string(components[m].get_name()));
271268
}
272269
}
273270
else if(expr.id() == ID_union)

0 commit comments

Comments
 (0)