Parameters: type the type of the object whose state should be tracked

top does the type of the object start as top in the two-value domain

bottom does the type of the object start as bottom in the two-value domain

e the starting value of the symbol if top and bottom are both false

environment the current environment (normally *this)

ns the current variable namespace

Returns: The abstract object that has been created

Definition at line 336 of file abstract_environment.cpp.

◆ abstract_object_factory() [2/3]

abstract_object_pointert abstract_environmentt::abstract_object_factory ( const typet & type,

const exprt & e,

const namespacet & ns

) const

virtual

For converting constants in the program.

Parameters: type the type of the object whose state should be tracked

e the starting value of the symbol

ns the current variable namespace

Returns: The abstract object that has been created

Look at the configuration for the sensitivity and create an appropriate abstract_object, assigning an appropriate value Maybe the two abstract_object_factory methods should be compacted to one call...

Definition at line 328 of file abstract_environment.cpp.

◆ abstract_object_factory() [3/3]

abstract_object_pointert abstract_environmentt::abstract_object_factory ( const typet & type,

const namespacet & ns,

bool top,

bool bottom

) const

virtual

Look at the configuration for the sensitivity and create an appropriate abstract_object.

Parameters: type the type of the object whose state should be tracked

top does the type of the object start as top

bottom does the type of the object start as bottom in the two-value domain

ns the current variable namespace

Returns: The abstract object that has been created

Definition at line 317 of file abstract_environment.cpp.

◆ assign()

bool abstract_environmentt::assign ( const exprt & expr,

const abstract_object_pointert & value,

const namespacet & ns

)

virtual

Assign a value to an expression.

Parameters: expr the expression to assign to

value the value to assign to the expression

ns the namespace

Returns: A boolean, true if the assignment has changed the domain.

Assign is in principe simple, it updates the map with the new abstract object. The challenge is how to handle write to compound objects, for example: a[i].x.y = 23; In this case we clearly want to update a, but we need to delegate to the object in a so that it updates the right part of it (depending on what kind of array abstraction it is). So, as we find the variable ('a' in this case) we build a stack of which part of it is accessed.

As abstractions may split the assignment into multiple writes (for example pointers that could point to several locations, arrays with non-constant indexes), each of which has to handle the rest of the compound write, thus the stack is passed (to write, which does the actual updating) as an explicit argument rather than just via recursion.

The same use case (but for the opposite reason; because you will only update one of the multiple objects) is also why a merge_write flag is needed.

Definition at line 154 of file abstract_environment.cpp.

◆ assume()

bool abstract_environmentt::assume ( const exprt & expr,

const namespacet & ns

)

virtual

Reduces the domain based on a condition.

Parameters: expr the expression that is to be assumed

ns the current namespace

Returns: True if the assume changed the domain.

Reduces the domain to (an over-approximation) of the cases when the the expression holds. Used to implement assume statements and conditional branches. It would be valid to simply return false here because it is an over-approximation. We try to do better than that. The better the implementation the more precise the results will be.

Definition at line 263 of file abstract_environment.cpp.

◆ configuration()

const vsd_configt & abstract_environmentt::configuration ( ) const

Exposes the environment configuration.

Definition at line 348 of file abstract_environment.cpp.

◆ do_assume()

exprt abstract_environmentt::do_assume ( const exprt & e,

const namespacet & ns

)

Definition at line 305 of file abstract_environment.cpp.

◆ erase()

void abstract_environmentt::erase ( const symbol_exprt & expr )

Delete a symbol from the map.

This is necessary if the symbol falls out of scope and should no longer be tracked.

Parameters: expr A symbol to delete from the map

Definition at line 481 of file abstract_environment.cpp.

◆ eval()

abstract_object_pointert abstract_environmentt::eval ( const exprt & expr,

const namespacet & ns

) const

virtual

These three are really the heart of the method.

Evaluate the value of an expression relative to the current domain

Parameters: expr the expression to evaluate

ns the current namespace

Returns: The abstract_object representing the value of the expression

Definition at line 101 of file abstract_environment.cpp.

◆ eval_expression()

abstract_object_pointert abstract_environmentt::eval_expression ( const exprt & e,

const namespacet & ns

) const

protectedvirtual

Definition at line 466 of file abstract_environment.cpp.

◆ gather_statistics()

abstract_object_statisticst abstract_environmentt::gather_statistics ( const namespacet & ns ) const

Definition at line 532 of file abstract_environment.cpp.

◆ havoc()

void abstract_environmentt::havoc ( const std::string & havoc_string )

virtual

This should be used as a default case / everything else has failed The string is so that I can easily find and diagnose cases where this occurs.

Parameters: havoc_string diagnostic string to track down havoc causing.

Set the domain to top

Definition at line 384 of file abstract_environment.cpp.

◆ is_bottom()

bool abstract_environmentt::is_bottom ( ) const

Gets whether the domain is bottom.

Definition at line 403 of file abstract_environment.cpp.

◆ is_top()

bool abstract_environmentt::is_top ( ) const

Gets whether the domain is top.

Definition at line 408 of file abstract_environment.cpp.

◆ make_bottom()

void abstract_environmentt::make_bottom ( )

Set the domain to top (i.e. no possible states / unreachable)

Definition at line 397 of file abstract_environment.cpp.

◆ make_top()

void abstract_environmentt::make_top ( )

Set the domain to top (i.e. everything)

Definition at line 390 of file abstract_environment.cpp.

◆ merge()

bool abstract_environmentt::merge ( const abstract_environmentt & env,

const goto_programt::const_targett & merge_location,

widen_modet widen_mode

)

virtual

Computes the join between "this" and "b".

Parameters: env the other environment

merge_location when the merge is happening

widen_mode indicates if this is a widening merge

Returns: A Boolean, true when the merge has changed something

Definition at line 353 of file abstract_environment.cpp.

◆ modified_symbols()

std::vector< abstract_environmentt::map_keyt > abstract_environmentt::modified_symbols ( const abstract_environmentt & first,

const abstract_environmentt & second

)

static

For our implementation of variable sensitivity domains, we need to be able to efficiently find symbols that have changed between different domains.

To do this, we need to be able to quickly find which symbols have new written locations, which we do by finding the intersection between two different domains (environments).

Inputs are two abstract_environmentt's that need to be intersected for, so that we can find symbols that have changed between different domains.

Returns: An std::vector containing the symbols that are present in both environments.

Definition at line 487 of file abstract_environment.cpp.

◆ output()

void abstract_environmentt::output ( std::ostream & out,

const class ai_baset & ai,

const namespacet & ns

) const

Print out all the values in the abstract object map.

Parameters: out the stream to write to

ai the abstract interpreter that contains this domain

ns the current namespace

Definition at line 413 of file abstract_environment.cpp.

◆ resolve_symbol()

abstract_object_pointert abstract_environmentt::resolve_symbol ( const exprt & e,

const namespacet & ns

) const

protected

Definition at line 142 of file abstract_environment.cpp.

◆ to_predicate()

exprt abstract_environmentt::to_predicate ( ) const

Gives a boolean condition that is true for all values represented by the environment.

Returns: An exprt describing the environment

Definition at line 430 of file abstract_environment.cpp.

◆ verify()

bool abstract_environmentt::verify ( ) const

Check the structural invariants are maintained.

In this case this is checking there aren't any null pointer mapped values

Definition at line 454 of file abstract_environment.cpp.

◆ write()

abstract_object_pointert abstract_environmentt::write ( const abstract_object_pointert & lhs,

const abstract_object_pointert & rhs,

std::stack< exprt > remaining_stack,

const namespacet & ns,

bool merge_write

)

virtual

Used within assign to do the actual dispatch.

Parameters: lhs the abstract object for the left hand side of the write (i.e. the one to update).

rhs the value we are trying to write to the left hand side

remaining_stack what is left of the stack before the rhs can replace or be merged with the rhs

ns the namespace

merge_write Are we replacing the left hand side with the right hand side (e.g. we know for a fact that we are overwriting this object) or could the write in fact not take place and therefore we should merge to model the case where it did not.

Returns: A modified version of the rhs after the write has taken place

Write an abstract object onto another respecting a stack of member, index and dereference access. This ping-pongs between this method and the relevant write methods in abstract_struct, abstract_pointer and abstract_array until the stack is empty

Definition at line 243 of file abstract_environment.cpp.

Member Data Documentation

◆ bottom

bool abstract_environmentt::bottom

protected

Definition at line 251 of file abstract_environment.h.

◆ map

sharing_mapt<map_keyt, abstract_object_pointert> abstract_environmentt::map

protected

Definition at line 260 of file abstract_environment.h.

◆ object_factory

variable_sensitivity_object_factory_ptrt abstract_environmentt::object_factory

private

Definition at line 285 of file abstract_environment.h.

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

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