Skip to content

Add CoW base to value-set #3053

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

Closed
wants to merge 4 commits into from
Closed

Add CoW base to value-set #3053

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
48e1e6c
Value set: indirect values.find operations via a helper function
smowton Sep 26, 2018
7b5d5e5
Remove unused value_sett::do_free
smowton Sep 26, 2018
ca2a7b3
Value-set: add support for a base value-set
smowton Sep 26, 2018
e8015b8
Add unit test to check value-set behaviour in the presence of constants
smowton Apr 18, 2018
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
155 changes: 51 additions & 104 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,16 @@ bool value_sett::field_sensitive(
return ns.follow(type).id()==ID_struct;
}

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

value_sett::entryt &value_sett::get_entry(
const entryt &e,
const typet &type,
Expand All @@ -66,6 +76,14 @@ value_sett::entryt &value_sett::get_entry(
std::pair<valuest::iterator, bool> r=
values.insert(std::pair<idt, entryt>(index, e));

if(base_value_set && r.second)
{
// New entry; copy the existing base entry if found.
const entryt *base_entry = base_value_set->find_entry(index);
if(base_entry)
r.first->second = *base_entry;
}

return r.first->second;
}

Expand Down Expand Up @@ -181,6 +199,12 @@ void value_sett::output(

out << " } \n";
}

if(base_value_set)
{
out << "NB. the base value-set (" << base_value_set << ") has a further "
<< base_value_set->size() << " entries\n";
}
}

exprt value_sett::to_expr(const object_map_dt::value_type &it) const
Expand All @@ -205,6 +229,10 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const

bool value_sett::make_union(const value_sett::valuest &new_values)
{
// Note this method makes no reference to base_value_set -- we assume that
// we share the same base, if any, with new_values. This is enforced in the
// make_union(const value_sett &) overload.

bool result=false;

valuest::iterator v_it=values.begin();
Expand Down Expand Up @@ -429,31 +457,29 @@ void value_sett::get_value_set_rec(
expr_type.id()==ID_array)
{
// look it up
valuest::const_iterator v_it=
values.find(id2string(identifier)+suffix);
const entryt *entry =
find_entry(id2string(identifier) + suffix);

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

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

v_it = values.find(
entry = find_entry(
id2string(identifier) + "." + id2string(first_component_name) +
suffix);
}

// not found? try without suffix
if(v_it==values.end())
v_it=values.find(identifier);
if(!entry)
entry = find_entry(identifier);

if(v_it!=values.end())
make_union(dest, v_it->second.object_map);
if(entry)
make_union(dest, entry->object_map);
else
insert(dest, exprt(ID_unknown, original_type));
}
Expand Down Expand Up @@ -857,16 +883,16 @@ void value_sett::get_value_set_rec(
const std::string full_name=prefix+suffix;

// look it up
valuest::const_iterator v_it=values.find(full_name);
const entryt *entry = find_entry(full_name);

// not found? try without suffix
if(v_it==values.end())
v_it=values.find(prefix);
if(!entry)
entry = find_entry(prefix);

if(v_it==values.end())
if(!entry)
insert(dest, exprt(ID_unknown, original_type));
else
make_union(dest, v_it->second.object_map);
make_union(dest, entry->object_map);
}
else if(expr.id()==ID_byte_extract_little_endian ||
expr.id()==ID_byte_extract_big_endian)
Expand Down Expand Up @@ -1267,86 +1293,6 @@ void value_sett::assign(
}
}

void value_sett::do_free(
const exprt &op,
const namespacet &ns)
{
// op must be a pointer
if(op.type().id()!=ID_pointer)
throw "free expected to have pointer-type operand";

// find out what it points to
object_mapt value_set;
get_value_set(op, value_set, ns, false);

const object_map_dt &object_map=value_set.read();

// find out which *instances* interest us
dynamic_object_id_sett to_mark;

for(object_map_dt::const_iterator
it=object_map.begin();
it!=object_map.end();
it++)
{
const exprt &object=object_numbering[it->first];

if(object.id()==ID_dynamic_object)
{
const dynamic_object_exprt &dynamic_object=
to_dynamic_object_expr(object);

if(dynamic_object.valid().is_true())
to_mark.insert(dynamic_object.get_instance());
}
}

// mark these as 'may be invalid'
// this, unfortunately, destroys the sharing
for(valuest::iterator v_it=values.begin();
v_it!=values.end();
v_it++)
{
object_mapt new_object_map;

const object_map_dt &old_object_map=
v_it->second.object_map.read();

bool changed=false;

for(object_map_dt::const_iterator
o_it=old_object_map.begin();
o_it!=old_object_map.end();
o_it++)
{
const exprt &object=object_numbering[o_it->first];

if(object.id()==ID_dynamic_object)
{
const dynamic_object_exprt &dynamic_object=
to_dynamic_object_expr(object);

if(to_mark.count(dynamic_object.get_instance())==0)
set(new_object_map, *o_it);
else
{
// adjust
offsett o = o_it->second;
exprt tmp(object);
to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
insert(new_object_map, tmp, o);
changed=true;
}
}
else
set(new_object_map, *o_it);
}

if(changed)
v_it->second.object_map=new_object_map;
}
}

void value_sett::assign_rec(
const exprt &lhs,
const object_mapt &values_rhs,
Expand Down Expand Up @@ -1603,15 +1549,6 @@ void value_sett::apply_code_rec(
{
// does nothing
}
else if(statement==ID_free)
{
// this may kill a valid bit

if(code.operands().size()!=1)
throw "free expected to have one operand";

do_free(code.op0(), ns);
}
else if(statement=="lock" || statement=="unlock")
{
// ignore for now
Expand Down Expand Up @@ -1750,3 +1687,13 @@ exprt value_sett::make_member(

return member_expr;
}

void value_sett::set_base_value_set(const value_sett *base)
{
// Simplifying assumptions -- this way we don't need to check for clashing
// keys, for example:
INVARIANT(size() == 0, "base_value_set cannot be set for a non-empty set");
INVARIANT(!base_value_set, "base_value_set cannot be reset");

base_value_set = base;
}
45 changes: 37 additions & 8 deletions src/pointer-analysis/value_set.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,10 +38,21 @@ class namespacet;
/// pairs of an `exprt` and an optional offset if known (0 for both dynamic
/// objects in the example given above). RHS expressions are represented using
/// numbering to avoid storing redundant duplicate expressions.
///
/// A value_sett may have a base (stored in field base_value_set), in which case
/// any lookup that fails in this value-set will check the base, and any write
/// to this value-set will copy any entry in the base into this value-set before
/// performing the write (i.e. we act as a copy-on-write layer on top of the
/// base). This makes copying or union'ing value-sets with a common base
/// cheaper -- the intended use case is for faster local analysis on top of a
/// large, expensive-to-copy global context. value_sett::make_union requires
/// that the value-sets being merged have the same base (or both have no base);
/// it is up to the user to make sure this is true.

class value_sett
{
public:
value_sett():location_number(0)
value_sett():location_number(0), base_value_set(nullptr)
{
}

Expand Down Expand Up @@ -317,6 +328,15 @@ class value_sett
values.clear();
}

/// Finds an entry in this value-set. The interface differs from get_entry
/// because get_value_set_rec wants to check for a struct's first component
/// before stripping the suffix as is done in get_entry.
/// \param id: identifier to find.
/// \return a constant pointer to an entry if found, or null otherwise.
/// Note the pointer may be invalidated by insert operations, including
/// get_entry.
const entryt *find_entry(const idt &id) const;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Would optionalt be a possibility?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Personal preference: T * not optionalt<reference_wrapper<T>>

Copy link
Contributor

Choose a reason for hiding this comment

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

What about optionalt<T *>? It would more clearly express the intent and remove the role of nullptr as a sentinel value that can accidentally be dereferenced.


/// Gets or inserts an entry in this value-set.
/// \param e: entry to find. Its `id` and `suffix` fields will be used
/// to find a corresponding entry; if a fresh entry is created its
Expand All @@ -331,6 +351,12 @@ class value_sett
const entryt &e, const typet &type,
const namespacet &ns);

/// Gets the number of entries in this value-set.
valuest::size_type size() const
{
return values.size();
}

/// Pretty-print this value-set
/// \param ns: global namespace
/// \param [out] out: stream to write to
Expand All @@ -357,6 +383,9 @@ class value_sett
/// \return true if anything changed.
bool make_union(const value_sett &new_values)
{
INVARIANT(
new_values.base_value_set == base_value_set,
"Unioned value-sets must have the same base");
return make_union(new_values.values);
}

Expand Down Expand Up @@ -450,6 +479,11 @@ class value_sett
exprt &expr,
const namespacet &ns) const;

/// Set the base value-set, to which failing queries fall through. Note for
/// simplicity's sake, at the moment this value-set must be empty when this
/// is called, and the base value-set cannot be reset later.
void set_base_value_set(const value_sett *base);

protected:
/// Reads the set of objects pointed to by `expr`, including making
/// recursive lookups for dereference operations etc.
Expand Down Expand Up @@ -484,13 +518,6 @@ class value_sett
const exprt &src,
exprt &dest) const;

/// Marks objects that may be pointed to by `op` as maybe-invalid
/// \param op: pointer to invalidate
/// \param ns: global namespace
void do_free(
const exprt &op,
const namespacet &ns);

/// Extracts a member from a struct- or union-typed expression.
/// Usually that means making a `member_exprt`, but this can shortcut
/// extracting members from constants or with-expressions.
Expand Down Expand Up @@ -548,6 +575,8 @@ class value_sett
const namespacet &)
{
}

const value_sett *base_value_set;
};

#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H
Loading