cprover
value_set_abstract_objectt Class Reference

#include <value_set_abstract_object.h>

+ Inheritance diagram for value_set_abstract_objectt:
+ Collaboration diagram for value_set_abstract_objectt:

Public Member Functions

 value_set_abstract_objectt (const typet &type)
 
 value_set_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...
 
 value_set_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 
index_range_implementation_ptrt index_range_implementation (const namespacet &ns) const override
 
value_range_implementation_ptrt value_range_implementation () const override
 
exprt to_constant () const override
 Converts to a constant expression if possible. More...
 
constant_interval_exprt to_interval () const override
 
const abstract_object_settget_values () const override
 Getter for the set of stored abstract objects. More...
 
void set_values (const abstract_object_sett &other_values)
 Setter for updating the stored values. 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...
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
 
- Public Member Functions inherited from abstract_value_objectt
 abstract_value_objectt (const typet &type)
 
 abstract_value_objectt (const typet &type, bool tp, bool bttm)
 
 abstract_value_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 
index_ranget index_range (const namespacet &ns) const
 
value_ranget value_range () const
 
abstract_object_pointert expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
 Interface for transforms. More...
 
- Public Member Functions inherited from abstract_objectt
 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 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 Attributes

static const size_t max_value_set_size = 10
 The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top. More...
 

Protected Member Functions

CLONE abstract_object_pointert merge (abstract_object_pointert other) const override
 Merge two sets of constraints by appending to the first one. More...
 
- Protected Member Functions inherited from abstract_objectt
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 Member Functions

abstract_object_pointert resolve_new_values (const abstract_object_sett &new_values, const abstract_environmentt &environment) const
 Update the set of stored values to new_values. More...
 
abstract_object_pointert resolve_values (const abstract_object_sett &new_values) const
 Update the set of stored values to new_values. More...
 
void set_top_internal () override
 

Private Attributes

abstract_object_sett values
 

Additional Inherited Members

- Public Types inherited from abstract_objectt
typedef std::set< goto_programt::const_targettlocationst
 
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hashshared_mapt
 
- Static Public Member Functions inherited from abstract_objectt
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 inherited from abstract_objectt
template<class T >
using internal_sharing_ptrt = std::shared_ptr< T >
 
typedef internal_sharing_ptrt< class abstract_objecttinternal_abstract_object_pointert
 

Detailed Description

Definition at line 18 of file value_set_abstract_object.h.

Constructor & Destructor Documentation

◆ value_set_abstract_objectt() [1/3]

value_set_abstract_objectt::value_set_abstract_objectt ( const typet type)
explicit

Parameters
typethe type the abstract_object is representing

Definition at line 114 of file value_set_abstract_object.cpp.

◆ value_set_abstract_objectt() [2/3]

value_set_abstract_objectt::value_set_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 121 of file value_set_abstract_object.cpp.

◆ value_set_abstract_objectt() [3/3]

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

Definition at line 131 of file value_set_abstract_object.cpp.

Member Function Documentation

◆ get_values()

const abstract_object_sett& value_set_abstract_objectt::get_values ( ) const
inlineoverridevirtual

Getter for the set of stored abstract objects.

Returns
the values represented by this abstract object

Implements value_set_tag.

Definition at line 44 of file value_set_abstract_object.h.

◆ index_range_implementation()

index_range_implementation_ptrt value_set_abstract_objectt::index_range_implementation ( const namespacet ns) const
overridevirtual

Implements abstract_value_objectt.

Definition at line 143 of file value_set_abstract_object.cpp.

◆ merge()

abstract_object_pointert value_set_abstract_objectt::merge ( abstract_object_pointert  other) const
overrideprotectedvirtual

Merge two sets of constraints by appending to the first one.

Reimplemented from abstract_objectt.

Definition at line 237 of file value_set_abstract_object.cpp.

◆ output()

void value_set_abstract_objectt::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
override

Definition at line 282 of file value_set_abstract_object.cpp.

◆ resolve_new_values()

abstract_object_pointert value_set_abstract_objectt::resolve_new_values ( const abstract_object_sett new_values,
const abstract_environmentt environment 
) const
private

Update the set of stored values to new_values.

Build a new abstract object of the right type if necessary.

Parameters
new_valuespotentially new set of values
environmentthe abstract environment
Returns
the abstract object representing new_values (either 'this' or something new)

Definition at line 202 of file value_set_abstract_object.cpp.

◆ resolve_values()

abstract_object_pointert value_set_abstract_objectt::resolve_values ( const abstract_object_sett new_values) const
private

Update the set of stored values to new_values.

Build a new abstract object of the right type if necessary.

Parameters
new_valuespotentially new set of values
Returns
the abstract object representing new_values (either 'this' or something new)

Definition at line 210 of file value_set_abstract_object.cpp.

◆ set_top_internal()

void value_set_abstract_objectt::set_top_internal ( )
overrideprivatevirtual

Reimplemented from abstract_objectt.

Definition at line 259 of file value_set_abstract_object.cpp.

◆ set_values()

void value_set_abstract_objectt::set_values ( const abstract_object_sett other_values)

Setter for updating the stored values.

Parameters
other_valuesthe new (non-empty) set of values

Definition at line 265 of file value_set_abstract_object.cpp.

◆ to_constant()

exprt value_set_abstract_objectt::to_constant ( ) const
overridevirtual

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 from abstract_objectt.

Definition at line 166 of file value_set_abstract_object.cpp.

◆ to_interval()

constant_interval_exprt value_set_abstract_objectt::to_interval ( ) const
overridevirtual

Implements abstract_value_objectt.

Definition at line 180 of file value_set_abstract_object.cpp.

◆ value_range_implementation()

value_range_implementation_ptrt value_set_abstract_objectt::value_range_implementation ( ) const
overridevirtual

Implements abstract_value_objectt.

Definition at line 161 of file value_set_abstract_object.cpp.

◆ write()

abstract_object_pointert value_set_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
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.

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.

Delegate writing to stored values.

Reimplemented from abstract_objectt.

Definition at line 185 of file value_set_abstract_object.cpp.

Member Data Documentation

◆ max_value_set_size

const size_t value_set_abstract_objectt::max_value_set_size = 10
static

The threshold size for value-sets: past this threshold the object is either converted to interval or marked as top.

Definition at line 55 of file value_set_abstract_object.h.

◆ values

abstract_object_sett value_set_abstract_objectt::values
private

Definition at line 97 of file value_set_abstract_object.h.


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