string_refinement.h File Reference

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	OPT_STRING_REFINEMENT
#define	HELP_STRING_REFINEMENT
#define	OPT_STRING_REFINEMENT_CBMC
#define	HELP_STRING_REFINEMENT_CBMC
#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 60 of file string_refinement.h.

HELP_STRING_REFINEMENT

#define HELP_STRING_REFINEMENT

Value:

" --no-refine-strings          turn off string refinement\n" \
  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
  " --string-non-empty           restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
  " --string-printable st        restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \
  "                              the switch can be used multiple times to give\n" /* NOLINT(*) */ \
  "                              several strings\n" /* NOLINT(*) */ \
  " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */

Definition at line 40 of file string_refinement.h.

HELP_STRING_REFINEMENT_CBMC

#define HELP_STRING_REFINEMENT_CBMC

Value:

" --refine-strings             use string refinement (experimental)\n" \
  " --string-printable           restrict to printable strings (experimental)\n" /* NOLINT(*) */

Definition at line 55 of file string_refinement.h.

OPT_STRING_REFINEMENT

#define OPT_STRING_REFINEMENT

Value:

"(no-refine-strings)" \
  "(string-printable)" \
  "(string-input-value):" \
  "(string-non-empty)" \
  "(max-nondet-string-length):"

Definition at line 33 of file string_refinement.h.

OPT_STRING_REFINEMENT_CBMC

#define OPT_STRING_REFINEMENT_CBMC

Value:

"(refine-strings)" \
  "(string-printable)"

Definition at line 51 of file string_refinement.h.

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 463 of file string_refinement.cpp.

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 1169 of file string_refinement.cpp.

substitute_array_lists()

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