#include <abstract_environment.h>

Collaboration diagram for abstract_environmentt:

Public Types
using	map_keyt = irep_idt

Public Member Functions
	abstract_environmentt ()=delete

	abstract_environmentt (variable_sensitivity_object_factory_ptrt _object_factory)

virtual abstract_object_pointert	eval (const exprt &expr, const namespacet &ns) const
	These three are really the heart of the method. More...

virtual bool	assign (const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
	Assign a value to an expression. More...

virtual bool	assume (const exprt &expr, const namespacet &ns)
	Reduces the domain based on a condition. More...

exprt	do_assume (const exprt &e, const namespacet &ns)

virtual abstract_object_pointert	write (const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
	Used within assign to do the actual dispatch. More...

void	erase (const symbol_exprt &expr)
	Delete a symbol from the map. More...

virtual abstract_object_pointert	abstract_object_factory (const typet &type, const namespacet &ns, bool top, bool bottom) const
	Look at the configuration for the sensitivity and create an appropriate abstract_object. More...

virtual abstract_object_pointert	abstract_object_factory (const typet &type, const exprt &e, const namespacet &ns) const
	For converting constants in the program. More...

const vsd_configt &	configuration () const
	Exposes the environment configuration. More...

virtual bool	merge (const abstract_environmentt &env, const goto_programt::const_targett &merge_location, widen_modet widen_mode)
	Computes the join between "this" and "b". More...

virtual void	havoc (const std::string &havoc_string)
	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. More...

void	make_top ()
	Set the domain to top (i.e. everything) More...

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

bool	is_bottom () const
	Gets whether the domain is bottom. More...

bool	is_top () const
	Gets whether the domain is top. More...

void	output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
	Print out all the values in the abstract object map. More...

exprt	to_predicate () const
	Gives a boolean condition that is true for all values represented by the environment. More...

bool	verify () const
	Check the structural invariants are maintained. More...

abstract_object_statisticst	gather_statistics (const namespacet &ns) const

Static Public Member Functions
static std::vector< abstract_environmentt::map_keyt >	modified_symbols (const abstract_environmentt &first, const abstract_environmentt &second)
	For our implementation of variable sensitivity domains, we need to be able to efficiently find symbols that have changed between different domains. More...

Protected Member Functions
virtual abstract_object_pointert	eval_expression (const exprt &e, const namespacet &ns) const

abstract_object_pointert	resolve_symbol (const exprt &e, const namespacet &ns) const

Protected Attributes
bool	bottom

sharing_mapt< map_keyt, abstract_object_pointert >	map

Private Member Functions
abstract_object_pointert	abstract_object_factory (const typet &type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const
	Look at the configuration for the sensitivity and create an appropriate abstract_object. More...

Private Attributes
variable_sensitivity_object_factory_ptrt	object_factory

Detailed Description

Definition at line 40 of file abstract_environment.h.

Member Typedef Documentation

◆ map_keyt

using abstract_environmentt::map_keyt = irep_idt

Definition at line 43 of file abstract_environment.h.

Constructor & Destructor Documentation

◆ abstract_environmentt() [1/2]

abstract_environmentt::abstract_environmentt ( )

delete

◆ abstract_environmentt() [2/2]

abstract_environmentt::abstract_environmentt ( variable_sensitivity_object_factory_ptrt _object_factory )

inlineexplicit

Definition at line 47 of file abstract_environment.h.

Member Function Documentation

◆ abstract_object_factory() [1/3]

abstract_object_pointert abstract_environmentt::abstract_object_factory	(	const typet &	type,
		bool	top,
		bool	bottom,
		const exprt &	e,
		const abstract_environmentt &	environment,
		const namespacet &	ns
	)		const

private

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 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 331 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 323 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 312 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 147 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 257 of file abstract_environment.cpp.

◆ configuration()

const vsd_configt & abstract_environmentt::configuration ( ) const

Exposes the environment configuration.

Definition at line 343 of file abstract_environment.cpp.

◆ do_assume()

exprt abstract_environmentt::do_assume	(	const exprt &	e,
		const namespacet &	ns
	)

Definition at line 300 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 476 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 94 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 461 of file abstract_environment.cpp.

◆ gather_statistics()

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

Definition at line 527 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 379 of file abstract_environment.cpp.

◆ is_bottom()

bool abstract_environmentt::is_bottom ( ) const

Gets whether the domain is bottom.

Definition at line 398 of file abstract_environment.cpp.

◆ is_top()

bool abstract_environmentt::is_top ( ) const

Gets whether the domain is top.

Definition at line 403 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 392 of file abstract_environment.cpp.

◆ make_top()

void abstract_environmentt::make_top ( )

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

Definition at line 385 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 348 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 482 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 408 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 135 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 425 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 449 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 237 of file abstract_environment.cpp.

Member Data Documentation

◆ bottom

bool abstract_environmentt::bottom

protected

Definition at line 253 of file abstract_environment.h.

◆ map

sharing_mapt<map_keyt, abstract_object_pointert> abstract_environmentt::map

protected

Definition at line 262 of file abstract_environment.h.

◆ object_factory

variable_sensitivity_object_factory_ptrt abstract_environmentt::object_factory

private

Definition at line 287 of file abstract_environment.h.

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

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

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ map_keyt

Constructor & Destructor Documentation

◆ abstract_environmentt() [1/2]

◆ abstract_environmentt() [2/2]

Member Function Documentation

◆ abstract_object_factory() [1/3]

◆ abstract_object_factory() [2/3]

◆ abstract_object_factory() [3/3]

◆ assign()

◆ assume()

◆ configuration()

◆ do_assume()

◆ erase()

◆ eval()

◆ eval_expression()

◆ gather_statistics()

◆ havoc()

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_top()

◆ merge()

◆ modified_symbols()

◆ output()

◆ resolve_symbol()

◆ to_predicate()

◆ verify()

◆ write()

Member Data Documentation

◆ bottom

◆ map

◆ object_factory