cprover
|
#include <string_refinement.h>
Classes | |
struct | configt |
struct | infot |
string_refinementt constructor arguments More... | |
Public Member Functions | |
string_refinementt (const infot &) | |
std::string | decision_procedure_text () const override |
exprt | get (const exprt &expr) const override |
Evaluates the given expression in the valuation found by string_refinementt::dec_solve. More... | |
void | set_to (const exprt &expr, bool value) override |
Record the constraints to ensure that the expression is true when the boolean is true and false otherwise. More... | |
decision_proceduret::resultt | dec_solve () override |
Main decision procedure of the solver. More... | |
![]() | |
bv_refinementt (const infot &info) | |
![]() | |
bv_pointerst (const namespacet &_ns, propt &_prop) | |
void | post_process () override |
![]() | |
boolbvt (const namespacet &_ns, propt &_prop) | |
virtual const bvt & | convert_bv (const exprt &expr) |
void | print_assignment (std::ostream &out) const override |
void | clear_cache () override |
virtual bool | literal (const exprt &expr, std::size_t bit, literalt &literal) const |
mp_integer | get_value (const bvt &bv) |
mp_integer | get_value (const bvt &bv, std::size_t offset, std::size_t width) |
const boolbv_mapt & | get_map () const |
![]() | |
arrayst (const namespacet &_ns, propt &_prop) | |
literalt | record_array_equality (const equal_exprt &expr) |
void | record_array_index (const index_exprt &expr) |
![]() | |
equalityt (const namespacet &_ns, propt &_prop) | |
virtual literalt | equality (const exprt &e1, const exprt &e2) |
void | post_process () override |
![]() | |
prop_conv_solvert (const namespacet &_ns, propt &_prop) | |
virtual | ~prop_conv_solvert ()=default |
void | print_assignment (std::ostream &out) const override |
virtual tvt | l_get (literalt a) const override |
void | set_frozen (literalt a) override |
bool | has_set_assumptions () const override |
void | set_all_frozen () override |
literalt | convert (const exprt &expr) override |
bool | is_in_conflict (literalt l) const override |
determine whether a variable is in the final conflict More... | |
bool | has_is_in_conflict () const override |
virtual bool | literal (const exprt &expr, literalt &literal) const |
const cachet & | get_cache () const |
const symbolst & | get_symbols () const |
void | set_time_limit_seconds (uint32_t lim) override |
virtual void | set_frozen (literalt a) |
virtual void | set_frozen (const bvt &) |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual void | set_frozen (const bvt &) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
resultt | operator() () |
Private Types | |
typedef bv_refinementt | supert |
Private Member Functions | |
string_refinementt (const infot &, bool) | |
void | add_lemma (const exprt &lemma, bool simplify_lemma=true) |
Add the given lemma to the solver. More... | |
Private Attributes | |
const configt | config_ |
std::size_t | loop_bound_ |
std::size_t | max_string_length |
string_constraint_generatort | generator |
std::set< exprt > | seen_instances |
string_axiomst | axioms |
std::vector< exprt > | current_constraints |
index_set_pairt | index_sets |
union_find_replacet | symbol_resolve |
std::vector< equal_exprt > | equations |
string_dependenciest | dependencies |
Related Functions | |
(Note that these are not member functions.) | |
std::vector< exprt > | instantiate_not_contains (const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const string_constraint_generatort &generator) |
Instantiates a quantified formula representing not_contains by substituting the quantifiers and generating axioms. More... | |
Additional Inherited Members | |
![]() | |
enum | unbounded_arrayt { unbounded_arrayt::U_NONE, unbounded_arrayt::U_ALL, unbounded_arrayt::U_AUTO } |
![]() | |
typedef equalityt | SUB |
![]() | |
typedef std::map< irep_idt, literalt > | symbolst |
typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
![]() | |
unbounded_arrayt | unbounded_array |
boolbv_widtht | boolbv_width |
![]() | |
bool | use_cache = true |
bool | equality_propagation = true |
bool | freeze_all = false |
![]() | |
typedef boolbvt | SUB |
typedef std::list< postponedt > | postponed_listt |
![]() | |
typedef arrayst | SUB |
typedef std::unordered_map< const exprt, bvt, irep_hash > | bv_cachet |
typedef std::list< quantifiert > | quantifier_listt |
typedef std::vector< std::size_t > | offset_mapt |
![]() | |
enum | lazy_typet { lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF, lazy_typet::ARRAY_TYPECAST } |
typedef std::list< array_equalityt > | array_equalitiest |
typedef std::set< exprt > | index_sett |
typedef std::map< std::size_t, index_sett > | index_mapt |
![]() | |
typedef std::unordered_map< const exprt, unsigned, irep_hash > | elementst |
typedef std::map< std::pair< unsigned, unsigned >, literalt > | equalitiest |
typedef std::map< unsigned, exprt > | elements_revt |
typedef std::unordered_map< const typet, typestructt, irep_hash > | typemapt |
![]() | |
void | post_process_arrays () override |
generate array constraints More... | |
bvt | convert_mult (const exprt &expr) override |
bvt | convert_div (const div_exprt &expr) override |
bvt | convert_mod (const mod_exprt &expr) override |
bvt | convert_floatbv_op (const exprt &expr) override |
void | set_assumptions (const bvt &_assumptions) override |
![]() | |
void | encode (std::size_t object, bvt &bv) |
virtual bvt | convert_pointer_type (const exprt &expr) |
virtual void | add_addr (const exprt &expr, bvt &bv) |
literalt | convert_rest (const exprt &expr) override |
bvt | convert_bitvector (const exprt &expr) override |
Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit. More... | |
exprt | bv_get_rec (const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override |
bool | convert_address_of_rec (const exprt &expr, bvt &bv) |
void | offset_arithmetic (bvt &bv, const mp_integer &x) |
void | offset_arithmetic (bvt &bv, const mp_integer &factor, const exprt &index) |
void | offset_arithmetic (bvt &bv, const mp_integer &factor, const bvt &index_bv) |
void | do_postponed (const postponedt &postponed) |
![]() | |
virtual bool | boolbv_set_equality_to_true (const equal_exprt &expr) |
void | conversion_failed (const exprt &expr, bvt &bv) |
bvt | conversion_failed (const exprt &expr) |
bool | type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest) |
virtual literalt | convert_bv_rel (const exprt &expr) |
virtual literalt | convert_typecast (const typecast_exprt &expr) |
conversion from bitvector types to boolean More... | |
virtual literalt | convert_reduction (const unary_exprt &expr) |
virtual literalt | convert_onehot (const unary_exprt &expr) |
virtual literalt | convert_extractbit (const extractbit_exprt &expr) |
virtual literalt | convert_overflow (const exprt &expr) |
virtual literalt | convert_equality (const equal_exprt &expr) |
virtual literalt | convert_verilog_case_equality (const binary_relation_exprt &expr) |
virtual literalt | convert_ieee_float_rel (const exprt &expr) |
virtual literalt | convert_quantifier (const exprt &expr) |
virtual bvt | convert_index (const exprt &array, const mp_integer &index) |
index operator with constant index More... | |
virtual bvt | convert_index (const index_exprt &expr) |
virtual bvt | convert_bswap (const bswap_exprt &expr) |
virtual bvt | convert_byte_extract (const byte_extract_exprt &expr) |
virtual bvt | convert_byte_update (const byte_update_exprt &expr) |
virtual bvt | convert_constraint_select_one (const exprt &expr) |
virtual bvt | convert_if (const if_exprt &expr) |
virtual bvt | convert_struct (const struct_exprt &expr) |
virtual bvt | convert_array (const exprt &expr) |
virtual bvt | convert_vector (const exprt &expr) |
virtual bvt | convert_complex (const exprt &expr) |
virtual bvt | convert_complex_real (const exprt &expr) |
virtual bvt | convert_complex_imag (const exprt &expr) |
virtual bvt | convert_lambda (const exprt &expr) |
virtual bvt | convert_let (const let_exprt &) |
virtual bvt | convert_array_of (const array_of_exprt &expr) |
virtual bvt | convert_union (const union_exprt &expr) |
virtual bvt | convert_bv_typecast (const typecast_exprt &expr) |
virtual bvt | convert_add_sub (const exprt &expr) |
virtual bvt | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
virtual bvt | convert_member (const member_exprt &expr) |
virtual bvt | convert_with (const exprt &expr) |
virtual bvt | convert_update (const exprt &expr) |
virtual bvt | convert_case (const exprt &expr) |
virtual bvt | convert_cond (const exprt &expr) |
virtual bvt | convert_shift (const binary_exprt &expr) |
virtual bvt | convert_bitwise (const exprt &expr) |
virtual bvt | convert_unary_minus (const unary_exprt &expr) |
virtual bvt | convert_abs (const abs_exprt &expr) |
virtual bvt | convert_concatenation (const exprt &expr) |
virtual bvt | convert_replication (const replication_exprt &expr) |
virtual bvt | convert_bv_literals (const exprt &expr) |
virtual bvt | convert_constant (const constant_exprt &expr) |
virtual bvt | convert_extractbits (const extractbits_exprt &expr) |
virtual bvt | convert_symbol (const exprt &expr) |
virtual bvt | convert_bv_reduction (const unary_exprt &expr) |
virtual bvt | convert_not (const not_exprt &expr) |
virtual bvt | convert_power (const binary_exprt &expr) |
virtual bvt | convert_function_application (const function_application_exprt &expr) |
virtual exprt | make_bv_expr (const typet &type, const bvt &bv) |
virtual exprt | make_free_bv_expr (const typet &type) |
void | convert_with (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_bv (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_array (const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_union (const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_struct (const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_update_rec (const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv) |
virtual exprt | bv_get_unbounded_array (const exprt &) const |
exprt | bv_get (const bvt &bv, const typet &type) const |
exprt | bv_get_cache (const exprt &expr) const |
bool | is_unbounded_array (const typet &type) const override |
void | post_process_quantifiers () |
offset_mapt | build_offset_map (const struct_typet &src) |
![]() | |
void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
adds array constraints (refine=true...lazily for the refinement loop) More... | |
void | add_array_constraints () |
void | add_array_Ackermann_constraints () |
void | add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality) |
void | add_array_constraints (const index_sett &index_set, const exprt &expr) |
void | add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt) |
void | add_array_constraints_with (const index_sett &index_set, const with_exprt &expr) |
void | add_array_constraints_update (const index_sett &index_set, const update_exprt &expr) |
void | add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt) |
void | update_index_map (bool update_all) |
void | update_index_map (std::size_t i) |
merge the indices into the root More... | |
void | collect_arrays (const exprt &a) |
void | collect_indices () |
void | collect_indices (const exprt &a) |
![]() | |
virtual literalt | equality2 (const exprt &e1, const exprt &e2) |
virtual void | add_equality_constraints () |
virtual void | add_equality_constraints (const typestructt &typestruct) |
![]() | |
virtual bool | get_bool (const exprt &expr, tvt &value) const |
get a boolean value from counter example if not valid More... | |
virtual literalt | convert_bool (const exprt &expr) |
virtual bool | set_equality_to_true (const equal_exprt &expr) |
virtual literalt | get_literal (const irep_idt &symbol) |
virtual void | ignoring (const exprt &expr) |
![]() | |
configt | config_ |
![]() | |
pointer_logict | pointer_logic |
unsigned | object_bits |
unsigned | offset_bits |
unsigned | bits |
postponed_listt | postponed_list |
![]() | |
bv_utilst | bv_utils |
functionst | functions |
boolbv_mapt | map |
bv_cachet | bv_cache |
quantifier_listt | quantifier_list |
numbering< irep_idt > | string_numbering |
![]() | |
array_equalitiest | array_equalities |
union_find< exprt > | arrays |
index_mapt | index_map |
bool | lazy_arrays |
bool | incremental_cache |
std::list< lazy_constraintt > | lazy_array_constraints |
std::map< exprt, bool > | expr_map |
std::set< std::size_t > | update_indices |
![]() | |
typemapt | typemap |
![]() | |
bool | post_processing_done = false |
symbolst | symbols |
cachet | cache |
propt & | prop |
![]() | |
const namespacet & | ns |
Definition at line 35 of file string_refinement.h.
|
private |
Definition at line 64 of file string_refinement.h.
|
explicit |
Definition at line 179 of file string_refinement.cpp.
|
private |
Definition at line 170 of file string_refinement.cpp.
|
private |
Add the given lemma to the solver.
lemma | a Boolean expression |
simplify_lemma | whether the lemma should be simplified before being given to the underlying solver. |
Definition at line 854 of file string_refinement.cpp.
References CHARACTER_FOR_UNKNOWN, prop_conv_solvert::convert(), current_constraints, messaget::debug(), exprt::depth_begin(), exprt::depth_end(), messaget::eom(), format(), from_integer(), exprt::is_true(), propt::l_set_to_true(), decision_proceduret::ns, prop_conv_solvert::prop, union_find_replacet::replace_expr(), seen_instances, simplify(), symbol_resolve, and to_array_type().
Referenced by dec_solve().
|
overridevirtual |
Main decision procedure of the solver.
Looks for a valuation of variables compatible with the constraints that have been given to set_to
so far.
The decision procedure initiated by string_refinementt::dec_solve is composed of several steps detailed below.
Pointer symbols which are set to be equal by constraints, are replaced by an single symbol in the solver. The symbol_solvert
object used for this substitution is constructed by generate_symbol_resolution_from_equations(const std::vector<equal_exprt>&,const namespacet&,messaget::mstreamt&)
. All these symbols are then replaced using replace_symbols_in_equations(const union_find_replacet &, std::vector<equal_exprt> &)
.
Each string primitive is converted to a list of first order formulas by the function substitute_function_applications_in_equations(std::vector<equal_exprt>&,string_constraint_generatort&)
. These formulas should be unquantified or be either a string_constraintt
or a string_not_contains_constraintt
. The constraints corresponding to each primitive can be found by following the links in section String primitives.
Since only arrays appear in the string constraints, during the conversion to first order formulas, pointers are associated to arrays. The string_constraint_generatort
object keeps track of this association. It can either be set manually using the primitives cprover_associate_array_to_pointer
or a fresh array is created.
We use super_dec_solve
and super_get
to denote the methods of the underlying solver (bv_refinementt
by default). The refinement loop relies on functions string_refinementt::check_axioms
which returns true when the set of quantified constraints q
is satisfied by the valuation given bysuper_get
and string_refinementt::instantiate
which gives propositional formulas implied by a string constraint. If the following algorithm returns SAT
or UNSAT
, the given constraints are SAT
or UNSAT
respectively:
resultt::D_SATISFIABLE
if the constraints are satisfiable, resultt::D_UNSATISFIABLE
if they are unsatisfiable, resultt::D_ERROR
if the limit of iteration was reached. Reimplemented from bv_refinementt.
Definition at line 610 of file string_refinement.cpp.
References string_dependenciest::add_constraints(), add_lemma(), add_node(), string_constraint_generatort::array_pool, axioms, can_cast_expr< function_application_exprt >(), check_axioms(), string_dependenciest::clean_cache(), string_constraint_generatort::clear_constraints(), config_, bv_refinementt::config_, index_set_pairt::current, current_constraints, decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, DATA_INVARIANT, messaget::debug(), bv_refinementt::dec_solve(), dependencies, display_index_set(), messaget::eom(), equations, messaget::error(), format(), string_constraint_generatort::fresh_symbol, generate_instantiations(), generate_symbol_resolution_from_equations(), generator, array_poolt::get_arrays_of_pointers(), string_constraint_generatort::get_constraints(), string_constraint_generatort::get_lemmas(), string_constraint_generatort::get_not_contains_constraints(), index_sets, index_type(), initial_index_set(), is_valid_string_constraint(), loop_bound_, make_char_array_pointer_associations(), max_string_length, string_axiomst::not_contains, decision_proceduret::ns, string_dependenciest::output_dot(), output_equations(), union_find_replacet::replace_expr(), replace_symbols_in_equations(), boolbvt::set_to(), string_identifiers_resolution_from_equations(), string_refinement_invariantt, symbol_resolve, to_array_type(), union_find_replacet::to_vector(), string_axiomst::universal, update_index_set(), string_refinementt::configt::use_counter_example, and string_constraint_generatort::witness.
|
inlineoverridevirtual |
Reimplemented from bv_refinementt.
Definition at line 55 of file string_refinement.h.
References prop_conv_solvert::prop, and propt::solver_text().
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
Arrays of characters are interpreted differently from the result of supert::get: values are propagated to the left to fill unknown.
expr | an expression |
Reimplemented from boolbvt.
Definition at line 1997 of file string_refinement.cpp.
References index_exprt::array(), string_constraint_generatort::array_pool, CHARACTER_FOR_UNKNOWN, interval_sparse_arrayt::concretize(), if_exprt::cond(), messaget::debug(), dependencies, string_dependenciest::eval(), expr_dynamic_cast(), expr_try_dynamic_cast(), if_exprt::false_case(), from_integer(), generator, boolbvt::get(), get_array(), string_constraint_generatort::get_created_strings(), array_poolt::get_length(), id2string(), index_exprt::index(), INVARIANT, is_char_array_type(), is_char_type(), array_string_exprt::length(), max_string_length, decision_proceduret::ns, interval_sparse_arrayt::of_expr(), union_find_replacet::replace_expr(), typet::subtype(), symbol_resolve, to_array_string_expr(), if_exprt::true_case(), exprt::type(), and UNREACHABLE.
|
overridevirtual |
Record the constraints to ensure that the expression is true when the boolean is true and false otherwise.
expr | an expression of type bool |
value | the boolean value to set it to |
Reimplemented from boolbvt.
Definition at line 288 of file string_refinement.cpp.
References prop_conv_solvert::equality_propagation, equations, has_char_array_subexpr(), irept::id(), INVARIANT, decision_proceduret::ns, PRECONDITION, boolbvt::set_to(), to_equal_expr(), and exprt::type().
|
related |
Instantiates a quantified formula representing not_contains
by substituting the quantifiers and generating axioms.
[in] | axiom | the axiom to instantiate |
[in] | index_pairs | pair of indexes for axiom.s0() and axiom.s1() |
[in] | generator | generator to be used to get axiom 's witness |
Definition at line 21 of file string_constraint_instantiation.cpp.
References string_not_contains_constraintt::exists_lower_bound(), string_not_contains_constraintt::exists_upper_bound(), string_constraint_generatort::get_witness_of(), string_not_contains_constraintt::premise(), string_not_contains_constraintt::s0(), string_not_contains_constraintt::s1(), string_not_contains_constraintt::univ_lower_bound(), and string_not_contains_constraintt::univ_upper_bound().
Referenced by check_axioms().
|
private |
Definition at line 76 of file string_refinement.h.
Referenced by dec_solve().
|
private |
Definition at line 68 of file string_refinement.h.
Referenced by dec_solve().
|
private |
Definition at line 79 of file string_refinement.h.
Referenced by add_lemma(), and dec_solve().
|
private |
Definition at line 89 of file string_refinement.h.
Referenced by dec_solve(), and get().
|
private |
Definition at line 87 of file string_refinement.h.
Referenced by dec_solve(), and set_to().
|
private |
Definition at line 71 of file string_refinement.h.
Referenced by dec_solve(), and get().
|
private |
Definition at line 84 of file string_refinement.h.
Referenced by dec_solve().
|
private |
Definition at line 69 of file string_refinement.h.
Referenced by dec_solve().
|
private |
Definition at line 70 of file string_refinement.h.
Referenced by dec_solve(), and get().
|
private |
Definition at line 74 of file string_refinement.h.
Referenced by add_lemma().
|
private |
Definition at line 85 of file string_refinement.h.
Referenced by add_lemma(), dec_solve(), and get().