String support via creating string constraints and progressively instantiating the universal constraints as needed. More...

#include <limits>
#include <util/string_expr.h>
#include <util/replace_expr.h>
#include <util/union_find_replace.h>
#include <solvers/refinement/string_constraint.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_refinement_util.h>

Include dependency graph for string_refinement.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	string_refinementt

struct	string_refinementt::configt

struct	string_refinementt::infot
	string_refinementt constructor arguments More...

Macros
#define	DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()

Functions
exprt	substitute_array_lists (exprt expr, std::size_t string_max_length)

union_find_replacet	string_identifiers_resolution_from_equations (std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
	Symbol resolution for expressions of type string typet. More...

exprt	substitute_array_access (exprt expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
	Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expressions, in particular: More...

Detailed Description

String support via creating string constraints and progressively instantiating the universal constraints as needed.

The procedure is described in the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh

Definition in file string_refinement.h.

Macro Definition Documentation

◆ DEFAULT_MAX_NB_REFINEMENT

#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()

Definition at line 32 of file string_refinement.h.

Referenced by cbmc_solverst::get_string_refinement().

Function Documentation

◆ string_identifiers_resolution_from_equations()

union_find_replacet string_identifiers_resolution_from_equations	(	std::vector< equal_exprt > &	equations,
		const namespacet &	ns,
		messaget::mstreamt &	stream
	)

Symbol resolution for expressions of type string typet.

We record equality between these expressions in the output if one of the function calls depends on them.

Parameters

equations	list of equations
ns	namespace
stream	output stream

Returns: union_find_replacet structure containing the correspondences.

Definition at line 458 of file string_refinement.cpp.

References equation_symbol_mappingt::add(), add_string_equation_to_symbol_resolution(), messaget::eom(), extract_strings(), extract_strings_from_lhs(), equation_symbol_mappingt::find_equations(), equation_symbol_mappingt::find_expressions(), format(), has_subtype(), irept::id(), binary_relation_exprt::lhs(), binary_relation_exprt::rhs(), and exprt::type().

Referenced by string_refinementt::dec_solve().

◆ substitute_array_access()

exprt substitute_array_access	(	exprt	expr,
		const std::function< symbol_exprt(const irep_idt &, const typet &)> &	symbol_generator,
		const bool	left_propagate
	)

Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expressions, in particular:

for an array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48
for an array access arr[index], where: arr := array_of(12) with {0:=24} with {2:=42} the constructed expression will be: index==0 ? 24 : index==2 ? 42 : 12
for an array access (g1?arr1:arr2)[x] where arr1 := {12} and arr2 := {34}, the constructed expression will be: g1 ? 12 : 34

for an access in an empty array { }[x] returns a fresh symbol, this corresponds to a non-deterministic result Note that if left_propagate is set to true, the with case will result in something like: index <= 0 ? 24 : index <= 2 ? 42 : 12

Parameters

expr	an expression containing array accesses
symbol_generator	function which given a prefix and a type generates a fresh symbol of the given type
left_propagate	should values be propagated to the left in with expressions

Returns: an expression containing no array access

Definition at line 1170 of file string_refinement.cpp.

References substitute_array_access_in_place().

◆ substitute_array_lists()

exprt substitute_array_lists	(	exprt	expr,
		std::size_t	string_max_length
	)

Classes

Macros