Skip to content

Commit 7241dd9

Browse files
committed
Pointer analysis: Replace uses of namespacet::follow
This is deprecated. Use suitable variants of `follow_tag` instead.
1 parent d7b229e commit 7241dd9

File tree

5 files changed

+93
-91
lines changed

5 files changed

+93
-91
lines changed

src/pointer-analysis/value_set.cpp

Lines changed: 49 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -516,8 +516,6 @@ void value_sett::get_value_set_rec(
516516
std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
517517
#endif
518518

519-
const typet &expr_type=ns.follow(expr.type());
520-
521519
if(expr.id()==ID_unknown || expr.id()==ID_invalid)
522520
{
523521
insert(dest, exprt(ID_unknown, original_type));
@@ -539,17 +537,20 @@ void value_sett::get_value_set_rec(
539537
}
540538
else if(expr.id()==ID_member)
541539
{
542-
const typet &type = ns.follow(to_member_expr(expr).compound().type());
540+
const exprt &compound = to_member_expr(expr).compound();
543541

544542
DATA_INVARIANT(
545-
type.id() == ID_struct || type.id() == ID_union,
543+
compound.type().id() == ID_struct ||
544+
compound.type().id() == ID_struct_tag ||
545+
compound.type().id() == ID_union ||
546+
compound.type().id() == ID_union_tag,
546547
"compound of member expression must be struct or union");
547548

548549
const std::string &component_name=
549550
expr.get_string(ID_component_name);
550551

551552
get_value_set_rec(
552-
to_member_expr(expr).compound(),
553+
compound,
553554
dest,
554555
includes_nondet_pointer,
555556
"." + component_name + suffix,
@@ -559,7 +560,7 @@ void value_sett::get_value_set_rec(
559560
else if(expr.id()==ID_symbol)
560561
{
561562
auto entry_index = get_index_of_symbol(
562-
to_symbol_expr(expr).get_identifier(), expr_type, suffix, ns);
563+
to_symbol_expr(expr).get_identifier(), expr.type(), suffix, ns);
563564

564565
if(entry_index.has_value())
565566
make_union(dest, find_entry(*entry_index)->object_map);
@@ -624,11 +625,11 @@ void value_sett::get_value_set_rec(
624625
{
625626
insert(
626627
dest,
627-
exprt(ID_null_object, to_pointer_type(expr_type).base_type()),
628+
exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
628629
mp_integer{0});
629630
}
630-
else if(expr_type.id()==ID_unsignedbv ||
631-
expr_type.id()==ID_signedbv)
631+
else if(
632+
expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
632633
{
633634
// an integer constant got turned into a pointer
634635
insert(dest, exprt(ID_integer_address, unsigned_char_type()));
@@ -703,7 +704,7 @@ void value_sett::get_value_set_rec(
703704
// special case for plus/minus and exactly one pointer
704705
std::optional<exprt> ptr_operand;
705706
if(
706-
expr_type.id() == ID_pointer &&
707+
expr.type().id() == ID_pointer &&
707708
(expr.id() == ID_plus || expr.id() == ID_minus))
708709
{
709710
bool non_const_offset = false;
@@ -879,10 +880,10 @@ void value_sett::get_value_set_rec(
879880
statement==ID_cpp_new_array)
880881
{
881882
PRECONDITION(suffix.empty());
882-
PRECONDITION(expr_type.id() == ID_pointer);
883+
PRECONDITION(expr.type().id() == ID_pointer);
883884

884885
dynamic_object_exprt dynamic_object(
885-
to_pointer_type(expr_type).base_type());
886+
to_pointer_type(expr.type()).base_type());
886887
dynamic_object.set_instance(location_number);
887888
dynamic_object.valid()=true_exprt();
888889

@@ -893,7 +894,10 @@ void value_sett::get_value_set_rec(
893894
}
894895
else if(expr.id()==ID_struct)
895896
{
896-
const auto &struct_components = to_struct_type(expr_type).components();
897+
const auto &struct_components =
898+
expr.type().id() == ID_struct_tag
899+
? ns.follow_tag(to_struct_tag_type(expr.type())).components()
900+
: to_struct_type(expr.type()).components();
897901
INVARIANT(
898902
struct_components.size() == expr.operands().size(),
899903
"struct expression should have an operand per component");
@@ -950,7 +954,7 @@ void value_sett::get_value_set_rec(
950954

951955
// If the suffix is empty we're looking for the whole struct:
952956
// default to combining both options as below.
953-
if(expr_type.id() == ID_struct && !suffix.empty())
957+
if(expr.type().id() == ID_struct_tag && !suffix.empty())
954958
{
955959
irep_idt component_name = with_expr.where().get(ID_component_name);
956960
if(suffix_starts_with_field(suffix, id2string(component_name)))
@@ -966,7 +970,8 @@ void value_sett::get_value_set_rec(
966970
original_type,
967971
ns);
968972
}
969-
else if(to_struct_type(expr_type).has_component(component_name))
973+
else if(ns.follow_tag(to_struct_tag_type(expr.type()))
974+
.has_component(component_name))
970975
{
971976
// Looking for a non-overwritten member, look through this expression
972977
get_value_set_rec(
@@ -998,7 +1003,7 @@ void value_sett::get_value_set_rec(
9981003
ns);
9991004
}
10001005
}
1001-
else if(expr_type.id() == ID_array && !suffix.empty())
1006+
else if(expr.type().id() == ID_array && !suffix.empty())
10021007
{
10031008
std::string new_value_suffix;
10041009
if(has_prefix(suffix, "[]"))
@@ -1105,8 +1110,7 @@ void value_sett::get_value_set_rec(
11051110

11061111
bool found=false;
11071112

1108-
const typet &op_type = ns.follow(byte_extract_expr.op().type());
1109-
if(op_type.id() == ID_struct)
1113+
if(byte_extract_expr.op().type().id() == ID_struct_tag)
11101114
{
11111115
exprt offset = byte_extract_expr.offset();
11121116
if(eval_pointer_offset(offset, ns))
@@ -1115,7 +1119,8 @@ void value_sett::get_value_set_rec(
11151119
const auto offset_int = numeric_cast<mp_integer>(offset);
11161120
const auto type_size = pointer_offset_size(expr.type(), ns);
11171121

1118-
const struct_typet &struct_type = to_struct_type(op_type);
1122+
const struct_typet &struct_type =
1123+
ns.follow_tag(to_struct_tag_type(byte_extract_expr.op().type()));
11191124

11201125
for(const auto &c : struct_type.components())
11211126
{
@@ -1150,10 +1155,13 @@ void value_sett::get_value_set_rec(
11501155
}
11511156
}
11521157

1153-
if(op_type.id() == ID_union)
1158+
if(byte_extract_expr.op().type().id() == ID_union_tag)
11541159
{
11551160
// just collect them all
1156-
for(const auto &c : to_union_type(op_type).components())
1161+
const auto &components =
1162+
ns.follow_tag(to_union_tag_type(byte_extract_expr.op().type()))
1163+
.components();
1164+
for(const auto &c : components)
11571165
{
11581166
const irep_idt &name = c.get_name();
11591167
member_exprt member(byte_extract_expr.op(), name, c.type());
@@ -1429,13 +1437,12 @@ void value_sett::get_reference_set_rec(
14291437
// We cannot introduce a cast from scalar to non-scalar,
14301438
// thus, we can only adjust the types of structs and unions.
14311439

1432-
const typet &final_object_type = ns.follow(object.type());
1433-
1434-
if(final_object_type.id()==ID_struct ||
1435-
final_object_type.id()==ID_union)
1440+
if(
1441+
object.type().id() == ID_struct_tag ||
1442+
object.type().id() == ID_union_tag)
14361443
{
14371444
// adjust type?
1438-
if(ns.follow(struct_op.type())!=final_object_type)
1445+
if(struct_op.type() != object.type())
14391446
{
14401447
member_expr.compound() =
14411448
typecast_exprt(member_expr.compound(), struct_op.type());
@@ -1478,11 +1485,10 @@ void value_sett::assign(
14781485
output(std::cout);
14791486
#endif
14801487

1481-
const typet &type=ns.follow(lhs.type());
1482-
1483-
if(type.id() == ID_struct)
1488+
if(lhs.type().id() == ID_struct_tag)
14841489
{
1485-
for(const auto &c : to_struct_type(type).components())
1490+
for(const auto &c :
1491+
ns.follow_tag(to_struct_tag_type(lhs.type())).components())
14861492
{
14871493
const typet &subtype = c.type();
14881494
const irep_idt &name = c.get_name();
@@ -1513,12 +1519,10 @@ void value_sett::assign(
15131519
"rhs.type():\n" +
15141520
rhs.type().pretty() + "\n" + "lhs.type():\n" + lhs.type().pretty());
15151521

1516-
const typet &followed = ns.follow(rhs.type());
1517-
1518-
if(followed.id() == ID_struct || followed.id() == ID_union)
1522+
if(rhs.type().id() == ID_struct_tag || rhs.type().id() == ID_union_tag)
15191523
{
15201524
const struct_union_typet &rhs_struct_union_type =
1521-
to_struct_union_type(followed);
1525+
ns.follow_tag(to_struct_or_union_tag_type(rhs.type()));
15221526

15231527
const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
15241528
rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
@@ -1528,30 +1532,30 @@ void value_sett::assign(
15281532
}
15291533
}
15301534
}
1531-
else if(type.id()==ID_array)
1535+
else if(lhs.type().id() == ID_array)
15321536
{
15331537
const index_exprt lhs_index(
15341538
lhs,
15351539
exprt(ID_unknown, c_index_type()),
1536-
to_array_type(type).element_type());
1540+
to_array_type(lhs.type()).element_type());
15371541

15381542
if(rhs.id()==ID_unknown ||
15391543
rhs.id()==ID_invalid)
15401544
{
15411545
assign(
15421546
lhs_index,
1543-
exprt(rhs.id(), to_array_type(type).element_type()),
1547+
exprt(rhs.id(), to_array_type(lhs.type()).element_type()),
15441548
ns,
15451549
is_simplified,
15461550
add_to_sets);
15471551
}
15481552
else
15491553
{
15501554
DATA_INVARIANT(
1551-
rhs.type() == type,
1555+
rhs.type() == lhs.type(),
15521556
"value_sett::assign types should match, got: "
15531557
"rhs.type():\n" +
1554-
rhs.type().pretty() + "\n" + "type:\n" + type.pretty());
1558+
rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());
15551559

15561560
if(rhs.id()==ID_array_of)
15571561
{
@@ -1575,7 +1579,7 @@ void value_sett::assign(
15751579
const index_exprt op0_index(
15761580
to_with_expr(rhs).old(),
15771581
exprt(ID_unknown, c_index_type()),
1578-
to_array_type(type).element_type());
1582+
to_array_type(lhs.type()).element_type());
15791583

15801584
assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
15811585
assign(
@@ -1586,7 +1590,7 @@ void value_sett::assign(
15861590
const index_exprt rhs_index(
15871591
rhs,
15881592
exprt(ID_unknown, c_index_type()),
1589-
to_array_type(type).element_type());
1593+
to_array_type(lhs.type()).element_type());
15901594
assign(lhs_index, rhs_index, ns, is_simplified, true);
15911595
}
15921596
}
@@ -1683,15 +1687,15 @@ void value_sett::assign_rec(
16831687
{
16841688
const auto &lhs_member_expr = to_member_expr(lhs);
16851689
const auto &component_name = lhs_member_expr.get_component_name();
1686-
1687-
const typet &type = ns.follow(lhs_member_expr.compound().type());
1690+
const exprt &compound = lhs_member_expr.compound();
16881691

16891692
DATA_INVARIANT(
1690-
type.id() == ID_struct || type.id() == ID_union,
1693+
compound.type().id() == ID_struct_tag ||
1694+
compound.type().id() == ID_union_tag,
16911695
"operand 0 of member expression must be struct or union");
16921696

16931697
assign_rec(
1694-
lhs_member_expr.compound(),
1698+
compound,
16951699
values_rhs,
16961700
"." + id2string(component_name) + suffix,
16971701
ns,

src/pointer-analysis/value_set_analysis_fi.cpp

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

1313
#include "value_set_analysis_fi.h"
1414

15+
#include <util/c_types.h>
1516
#include <util/namespace.h>
1617
#include <util/pointer_expr.h>
1718
#include <util/symbol_table_base.h>
@@ -91,23 +92,22 @@ void value_set_analysis_fit::get_entries_rec(
9192
const typet &type,
9293
std::list<value_set_fit::entryt> &dest)
9394
{
94-
const typet &t=ns.follow(type);
95-
96-
if(t.id()==ID_struct ||
97-
t.id()==ID_union)
95+
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
9896
{
99-
for(const auto &c : to_struct_union_type(t).components())
97+
const auto &components =
98+
ns.follow_tag(to_struct_or_union_tag_type(type)).components();
99+
for(const auto &c : components)
100100
{
101101
get_entries_rec(
102102
identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
103103
}
104104
}
105-
else if(t.id()==ID_array)
105+
else if(type.id() == ID_array)
106106
{
107107
get_entries_rec(
108-
identifier, suffix + "[]", to_array_type(t).element_type(), dest);
108+
identifier, suffix + "[]", to_array_type(type).element_type(), dest);
109109
}
110-
else if(check_type(t))
110+
else if(check_type(type))
111111
{
112112
dest.push_back(value_set_fit::entryt(identifier, suffix));
113113
}
@@ -189,8 +189,10 @@ bool value_set_analysis_fit::check_type(const typet &type)
189189
}
190190
else if(type.id()==ID_array)
191191
return check_type(to_array_type(type).element_type());
192-
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
193-
return check_type(ns.follow(type));
192+
else if(type.id() == ID_struct_tag)
193+
return check_type(ns.follow_tag(to_struct_tag_type(type)));
194+
else if(type.id() == ID_union_tag)
195+
return check_type(ns.follow_tag(to_union_tag_type(type)));
194196

195197
return false;
196198
}

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -373,15 +373,14 @@ bool value_set_dereferencet::dereference_type_compare(
373373

374374
// check for struct prefixes
375375

376-
const typet ot_base=ns.follow(object_type),
377-
dt_base=ns.follow(dereference_type);
378-
379-
if(ot_base.id()==ID_struct &&
380-
dt_base.id()==ID_struct)
376+
if(
377+
object_type.id() == ID_struct_tag && dereference_type.id() == ID_struct_tag)
381378
{
382-
if(to_struct_type(dt_base).is_prefix_of(
383-
to_struct_type(ot_base)))
379+
if(ns.follow_tag(to_struct_tag_type(dereference_type))
380+
.is_prefix_of(ns.follow_tag(to_struct_tag_type(object_type))))
381+
{
384382
return true; // ok, dt is a prefix of ot
383+
}
385384
}
386385

387386
// we are generous about code pointers

0 commit comments

Comments
 (0)