cprover
|
#include <data_dependency_context.h>
Classes | |
class | location_ordert |
Public Member Functions | |
data_dependency_contextt (const abstract_object_pointert child, const typet &type) | |
data_dependency_contextt (const abstract_object_pointert child, const typet &type, bool top, bool bottom) | |
data_dependency_contextt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
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 override |
A helper function to evaluate writing to a component of an abstract object. More... | |
abstract_object_pointert | update_location_context (const abstract_objectt::locationst &locations, const bool update_sub_elements) const override |
Update the location context for an abstract object, potentially propogating the update to any children of this abstract object. More... | |
bool | has_been_modified (const abstract_object_pointert before) const override |
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More... | |
std::set< goto_programt::const_targett > | get_data_dependencies () const |
Return the set of data dependencies associated with this node. More... | |
std::set< goto_programt::const_targett > | get_data_dominators () const |
Return the set of data dominators associated with this node. More... | |
void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override |
Output a representation of the value of this abstract object. More... | |
![]() | |
write_location_contextt (const abstract_object_pointert child, const typet &type) | |
write_location_contextt (const abstract_object_pointert child, const typet &type, bool top, bool bottom) | |
write_location_contextt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
virtual | ~write_location_contextt () |
bool | has_been_modified (const abstract_object_pointert before) const override |
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More... | |
abstract_object_pointert | update_location_context (const abstract_objectt::locationst &locations, const bool update_sub_elements) const override |
Update the location context for an abstract object, potentially propagating the update to any children of this abstract object. More... | |
locationst | get_location_union (const locationst &locations) const |
Construct the union of the location set of the current object, and a the provided location set. More... | |
void | output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override |
Output a representation of the value of this abstract object. More... | |
![]() | |
context_abstract_objectt (const abstract_object_pointert child, const typet &type) | |
context_abstract_objectt (const abstract_object_pointert child, const typet &type, bool top, bool bottom) | |
context_abstract_objectt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns) | |
virtual | ~context_abstract_objectt () |
const typet & | type () const override |
Get the real type of the variable this abstract object is representing. More... | |
bool | is_top () const override |
Find out if the abstract object is top. More... | |
bool | is_bottom () const override |
Find out if the abstract object is bottom. More... | |
exprt | to_constant () const override |
Converts to a constant expression if possible. More... | |
abstract_object_pointert | expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override |
Try to resolve an expression with the maximum level of precision available. More... | |
abstract_object_pointert | unwrap_context () const override |
void | get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override |
abstract_object_pointert | get_child () const |
![]() | |
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 bool | verify () const |
Verify the internal structure of an abstract_object is correct. 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... | |
abstract_object_pointert | make_top () const |
abstract_object_pointert | clear_top () 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 |
Protected Member Functions | |
CLONE abstract_object_pointert | merge (abstract_object_pointert other) const override |
Create a new abstract object that is the result of merging this abstract object with a given abstract_object. More... | |
abstract_object_pointert | abstract_object_merge_internal (const abstract_object_pointert other) const override |
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning. More... | |
![]() | |
CLONE abstract_object_pointert | merge (abstract_object_pointert other) const override |
Create a new abstract object that is the result of merging this abstract object with a given abstract_object. More... | |
abstract_object_pointert | abstract_object_merge_internal (const abstract_object_pointert other) const override |
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning. More... | |
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 override |
A helper function to evaluate writing to a component of an abstract object. More... | |
virtual abstract_objectt::locationst | get_last_written_locations () const |
![]() | |
void | set_child (const abstract_object_pointert &child) |
void | set_top_internal () override |
void | set_not_top_internal () override |
![]() | |
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... | |
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 Types | |
typedef std::set< goto_programt::const_targett, location_ordert > | dependencest |
Private Member Functions | |
abstract_object_pointert | insert_data_deps (const dependencest &dependencies) const |
Insert the given set of data dependencies into the data dependencies set for this data_dependency_context object. More... | |
abstract_object_pointert | set_data_deps (const dependencest &dependencies) const |
Set the given set of data dependencies for this data_dependency_context object. More... | |
abstract_object_pointert | insert_data_deps (const locationst &locations) const |
abstract_object_pointert | set_data_deps (const locationst &locations) const |
Private Attributes | |
dependencest | data_deps |
dependencest | data_dominators |
Additional Inherited Members | |
![]() | |
typedef std::set< goto_programt::const_targett > | locationst |
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > | shared_mapt |
![]() | |
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... | |
![]() | |
template<class T > | |
using | internal_sharing_ptrt = std::shared_ptr< T > |
typedef internal_sharing_ptrt< class abstract_objectt > | internal_abstract_object_pointert |
![]() | |
static void | output_last_written_locations (std::ostream &out, const abstract_objectt::locationst &locations) |
Internal helper function to format and output a given set of locations. More... | |
![]() | |
CLONE abstract_object_pointert | child_abstract_object |
Definition at line 20 of file data_dependency_context.h.
|
private |
Definition at line 89 of file data_dependency_context.h.
|
inlineexplicit |
Definition at line 25 of file data_dependency_context.h.
|
inline |
Definition at line 32 of file data_dependency_context.h.
|
inlineexplicit |
Definition at line 41 of file data_dependency_context.h.
|
overrideprotectedvirtual |
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after the base abstract_object_merge has completed its actions but immediately prior to it returning.
As such, this function gives the ability to perform additional work for a merge.
For the dependency context, this additional work is the tracking of last_written_locations across the merge
other | the object to merge with this |
Reimplemented from abstract_objectt.
Definition at line 295 of file data_dependency_context.cpp.
std::set< goto_programt::const_targett > data_dependency_contextt::get_data_dependencies | ( | ) | const |
Return the set of data dependencies associated with this node.
Definition at line 318 of file data_dependency_context.cpp.
std::set< goto_programt::const_targett > data_dependency_contextt::get_data_dominators | ( | ) | const |
Return the set of data dominators associated with this node.
Definition at line 332 of file data_dependency_context.cpp.
|
overridevirtual |
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 |
Reimplemented from context_abstract_objectt.
Definition at line 28 of file data_dependency_context.cpp.
|
private |
Insert the given set of data dependencies into the data dependencies set for this data_dependency_context object.
dependencies | the set of dependencies to add |
Definition at line 82 of file data_dependency_context.cpp.
|
inlineprivate |
Definition at line 99 of file data_dependency_context.h.
|
overrideprotectedvirtual |
Create a new abstract object that is the result of merging this abstract object with a given abstract_object.
other | the abstract object to merge with |
Reimplemented from abstract_objectt.
Definition at line 238 of file data_dependency_context.cpp.
|
overridevirtual |
Output a representation of the value of this 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 from context_abstract_objectt.
Definition at line 340 of file data_dependency_context.cpp.
|
private |
Set the given set of data dependencies for this data_dependency_context object.
dependencies | the set of dependencies to set |
Definition at line 139 of file data_dependency_context.cpp.
|
inlineprivate |
Definition at line 107 of file data_dependency_context.h.
|
overridevirtual |
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 from abstract_objectt.
Definition at line 216 of file data_dependency_context.cpp.
|
overridevirtual |
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 from context_abstract_objectt.
Definition at line 186 of file data_dependency_context.cpp.
|
private |
Definition at line 90 of file data_dependency_context.h.
|
private |
Definition at line 91 of file data_dependency_context.h.