Keep track of dependencies between strings. More...

#include <string_dependencies.h>

Collaboration diagram for string_dependenciest:

Classes
class	builtin_function_nodet
	A builtin function node contains a builtin function call. More...

struct	node_hash
	Hash function for nodes. More...

class	nodet

class	string_nodet
	A string node points to builtin_function on which it depends. More...

Public Member Functions
string_nodet &	get_node (const array_string_exprt &e)

std::unique_ptr< const string_nodet >	node_at (const array_string_exprt &e) const

builtin_function_nodet &	make_node (std::unique_ptr< string_builtin_functiont > builtin_function)

const string_builtin_functiont &	get_builtin_function (const builtin_function_nodet &node) const

void	add_dependency (const array_string_exprt &e, const builtin_function_nodet &builtin_function)
	Add edge from node for `e` to node for `builtin_function` if `e` is a simple array expression. More...

void	for_each_dependency (const string_nodet &node, const std::function< void(const builtin_function_nodet &)> &f) const
	Applies `f` to each node on which `node` depends. More...

void	for_each_dependency (const builtin_function_nodet &node, const std::function< void(const string_nodet &)> &f) const

std::optional< exprt >	eval (const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
	Attempt to evaluate the given string from the dependencies and valuation of strings on which it depends Warning: eval uses a cache which must be cleaned everytime the valuations given by get_value can change. More...

void	clean_cache ()
	Clean the cache used by `eval` More...

void	output_dot (std::ostream &stream) const

string_constraintst	add_constraints (string_constraint_generatort &generatort, message_handlert &message_handler)
	For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding constraints. More...

void	clear ()
	Clear the content of the dependency graph. More...

Private Member Functions
void	for_each_node (const std::function< void(const nodet &)> &f) const
	Applies `f` on all nodes. More...

void	for_each_successor (const nodet &i, const std::function< void(const nodet &)> &f) const
	Applies `f` on all successors of the node n. More...

Private Attributes
std::vector< builtin_function_nodet >	builtin_function_nodes
	Set of nodes representing builtin_functions. More...

std::vector< string_nodet >	string_nodes
	Set of nodes representing strings. More...

std::unordered_map< array_string_exprt, std::size_t, irep_hash >	node_index_pool
	Nodes describing dependencies of a string: values of the map correspond to indexes in the vector `string_nodes`. More...

std::vector< std::optional< exprt > >	eval_string_cache

Detailed Description

Keep track of dependencies between strings.

Each string points to the builtin_function calls on which it depends. Each builtin_function points to the strings on which the result depends.

Definition at line 22 of file string_dependencies.h.

Member Function Documentation

◆ add_constraints()

string_constraintst string_dependenciest::add_constraints	(	string_constraint_generatort &	generatort,
		message_handlert &	message_handler
	)

For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding constraints.

For the other builtin only add constraints on the length.

Definition at line 347 of file string_dependencies.cpp.

◆ add_dependency()

void string_dependenciest::add_dependency	(	const array_string_exprt &	e,
		const builtin_function_nodet &	builtin_function
	)

Add edge from node for e to node for builtin_function if e is a simple array expression.

If it is an if_exprt we add the sub-expressions that are not if_exprts instead.

Definition at line 117 of file string_dependencies.cpp.

◆ clean_cache()

void string_dependenciest::clean_cache ( )

Clean the cache used by eval

Definition at line 190 of file string_dependencies.cpp.

◆ clear()

void string_dependenciest::clear ( void )

Clear the content of the dependency graph.

Definition at line 127 of file string_dependencies.cpp.

◆ eval()

std::optional< exprt > string_dependenciest::eval	(	const array_string_exprt &	s,
		const std::function< exprt(const exprt &)> &	get_value
	)		const

Attempt to evaluate the given string from the dependencies and valuation of strings on which it depends Warning: eval uses a cache which must be cleaned everytime the valuations given by get_value can change.

Definition at line 168 of file string_dependencies.cpp.

◆ for_each_dependency() [1/2]

void string_dependenciest::for_each_dependency	(	const builtin_function_nodet &	node,
		const std::function< void(const string_nodet &)> &	f
	)		const

Definition at line 255 of file string_dependencies.cpp.

◆ for_each_dependency() [2/2]

void string_dependenciest::for_each_dependency	(	const string_nodet &	node,
		const std::function< void(const builtin_function_nodet &)> &	f
	)		const

Applies f to each node on which node depends.

Definition at line 285 of file string_dependencies.cpp.

◆ for_each_node()

void string_dependenciest::for_each_node ( const std::function< void(const nodet &)> & f ) const

private

Applies f on all nodes.

Definition at line 313 of file string_dependencies.cpp.

◆ for_each_successor()

void string_dependenciest::for_each_successor	(	const nodet &	i,
		const std::function< void(const nodet &)> &	f
	)		const

private

Applies f on all successors of the node n.

Definition at line 293 of file string_dependencies.cpp.

◆ get_builtin_function()

const string_builtin_functiont & string_dependenciest::get_builtin_function ( const builtin_function_nodet & node ) const

Definition at line 99 of file string_dependencies.cpp.

◆ get_node()

string_dependenciest::string_nodet & string_dependenciest::get_node ( const array_string_exprt & e )

Definition at line 72 of file string_dependencies.cpp.

◆ make_node()

string_dependenciest::builtin_function_nodet & string_dependenciest::make_node ( std::unique_ptr< string_builtin_functiont > builtin_function )

Definition at line 91 of file string_dependencies.cpp.

◆ node_at()

std::unique_ptr< const string_dependenciest::string_nodet > string_dependenciest::node_at ( const array_string_exprt & e ) const

Definition at line 83 of file string_dependencies.cpp.

◆ output_dot()

void string_dependenciest::output_dot ( std::ostream & stream ) const

Definition at line 322 of file string_dependencies.cpp.

Member Data Documentation

◆ builtin_function_nodes

std::vector<builtin_function_nodet> string_dependenciest::builtin_function_nodes

private

Set of nodes representing builtin_functions.

Definition at line 125 of file string_dependencies.h.

◆ eval_string_cache

std::vector<std::optional<exprt> > string_dependenciest::eval_string_cache

mutableprivate

Definition at line 172 of file string_dependencies.h.

◆ node_index_pool

std::unordered_map<array_string_exprt, std::size_t, irep_hash> string_dependenciest::node_index_pool

private

Nodes describing dependencies of a string: values of the map correspond to indexes in the vector string_nodes.

Definition at line 133 of file string_dependencies.h.

◆ string_nodes

std::vector<string_nodet> string_dependenciest::string_nodes

private

Set of nodes representing strings.

Definition at line 128 of file string_dependencies.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/strings/string_dependencies.h
/home/runner/work/cbmc/cbmc/src/solvers/strings/string_dependencies.cpp

Classes

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Function Documentation

◆ add_constraints()

◆ add_dependency()

◆ clean_cache()

◆ clear()

◆ eval()

◆ for_each_dependency() [1/2]

◆ for_each_dependency() [2/2]

◆ for_each_node()

◆ for_each_successor()

◆ get_builtin_function()

◆ get_node()

◆ make_node()

◆ node_at()

◆ output_dot()

Member Data Documentation

◆ builtin_function_nodes

◆ eval_string_cache

◆ node_index_pool

◆ string_nodes