cprover
|
#include <abstract_object.h>
Classes | |
struct | abstract_object_visitort |
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstract_object_pointert. More... | |
Public Types | |
typedef std::set< goto_programt::const_targett > | locationst |
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | shared_mapt |
Public Member Functions | |
abstract_objectt (const typet &type) | |
abstract_objectt (const typet &type, bool top, bool bottom) | |
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More... | |
abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
Construct an abstract object from the expression. More... | |
abstract_objectt (const typet &type, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
Ctor for building object of types that differ from the types of input expressions. More... | |
virtual | ~abstract_objectt () |
virtual const typet & | type () const |
Get the real type of the variable this abstract object is representing. More... | |
virtual bool | is_top () const |
Find out if the abstract object is top. More... | |
virtual bool | is_bottom () const |
Find out if the abstract object is bottom. More... | |
virtual bool | verify () const |
Verify the internal structure of an abstract_object is correct. More... | |
virtual void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const |
virtual abstract_object_pointert | expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const |
Interface for transforms. More... | |
virtual exprt | to_constant () const |
Converts to a constant expression if possible. More... | |
virtual abstract_object_pointert | write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const |
A helper function to evaluate writing to a component of an abstract object. More... | |
virtual void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const |
Print the value of the abstract object. More... | |
virtual bool | has_been_modified (const abstract_object_pointert before) const |
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More... | |
virtual abstract_object_pointert | meet (const abstract_object_pointert &other) const |
Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}. More... | |
virtual abstract_object_pointert | update_location_context (const locationst &locations, const bool update_sub_elements) const |
Update the location context for an abstract object, potentially propogating the update to any children of this abstract object. More... | |
abstract_object_pointert | make_top () const |
abstract_object_pointert | clear_top () const |
virtual abstract_object_pointert | unwrap_context () const |
virtual abstract_object_pointert | visit_sub_elements (const abstract_object_visitort &visitor) const |
Apply a visitor operation to all sub elements of this abstract_object. More... | |
virtual size_t | internal_hash () const |
virtual bool | internal_equality (const abstract_object_pointert &other) const |
Static Public Member Functions | |
static void | dump_map (std::ostream out, const shared_mapt &m) |
static void | dump_map_diff (std::ostream out, const shared_mapt &m1, const shared_mapt &m2) |
Dump all elements in m1 that are different or missing in m2. More... | |
static abstract_object_pointert | merge (abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications) |
Clones the first parameter and merges it with the second. More... | |
static abstract_object_pointert | merge (abstract_object_pointert op1, abstract_object_pointert op2) |
static abstract_object_pointert | meet (abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications) |
Interface method for the meet operation. More... | |
Protected Types | |
template<class T > | |
using | internal_sharing_ptrt = std::shared_ptr< T > |
typedef internal_sharing_ptrt< class abstract_objectt > | internal_abstract_object_pointert |
Protected Member Functions | |
virtual internal_abstract_object_pointert | mutable_clone () const |
abstract_object_pointert | abstract_object_merge (const abstract_object_pointert other) const |
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More... | |
bool | should_use_base_merge (const abstract_object_pointert other) const |
To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific. More... | |
virtual abstract_object_pointert | merge (abstract_object_pointert other) const |
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More... | |
abstract_object_pointert | abstract_object_meet (const abstract_object_pointert &other) const |
Helper function for base meet. More... | |
bool | should_use_base_meet (const abstract_object_pointert &other) const |
Helper function to decide if base meet implementation should be used. More... | |
void | set_top () |
void | set_not_top () |
void | set_not_bottom () |
Private Member Functions | |
virtual void | set_top_internal () |
virtual void | set_not_top_internal () |
virtual abstract_object_pointert | abstract_object_merge_internal (const abstract_object_pointert other) const |
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed it's actions but immediately prior to it returning. More... | |
virtual abstract_object_pointert | abstract_object_meet_internal (const abstract_object_pointert &other) const |
Helper function for base meet, in case additional work was needed. More... | |
Private Attributes | |
typet | t |
To enforce copy-on-write these are private and have read-only accessors. More... | |
bool | bottom |
bool | top |
Definition at line 78 of file abstract_object.h.
|
protected |
Definition at line 401 of file abstract_object.h.
|
protected |
Definition at line 398 of file abstract_object.h.
typedef std::set<goto_programt::const_targett> abstract_objectt::locationst |
Definition at line 215 of file abstract_object.h.
typedef sharing_mapt<irep_idt, abstract_object_pointert, false, irep_id_hash> abstract_objectt::shared_mapt |
Definition at line 217 of file abstract_object.h.
|
explicit |
type | the type the abstract_object is representing |
Definition at line 25 of file abstract_object.cpp.
abstract_objectt::abstract_objectt | ( | const typet & | type, |
bool | top, | ||
bool | bottom | ||
) |
Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true.
type | the type the abstract_object is representing |
top | is the abstract_object starting as top |
bottom | is the abstract_object starting as bottom |
Definition at line 30 of file abstract_object.cpp.
abstract_objectt::abstract_objectt | ( | const exprt & | expr, |
const abstract_environmentt & | environment, | ||
const namespacet & | ns | ||
) |
Construct an abstract object from the expression.
expr | The expression to use as the starting pointer for an abstract object |
environment | The environment this abstract object is being created in |
ns | The namespace |
Definition at line 36 of file abstract_object.cpp.
abstract_objectt::abstract_objectt | ( | const typet & | type, |
const exprt & | expr, | ||
const abstract_environmentt & | environment, | ||
const namespacet & | ns | ||
) |
Ctor for building object of types that differ from the types of input expressions.
type | explicitly declared type the resulting object should have |
expr | expression used to build the object |
environment | abstract environment to evaluate the expression |
ns | namespace to uncover names inside the expression |
Definition at line 44 of file abstract_object.cpp.
|
inlinevirtual |
Definition at line 117 of file abstract_object.h.
|
protected |
Helper function for base meet.
Two cases: return itself (if trivially contained in other); return BOTTOM otherwise.
other | pointer to the other object |
Definition at line 89 of file abstract_object.cpp.
|
privatevirtual |
Helper function for base meet, in case additional work was needed.
Base implementation simply return pointer to itself.
other | pointer to the other object |
Definition at line 101 of file abstract_object.cpp.
|
protected |
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.
other | The object to merge with this |
Definition at line 64 of file abstract_object.cpp.
|
privatevirtual |
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed it's actions but immediately prior to it returning.
As such, this function gives the ability to perform additional work for a merge.
This default implementation just returns itself.
other | the object to merge with this |
Reimplemented in write_location_contextt, and data_dependency_contextt.
Definition at line 76 of file abstract_object.cpp.
|
inline |
Definition at line 310 of file abstract_object.h.
|
static |
Definition at line 244 of file abstract_object.cpp.
|
static |
Dump all elements in m1 that are different or missing in m2.
out | the stream to write output to |
m1 | the 'target' sharing_map |
m2 | the reference sharing map |
Definition at line 261 of file abstract_object.cpp.
|
virtual |
Interface for transforms.
expr | the expression to evaluate and find the result of it. This will be the symbol referred to be op0() |
operands | an abstract_object (pointer) that represent the possible values of each operand |
environment | the abstract environment in which the expression is being evaluated |
ns | the current variable namespace |
To try and resolve different expressions with the maximum level of precision available.
Reimplemented in value_set_abstract_valuet, context_abstract_objectt, abstract_pointer_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >, and abstract_value_objectt.
Definition at line 108 of file abstract_object.cpp.
|
virtual |
Reimplemented in interval_abstract_valuet, context_abstract_objectt, constant_pointer_abstract_objectt, constant_abstract_valuet, abstract_pointer_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, and abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.
Definition at line 284 of file abstract_object.cpp.
|
inlinevirtual |
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.
before | The abstract_object_pointert to use as a reference to compare against |
Default implementation, with no other information to go on falls back to relying on copy-on-write and pointer inequality to indicate if an abstract_objectt has been modified
Reimplemented in write_location_contextt, data_dependency_contextt, and context_abstract_objectt.
Definition at line 238 of file abstract_object.h.
|
inlinevirtual |
Reimplemented in interval_abstract_valuet, and constant_abstract_valuet.
Definition at line 354 of file abstract_object.h.
|
inlinevirtual |
Reimplemented in interval_abstract_valuet, and constant_abstract_valuet.
Definition at line 349 of file abstract_object.h.
|
virtual |
Find out if the abstract object is bottom.
Reimplemented in context_abstract_objectt.
Definition at line 155 of file abstract_object.cpp.
|
virtual |
Find out if the abstract object is top.
Reimplemented in context_abstract_objectt.
Definition at line 150 of file abstract_object.cpp.
|
inline |
Definition at line 300 of file abstract_object.h.
|
static |
Interface method for the meet operation.
Decides whether to use the base implementation or if a more precise abstraction is attainable.
op1 | lhs object for meet |
op2 | rhs object for meet |
out_modifications | reference to a flag indicating modification (result is not op1) |
Definition at line 217 of file abstract_object.cpp.
|
virtual |
Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}.
other | pointer to the abstract object to meet |
Reimplemented in interval_abstract_valuet.
Definition at line 84 of file abstract_object.cpp.
|
static |
Definition at line 203 of file abstract_object.cpp.
|
static |
Clones the first parameter and merges it with the second.
op1 | the first abstract object to merge, this object determines the sensitivity of the output and is the object compared against to choose whether this merge changed anything |
op2 | the second abstract object to merge |
out_modifications | reference to a flag indicating modification |
Definition at line 189 of file abstract_object.cpp.
|
protectedvirtual |
Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.
other | The object to merge with this |
Reimplemented in write_location_contextt, value_set_pointer_abstract_objectt, value_set_abstract_valuet, value_set_abstract_objectt, interval_abstract_valuet, full_struct_abstract_objectt, full_array_abstract_objectt, data_dependency_contextt, constant_abstract_valuet, and constant_pointer_abstract_objectt.
Definition at line 59 of file abstract_object.cpp.
|
inlineprotectedvirtual |
Definition at line 404 of file abstract_object.h.
|
virtual |
Print the value of the abstract object.
out | the stream to write to |
ai | the abstract interpreter that contains the abstract domain (that contains the object ... ) |
ns | the current namespace |
Reimplemented in write_location_contextt, value_set_abstract_valuet, data_dependency_contextt, and context_abstract_objectt.
Definition at line 170 of file abstract_object.cpp.
|
inlineprotected |
Definition at line 459 of file abstract_object.h.
|
inlineprotected |
Definition at line 454 of file abstract_object.h.
|
inlineprivatevirtual |
Reimplemented in context_abstract_objectt.
Definition at line 370 of file abstract_object.h.
|
inlineprotected |
Definition at line 449 of file abstract_object.h.
|
inlineprivatevirtual |
Reimplemented in value_set_abstract_objectt, full_array_abstract_objectt, and context_abstract_objectt.
Definition at line 367 of file abstract_object.h.
|
protected |
Helper function to decide if base meet implementation should be used.
other | pointer to the other object to meet |
Definition at line 231 of file abstract_object.cpp.
|
protected |
To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific.
other | the object being merged with |
Definition at line 211 of file abstract_object.cpp.
|
virtual |
Converts to a constant expression if possible.
If abstract element represents a single value, then that value, otherwise nil. E.G. if it is an interval then this will be x if it is [x,x] This is the (sort of) dual to the constant_exprt constructor that allows an object to be built from a value.
Reimplemented in value_set_pointer_abstract_objectt, value_set_abstract_valuet, value_set_abstract_objectt, interval_abstract_valuet, context_abstract_objectt, constant_pointer_abstract_objectt, and constant_abstract_valuet.
Definition at line 165 of file abstract_object.cpp.
|
virtual |
Get the real type of the variable this abstract object is representing.
Reimplemented in context_abstract_objectt.
Definition at line 53 of file abstract_object.cpp.
|
virtual |
Reimplemented in context_abstract_objectt.
Definition at line 279 of file abstract_object.cpp.
|
virtual |
Update the location context for an abstract object, potentially propogating the update to any children of this abstract object.
locations | the set of locations to be updated |
update_sub_elements | if true, propogate the update operation to any children of this abstract object |
Reimplemented in write_location_contextt, and data_dependency_contextt.
Definition at line 237 of file abstract_object.cpp.
|
virtual |
Verify the internal structure of an abstract_object is correct.
Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.
Definition at line 160 of file abstract_object.cpp.
|
inlinevirtual |
Apply a visitor operation to all sub elements of this abstract_object.
A sub element might be a member of a struct, or an element of an array, for instance, but this is entirely determined by the particular derived instance of abstract_objectt.
visitor | an instance of a visitor class that will be applied to all sub elements |
Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.
Definition at line 344 of file abstract_object.h.
|
virtual |
A helper function to evaluate writing to a component of an abstract object.
More precise abstractions may override this to update what they are storing for a specific component.
environment | the abstract environment |
ns | the current namespace |
stack | the remaining stack of expressions on the LHS to evaluate |
specifier | the expression uses to access a specific component |
value | the value we are trying to write to the component |
merging_write | if true, this and all future writes will be merged with the current value |
Reimplemented in write_location_contextt, value_set_abstract_objectt, data_dependency_contextt, context_abstract_objectt, abstract_pointer_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< two_value_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< full_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_array_abstract_objectt, array_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, and abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.
Definition at line 139 of file abstract_object.cpp.
|
private |
Definition at line 362 of file abstract_object.h.
|
private |
To enforce copy-on-write these are private and have read-only accessors.
Definition at line 361 of file abstract_object.h.
|
private |
Definition at line 363 of file abstract_object.h.