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}.

virtual abstract_object_pointert write_location_context (const locationt &location) const

Update the write location context for an abstract object.

virtual abstract_object_pointert merge_location_context (const locationt &location) const

Update the merge location context for an abstract object.

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.

virtual size_t internal_hash () const

virtual bool internal_equality (const abstract_object_pointert &other) const

virtual exprt to_predicate_internal (const exprt &name) const

to_predicate implementation - derived classes will override

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.

static combine_result merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)

static combine_result merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode)

static combine_result meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2)

Interface method for the meet operation.

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.

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.

virtual abstract_object_pointert merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const

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

abstract_object_pointert abstract_object_meet (const abstract_object_pointert &other) const

Helper function for base meet.

bool should_use_base_meet (const abstract_object_pointert &other) const

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

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.

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.

Private Attributes

typet t

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

bool bottom

bool top

Detailed Description

Definition at line 72 of file abstract_object.h.

Member Typedef Documentation

◆ internal_abstract_object_pointert

typedef internal_sharing_ptrt<class abstract_objectt> abstract_objectt::internal_abstract_object_pointert

protected

Definition at line 409 of file abstract_object.h.

◆ internal_sharing_ptrt

template<class T >

using abstract_objectt::internal_sharing_ptrt = std::shared_ptr<T>

protected

Definition at line 406 of file abstract_object.h.

◆ locationt

typedef goto_programt::const_targett abstract_objectt::locationt

Definition at line 204 of file abstract_object.h.

◆ shared_mapt

typedef sharing_mapt<irep_idt, abstract_object_pointert, false, irep_id_hash> abstract_objectt::shared_mapt

Definition at line 206 of file abstract_object.h.

Constructor & Destructor Documentation

◆ abstract_objectt() [1/2]

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: 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 19 of file abstract_object.cpp.

◆ abstract_objectt() [2/2]

abstract_objectt::abstract_objectt ( const exprt & expr,

const abstract_environmentt & environment,

const namespacet & ns

)

Construct an abstract object from the expression.

Parameters: 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 25 of file abstract_object.cpp.

◆ ~abstract_objectt()

virtual abstract_objectt::~abstract_objectt ( )

inlinevirtual

Definition at line 95 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: other pointer to the other object

Returns: the resulting object

Definition at line 70 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: other pointer to the other object

Returns: the resulting object

Definition at line 85 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: other The object to merge with this

Returns: Returns the result of the abstract object.

Definition at line 45 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: other the object to merge with this

Returns: the result of the merge

Reimplemented in data_dependency_contextt, liveness_contextt, and write_location_contextt.

Definition at line 57 of file abstract_object.cpp.

◆ clear_top()

abstract_object_pointert abstract_objectt::clear_top ( ) const

inline

Definition at line 313 of file abstract_object.h.

◆ dump_map()

void abstract_objectt::dump_map ( std::ostream out,

const shared_mapt & m

)

static

Definition at line 256 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: out the stream to write output to

m1 the 'target' sharing_map

m2 the reference sharing map

Definition at line 273 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: 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

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 abstract_value_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< full_array_abstract_objectt, array_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_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, abstract_pointer_objectt, and context_abstract_objectt.

Definition at line 98 of file abstract_object.cpp.

◆ get_statistics()

void abstract_objectt::get_statistics ( abstract_object_statisticst & statistics,

abstract_object_visitedt & visited,

const abstract_environmentt & env,

const namespacet & ns

) const

virtual

Reimplemented in abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< full_array_abstract_objectt, array_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_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, abstract_pointer_objectt, constant_abstract_valuet, constant_pointer_abstract_objectt, context_abstract_objectt, and interval_abstract_valuet.

Definition at line 296 of file abstract_object.cpp.

◆ 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: before The 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 context_abstract_objectt, data_dependency_contextt, and write_location_contextt.

Definition at line 227 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, and interval_abstract_valuet.

Definition at line 357 of file abstract_object.h.

◆ internal_hash()

virtual size_t abstract_objectt::internal_hash ( ) const

inlinevirtual

Reimplemented in constant_abstract_valuet, and interval_abstract_valuet.

Definition at line 352 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 146 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 141 of file abstract_object.cpp.

◆ make_top()

abstract_object_pointert abstract_objectt::make_top ( ) const

inline

Definition at line 303 of file abstract_object.h.

◆ meet() [1/2]

abstract_objectt::combine_result abstract_objectt::meet ( const abstract_object_pointert & op1,

const abstract_object_pointert & op2

)

static

Interface method for the meet operation.

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

Parameters: op1 lhs object for meet

op2 rhs object for meet

Returns: A pair containing the merged abstract object with the same sensitivity as op1, and a modified flag which will be true if the returned object is different from op1

Definition at line 227 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: other pointer to the abstract object to meet

Returns: the resulting abstract object pointer

Reimplemented in abstract_value_objectt, data_dependency_contextt, and write_location_contextt.

Definition at line 65 of file abstract_object.cpp.

◆ merge() [1/3]

abstract_objectt::combine_result abstract_objectt::merge ( const abstract_object_pointert & op1,

const abstract_object_pointert & op2,

const locationt & merge_location,

const widen_modet & widen_mode

)

static

Definition at line 195 of file abstract_object.cpp.

◆ merge() [2/3]

abstract_objectt::combine_result abstract_objectt::merge ( const abstract_object_pointert & op1,

const abstract_object_pointert & op2,

const widen_modet & widen_mode

)

static

Definition at line 208 of file abstract_object.cpp.

◆ merge() [3/3]

abstract_object_pointert abstract_objectt::merge ( const abstract_object_pointert & other,

const widen_modet & widen_mode

) 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: other The object to merge with this

widen_mode Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented in constant_pointer_abstract_objectt, abstract_value_objectt, data_dependency_contextt, full_array_abstract_objectt, full_struct_abstract_objectt, liveness_contextt, value_set_pointer_abstract_objectt, and write_location_contextt.

Definition at line 38 of file abstract_object.cpp.

◆ merge_location_context()

abstract_object_pointert abstract_objectt::merge_location_context ( const locationt & location ) const

virtual

Update the merge location context for an abstract object.

Parameters: location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented in full_array_abstract_objectt, full_struct_abstract_objectt, and liveness_contextt.

Definition at line 251 of file abstract_object.cpp.

◆ mutable_clone()

virtual internal_abstract_object_pointert abstract_objectt::mutable_clone ( ) const

inlineprotectedvirtual

Reimplemented in constant_abstract_valuet, constant_pointer_abstract_objectt, data_dependency_contextt, full_array_abstract_objectt, full_struct_abstract_objectt, interval_abstract_valuet, liveness_contextt, value_set_abstract_objectt, value_set_pointer_abstract_objectt, and write_location_contextt.

Definition at line 412 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: 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 context_abstract_objectt, data_dependency_contextt, liveness_contextt, and write_location_contextt.

Definition at line 176 of file abstract_object.cpp.

◆ set_not_bottom()

void abstract_objectt::set_not_bottom ( )

inlineprotected

Definition at line 470 of file abstract_object.h.

◆ set_not_top()

void abstract_objectt::set_not_top ( )

inlineprotected

Definition at line 465 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 378 of file abstract_object.h.

◆ set_top()

void abstract_objectt::set_top ( )

inlineprotected

Definition at line 460 of file abstract_object.h.

◆ set_top_internal()

virtual void abstract_objectt::set_top_internal ( )

inlineprivatevirtual

Reimplemented in context_abstract_objectt, full_array_abstract_objectt, interval_abstract_valuet, and value_set_abstract_objectt.

Definition at line 375 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: other pointer to the other object to meet

Returns: true if base implementation would yield the most precise abstraction anyway

Definition at line 238 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: other the object being merged with

Returns: Returns true if the base class is capable of doing a complete merge

Definition at line 221 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 constant_abstract_valuet, constant_pointer_abstract_objectt, context_abstract_objectt, interval_abstract_valuet, value_set_abstract_objectt, and value_set_pointer_abstract_objectt.

Definition at line 156 of file abstract_object.cpp.

◆ to_predicate()

exprt abstract_objectt::to_predicate ( const exprt & name ) const

Converts to an invariant expression.

Parameters: name - the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

The the abstract element represents a single value the expression will have the form name = value, if the value is an interval it will have the the form lower <= name <= upper, etc. If the value is bottom returns false, if top returns true.

Definition at line 161 of file abstract_object.cpp.

◆ to_predicate_internal()

exprt abstract_objectt::to_predicate_internal ( const exprt & name ) const

virtual

to_predicate implementation - derived classes will override

Parameters: name - the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

Reimplemented in constant_abstract_valuet, constant_pointer_abstract_objectt, context_abstract_objectt, full_array_abstract_objectt, full_struct_abstract_objectt, interval_abstract_valuet, value_set_abstract_objectt, and value_set_pointer_abstract_objectt.

Definition at line 170 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 33 of file abstract_object.cpp.

◆ unwrap_context()

abstract_object_pointert abstract_objectt::unwrap_context ( ) const

virtual

Reimplemented in context_abstract_objectt.

Definition at line 291 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_array_abstract_objectt, and full_struct_abstract_objectt.

Definition at line 151 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: visitor an 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_array_abstract_objectt, and full_struct_abstract_objectt.

Definition at line 347 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: 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

Returns: the abstract_objectt representing the result of writing to a specific component.

Reimplemented in abstract_value_objectt, abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >, abstract_aggregate_objectt< full_array_abstract_objectt, array_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_struct_abstract_objectt, struct_aggregate_typet >, abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet >, abstract_pointer_objectt, context_abstract_objectt, data_dependency_contextt, liveness_contextt, and write_location_contextt.

Definition at line 130 of file abstract_object.cpp.

◆ write_location_context()

abstract_object_pointert abstract_objectt::write_location_context ( const locationt & location ) const

virtual

Update the write location context for an abstract object.

Parameters: location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented in context_abstract_objectt, full_array_abstract_objectt, and full_struct_abstract_objectt.

Definition at line 245 of file abstract_object.cpp.

Member Data Documentation

◆ bottom

bool abstract_objectt::bottom

private

Definition at line 370 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 369 of file abstract_object.h.

◆ top

bool abstract_objectt::top

private

Definition at line 371 of file abstract_object.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_object.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_object.cpp