CBMC
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 (const 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, symbol_generatort &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 61 of file string_refinement.h.

◆ HELP_STRING_REFINEMENT

#define HELP_STRING_REFINEMENT
Value:
" {y--no-refine-strings} \t turn off string refinement\n" \
" {y--string-printable} \t restrict to printable strings and characters\n" \
" {y--string-non-empty} \t restrict to non-empty strings (experimental)\n" \
" {y--string-input-value} {ust} \t " \
"restrict non-null strings to a fixed value {ust}; the switch can be used " \
"multiple times to give several strings\n" \
" {y--max-nondet-string-length} {un} \t " \
"bound the length of nondet (e.g. input) strings. Default is " + \
"; note that setting the value higher than this does not work " \
"with {y--trace} or {y--validate-trace}.\n"
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition: magic.h:14
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.

Definition at line 38 of file string_refinement.h.

◆ HELP_STRING_REFINEMENT_CBMC

#define HELP_STRING_REFINEMENT_CBMC
Value:
" {y--refine-strings} \t use string refinement (experimental)\n" \
" {y--string-printable} \t restrict to printable strings (experimental)\n"

Definition at line 57 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 31 of file string_refinement.h.

◆ OPT_STRING_REFINEMENT_CBMC

#define OPT_STRING_REFINEMENT_CBMC
Value:
"(refine-strings)" \
"(string-printable)"

Definition at line 53 of file string_refinement.h.

Function Documentation

◆ string_identifiers_resolution_from_equations()

union_find_replacet string_identifiers_resolution_from_equations ( const 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 470 of file string_refinement.cpp.

◆ substitute_array_access()

exprt substitute_array_access ( exprt  expr,
symbol_generatort 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_generatora symbol generator
    left_propagateshould values be propagated to the left in with expressions
    Returns
    an expression containing no array access

Definition at line 1281 of file string_refinement.cpp.

◆ substitute_array_lists()

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