Skip to content

Replace objectt with optional<mp_integer> #1629

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 4 commits into from
Nov 30, 2017
Merged

Replace objectt with optional<mp_integer> #1629

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
1a51d67
Replace objectt with optional<mp_integer>
Nov 27, 2017
5ecee62
Replace objectt in value_set_fi.*
Nov 29, 2017
cc8495a
Replace objectt in value_set_fivr.*
Nov 29, 2017
c543892
Replace objectt in value_set_fivrns.*
Nov 29, 2017
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
54 changes: 26 additions & 28 deletions src/pointer-analysis/value_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,24 +75,23 @@ value_sett::entryt &value_sett::get_entry(
bool value_sett::insert(
object_mapt &dest,
object_numberingt::number_type n,
const objectt &object) const
const offsett &offset) const
{
auto entry=dest.read().find(n);

if(entry==dest.read().end())
{
// new
dest.write()[n]=object;
dest.write()[n] = offset;
return true;
}
else if(!entry->second.offset_is_set)
else if(!entry->second)
return false; // no change
else if(object.offset_is_set &&
entry->second.offset==object.offset)
else if(offset && *entry->second == *offset)
return false; // no change
else
{
dest.write()[n].offset_is_set=false;
dest.write()[n].reset();
return true;
}
}
Expand Down Expand Up @@ -155,8 +154,8 @@ void value_sett::output(
{
result="<"+from_expr(ns, identifier, o)+", ";

if(o_it->second.offset_is_set)
result+=integer2string(o_it->second.offset)+"";
if(o_it->second)
result += integer2string(*o_it->second) + "";
else
result+='*';

Expand Down Expand Up @@ -199,8 +198,8 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const

od.object()=object;

if(it.second.offset_is_set)
od.offset()=from_integer(it.second.offset, index_type());
if(it.second)
od.offset() = from_integer(*it.second, index_type());

od.type()=od.object().type();

Expand Down Expand Up @@ -282,7 +281,7 @@ bool value_sett::eval_pointer_offset(
it=object_map.begin();
it!=object_map.end();
it++)
if(!it->second.offset_is_set)
if(!it->second)
return false;
else
{
Expand All @@ -292,7 +291,7 @@ bool value_sett::eval_pointer_offset(
if(ptr_offset<0)
return false;

ptr_offset+=it->second.offset;
ptr_offset += *it->second;

if(mod && ptr_offset!=previous_offset)
return false;
Expand Down Expand Up @@ -635,15 +634,15 @@ void value_sett::get_value_set_rec(
it!=pointer_expr_set.read().end();
it++)
{
objectt object=it->second;
offsett offset = it->second;

// adjust by offset
if(object.offset_is_set && i_is_set)
object.offset+=i;
if(offset && i_is_set)
*offset += i;
else
object.offset_is_set=false;
offset.reset();

insert(dest, it->first, object);
insert(dest, it->first, offset);
}
}
else if(expr.id()==ID_mult)
Expand All @@ -668,12 +667,12 @@ void value_sett::get_value_set_rec(
it!=pointer_expr_set.read().end();
it++)
{
objectt object=it->second;
offsett offset = it->second;

// kill any offset
object.offset_is_set=false;
offset.reset();

insert(dest, it->first, object);
insert(dest, it->first, offset);
}
}
else if(expr.id()==ID_side_effect)
Expand Down Expand Up @@ -1002,24 +1001,23 @@ void value_sett::get_reference_set_rec(
if(ns.follow(object.type())!=array_type)
index_expr.make_typecast(array.type());

objectt o=a_it->second;
offsett o = a_it->second;
mp_integer i;

if(offset.is_zero())
{
}
else if(!to_integer(offset, i) &&
o.offset_is_set)
else if(!to_integer(offset, i) && o)
{
mp_integer size=pointer_offset_size(array_type.subtype(), ns);

if(size<=0)
o.offset_is_set=false;
o.reset();
else
o.offset=i*size;
*o = i * size;
}
else
o.offset_is_set=false;
o.reset();

insert(dest, index_expr, o);
}
Expand Down Expand Up @@ -1052,7 +1050,7 @@ void value_sett::get_reference_set_rec(
insert(dest, exprt(ID_unknown, expr.type()));
else
{
objectt o=it->second;
offsett o = it->second;

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

Expand Down Expand Up @@ -1282,7 +1280,7 @@ void value_sett::do_free(
else
{
// adjust
objectt o=o_it->second;
offsett o = o_it->second;
exprt tmp(object);
to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
insert(new_object_map, tmp, o);
Expand Down
76 changes: 27 additions & 49 deletions src/pointer-analysis/value_set.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,54 +61,23 @@ class value_sett
typedef irep_idt idt;

/// Represents the offset into an object: either a unique integer offset,
/// or an unknown value, represented by `!offset_is_set`.
class objectt
/// or an unknown value, represented by `!offset`.
typedef optionalt<mp_integer> offsett;
bool offset_is_zero(const offsett &offset) const
{
public:
/// Constructs an unknown offset
objectt():offset_is_set(false)
{
}

/// Constructs a known offset
explicit objectt(const mp_integer &_offset):
offset(_offset),
offset_is_set(true)
{
}

/// Offset into the target object. Ignored if `offset_is_set` is false.
mp_integer offset;

/// If true, `offset` gives a unique integer offset; if false, represents
/// an unknown offset.
bool offset_is_set;

bool offset_is_zero() const
{ return offset_is_set && offset.is_zero(); }

bool operator==(const objectt &other) const
{
return
offset_is_set==other.offset_is_set &&
(!offset_is_set || offset==other.offset);
}
bool operator!=(const objectt &other) const
{
return !(*this==other);
}
};
return offset && offset->is_zero();
}

/// Represents a set of expressions (`exprt` instances) with corresponding
/// offsets (`objectt` instances). This is the RHS set of a single row of
/// offsets (`offsett` instances). This is the RHS set of a single row of
/// the enclosing `value_sett`, such as `{ null, dynamic_object1 }`.
/// The set is represented as a map from numbered `exprt`s to `objectt`
/// The set is represented as a map from numbered `exprt`s to `offsett`
/// instead of a set of pairs to make lookup by `exprt` easier. All
/// methods matching the interface of `std::map` forward those methods
/// to the internal map.
class object_map_dt
{
typedef std::map<object_numberingt::number_type, objectt> data_typet;
typedef std::map<object_numberingt::number_type, offsett> data_typet;
data_typet data;

public:
Expand All @@ -135,9 +104,18 @@ class value_sett
void erase(key_type i) { data.erase(i); }
void erase(const_iterator it) { data.erase(it); }

objectt &operator[](key_type i) { return data[i]; }
objectt &at(key_type i) { return data.at(i); }
const objectt &at(key_type i) const { return data.at(i); }
offsett &operator[](key_type i)
{
return data[i];
}
offsett &at(key_type i)
{
return data.at(i);
}
const offsett &at(key_type i) const
{
return data.at(i);
}

template <typename It>
void insert(It b, It e) { data.insert(b, e); }
Expand Down Expand Up @@ -210,21 +188,21 @@ class value_sett
/// \param src: expression to add
bool insert(object_mapt &dest, const exprt &src) const
{
return insert(dest, object_numbering.number(src), objectt());
return insert(dest, object_numbering.number(src), offsett());
}

/// Adds an expression to an object map, with known offset. If the
/// destination map has an existing entry for the same expression
/// with a differing offset its offset is marked unknown.
/// \param dest: object map to update
/// \param src: expression to add
/// \param offset: offset into `src`
/// \param offset_value: offset into `src`
bool insert(
object_mapt &dest,
const exprt &src,
const mp_integer &offset) const
const mp_integer &offset_value) const
{
return insert(dest, object_numbering.number(src), objectt(offset));
return insert(dest, object_numbering.number(src), offsett(offset_value));
}

/// Adds a numbered expression and offset to an object map. If the
Expand All @@ -237,17 +215,17 @@ class value_sett
bool insert(
object_mapt &dest,
object_numberingt::number_type n,
const objectt &object) const;
const offsett &offset) const;

/// Adds an expression and offset to an object map. If the
/// destination map has an existing entry for the same expression
/// with a differing offset its offset is marked unknown.
/// \param dest: object map to update
/// \param expr: expression to add
/// \param object: offset into `expr` (may be unknown).
bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
{
return insert(dest, object_numbering.number(expr), object);
return insert(dest, object_numbering.number(expr), offset);
}

/// Represents a row of a `value_sett`. For example, this might represent
Expand Down
Loading