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.

void clean_cache ()

Clean the cache used by eval

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.

void clear ()

Clear the content of the dependency graph.

Private Member Functions

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

Applies f on all nodes.

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

Applies f on all successors of the node n.

Private Attributes

std::vector< builtin_function_nodet > builtin_function_nodes

Set of nodes representing builtin_functions.

std::vector< string_nodet > string_nodes

Set of nodes representing strings.

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.

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_exprt s 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 ( )

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