CBMC
string_refinement.cpp File Reference

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

#include "string_refinement.h"
#include <solvers/sat/satcheck.h>
#include <stack>
#include <unordered_set>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/format_type.h>
#include <util/magic.h>
#include <util/range.h>
#include <util/simplify_expr.h>
#include "equation_symbol_mapping.h"
#include "string_constraint_instantiation.h"
#include "string_dependencies.h"
#include "string_refinement_invariant.h"
+ Include dependency graph for string_refinement.cpp:

Go to the source code of this file.

Functions

static bool is_valid_string_constraint (messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
 
static std::optional< exprtfind_counter_example (const namespacet &ns, const exprt &axiom, const symbol_exprt &var, message_handlert &message_handler)
 Creates a solver with axiom as the only formula added and runs it. More...
 
static std::pair< bool, std::vector< exprt > > check_axioms (const string_axiomst &axioms, string_constraint_generatort &generator, const std::function< exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &not_contain_witnesses)
 Check axioms takes the model given by the underlying solver and answers whether it satisfies the string constraints. More...
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const string_not_contains_constraintt &axiom)
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const string_axiomst &axioms)
 Add to the index set all the indices that appear in the formulas and the upper bound minus one. More...
 
exprt simplify_sum (const exprt &f)
 
static void update_index_set (index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > &current_constraints)
 Add to the index set all the indices that appear in the formulas. More...
 
static void update_index_set (index_set_pairt &index_set, const namespacet &ns, const exprt &formula)
 Add to the index set all the indices that appear in the formula. More...
 
static std::vector< exprtinstantiate (const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
 Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms. More...
 
static std::optional< exprtget_array (const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool)
 Get a model of an array and put it in a certain form. More...
 
static std::optional< exprtsubstitute_array_access (const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
 
template<typename T >
static std::vector< T > fill_in_map_as_vector (const std::map< std::size_t, T > &index_value)
 Convert index-value map to a vector of values. More...
 
static bool validate (const string_refinementt::infot &info)
 
static void display_index_set (messaget::mstreamt &stream, const index_set_pairt &index_set)
 Write index set to the given stream, use for debugging. More...
 
static std::vector< exprtgenerate_instantiations (const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &not_contain_witnesses)
 Instantiation of all constraints. More...
 
static void make_char_array_pointer_associations (string_constraint_generatort &generator, exprt &expr)
 If expr is an equation whose right-hand-side is a associate_array_to_pointer call, add the correspondence and replace the call by an expression representing its result. More...
 
static exprt replace_expr_copy (const union_find_replacet &symbol_resolve, exprt expr)
 Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible. More...
 
static void add_equations_for_symbol_resolution (union_find_replacet &symbol_solver, const std::vector< exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
 Add association for each char pointer in the equation. More...
 
static std::vector< exprtextract_strings_from_lhs (const exprt &lhs, const namespacet &ns)
 This is meant to be used on the lhs of an equation with string subtype. More...
 
static std::vector< exprtextract_strings (const exprt &expr, const namespacet &ns)
 
static void add_string_equation_to_symbol_resolution (const equal_exprt &eq, union_find_replacet &symbol_resolve, const namespacet &ns)
 Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve structure. More...
 
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...
 
static std::optional< exprtget_valid_array_size (const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool)
 Get a model of the size of the input string. More...
 
static std::string string_of_array (const array_exprt &arr)
 convert the content of a string to a more readable representation. More...
 
static exprt get_char_array_and_concretize (const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, array_poolt &array_pool)
 Debugging function which finds the valuation of the given array in super_get and concretize unknown characters. More...
 
void debug_model (const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &symbols, array_poolt &array_pool)
 Display part of the current model by mapping the variables created by the solver to constant expressions given by the current model. More...
 
static exprt substitute_array_access (const with_exprt &expr, const exprt &index, const bool left_propagate)
 Create a new expression where 'with' expressions on arrays are replaced by 'if' expressions. More...
 
static exprt substitute_array_access (const array_exprt &array_expr, const exprt &index, symbol_generatort &symbol_generator)
 Create an equivalent expression where array accesses are replaced by 'if' expressions: for instance in array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48 Avoids repetition so arr := {12, 12, 24, 48} will give index<=1 ? 12 : index==1 ? 24 : 48 More...
 
static exprt substitute_array_access (const if_exprt &if_expr, const exprt &index, symbol_generatort &symbol_generator, const bool left_propagate)
 
static void substitute_array_access_in_place (exprt &expr, symbol_generatort &symbol_generator, const bool left_propagate)
 Auxiliary function for substitute_array_access Performs the same operation but modifies the argument instead of returning the resulting expression. 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...
 
static exprt negation_of_not_contains_constraint (const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, const std::function< exprt(const exprt &)> &get)
 Negates the constraint to be fed to a solver. More...
 
template<typename T >
static void debug_check_axioms_step (messaget::mstreamt &stream, const T &axiom, const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays)
 Debugging function which outputs the different steps an axiom goes through to be checked in check axioms. More...
 
static void get_sub_arrays (const exprt &array_expr, std::vector< exprt > &accu)
 An expression representing an array of characters can be in the form of an if expression for instance cond?array1:(cond2:array2:array3). More...
 
static void add_to_index_set (index_set_pairt &index_set, const namespacet &ns, const exprt &s, exprt i)
 Add i to the index set all the indices that appear in the formula. More...
 
static void initial_index_set (index_set_pairt &index_set, const namespacet &ns, const exprt &qvar, const exprt &upper_bound, const exprt &s, const exprt &i)
 Given an array access of the form s[i] assumed to be part of a formula \( \forall q < u. charconstraint \), initialize the index set of s so that: More...
 
exprt substitute_array_lists (exprt expr, size_t string_max_length)
 Replace array-lists by 'with' expressions. 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.cpp.

Function Documentation

◆ add_equations_for_symbol_resolution()

static void add_equations_for_symbol_resolution ( union_find_replacet symbol_solver,
const std::vector< exprt > &  equations,
const namespacet ns,
messaget::mstreamt stream 
)
static

Add association for each char pointer in the equation.

Parameters
[in,out]symbol_solvera union_find_replacet object to keep track of char pointer equations. Char pointers that have been set equal by an equation are associated to the same element.
equationsvector of equations
nsnamespace
streamoutput stream

Definition at line 300 of file string_refinement.cpp.

◆ add_string_equation_to_symbol_resolution()

static void add_string_equation_to_symbol_resolution ( const equal_exprt eq,
union_find_replacet symbol_resolve,
const namespacet ns 
)
static

Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve structure.

The lhs and rhs of the equation, should have string type or be struct with string members.

Parameters
eqequation to add
symbol_resolvestructure to which the equation will be added
nsnamespace

Definition at line 426 of file string_refinement.cpp.

◆ add_to_index_set()

static void add_to_index_set ( index_set_pairt index_set,
const namespacet ns,
const exprt s,
exprt  i 
)
static

Add i to the index set all the indices that appear in the formula.

Parameters
index_setset of indexes
nsnamespace
san expression containing strings
ian expression representing an index

Definition at line 1575 of file string_refinement.cpp.

◆ check_axioms()

static std::pair< bool, std::vector< exprt > > check_axioms ( const string_axiomst axioms,
string_constraint_generatort generator,
const std::function< exprt(const exprt &)> &  get,
messaget::mstreamt stream,
const namespacet ns,
bool  use_counter_example,
const union_find_replacet symbol_resolve,
const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  not_contain_witnesses 
)
static

Check axioms takes the model given by the underlying solver and answers whether it satisfies the string constraints.

For each string_constraint a:

  • the negation of a is an existential formula b;
  • we substituted symbols in b by their values found in get;
  • arrays are concretized, meaning we attribute a value for characters that are unknown to get, for details see substitute_array_access;
  • b is simplified and array accesses are replaced by expressions without arrays;
  • we give lemma b to a fresh solver;
  • if no counter-example to b is found, this means the constraint a is satisfied by the valuation given by get.
    Returns
    true if the current model satisfies all the axioms, false otherwise with a list of lemmas which are obtained by instantiating constraints at indexes given by counter-examples.
    true if the current model satisfies all the axioms

Definition at line 1353 of file string_refinement.cpp.

◆ debug_check_axioms_step()

template<typename T >
static void debug_check_axioms_step ( messaget::mstreamt stream,
const T &  axiom,
const T &  axiom_in_model,
const exprt negaxiom,
const exprt with_concretized_arrays 
)
static

Debugging function which outputs the different steps an axiom goes through to be checked in check axioms.

Template Parameters
Tcan be either string_constraintt or string_not_contains_constraintt

Definition at line 1333 of file string_refinement.cpp.

◆ debug_model()

void debug_model ( const string_constraint_generatort generator,
messaget::mstreamt stream,
const namespacet ns,
const std::function< exprt(const exprt &)> &  super_get,
const std::vector< symbol_exprt > &  symbols,
array_poolt array_pool 
)

Display part of the current model by mapping the variables created by the solver to constant expressions given by the current model.

Definition at line 1118 of file string_refinement.cpp.

◆ display_index_set()

static void display_index_set ( messaget::mstreamt stream,
const index_set_pairt index_set 
)
static

Write index set to the given stream, use for debugging.

Definition at line 172 of file string_refinement.cpp.

◆ extract_strings()

static std::vector<exprt> extract_strings ( const exprt expr,
const namespacet ns 
)
static
Parameters
expran expression
nsnamespace to resolve type tags
Returns
all subexpressions of type string which are not if_exprt expressions this includes expressions of the form e.x if e is a symbol subexpression with a field x of type string

Definition at line 398 of file string_refinement.cpp.

◆ extract_strings_from_lhs()

static std::vector<exprt> extract_strings_from_lhs ( const exprt lhs,
const namespacet ns 
)
static

This is meant to be used on the lhs of an equation with string subtype.

Parameters
lhsexpression which is either of string type, or a symbol representing a struct with some string members
nsnamespace to resolve type tags
Returns
if lhs is a string return this string, if it is a struct return the members of the expression that have string type.

Definition at line 373 of file string_refinement.cpp.

◆ fill_in_map_as_vector()

template<typename T >
static std::vector<T> fill_in_map_as_vector ( const std::map< std::size_t, T > &  index_value)
static

Convert index-value map to a vector of values.

If a value for an index is not defined, set it to the value referenced by the next higher index. The length of the resulting vector is the key of the map's last element + 1

Parameters
index_valuemap containing values of specific vector cells
Returns
Vector containing values as described in the map

Definition at line 130 of file string_refinement.cpp.

◆ find_counter_example()

static std::optional< exprt > find_counter_example ( const namespacet ns,
const exprt axiom,
const symbol_exprt var,
message_handlert message_handler 
)
static

Creates a solver with axiom as the only formula added and runs it.

If it is SAT, then true is returned and the given evaluation of var is stored in witness. If UNSAT, then what witness is is undefined.

Parameters
nsnamespace
[in]axiomthe axiom to be checked
[in]varthe variable whose evaluation will be stored in witness
message_handlermessage handler
Returns
the witness of the satisfying assignment if one exists. If UNSAT, then behaviour is undefined.

Definition at line 1910 of file string_refinement.cpp.

◆ generate_instantiations()

static std::vector<exprt> generate_instantiations ( const index_set_pairt index_set,
const string_axiomst axioms,
const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  not_contain_witnesses 
)
static

Instantiation of all constraints.

The string refinement decision procedure works with two types of quantified axioms, which are of the form \(\forall x.\ P(x)\) (string_constraintt) or of the form \(\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y] \) (string_not_contains_constraintt). They are instantiated in a way which depends on their form:

  • For formulas of the form \(\forall x.\ P(x)\) if string str appears in P indexed by some f(x) and val is in the index set of str we find y such that f(y)=val and add lemma P(y). (See instantiate(messaget::mstreamt&, const string_constraintt&, const exprt &, const exprt&) for details.)
  • For formulas of the form \(\forall x. P(x) \Rightarrow \exists y .s_0[x+y] \ne s_1[y]) \) we need to look at the index set of both s_0 and s_1. (See instantiate(const string_not_contains_constraintt&, const index_set_pairt&, const std::map<string_not_contains_constraintt, symbol_exprt>&) for details.)

Definition at line 220 of file string_refinement.cpp.

◆ get_array()

static std::optional< exprt > get_array ( const std::function< exprt(const exprt &)> &  super_get,
const namespacet ns,
messaget::mstreamt stream,
const array_string_exprt arr,
const array_poolt array_pool 
)
static

Get a model of an array and put it in a certain form.

If the model is incomplete or if it is too big, return no value.

Parameters
super_getfunction returning the valuation of an expression in a model
nsnamespace
streamoutput stream for warning messages
arrexpression of type array representing a string
array_poolpool of arrays representing strings
Returns
an optional array expression or array_of_exprt

Definition at line 1004 of file string_refinement.cpp.

◆ get_char_array_and_concretize()

static exprt get_char_array_and_concretize ( const std::function< exprt(const exprt &)> &  super_get,
const namespacet ns,
messaget::mstreamt stream,
const array_string_exprt arr,
array_poolt array_pool 
)
static

Debugging function which finds the valuation of the given array in super_get and concretize unknown characters.

Parameters
super_getgive a valuation to variables
nsnamespace
streamoutput stream
arrarray expression
array_poolpool of arrays representing strings
Returns
expression corresponding to arr in the model

Definition at line 1070 of file string_refinement.cpp.

◆ get_sub_arrays()

static void get_sub_arrays ( const exprt array_expr,
std::vector< exprt > &  accu 
)
static

An expression representing an array of characters can be in the form of an if expression for instance cond?array1:(cond2:array2:array3).

We return all the array expressions contained in array_expr.

Parameters
array_expran expression representing an array
accua vector to which symbols and constant arrays contained in the expression will be appended

Definition at line 1548 of file string_refinement.cpp.

◆ get_valid_array_size()

static std::optional<exprt> get_valid_array_size ( const std::function< exprt(const exprt &)> &  super_get,
const namespacet ns,
messaget::mstreamt stream,
const array_string_exprt arr,
const array_poolt array_pool 
)
static

Get a model of the size of the input string.

First ask the solver for a size value. If the solver has no value, get the size directly from the type. This is the case for string literals that are not part of the decision procedure (e.g. literals in return values). If the size value is not a constant or not a valid integer (size_t), return no value.

Parameters
super_getfunction returning the valuation of an expression in a model
nsnamespace
streamoutput stream for warning messages
arrexpression of type array representing a string
array_poolpool of arrays representing strings
Returns
an optional expression representing the size of the array that can be cast to size_t

Definition at line 960 of file string_refinement.cpp.

◆ initial_index_set() [1/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const exprt qvar,
const exprt upper_bound,
const exprt s,
const exprt i 
)
static

Given an array access of the form s[i] assumed to be part of a formula \( \forall q < u. charconstraint \), initialize the index set of s so that:

  • \( i[q -> u - 1] \) appears in the index set of s if s is a symbol
  • if s is an array expression, all index from 0 to \( s.length - 1 \) are in the index set
  • if s is an if expression we apply this procedure to the true and false cases
    Parameters
    index_setthe index_set to initialize
    nsnamespace, used for simplifying indexes
    qvarthe quantified variable q
    upper_boundbound u on the quantified variable
    sexpression representing a string
    iexpression representing the index at which s is accessed

Definition at line 1608 of file string_refinement.cpp.

◆ initial_index_set() [2/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const string_axiomst axioms 
)
static

Add to the index set all the indices that appear in the formulas and the upper bound minus one.

Parameters
index_setset of indexes to update
nsnamespace
axiomsa list of string axioms

Definition at line 1518 of file string_refinement.cpp.

◆ initial_index_set() [3/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const string_constraintt axiom 
)
static

Definition at line 1637 of file string_refinement.cpp.

◆ initial_index_set() [4/4]

static void initial_index_set ( index_set_pairt index_set,
const namespacet ns,
const string_not_contains_constraintt axiom 
)
static

Definition at line 1660 of file string_refinement.cpp.

◆ instantiate()

static std::vector< exprt > instantiate ( const string_not_contains_constraintt axiom,
const index_set_pairt index_set,
const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &  witnesses 
)
static

Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms.

For a formula of the form \(\phi = \forall x. P(x) \Rightarrow Q(x, f(x))\) let \(instantiate\_not\_contains(\phi) = ( (f(t) = u) \land P(t) ) \Rightarrow Q(t, u)\). Then \(\forall x.\ P(x) \Rightarrow Q(x, f(x)) \models \) Axioms of the form \(\forall x. P(x) \Rightarrow \exists y .Q(x, y) \) can be transformed into the the equisatisfiable formula \(\forall x. P(x) \Rightarrow Q(x, f(x))\) for a new function symbol f. Hence, after transforming axioms of the second type and by the above lemmas, we can create quantifier free formulas that are entailed by a (transformed) axiom.

Parameters
[in]axiomthe axiom to instantiate
index_setset of indexes
witnessesaxiom's witnesses for non-containment
Returns
the lemmas produced through instantiation

Definition at line 1741 of file string_refinement.cpp.

◆ is_valid_string_constraint()

static bool is_valid_string_constraint ( messaget::mstreamt stream,
const namespacet ns,
const string_constraintt constraint 
)
related

◆ make_char_array_pointer_associations()

static void make_char_array_pointer_associations ( string_constraint_generatort generator,
exprt expr 
)
static

If expr is an equation whose right-hand-side is a associate_array_to_pointer call, add the correspondence and replace the call by an expression representing its result.

Definition at line 247 of file string_refinement.cpp.

◆ negation_of_not_contains_constraint()

static exprt negation_of_not_contains_constraint ( const string_not_contains_constraintt constraint,
const symbol_exprt univ_var,
const std::function< exprt(const exprt &)> &  get 
)
static

Negates the constraint to be fed to a solver.

The intended usage is to find an assignment of the universal variable that would violate the axiom. To avoid false positives, the symbols other than the universal variable should have been replaced by their valuation in the current model.

Precondition
Symbols other than the universal variable should have been replaced by their valuation in the current model.
Parameters
constraintthe not_contains constraint to add the negation of
univ_varthe universal variable for the negation of the axiom
getvaluation function, the result should have been simplified
Returns
the negation of the axiom under the current evaluation

Definition at line 1292 of file string_refinement.cpp.

◆ replace_expr_copy()

static exprt replace_expr_copy ( const union_find_replacet symbol_resolve,
exprt  expr 
)
static

Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible.

Similar to symbol_resolve.replace_expr but doesn't mutate the expression and returns the transformed expression instead.

Definition at line 273 of file string_refinement.cpp.

◆ simplify_sum()

exprt simplify_sum ( const exprt f)
Parameters
fan expression with only plus and minus expr
Returns
an equivalent expression in a canonical form

Definition at line 1508 of file string_refinement.cpp.

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

◆ string_of_array()

static std::string string_of_array ( const array_exprt arr)
static

convert the content of a string to a more readable representation.

This should only be used for debugging.

Parameters
arra constant array expression
Returns
a string

Definition at line 1052 of file string_refinement.cpp.

◆ substitute_array_access() [1/5]

static exprt substitute_array_access ( const array_exprt array_expr,
const exprt index,
symbol_generatort symbol_generator 
)
static

Create an equivalent expression where array accesses are replaced by 'if' expressions: for instance in array access arr[index], where: arr := {12, 24, 48} the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48 Avoids repetition so arr := {12, 12, 24, 48} will give index<=1 ? 12 : index==1 ? 24 : 48

Definition at line 1173 of file string_refinement.cpp.

◆ substitute_array_access() [2/5]

static exprt substitute_array_access ( const if_exprt if_expr,
const exprt index,
symbol_generatort symbol_generator,
const bool  left_propagate 
)
static

Definition at line 1184 of file string_refinement.cpp.

◆ substitute_array_access() [3/5]

static std::optional< exprt > substitute_array_access ( const index_exprt index_expr,
symbol_generatort symbol_generator,
const bool  left_propagate 
)
static

Definition at line 1205 of file string_refinement.cpp.

◆ substitute_array_access() [4/5]

static exprt substitute_array_access ( const with_exprt expr,
const exprt index,
const bool  left_propagate 
)
static

Create a new expression where 'with' expressions on arrays are replaced by 'if' expressions.

e.g. 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

Parameters
exprA (possibly nested) 'with' expression on an array_of expression. The function checks that the expression is of the form with_expr(with_expr(...(array_of(...))). This is the form in which array valuations coming from the underlying solver are given.
indexAn index with which to build the equality condition
left_propagateIf set to true, the expression will look like index<=0 ? 24 : index<=2 ? 42 : 12
Returns
An expression containing no 'with' expression

Definition at line 1158 of file string_refinement.cpp.

◆ substitute_array_access() [5/5]

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

◆ substitute_array_access_in_place()

static void substitute_array_access_in_place ( exprt expr,
symbol_generatort symbol_generator,
const bool  left_propagate 
)
static

Auxiliary function for substitute_array_access Performs the same operation but modifies the argument instead of returning the resulting expression.

Definition at line 1234 of file string_refinement.cpp.

◆ substitute_array_lists()

exprt substitute_array_lists ( exprt  expr,
size_t  string_max_length 
)

Replace array-lists by 'with' expressions.

For instance array-list [ 0 , x , 1 , y ] is replaced by ARRAYOF(0) WITH [0:=x] WITH [1:=y]. Indexes exceeding the maximal string length are ignored.

Parameters
expran expression containing array-list expressions
string_max_lengthmaximum length allowed for strings
Returns
an expression containing no array-list

Definition at line 1783 of file string_refinement.cpp.

◆ update_index_set() [1/2]

static void update_index_set ( index_set_pairt index_set,
const namespacet ns,
const exprt formula 
)
static

Add to the index set all the indices that appear in the formula.

Parameters
index_setset of indexes
nsnamespace
formulaa string constraint

Definition at line 1692 of file string_refinement.cpp.

◆ update_index_set() [2/2]

static void update_index_set ( index_set_pairt index_set,
const namespacet ns,
const std::vector< exprt > &  current_constraints 
)
static

Add to the index set all the indices that appear in the formulas.

Parameters
index_setset of indexes to update
nsnamespace
current_constraintsa vector of string constraints

Definition at line 1533 of file string_refinement.cpp.

◆ validate()

static bool validate ( const string_refinementt::infot info)
static

Definition at line 150 of file string_refinement.cpp.