Skip to content

Use sharing_mapt as container in value_sett #4463

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
Apr 3, 2019
Merged

Use sharing_mapt as container in value_sett #4463

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
8 changes: 4 additions & 4 deletions src/goto-symex/symex_main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -676,16 +676,16 @@ void goto_symext::try_filter_value_sets(
}
if(jump_taken_value_set && !erase_from_jump_taken_value_set.empty())
{
value_sett::entryt *entry = jump_taken_value_set->get_entry_for_symbol(
auto entry_index = jump_taken_value_set->get_index_of_symbol(
symbol_expr->get_identifier(), symbol_type, "", ns);
jump_taken_value_set->erase_values_from_entry(
*entry, erase_from_jump_taken_value_set);
*entry_index, erase_from_jump_taken_value_set);
}
if(jump_not_taken_value_set && !erase_from_jump_not_taken_value_set.empty())
{
value_sett::entryt *entry = jump_not_taken_value_set->get_entry_for_symbol(
auto entry_index = jump_not_taken_value_set->get_index_of_symbol(
symbol_expr->get_identifier(), symbol_type, "", ns);
jump_not_taken_value_set->erase_values_from_entry(
*entry, erase_from_jump_not_taken_value_set);
*entry_index, erase_from_jump_not_taken_value_set);
}
}
179 changes: 84 additions & 95 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,19 +48,17 @@ bool value_sett::field_sensitive(const irep_idt &id, const typet &type)
return type.id() == ID_struct || type.id() == ID_struct_tag;
}

value_sett::entryt *value_sett::find_entry(const irep_idt &id)
{
auto found = values.find(id);
return found == values.end() ? nullptr : &found->second;
}

const value_sett::entryt *value_sett::find_entry(const irep_idt &id) const
{
auto found = values.find(id);
return found == values.end() ? nullptr : &found->second;
return !found.has_value() ? nullptr : &(found->get());
}

value_sett::entryt &value_sett::get_entry(const entryt &e, const typet &type)
void value_sett::update_entry(
const entryt &e,
const typet &type,
const object_mapt &new_values,
bool add_to_sets)
{
irep_idt index;

Expand All @@ -69,10 +67,27 @@ value_sett::entryt &value_sett::get_entry(const entryt &e, const typet &type)
else
index=e.identifier;

std::pair<valuest::iterator, bool> r =
values.insert(std::pair<irep_idt, entryt>(index, e));

return r.first->second;
auto existing_entry = values.find(index);
if(existing_entry.has_value())
{
entryt replacement = *existing_entry;
if(add_to_sets)
{
if(make_union(replacement.object_map, new_values))
values.replace(index, std::move(replacement));
}
else
{
replacement.object_map = new_values;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could check whether new_values.read() != existing_entry->object_map.read() before doing the replacement. Not sure about the impact on performance though. We might avoid breaking sharing in some cases but there'd be additional cost for the comparisons.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think there's a risk this is way too expensive and thus I'd rather not add this change.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah that's ok, we'd probably have to specifically benchmark this. My hunch is that the map comparisons could be cheap on average if it's likely that they differ in size or that we find a mismatch quickly.

values.replace(index, std::move(replacement));
}
}
else
{
entryt new_entry = e;
new_entry.object_map = new_values;
values.insert(index, std::move(new_entry));
}
}

bool value_sett::insert(
Expand Down Expand Up @@ -103,7 +118,10 @@ void value_sett::output(
const namespacet &ns,
std::ostream &out) const
{
for(const auto &values_entry : values)
valuest::viewt view;
values.get_view(view);

for(const auto &values_entry : view)
{
irep_idt identifier, display_name;

Expand Down Expand Up @@ -210,36 +228,26 @@ bool value_sett::make_union(const value_sett::valuest &new_values)
{
bool result=false;

valuest::iterator v_it=values.begin();
value_sett::valuest::delta_viewt delta_view;

new_values.get_delta_view(values, delta_view, false);

for(valuest::const_iterator
it=new_values.begin();
it!=new_values.end();
) // no it++
for(const auto &delta_entry : delta_view)
{
if(v_it==values.end() || it->first<v_it->first)
if(delta_entry.in_both)
{
values.insert(v_it, *it);
result=true;
it++;
continue;
entryt merged_entry = *values.find(delta_entry.k);
if(make_union(merged_entry.object_map, delta_entry.m.object_map))
{
values.replace(delta_entry.k, std::move(merged_entry));
result = true;
}
}
else if(v_it->first<it->first)
else
{
v_it++;
continue;
values.insert(delta_entry.k, delta_entry.m);
result = true;
}

assert(v_it->first==it->first);

entryt &e=v_it->second;
const entryt &new_e=it->second;

if(make_union(e.object_map, new_e.object_map))
result=true;

v_it++;
it++;
}

return result;
Expand Down Expand Up @@ -371,77 +379,55 @@ static std::string strip_first_field_from_suffix(
return suffix.substr(field.length() + 1);
}

template <class maybe_const_value_sett>
auto value_sett::get_entry_for_symbol(
maybe_const_value_sett &value_set,
const irep_idt identifier,
optionalt<irep_idt> value_sett::get_index_of_symbol(
irep_idt identifier,
const typet &type,
const std::string &suffix,
const namespacet &ns) ->
typename std::conditional<std::is_const<maybe_const_value_sett>::value,
const value_sett::entryt *,
value_sett::entryt *>::type
const namespacet &ns) const
{
if(
type.id() != ID_pointer && type.id() != ID_signedbv &&
type.id() != ID_unsignedbv && type.id() != ID_array &&
type.id() != ID_struct && type.id() != ID_struct_tag &&
type.id() != ID_union && type.id() != ID_union_tag)
{
return nullptr;
return {};
}

// look it up
irep_idt index = id2string(identifier) + suffix;
auto *entry = find_entry(index);
if(entry)
return std::move(index);

const typet &followed_type = type.id() == ID_struct_tag
? ns.follow_tag(to_struct_tag_type(type))
: type.id() == ID_union_tag
? ns.follow_tag(to_union_tag_type(type))
: type;

// look it up
auto *entry = value_set.find_entry(id2string(identifier) + suffix);

// try first component name as suffix if not yet found
if(
!entry &&
(followed_type.id() == ID_struct || followed_type.id() == ID_union))
if(followed_type.id() == ID_struct || followed_type.id() == ID_union)
{
const struct_union_typet &struct_union_type =
to_struct_union_type(followed_type);

const irep_idt &first_component_name =
struct_union_type.components().front().get_name();

entry = value_set.find_entry(
id2string(identifier) + "." + id2string(first_component_name) + suffix);
}

if(!entry)
{
// not found? try without suffix
entry = value_set.find_entry(identifier);
index =
id2string(identifier) + "." + id2string(first_component_name) + suffix;
entry = find_entry(index);
if(entry)
return std::move(index);
}

return entry;
}

// Explicitly instantiate the two possible versions of the method above:

value_sett::entryt *value_sett::get_entry_for_symbol(
irep_idt identifier,
const typet &type,
const std::string &suffix,
const namespacet &ns)
{
return get_entry_for_symbol(*this, identifier, type, suffix, ns);
}
// not found? try without suffix
entry = find_entry(identifier);
if(entry)
return std::move(identifier);

const value_sett::entryt *value_sett::get_entry_for_symbol(
irep_idt identifier,
const typet &type,
const std::string &suffix,
const namespacet &ns) const
{
return get_entry_for_symbol(*this, identifier, type, suffix, ns);
return {};
}

void value_sett::get_value_set_rec(
Expand Down Expand Up @@ -491,11 +477,11 @@ void value_sett::get_value_set_rec(
}
else if(expr.id()==ID_symbol)
{
const entryt *entry = get_entry_for_symbol(
auto entry_index = get_index_of_symbol(
to_symbol_expr(expr).get_identifier(), expr_type, suffix, ns);

if(entry)
make_union(dest, entry->object_map);
if(entry_index.has_value())
make_union(dest, find_entry(*entry_index)->object_map);
else
insert(dest, exprt(ID_unknown, original_type));
}
Expand Down Expand Up @@ -1314,12 +1300,8 @@ void value_sett::assign_rec(
{
const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();

entryt &e = get_entry(entryt(identifier, suffix), lhs.type());

if(add_to_sets)
make_union(e.object_map, values_rhs);
else
e.object_map=values_rhs;
update_entry(
entryt{identifier, suffix}, lhs.type(), values_rhs, add_to_sets);
}
else if(lhs.id()==ID_dynamic_object)
{
Expand All @@ -1330,9 +1312,7 @@ void value_sett::assign_rec(
"value_set::dynamic_object"+
std::to_string(dynamic_object.get_instance());

entryt &e = get_entry(entryt(name, suffix), lhs.type());

make_union(e.object_map, values_rhs);
update_entry(entryt{name, suffix}, lhs.type(), values_rhs, true);
}
else if(lhs.id()==ID_dereference)
{
Expand Down Expand Up @@ -1640,12 +1620,19 @@ void value_sett::guard(
}

void value_sett::erase_values_from_entry(
entryt &entry,
const irep_idt &index,
const std::unordered_set<exprt, irep_hash> &values_to_erase)
{
if(values_to_erase.empty())
return;

auto entry = find_entry(index);
if(!entry)
return;

std::vector<object_map_dt::key_type> keys_to_erase;

for(auto &key_value : entry.object_map.read())
for(auto &key_value : entry->object_map.read())
{
const auto &rhs_object = to_expr(key_value);
if(values_to_erase.count(rhs_object))
Expand All @@ -1659,8 +1646,10 @@ void value_sett::erase_values_from_entry(
"value_sett::erase_value_from_entry() should erase exactly one value for "
"each element in the set it is given");

entryt replacement = *entry;
for(const auto &key_to_erase : keys_to_erase)
{
entry.object_map.write().erase(key_to_erase);
replacement.object_map.write().erase(key_to_erase);
}
values.replace(index, std::move(replacement));
}
Loading