Skip to content

Remove {f,F}orall_objects #5766

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

Merged
merged 1 commit into from
Jan 19, 2021
Merged

Remove {f,F}orall_objects #5766

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
2 changes: 0 additions & 2 deletions .clang-format
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,6 @@ ForEachMacros: [
'Forall_goto_functions',
'forall_goto_program_instructions',
'Forall_goto_program_instructions',
'forall_objects',
'Forall_objects',
'forall_valid_objects',
'Forall_valid_objects',
'forall_nodes',
Expand Down
138 changes: 72 additions & 66 deletions src/pointer-analysis/value_set_fi.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,16 +32,6 @@ numberingt<irep_idt> value_set_fit::function_numbering;

static const char *alloc_adapter_prefix="alloc_adaptor::";

#define forall_objects(it, map) \
for(object_map_dt::const_iterator it = (map).begin(); \
it!=(map).end(); \
(it)++)

#define Forall_objects(it, map) \
for(object_map_dt::iterator it = (map).begin(); \
it!=(map).end(); \
(it)++)

void value_set_fit::output(
const namespacet &ns,
std::ostream &out) const
Expand Down Expand Up @@ -81,7 +71,10 @@ void value_set_fit::output(

std::size_t width=0;

forall_objects(o_it, object_map.read())
const auto &entries = object_map.read();
for(object_map_dt::const_iterator o_it = entries.begin();
o_it != entries.end();
++o_it)
{
const exprt &o=object_numbering[o_it->first];

Expand Down Expand Up @@ -124,7 +117,7 @@ void value_set_fit::output(
object_map_dt::const_iterator next(o_it);
next++;

if(next!=object_map.read().end())
if(next != entries.end())
{
out << ", ";
if(width>=40)
Expand Down Expand Up @@ -168,9 +161,9 @@ void value_set_fit::flatten_rec(

seen.insert(identifier + e.suffix);

forall_objects(it, e.object_map.read())
for(const auto &object_entry : e.object_map.read())
{
const exprt &o=object_numbering[it->first];
const exprt &o = object_numbering[object_entry.first];

if(o.type().id()=="#REF#")
{
Expand All @@ -196,26 +189,26 @@ void value_set_fit::flatten_rec(
t_it!=temp.write().end();
t_it++)
{
if(t_it->second && it->second)
if(t_it->second && object_entry.second)
{
*t_it->second += *it->second;
*t_it->second += *object_entry.second;
}
else
t_it->second.reset();
}

forall_objects(oit, temp.read())
insert(dest, *oit);
for(const auto &object_entry : temp.read())
insert(dest, object_entry);
}
}
else
insert(dest, *it);
insert(dest, object_entry);
}

if(generalize_index) // this means we had recursive symbols in there
{
Forall_objects(it, dest.write())
it->second.reset();
for(auto &object_entry : dest.write())
object_entry.second.reset();
}

seen.erase(identifier + e.suffix);
Expand Down Expand Up @@ -284,9 +277,9 @@ bool value_set_fit::make_union(object_mapt &dest, const object_mapt &src) const
{
bool result=false;

forall_objects(it, src.read())
for(const auto &object_entry : src.read())
{
if(insert(dest, *it))
if(insert(dest, object_entry))
result=true;
}

Expand All @@ -301,9 +294,9 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const

object_mapt flat_map;

forall_objects(it, object_map.read())
for(const auto &object_entry : object_map.read())
{
const exprt &object=object_numbering[it->first];
const exprt &object = object_numbering[object_entry.first];
if(object.type().id()=="#REF#")
{
assert(object.id()==ID_symbol);
Expand All @@ -320,9 +313,9 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
t_it!=temp.write().end();
t_it++)
{
if(t_it->second && it->second)
if(t_it->second && object_entry.second)
{
*t_it->second += *it->second;
*t_it->second += *object_entry.second;
}
else
t_it->second.reset();
Expand All @@ -332,12 +325,12 @@ value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
}
}
else
flat_map.write()[it->first]=it->second;
flat_map.write()[object_entry.first] = object_entry.second;
}

std::vector<exprt> result;
forall_objects(fit, flat_map.read())
result.push_back(to_expr(*fit));
for(const auto &object_entry : flat_map.read())
result.push_back(to_expr(object_entry));

#if 0
// Sanity check!
Expand Down Expand Up @@ -388,9 +381,16 @@ void value_set_fit::get_value_set_rec(

if(fi!=values.end())
{
forall_objects(it, fi->second.object_map.read())
get_value_set_rec(object_numbering[it->first], dest, suffix,
original_type, ns, recursion_set);
for(const auto &object_entry : fi->second.object_map.read())
{
get_value_set_rec(
object_numbering[object_entry.first],
dest,
suffix,
original_type,
ns,
recursion_set);
}
return;
}
else
Expand Down Expand Up @@ -502,9 +502,9 @@ void value_set_fit::get_value_set_rec(

if(object_map.begin()!=object_map.end())
{
forall_objects(it1, object_map)
for(const auto &object_entry : object_map)
{
const exprt &object=object_numbering[it1->first];
const exprt &object = object_numbering[object_entry.first];
get_value_set_rec(object, dest, suffix,
original_type, ns, recursion_set);
}
Expand Down Expand Up @@ -560,9 +560,9 @@ void value_set_fit::get_value_set_rec(
get_value_set_rec(*ptr_operand, pointer_expr_set, "",
ptr_operand->type(), ns, recursion_set);

forall_objects(it, pointer_expr_set.read())
for(const auto &object_entry : pointer_expr_set.read())
{
offsett offset = it->second;
offsett offset = object_entry.second;

if(offset_is_zero(offset) && expr.operands().size() == 2)
{
Expand All @@ -586,7 +586,7 @@ void value_set_fit::get_value_set_rec(
else
offset.reset();

insert(dest, it->first, offset);
insert(dest, object_entry.first, offset);
}

return;
Expand Down Expand Up @@ -699,9 +699,9 @@ void value_set_fit::get_reference_set(
object_mapt object_map;
get_reference_set_sharing(expr, object_map, ns);

forall_objects(it, object_map.read())
for(const auto &object_entry : object_map.read())
{
const exprt &object = object_numbering[it->first];
const exprt &object = object_numbering[object_entry.first];

if(object.type().id() == "#REF#")
{
Expand All @@ -722,9 +722,9 @@ void value_set_fit::get_reference_set(
t_it!=omt.write().end();
t_it++)
{
if(t_it->second && it->second)
if(t_it->second && object_entry.second)
{
*t_it->second += *it->second;
*t_it->second += *object_entry.second;
}
else
t_it->second.reset();
Expand All @@ -735,7 +735,7 @@ void value_set_fit::get_reference_set(
}
}
else
dest.insert(to_expr(*it));
dest.insert(to_expr(object_entry));
}
}

Expand All @@ -747,8 +747,8 @@ void value_set_fit::get_reference_set_sharing(
object_mapt object_map;
get_reference_set_sharing(expr, object_map, ns);

forall_objects(it, object_map.read())
dest.insert(to_expr(*it));
for(const auto &object_entry : object_map.read())
dest.insert(to_expr(object_entry));
}

void value_set_fit::get_reference_set_sharing_rec(
Expand All @@ -766,8 +766,11 @@ void value_set_fit::get_reference_set_sharing_rec(
valuest::const_iterator fi = values.find(expr.get(ID_identifier));
if(fi!=values.end())
{
forall_objects(it, fi->second.object_map.read())
get_reference_set_sharing_rec(object_numbering[it->first], dest, ns);
for(const auto &object_entry : fi->second.object_map.read())
{
get_reference_set_sharing_rec(
object_numbering[object_entry.first], dest, ns);
}
return;
}
}
Expand Down Expand Up @@ -796,9 +799,9 @@ void value_set_fit::get_reference_set_sharing_rec(
recset);

// REF's need to be dereferenced manually!
forall_objects(it, temp.read())
for(const auto &object_entry : temp.read())
{
const exprt &obj = object_numbering[it->first];
const exprt &obj = object_numbering[object_entry.first];
if(obj.type().id()=="#REF#")
{
const irep_idt &ident = obj.get(ID_identifier);
Expand All @@ -813,22 +816,22 @@ void value_set_fit::get_reference_set_sharing_rec(
t_it!=t2.write().end();
t_it++)
{
if(t_it->second && it->second)
if(t_it->second && object_entry.second)
{
*t_it->second += *it->second;
*t_it->second += *object_entry.second;
}
else
t_it->second.reset();
}

forall_objects(it2, t2.read())
insert(dest, *it2);
for(const auto &t2_object_entry : t2.read())
insert(dest, t2_object_entry);
}
else
insert(dest, exprt(ID_unknown, obj.type().subtype()));
}
else
insert(dest, *it);
insert(dest, object_entry);
}

#if 0
Expand All @@ -854,9 +857,9 @@ void value_set_fit::get_reference_set_sharing_rec(

const object_map_dt &object_map=array_references.read();

forall_objects(a_it, object_map)
for(const auto &object_entry : object_map)
{
const exprt &object=object_numbering[a_it->first];
const exprt &object = object_numbering[object_entry.first];

if(object.id()==ID_unknown)
insert(dest, exprt(ID_unknown, expr.type()));
Expand All @@ -873,7 +876,7 @@ void value_set_fit::get_reference_set_sharing_rec(
else
casted_index = index_expr;

offsett o = a_it->second;
offsett o = object_entry.second;
const auto i = numeric_cast<mp_integer>(offset);

if(offset.is_zero())
Expand All @@ -899,9 +902,9 @@ void value_set_fit::get_reference_set_sharing_rec(
object_mapt struct_references;
get_reference_set_sharing(struct_op, struct_references, ns);

forall_objects(it, struct_references.read())
for(const auto &object_entry : struct_references.read())
{
const exprt &object=object_numbering[it->first];
const exprt &object = object_numbering[object_entry.first];
const typet &obj_type = object.type();

if(object.id()==ID_unknown)
Expand All @@ -917,7 +920,7 @@ void value_set_fit::get_reference_set_sharing_rec(
}
else
{
offsett o = it->second;
offsett o = object_entry.second;

member_exprt member_expr(object, component_name, expr.type());

Expand Down Expand Up @@ -1127,10 +1130,13 @@ void value_set_fit::assign_rec(
{
recursion_set.insert(ident);

forall_objects(it, temp.read())
if(object_numbering[it->first].id()!=ID_unknown)
assign_rec(object_numbering[it->first], values_rhs,
suffix, ns, recursion_set);
for(const auto &object_entry : temp.read())
{
const exprt &object = object_numbering[object_entry.first];

if(object.id() != ID_unknown)
assign_rec(object, values_rhs, suffix, ns, recursion_set);
}

recursion_set.erase(ident);
}
Expand Down Expand Up @@ -1172,9 +1178,9 @@ void value_set_fit::assign_rec(
object_mapt reference_set;
get_reference_set_sharing(lhs, reference_set, ns);

forall_objects(it, reference_set.read())
for(const auto &object_entry : reference_set.read())
{
const exprt &object=object_numbering[it->first];
const exprt &object = object_numbering[object_entry.first];

if(object.id()!=ID_unknown)
assign_rec(object, values_rhs, suffix, ns, recursion_set);
Expand Down