cprover
abstract_objectt Class Reference

#include <abstract_object.h>

+ Inheritance diagram for abstract_objectt:
+ Collaboration diagram for abstract_objectt:

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_targettlocationst
 
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hashshared_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 typettype () 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_objecttinternal_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 ()
 

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
 

Detailed Description

Definition at line 78 of file abstract_object.h.

Member Typedef Documentation

◆ internal_abstract_object_pointert

◆ internal_sharing_ptrt

template<class T >
using abstract_objectt::internal_sharing_ptrt = std::shared_ptr<T>
protected

Definition at line 398 of file abstract_object.h.

◆ locationst

Definition at line 215 of file abstract_object.h.

◆ shared_mapt

Constructor & Destructor Documentation

◆ abstract_objectt() [1/4]

abstract_objectt::abstract_objectt ( const typet type)
explicit
Parameters
typethe type the abstract_object is representing

Definition at line 25 of file abstract_object.cpp.

◆ abstract_objectt() [2/4]

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.

Parameters
typethe type the abstract_object is representing
topis the abstract_object starting as top
bottomis the abstract_object starting as bottom

Definition at line 30 of file abstract_object.cpp.

◆ abstract_objectt() [3/4]

abstract_objectt::abstract_objectt ( const exprt expr,
const abstract_environmentt environment,
const namespacet ns 
)

Construct an abstract object from the expression.

Parameters
exprThe expression to use as the starting pointer for an abstract object
environmentThe environment this abstract object is being created in
nsThe namespace

Definition at line 36 of file abstract_object.cpp.

◆ abstract_objectt() [4/4]

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.

Parameters
typeexplicitly declared type the resulting object should have
exprexpression used to build the object
environmentabstract environment to evaluate the expression
nsnamespace to uncover names inside the expression

Definition at line 44 of file abstract_object.cpp.

◆ ~abstract_objectt()

virtual abstract_objectt::~abstract_objectt ( )
inlinevirtual

Definition at line 117 of file abstract_object.h.

Member Function Documentation

◆ abstract_object_meet()

abstract_object_pointert abstract_objectt::abstract_object_meet ( const abstract_object_pointert other) const
protected

Helper function for base meet.

Two cases: return itself (if trivially contained in other); return BOTTOM otherwise.

Parameters
otherpointer to the other object
Returns
the resulting object

Definition at line 89 of file abstract_object.cpp.

◆ abstract_object_meet_internal()

abstract_object_pointert abstract_objectt::abstract_object_meet_internal ( const abstract_object_pointert other) const
privatevirtual

Helper function for base meet, in case additional work was needed.

Base implementation simply return pointer to itself.

Parameters
otherpointer to the other object
Returns
the resulting object

Definition at line 101 of file abstract_object.cpp.

◆ abstract_object_merge()

abstract_object_pointert abstract_objectt::abstract_object_merge ( const abstract_object_pointert  other) const
protected

Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

Parameters
otherThe object to merge with this
Returns
Returns the result of the abstract object.

Definition at line 64 of file abstract_object.cpp.

◆ abstract_object_merge_internal()

abstract_object_pointert abstract_objectt::abstract_object_merge_internal ( const abstract_object_pointert  other) const
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.

Parameters
otherthe object to merge with this
Returns
the result of the merge

Reimplemented in write_location_contextt, and data_dependency_contextt.

Definition at line 76 of file abstract_object.cpp.

◆ clear_top()

abstract_object_pointert abstract_objectt::clear_top ( ) const
inline

Definition at line 310 of file abstract_object.h.

◆ dump_map()

void abstract_objectt::dump_map ( std::ostream  out,
const shared_mapt m 
)
static

Definition at line 244 of file abstract_object.cpp.

◆ dump_map_diff()

void abstract_objectt::dump_map_diff ( std::ostream  out,
const shared_mapt m1,
const shared_mapt m2 
)
static

Dump all elements in m1 that are different or missing in m2.

Parameters
outthe stream to write output to
m1the 'target' sharing_map
m2the reference sharing map

Definition at line 261 of file abstract_object.cpp.

◆ expression_transform()

abstract_object_pointert abstract_objectt::expression_transform ( const exprt expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt environment,
const namespacet ns 
) const
virtual

Interface for transforms.

Parameters
exprthe expression to evaluate and find the result of it. This will be the symbol referred to be op0()
operandsan abstract_object (pointer) that represent the possible values of each operand
environmentthe abstract environment in which the expression is being evaluated
nsthe current variable namespace
Returns
Returns the abstract_object representing the result of this expression to the maximum precision available.

To try and resolve different expressions with the maximum level of precision available.

Reimplemented in value_set_abstract_valuet, value_set_abstract_objectt, interval_abstract_valuet, context_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 108 of file abstract_object.cpp.

◆ get_statistics()

◆ has_been_modified()

virtual bool abstract_objectt::has_been_modified ( const abstract_object_pointert  before) const
inlinevirtual

Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

Parameters
beforeThe abstract_object_pointert to use as a reference to compare against
Returns
true if 'this' is considered to have been modified in comparison to 'before', false otherwise.

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.

◆ internal_equality()

virtual bool abstract_objectt::internal_equality ( const abstract_object_pointert other) const
inlinevirtual

Reimplemented in constant_abstract_valuet.

Definition at line 354 of file abstract_object.h.

◆ internal_hash()

virtual size_t abstract_objectt::internal_hash ( ) const
inlinevirtual

Reimplemented in constant_abstract_valuet.

Definition at line 349 of file abstract_object.h.

◆ is_bottom()

bool abstract_objectt::is_bottom ( ) const
virtual

Find out if the abstract object is bottom.

Returns
Returns true if the abstract object is representing the bottom.

Reimplemented in context_abstract_objectt.

Definition at line 155 of file abstract_object.cpp.

◆ is_top()

bool abstract_objectt::is_top ( ) const
virtual

Find out if the abstract object is top.

Returns
Returns true if the abstract object is representing the top (i.e. we don't know anything about the value).

Reimplemented in context_abstract_objectt.

Definition at line 150 of file abstract_object.cpp.

◆ make_top()

abstract_object_pointert abstract_objectt::make_top ( ) const
inline

Definition at line 300 of file abstract_object.h.

◆ meet() [1/2]

abstract_object_pointert abstract_objectt::meet ( abstract_object_pointert  op1,
abstract_object_pointert  op2,
bool &  out_modifications 
)
static

Interface method for the meet operation.

Decides whether to use the base implementation or if a more precise abstraction is attainable.

Parameters
op1lhs object for meet
op2rhs object for meet
out_modificationsreference to a flag indicating modification (result is not op1)
Returns
resulting object after meet

Definition at line 217 of file abstract_object.cpp.

◆ meet() [2/2]

abstract_object_pointert abstract_objectt::meet ( const abstract_object_pointert other) const
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}.

Parameters
otherpointer to the abstract object to meet
Returns
the resulting abstract object pointer

Reimplemented in interval_abstract_valuet.

Definition at line 84 of file abstract_object.cpp.

◆ merge() [1/3]

abstract_object_pointert abstract_objectt::merge ( abstract_object_pointert  op1,
abstract_object_pointert  op2 
)
static

Definition at line 203 of file abstract_object.cpp.

◆ merge() [2/3]

abstract_object_pointert abstract_objectt::merge ( abstract_object_pointert  op1,
abstract_object_pointert  op2,
bool &  out_modifications 
)
static

Clones the first parameter and merges it with the second.

Parameters
op1the 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
op2the second abstract object to merge
out_modificationsreference to a flag indicating modification
Returns
The merged abstract object with the same sensitivity as the first parameter. out_modifications will be true if the resulting abstract object is different from op1

Definition at line 189 of file abstract_object.cpp.

◆ merge() [3/3]

abstract_object_pointert abstract_objectt::merge ( abstract_object_pointert  other) const
protectedvirtual

Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

Parameters
otherThe object to merge with this
Returns
Returns the result of the merge.

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.

◆ mutable_clone()

virtual internal_abstract_object_pointert abstract_objectt::mutable_clone ( ) const
inlineprotectedvirtual

Definition at line 404 of file abstract_object.h.

◆ output()

void abstract_objectt::output ( std::ostream &  out,
const class ai_baset ai,
const namespacet ns 
) const
virtual

Print the value of the abstract object.

Parameters
outthe stream to write to
aithe abstract interpreter that contains the abstract domain (that contains the object ... )
nsthe 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.

◆ set_not_top()

void abstract_objectt::set_not_top ( )
inlineprotected

Definition at line 454 of file abstract_object.h.

◆ set_not_top_internal()

virtual void abstract_objectt::set_not_top_internal ( )
inlineprivatevirtual

Reimplemented in context_abstract_objectt.

Definition at line 370 of file abstract_object.h.

◆ set_top()

void abstract_objectt::set_top ( )
inlineprotected

Definition at line 449 of file abstract_object.h.

◆ set_top_internal()

virtual void abstract_objectt::set_top_internal ( )
inlineprivatevirtual

Reimplemented in full_array_abstract_objectt, and context_abstract_objectt.

Definition at line 367 of file abstract_object.h.

◆ should_use_base_meet()

bool abstract_objectt::should_use_base_meet ( const abstract_object_pointert other) const
protected

Helper function to decide if base meet implementation should be used.

Parameters
otherpointer to the other object to meet
Returns
true if base implementation would yield the most precise abstraction anyway

Definition at line 231 of file abstract_object.cpp.

◆ should_use_base_merge()

bool abstract_objectt::should_use_base_merge ( const abstract_object_pointert  other) const
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.

Parameters
otherthe object being merged with
Returns
Returns true if the base class is capable of doing a complete merge

Definition at line 211 of file abstract_object.cpp.

◆ to_constant()

exprt abstract_objectt::to_constant ( ) const
virtual

Converts to a constant expression if possible.

Returns
Returns an exprt representing the value if the value is known and constant. Otherwise returns the nil expression

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.

◆ type()

const typet & abstract_objectt::type ( ) const
virtual

Get the real type of the variable this abstract object is representing.

Returns
The program type this abstract object represents

Reimplemented in context_abstract_objectt.

Definition at line 53 of file abstract_object.cpp.

◆ unwrap_context()

abstract_object_pointert abstract_objectt::unwrap_context ( ) const
virtual

Reimplemented in context_abstract_objectt.

Definition at line 279 of file abstract_object.cpp.

◆ update_location_context()

abstract_object_pointert abstract_objectt::update_location_context ( const locationst locations,
const bool  update_sub_elements 
) const
virtual

Update the location context for an abstract object, potentially propogating the update to any children of this abstract object.

Parameters
locationsthe set of locations to be updated
update_sub_elementsif true, propogate the update operation to any children of this abstract object
Returns
a clone of this abstract object with it's location context updated

Reimplemented in write_location_contextt, and data_dependency_contextt.

Definition at line 237 of file abstract_object.cpp.

◆ verify()

bool abstract_objectt::verify ( ) const
virtual

Verify the internal structure of an abstract_object is correct.

Returns
true if the abstract_object is correctly constructed, or false otherwise

Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 160 of file abstract_object.cpp.

◆ visit_sub_elements()

virtual abstract_object_pointert abstract_objectt::visit_sub_elements ( const abstract_object_visitort visitor) const
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.

Parameters
visitoran instance of a visitor class that will be applied to all sub elements
Returns
A new abstract_object if it's contents is modifed, or this if no modification is needed

Reimplemented in full_struct_abstract_objectt, and full_array_abstract_objectt.

Definition at line 344 of file abstract_object.h.

◆ write()

abstract_object_pointert abstract_objectt::write ( abstract_environmentt environment,
const namespacet ns,
const std::stack< exprt > &  stack,
const exprt specifier,
const abstract_object_pointert value,
bool  merging_write 
) const
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.

Parameters
environmentthe abstract environment
nsthe current namespace
stackthe remaining stack of expressions on the LHS to evaluate
specifierthe expression uses to access a specific component
valuethe value we are trying to write to the component
merging_writeif true, this and all future writes will be merged with the current value
Returns
the abstract_objectt representing the result of writing to a specific component.

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.

Member Data Documentation

◆ bottom

bool abstract_objectt::bottom
private

Definition at line 362 of file abstract_object.h.

◆ t

typet abstract_objectt::t
private

To enforce copy-on-write these are private and have read-only accessors.

Definition at line 361 of file abstract_object.h.

◆ top

bool abstract_objectt::top
private

Definition at line 363 of file abstract_object.h.


The documentation for this class was generated from the following files: