cprover
|
String support via creating string constraints and progressively instantiating the universal constraints as needed. More...
#include <solvers/refinement/string_refinement.h>
#include <iomanip>
#include <numeric>
#include <stack>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/simplify_expr.h>
#include <solvers/sat/satcheck.h>
#include <solvers/refinement/string_constraint_instantiation.h>
#include <unordered_set>
#include <util/magic.h>
Go to the source code of this file.
Classes | |
class | find_qvar_visitort |
Functions | |
static bool | is_valid_string_constraint (messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint) |
static optionalt< exprt > | find_counter_example (const namespacet &ns, const exprt &axiom, const symbol_exprt &var) |
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) |
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 > ¤t_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 exprt | instantiate (messaget::mstreamt &stream, const string_constraintt &axiom, const exprt &str, const exprt &val) |
Substitute qvar the universally quantified variable of axiom , by an index val , in axiom , so that the index used for str equals val . More... | |
static std::vector< exprt > | instantiate (const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const string_constraint_generatort &generator) |
Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms. More... | |
static optionalt< exprt > | get_array (const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr) |
Get a model of an array and put it in a certain form. More... | |
static exprt | substitute_array_access (const index_exprt &index_expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &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< exprt > | generate_instantiations (messaget::mstreamt &stream, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms) |
Instantiation of all constraints. More... | |
static void | make_char_array_pointer_associations (string_constraint_generatort &generator, std::vector< equal_exprt > &equations) |
Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations. More... | |
void | replace_symbols_in_equations (const union_find_replacet &symbol_resolve, std::vector< equal_exprt > &equations) |
static union_find_replacet | generate_symbol_resolution_from_equations (const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream) |
Add association for each char pointer in the equation. More... | |
static std::vector< exprt > | extract_strings_from_lhs (const exprt &lhs) |
This is meant to be used on the lhs of an equation with string subtype. More... | |
static std::vector< exprt > | extract_strings (const exprt &expr) |
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 (std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream) |
Symbol resolution for expressions of type string typet. 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) |
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 > &boolean_symbols, const std::vector< symbol_exprt > &index_symbols) |
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, const std::function< symbol_exprt(const irep_idt &, const typet &)> &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, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate) |
static void | substitute_array_access_in_place (exprt &expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &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, 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... | |
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 std::map< exprt, int > | map_representation_of_sum (const exprt &f) |
static exprt | sum_over_map (std::map< exprt, int > &m, const typet &type, bool negated=false) |
static exprt | compute_inverse_function (messaget::mstreamt &stream, const exprt &qvar, const exprt &val, const exprt &f) |
static bool | find_qvar (const exprt &index, const symbol_exprt &qvar) |
look for the symbol and return true if it is found 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... | |
static std::unordered_set< exprt, irep_hash > | find_indexes (const exprt &expr, const exprt &str, const symbol_exprt &qvar) |
Find indexes of str used in expr that contains qvar , for instance with arguments (str[k+1]=='a') , str , and k , the function should return k+1 . More... | |
exprt | substitute_array_lists (exprt expr, size_t string_max_length) |
Replace array-lists by 'with' expressions. More... | |
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.
|
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.
eq | equation to add |
symbol_resolve | structure to which the equation will be added |
ns | namespace |
Definition at line 425 of file string_refinement.cpp.
References struct_union_typet::components(), has_subtype(), irept::id(), binary_relation_exprt::lhs(), union_find_replacet::make_union(), binary_relation_exprt::rhs(), simplify_expr(), to_struct_type(), and exprt::type().
Referenced by string_identifiers_resolution_from_equations().
|
static |
Add i
to the index set all the indices that appear in the formula.
index_set | set of indexes |
ns | namespace |
s | an expression containing strings |
i | an expression representing an index |
Definition at line 1663 of file string_refinement.cpp.
References index_set_pairt::cumulative, index_set_pairt::current, get_sub_arrays(), irept::id(), numeric_cast(), and simplify().
Referenced by initial_index_set(), and update_index_set().
|
static |
Check axioms takes the model given by the underlying solver and answers whether it satisfies the string constraints.
For each string_constraint a
:
a
is an existential formula b
;b
by their values found in get
;b
is simplified and array accesses are replaced by expressions without arrays;b
to a fresh solver;b
is found, this means the constraint a
is satisfied by the valuation given by get. 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.Definition at line 1245 of file string_refinement.cpp.
References string_constraintt::body, debug_check_axioms_step(), debug_model(), messaget::eom(), find_counter_example(), format(), string_constraint_generatort::fresh_symbol, string_constraint_generatort::fresh_univ_index(), from_integer(), string_constraint_generatort::get_boolean_symbols(), symbol_exprt::get_identifier(), string_constraint_generatort::get_index_symbols(), string_constraint_generatort::get_witness_of(), string_refinementt::instantiate_not_contains(), array_string_exprt::length(), string_constraintt::lower_bound, string_constraintt::negation(), negation_of_not_contains_constraint(), string_axiomst::not_contains, replace_expr(), string_not_contains_constraintt::s0(), simplify_expr(), simplify_sum(), substitute_array_access(), union_find_replacet::to_vector(), exprt::type(), string_constraintt::univ_var, string_constraintt::univ_within_bounds(), string_axiomst::universal, and string_constraintt::upper_bound.
Referenced by string_refinementt::dec_solve().
|
static |
stream | an output stream |
qvar | a symbol representing a universally quantified variable |
val | an expression |
f | an expression containing + and - operations in which qvar should appear exactly once. |
qvar
for f
to be equal to val
. For instance, if f
corresponds to the expression $q + x$, compute_inverse_function(q,v,f)
returns an expression for $v - x$. Definition at line 1533 of file string_refinement.cpp.
References messaget::eom(), INVARIANT, map_representation_of_sum(), neg(), string_refinement_invariantt, sum_over_map(), and exprt::type().
Referenced by instantiate().
|
static |
Debugging function which outputs the different steps an axiom goes through to be checked in check axioms.
T | can be either string_constraintt or string_not_contains_constraintt |
Definition at line 1225 of file string_refinement.cpp.
References format(), and to_string().
Referenced by check_axioms().
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 > & | boolean_symbols, | ||
const std::vector< symbol_exprt > & | index_symbols | ||
) |
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 1015 of file string_refinement.cpp.
References string_constraint_generatort::array_pool, messaget::eom(), format(), array_poolt::get_arrays_of_pointers(), and get_char_array_and_concretize().
Referenced by check_axioms().
|
static |
Write index set to the given stream, use for debugging.
Definition at line 178 of file string_refinement.cpp.
References index_set_pairt::cumulative, index_set_pairt::current, messaget::eom(), and format().
Referenced by string_refinementt::dec_solve().
expr | an expression |
e.x
if e is a symbol subexpression with a field x
of type string Definition at line 397 of file string_refinement.cpp.
References exprt::depth_begin(), exprt::depth_end(), extract_strings_from_lhs(), and irept::id().
Referenced by string_identifiers_resolution_from_equations().
This is meant to be used on the lhs of an equation with string subtype.
lhs | expression which is either of string type, or a symbol representing a struct with some string members |
Definition at line 374 of file string_refinement.cpp.
References struct_union_typet::components(), irept::id(), to_struct_type(), and exprt::type().
Referenced by extract_strings(), and string_identifiers_resolution_from_equations().
|
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
index_value | map containing values of specific vector cells |
Definition at line 136 of file string_refinement.cpp.
|
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.
ns | namespace | |
[in] | axiom | the axiom to be checked |
[in] | var | the variable whose evaluation will be stored in witness |
Definition at line 2054 of file string_refinement.cpp.
References decision_proceduret::D_SATISFIABLE, and solver().
Referenced by check_axioms().
|
static |
Find indexes of str
used in expr
that contains qvar
, for instance with arguments (str[k+1]=='a')
, str
, and k
, the function should return k+1
.
[in] | expr | the expression to search |
[in] | str | the string which must be indexed |
[in] | qvar | the universal variable that must be in the index |
expr
on str
containing qvar
. Definition at line 1818 of file string_refinement.cpp.
References index_exprt::array(), exprt::depth_begin(), exprt::depth_end(), find_qvar(), index_exprt::index(), and to_index_expr().
Referenced by instantiate().
|
static |
look for the symbol and return true if it is found
index | an index expression |
qvar | a symbol expression |
Definition at line 1594 of file string_refinement.cpp.
References find_qvar_visitort::found, and exprt::visit().
Referenced by find_indexes(), and string_constraintt::is_linear_arithmetic_expr().
|
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:
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 &axiom)
for details)
Definition at line 228 of file string_refinement.cpp.
References index_set_pairt::current, instantiate(), string_axiomst::not_contains, and string_axiomst::universal.
Referenced by string_refinementt::dec_solve().
|
static |
Add association for each char pointer in the equation.
equations | vector of equations |
ns | namespace |
stream | output stream |
Definition at line 306 of file string_refinement.cpp.
References struct_union_typet::components(), messaget::eom(), format(), has_char_pointer_subtype(), irept::id(), is_char_pointer_type(), simplify_expr(), solver(), to_struct_type(), and exprt::type().
Referenced by string_refinementt::dec_solve().
|
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.
super_get | function returning the valuation of an expression in a model |
ns | namespace |
stream | output stream for warning messages |
arr | expression of type array representing a string |
Definition at line 894 of file string_refinement.cpp.
References char_type(), CHARACTER_FOR_UNKNOWN, messaget::eom(), format(), from_integer(), irept::id(), index_type(), array_string_exprt::length(), MAX_CONCRETE_STRING_SIZE, numeric_cast(), interval_sparse_arrayt::of_expr(), simplify_expr(), typet::subtype(), and exprt::type().
Referenced by string_refinementt::get(), and get_char_array_and_concretize().
|
static |
Debugging function which finds the valuation of the given array in super_get
and concretize unknown characters.
super_get | give a valuation to variables |
ns | namespace |
stream | output stream |
arr | array expression |
arr
in the model Definition at line 968 of file string_refinement.cpp.
References messaget::eom(), format(), get_array(), simplify_expr(), string_of_array(), to_array_string_expr(), and exprt::type().
Referenced by debug_model().
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
.
array_expr | : an expression representing an array |
accu | a vector to which symbols and constant arrays contained in the expression will be appended |
Definition at line 1636 of file string_refinement.cpp.
References irept::id(), exprt::operands(), to_if_expr(), and exprt::type().
Referenced by add_to_index_set().
|
static |
Definition at line 1723 of file string_refinement.cpp.
References index_exprt::array(), string_constraintt::body, exprt::depth_begin(), exprt::depth_end(), index_exprt::index(), is_char_type(), to_index_expr(), string_constraintt::univ_var, and string_constraintt::upper_bound.
Referenced by string_refinementt::dec_solve(), and initial_index_set().
|
static |
Definition at line 1746 of file string_refinement.cpp.
References add_to_index_set(), array_string_exprt::content(), exprt::depth_begin(), exprt::depth_end(), string_not_contains_constraintt::exists_upper_bound(), from_integer(), is_char_type(), exprt::op0(), exprt::op1(), string_not_contains_constraintt::premise(), string_not_contains_constraintt::s1(), and exprt::type().
|
static |
Add to the index set all the indices that appear in the formulas and the upper bound minus one.
index_set | set of indexes to update |
ns | namespace |
axioms | a list of string axioms |
Definition at line 1606 of file string_refinement.cpp.
References initial_index_set(), string_axiomst::not_contains, and string_axiomst::universal.
|
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:
index_set | the index_set to initialize |
ns | namespace, used for simplifying indexes |
qvar | the quantified variable q |
upper_bound | bound u on the quantified variable |
s | expression representing a string |
i | expression representing the index at which s is accessed |
Definition at line 1696 of file string_refinement.cpp.
References add_to_index_set(), from_integer(), irept::id(), initial_index_set(), exprt::operands(), PRECONDITION, replace_expr(), and exprt::type().
|
static |
Substitute qvar
the universally quantified variable of axiom
, by an index val
, in axiom
, so that the index used for str
equals val
.
Instantiates a string constraint by substituting the quantifiers.
For instance, if axiom
corresponds to \(\forall q.\ s[q+x]='a' \land t[q]='b'\), instantiate(axiom,s,v)
would return an expression for \(s[v]='a' \land t[v-x]='b'\).
stream | output stream |
axiom | a universally quantified formula |
str | an array of char variable |
val | an index expression |
axiom
with substitued qvar
For a string constraint of the form \(\forall q. P(x)\), substitute qvar
the universally quantified variable of axiom
, by an index val
, in axiom
, so that the index used for str
equals val
. For instance, if axiom
corresponds to \(\forall q. s[q+x]={\tt 'a'} \land t[q]={\tt 'b'} \), instantiate(axiom,s,v)
would return an expression for \(s[v]={\tt 'a'} \land t[v-x]={\tt 'b'}\).
stream | a message stream |
axiom | a universally quantified formula axiom |
str | an array of characters |
val | an index expression |
Definition at line 1850 of file string_refinement.cpp.
References string_constraintt::body, compute_inverse_function(), conjunction(), find_indexes(), irept::id(), INVARIANT, string_constraintt::lower_bound, replace_expr(), dstringt::size(), string_constraintt::univ_var, and string_constraintt::upper_bound.
Referenced by generate_instantiations().
|
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.
[in] | axiom | the axiom to instantiate |
index_set | set of indexes | |
generator | constraint generator object |
Definition at line 1894 of file string_refinement.cpp.
References array_string_exprt::content(), index_set_pairt::cumulative, index_set_pairt::current, instantiate_not_contains(), string_not_contains_constraintt::s0(), and string_not_contains_constraintt::s1().
|
related |
Referenced by string_refinementt::dec_solve().
|
static |
Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations.
Definition at line 254 of file string_refinement.cpp.
References string_constraint_generatort::make_array_pointer_association().
Referenced by string_refinementt::dec_solve().
f | an expression with only addition and subtraction |
Definition at line 1400 of file string_refinement.cpp.
References irept::id(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by compute_inverse_function(), and simplify_sum().
|
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.
constraint | the not_contains constraint to add the negation of |
univ_var | the universal variable for the negation of the axiom |
get | valuation function, the result should have been simplified |
Definition at line 1190 of file string_refinement.cpp.
References conjunction(), string_not_contains_constraintt::exists_lower_bound(), string_not_contains_constraintt::exists_upper_bound(), from_integer(), string_not_contains_constraintt::premise(), string_not_contains_constraintt::s0(), string_not_contains_constraintt::s1(), exprt::type(), string_not_contains_constraintt::univ_lower_bound(), and string_not_contains_constraintt::univ_upper_bound().
Referenced by check_axioms().
void replace_symbols_in_equations | ( | const union_find_replacet & | symbol_resolve, |
std::vector< equal_exprt > & | equations | ||
) |
Definition at line 270 of file string_refinement.cpp.
References union_find_replacet::replace_expr().
Referenced by string_refinementt::dec_solve().
f | an expression with only plus and minus expr |
Definition at line 1517 of file string_refinement.cpp.
References map_representation_of_sum(), sum_over_map(), and exprt::type().
Referenced by check_axioms(), and update_index_set().
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.
equations | list of equations |
ns | namespace |
stream | output stream |
Definition at line 458 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().
|
static |
convert the content of a string to a more readable representation.
This should only be used for debugging.
arr | a constant array expression |
Definition at line 951 of file string_refinement.cpp.
References irept::id(), to_array_type(), exprt::type(), and utf16_constant_array_to_java().
Referenced by get_char_array_and_concretize().
|
static |
Definition at line 1104 of file string_refinement.cpp.
References index_exprt::array(), irept::id(), id2string(), index_exprt::index(), INVARIANT, and irept::is_nil().
Referenced by check_axioms(), substitute_array_access(), and substitute_array_access_in_place().
|
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
If left_propagate
is set to true, the expression will look like index<=0 ? 24 : index<=2 ? 42 : 12
expr | A (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. |
index | An index with which to build the equality condition |
Definition at line 1061 of file string_refinement.cpp.
References sparse_arrayt::to_if_expression(), and interval_sparse_arrayt::to_if_expression().
|
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 1076 of file string_refinement.cpp.
References char_type(), typet::subtype(), interval_sparse_arrayt::to_if_expression(), and exprt::type().
|
static |
Definition at line 1088 of file string_refinement.cpp.
References if_exprt::cond(), if_exprt::false_case(), substitute_array_access(), and if_exprt::true_case().
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:
arr[index]
, where: arr := {12, 24, 48}
the constructed expression will be: index==0 ? 12 : index==1 ? 24 : 48
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
(g1?arr1:arr2)[x]
where arr1 := {12}
and arr2 := {34}
, the constructed expression will be: g1 ? 12 : 34
{ }[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
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 |
Definition at line 1170 of file string_refinement.cpp.
References substitute_array_access_in_place().
|
static |
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument instead of returning the resulting expression.
Definition at line 1134 of file string_refinement.cpp.
References exprt::operands(), and substitute_array_access().
Referenced by substitute_array_access().
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.
expr | an expression containing array-list expressions |
string_max_length | maximum length allowed for strings |
Definition at line 1934 of file string_refinement.cpp.
References char_type(), DATA_INVARIANT, from_integer(), irept::id(), exprt::is_constant(), numeric_cast(), exprt::operands(), and string_refinement_invariantt.
|
static |
m | a map from expressions to integers |
type | type for the returned expression |
negated | optinal Boolean asking to negates the sum |
Definition at line 1444 of file string_refinement.cpp.
References binary2integer(), from_integer(), irept::id(), index_type(), irept::is_nil(), irept::is_not_nil(), and to_constant_expr().
Referenced by compute_inverse_function(), and simplify_sum().
|
static |
Add to the index set all the indices that appear in the formulas.
index_set | set of indexes to update |
ns | namespace |
current_constraints | a vector of string constraints |
Definition at line 1621 of file string_refinement.cpp.
Referenced by string_refinementt::dec_solve().
|
static |
Add to the index set all the indices that appear in the formula.
index_set | set of indexes |
ns | namespace |
formula | a string constraint |
Definition at line 1779 of file string_refinement.cpp.
References add_to_index_set(), DATA_INVARIANT, forall_operands, irept::id(), is_char_type(), exprt::op0(), exprt::op1(), simplify_sum(), string_refinement_invariantt, and exprt::type().
|
static |
Definition at line 159 of file string_refinement.cpp.
References bv_refinementt::infot::ns, PRECONDITION, and bv_refinementt::infot::prop.