cprover
string_refinement.h File Reference

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

+ 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
equationslist of equations
nsnamespace
streamoutput 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
    expran expression containing array accesses
    symbol_generatorfunction which given a prefix and a type generates a fresh symbol of the given type
    left_propagateshould 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 
)