Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pointer analysis: Replace uses of namespacet::follow #8231

Merged
merged 1 commit into from
May 6, 2024
+140 −86
Merged

Pointer analysis: Replace uses of namespacet::follow #8231

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
123 changes: 79 additions & 44 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -516,8 +516,6 @@ void value_sett::get_value_set_rec(
std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
#endif

const typet &expr_type=ns.follow(expr.type());

if(expr.id()==ID_unknown || expr.id()==ID_invalid)
{
insert(dest, exprt(ID_unknown, original_type));
Expand All @@ -539,17 +537,20 @@ void value_sett::get_value_set_rec(
}
else if(expr.id()==ID_member)
{
const typet &type = ns.follow(to_member_expr(expr).compound().type());
const exprt &compound = to_member_expr(expr).compound();

DATA_INVARIANT(
type.id() == ID_struct || type.id() == ID_union,
compound.type().id() == ID_struct ||
compound.type().id() == ID_struct_tag ||
compound.type().id() == ID_union ||
compound.type().id() == ID_union_tag,
"compound of member expression must be struct or union");

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

get_value_set_rec(
to_member_expr(expr).compound(),
compound,
dest,
includes_nondet_pointer,
"." + component_name + suffix,
Expand All @@ -559,7 +560,7 @@ void value_sett::get_value_set_rec(
else if(expr.id()==ID_symbol)
{
auto entry_index = get_index_of_symbol(
to_symbol_expr(expr).get_identifier(), expr_type, suffix, ns);
to_symbol_expr(expr).get_identifier(), expr.type(), suffix, ns);

if(entry_index.has_value())
make_union(dest, find_entry(*entry_index)->object_map);
Expand Down Expand Up @@ -624,11 +625,11 @@ void value_sett::get_value_set_rec(
{
insert(
dest,
exprt(ID_null_object, to_pointer_type(expr_type).base_type()),
exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
mp_integer{0});
}
else if(expr_type.id()==ID_unsignedbv ||
expr_type.id()==ID_signedbv)
else if(
expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv)
{
// an integer constant got turned into a pointer
insert(dest, exprt(ID_integer_address, unsigned_char_type()));
Expand Down Expand Up @@ -703,7 +704,7 @@ void value_sett::get_value_set_rec(
// special case for plus/minus and exactly one pointer
std::optional<exprt> ptr_operand;
if(
expr_type.id() == ID_pointer &&
expr.type().id() == ID_pointer &&
(expr.id() == ID_plus || expr.id() == ID_minus))
{
bool non_const_offset = false;
Expand Down Expand Up @@ -879,10 +880,10 @@ void value_sett::get_value_set_rec(
statement==ID_cpp_new_array)
{
PRECONDITION(suffix.empty());
PRECONDITION(expr_type.id() == ID_pointer);
PRECONDITION(expr.type().id() == ID_pointer);

dynamic_object_exprt dynamic_object(
to_pointer_type(expr_type).base_type());
to_pointer_type(expr.type()).base_type());
dynamic_object.set_instance(location_number);
dynamic_object.valid()=true_exprt();

Expand All @@ -893,7 +894,10 @@ void value_sett::get_value_set_rec(
}
else if(expr.id()==ID_struct)
{
const auto &struct_components = to_struct_type(expr_type).components();
const auto &struct_components =
expr.type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(expr.type())).components()
: to_struct_type(expr.type()).components();
INVARIANT(
struct_components.size() == expr.operands().size(),
"struct expression should have an operand per component");
Expand Down Expand Up @@ -950,7 +954,9 @@ void value_sett::get_value_set_rec(

// If the suffix is empty we're looking for the whole struct:
// default to combining both options as below.
if(expr_type.id() == ID_struct && !suffix.empty())
if(
(expr.type().id() == ID_struct_tag || expr.type().id() == ID_struct) &&
!suffix.empty())
{
irep_idt component_name = with_expr.where().get(ID_component_name);
if(suffix_starts_with_field(suffix, id2string(component_name)))
Expand All @@ -966,7 +972,12 @@ void value_sett::get_value_set_rec(
original_type,
ns);
}
else if(to_struct_type(expr_type).has_component(component_name))
else if(
(expr.type().id() == ID_struct &&
to_struct_type(expr.type()).has_component(component_name)) ||
(expr.type().id() == ID_struct_tag &&
ns.follow_tag(to_struct_tag_type(expr.type()))
.has_component(component_name)))
{
// Looking for a non-overwritten member, look through this expression
get_value_set_rec(
Expand Down Expand Up @@ -998,7 +1009,7 @@ void value_sett::get_value_set_rec(
ns);
}
}
else if(expr_type.id() == ID_array && !suffix.empty())
else if(expr.type().id() == ID_array && !suffix.empty())
{
std::string new_value_suffix;
if(has_prefix(suffix, "[]"))
Expand Down Expand Up @@ -1105,8 +1116,9 @@ void value_sett::get_value_set_rec(

bool found=false;

const typet &op_type = ns.follow(byte_extract_expr.op().type());
if(op_type.id() == ID_struct)
if(
byte_extract_expr.op().type().id() == ID_struct ||
byte_extract_expr.op().type().id() == ID_struct_tag)
{
exprt offset = byte_extract_expr.offset();
if(eval_pointer_offset(offset, ns))
Expand All @@ -1115,7 +1127,10 @@ void value_sett::get_value_set_rec(
const auto offset_int = numeric_cast<mp_integer>(offset);
const auto type_size = pointer_offset_size(expr.type(), ns);

const struct_typet &struct_type = to_struct_type(op_type);
const struct_typet &struct_type =
byte_extract_expr.op().type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(byte_extract_expr.op().type()))
: to_struct_type(byte_extract_expr.op().type());

for(const auto &c : struct_type.components())
{
Expand Down Expand Up @@ -1150,10 +1165,17 @@ void value_sett::get_value_set_rec(
}
}

if(op_type.id() == ID_union)
if(
byte_extract_expr.op().type().id() == ID_union ||
byte_extract_expr.op().type().id() == ID_union_tag)
{
// just collect them all
for(const auto &c : to_union_type(op_type).components())
const auto &components =
byte_extract_expr.op().type().id() == ID_union_tag
? ns.follow_tag(to_union_tag_type(byte_extract_expr.op().type()))
.components()
: to_union_type(byte_extract_expr.op().type()).components();
for(const auto &c : components)
{
const irep_idt &name = c.get_name();
member_exprt member(byte_extract_expr.op(), name, c.type());
Expand Down Expand Up @@ -1429,13 +1451,13 @@ void value_sett::get_reference_set_rec(
// We cannot introduce a cast from scalar to non-scalar,
// thus, we can only adjust the types of structs and unions.

const typet &final_object_type = ns.follow(object.type());

if(final_object_type.id()==ID_struct ||
final_object_type.id()==ID_union)
if(
object.type().id() == ID_struct ||
object.type().id() == ID_struct_tag ||
tautschnig marked this conversation as resolved.
Show resolved Hide resolved
object.type().id() == ID_union || object.type().id() == ID_union_tag)
{
// adjust type?
if(ns.follow(struct_op.type())!=final_object_type)
if(struct_op.type() != object.type())
{
member_expr.compound() =
typecast_exprt(member_expr.compound(), struct_op.type());
Expand Down Expand Up @@ -1478,11 +1500,14 @@ void value_sett::assign(
output(std::cout);
#endif

const typet &type=ns.follow(lhs.type());

if(type.id() == ID_struct)
if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
{
for(const auto &c : to_struct_type(type).components())
const auto &components =
lhs.type().id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(lhs.type())).components()
: to_struct_type(lhs.type()).components();

for(const auto &c : components)
{
const typet &subtype = c.type();
const irep_idt &name = c.get_name();
Expand Down Expand Up @@ -1513,12 +1538,20 @@ void value_sett::assign(
"rhs.type():\n" +
rhs.type().pretty() + "\n" + "lhs.type():\n" + lhs.type().pretty());

const typet &followed = ns.follow(rhs.type());
if(rhs.type().id() == ID_struct_tag || rhs.type().id() == ID_union_tag)
{
const struct_union_typet &rhs_struct_union_type =
ns.follow_tag(to_struct_or_union_tag_type(rhs.type()));

const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);

if(followed.id() == ID_struct || followed.id() == ID_union)
assign(lhs_member, rhs_member, ns, true, add_to_sets);
}
else if(rhs.type().id() == ID_struct || rhs.type().id() == ID_union)
{
const struct_union_typet &rhs_struct_union_type =
to_struct_union_type(followed);
to_struct_union_type(rhs.type());

const typet &rhs_subtype = rhs_struct_union_type.component_type(name);
rhs_member = simplify_expr(member_exprt{rhs, name, rhs_subtype}, ns);
Expand All @@ -1528,30 +1561,30 @@ void value_sett::assign(
}
}
}
else if(type.id()==ID_array)
else if(lhs.type().id() == ID_array)
{
const index_exprt lhs_index(
lhs,
exprt(ID_unknown, c_index_type()),
to_array_type(type).element_type());
to_array_type(lhs.type()).element_type());

if(rhs.id()==ID_unknown ||
rhs.id()==ID_invalid)
{
assign(
lhs_index,
exprt(rhs.id(), to_array_type(type).element_type()),
exprt(rhs.id(), to_array_type(lhs.type()).element_type()),
ns,
is_simplified,
add_to_sets);
}
else
{
DATA_INVARIANT(
rhs.type() == type,
rhs.type() == lhs.type(),
"value_sett::assign types should match, got: "
"rhs.type():\n" +
rhs.type().pretty() + "\n" + "type:\n" + type.pretty());
rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());

if(rhs.id()==ID_array_of)
{
Expand All @@ -1575,7 +1608,7 @@ void value_sett::assign(
const index_exprt op0_index(
to_with_expr(rhs).old(),
exprt(ID_unknown, c_index_type()),
to_array_type(type).element_type());
to_array_type(lhs.type()).element_type());

assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
assign(
Expand All @@ -1586,7 +1619,7 @@ void value_sett::assign(
const index_exprt rhs_index(
rhs,
exprt(ID_unknown, c_index_type()),
to_array_type(type).element_type());
to_array_type(lhs.type()).element_type());
assign(lhs_index, rhs_index, ns, is_simplified, true);
}
}
Expand Down Expand Up @@ -1683,15 +1716,17 @@ void value_sett::assign_rec(
{
const auto &lhs_member_expr = to_member_expr(lhs);
const auto &component_name = lhs_member_expr.get_component_name();

const typet &type = ns.follow(lhs_member_expr.compound().type());
const exprt &compound = lhs_member_expr.compound();

DATA_INVARIANT(
type.id() == ID_struct || type.id() == ID_union,
compound.type().id() == ID_struct ||
compound.type().id() == ID_struct_tag ||
compound.type().id() == ID_union ||
compound.type().id() == ID_union_tag,
"operand 0 of member expression must be struct or union");

assign_rec(
lhs_member_expr.compound(),
compound,
values_rhs,
"." + id2string(component_name) + suffix,
ns,
Expand Down
31 changes: 21 additions & 10 deletions src/pointer-analysis/value_set_analysis_fi.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#include "value_set_analysis_fi.h"

#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/symbol_table_base.h>
Expand Down Expand Up @@ -91,23 +92,31 @@ void value_set_analysis_fit::get_entries_rec(
const typet &type,
std::list<value_set_fit::entryt> &dest)
{
const typet &t=ns.follow(type);

if(t.id()==ID_struct ||
t.id()==ID_union)
if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
{
const auto &components =
ns.follow_tag(to_struct_or_union_tag_type(type)).components();
for(const auto &c : components)
{
get_entries_rec(
identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
}
}
else if(type.id() == ID_struct || type.id() == ID_union)
{
for(const auto &c : to_struct_union_type(t).components())
const auto &components = to_struct_union_type(type).components();
for(const auto &c : components)
{
get_entries_rec(
identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
}
}
else if(t.id()==ID_array)
else if(type.id() == ID_array)
{
get_entries_rec(
identifier, suffix + "[]", to_array_type(t).element_type(), dest);
identifier, suffix + "[]", to_array_type(type).element_type(), dest);
}
else if(check_type(t))
else if(check_type(type))
{
dest.push_back(value_set_fit::entryt(identifier, suffix));
}
Expand Down Expand Up @@ -189,8 +198,10 @@ bool value_set_analysis_fit::check_type(const typet &type)
}
else if(type.id()==ID_array)
return check_type(to_array_type(type).element_type());
else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
return check_type(ns.follow(type));
else if(type.id() == ID_struct_tag)
return check_type(ns.follow_tag(to_struct_tag_type(type)));
else if(type.id() == ID_union_tag)
return check_type(ns.follow_tag(to_union_tag_type(type)));

return false;
}
Expand Down
9 changes: 6 additions & 3 deletions src/pointer-analysis/value_set_dereference.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -372,9 +372,12 @@ bool value_set_dereferencet::dereference_type_compare(
return true; // ok, they just match

// check for struct prefixes

const typet ot_base=ns.follow(object_type),
dt_base=ns.follow(dereference_type);
const typet &ot_base = object_type.id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(object_type))
: object_type;
const typet &dt_base = dereference_type.id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(dereference_type))
: dereference_type;

if(ot_base.id()==ID_struct &&
dt_base.id()==ID_struct)
Expand Down
Loading
Loading