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_ptrt index_range (const namespacet &ns) const override
 
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
 Interface for transforms. More...
 
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)
 
- 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 ()
 

Private Member Functions

abstract_object_pointert evaluate_conditional (const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const
 
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...
 
abstract_object_pointert to_interval (const abstract_object_sett &other_values) const
 Cast the set of values other_values to an interval. More...
 

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 113 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 120 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 130 of file value_set_abstract_object.cpp.

Member Function Documentation

◆ evaluate_conditional()

abstract_object_pointert value_set_abstract_objectt::evaluate_conditional ( const typet type,
const std::vector< abstract_object_sett > &  operands,
const abstract_environmentt env,
const namespacet ns 
) const
private

Definition at line 179 of file value_set_abstract_object.cpp.

◆ expression_transform()

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

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.

Transforms the expr for every combination of operands (since these can be value-sets as well).

Reimplemented from abstract_objectt.

Definition at line 150 of file value_set_abstract_object.cpp.

◆ 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 55 of file value_set_abstract_object.h.

◆ index_range()

index_range_ptrt value_set_abstract_objectt::index_range ( const namespacet ns) const
overridevirtual

Implements abstract_value_objectt.

Definition at line 142 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 259 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 298 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 225 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 233 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 289 of file value_set_abstract_object.cpp.

◆ to_constant()

exprt value_set_abstract_objectt::to_constant ( ) const
inlineoverridevirtual

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 36 of file value_set_abstract_object.h.

◆ to_interval()

abstract_object_pointert value_set_abstract_objectt::to_interval ( const abstract_object_sett other_values) const
private

Cast the set of values other_values to an interval.

Parameters
other_valuesthe value-set to be abstracted into an interval
Returns
the interval-abstract-object containing other_values

Definition at line 272 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 208 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 66 of file value_set_abstract_object.h.

◆ values

abstract_object_sett value_set_abstract_objectt::values
private

Definition at line 114 of file value_set_abstract_object.h.


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