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 DEFAULT_MAX_NB_REFINEMENT   std::numeric_limits<size_t>::max()
 
#define CHARACTER_FOR_UNKNOWN   '?'
 

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

◆ CHARACTER_FOR_UNKNOWN

#define CHARACTER_FOR_UNKNOWN   '?'

◆ 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
equationslist of equations
nsnamespace
streamoutput stream
Returns
union_find_replacet structure containing the correspondences.

Definition at line 464 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
    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 1189 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 
)