cprover
string_refinement.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String support via creating string constraints and progressively
4  instantiating the universal constraints as needed.
5  The procedure is described in the PASS paper at HVC'13:
6  "PASS: String Solving with Parameterized Array and Interval Automaton"
7  by Guodong Li and Indradeep Ghosh
8 
9 Author: Alberto Griggio, alberto.griggio@gmail.com
10 
11 \*******************************************************************/
12 
19 
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H
22 
23 #include <limits>
24 #include <util/magic.h>
25 #include <util/replace_expr.h>
26 #include <util/string_expr.h>
28 
29 #include "string_constraint.h"
31 #include "string_dependencies.h"
33 #include "string_refinement_util.h"
34 
35 // clang-format off
36 #define OPT_STRING_REFINEMENT \
37  "(no-refine-strings)" \
38  "(string-printable)" \
39  "(string-input-value):" \
40  "(string-non-empty)" \
41  "(max-nondet-string-length):"
42 
43 #define HELP_STRING_REFINEMENT \
44  " --no-refine-strings turn off string refinement\n" \
45  " --string-printable restrict to printable strings and characters\n" /* NOLINT(*) */ \
46  " --string-non-empty restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
47  " --string-input-value st restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \
48  " the switch can be used multiple times to give\n" /* NOLINT(*) */ \
49  " several strings\n" /* NOLINT(*) */ \
50  " --max-nondet-string-length n bound the length of nondet (e.g. input) strings.\n" /* NOLINT(*) */ \
51  " Default is " + std::to_string(MAX_CONCRETE_STRING_SIZE - 1) + "; note that\n" /* NOLINT(*) */ \
52  " setting the value higher than this does not work\n" /* NOLINT(*) */ \
53  " with --trace or --validate-trace.\n" /* NOLINT(*) */
54 
55 // The integration of the string solver into CBMC is incomplete. Therefore,
56 // it is not turned on by default and not all options are available.
57 #define OPT_STRING_REFINEMENT_CBMC \
58  "(refine-strings)" \
59  "(string-printable)"
60 
61 #define HELP_STRING_REFINEMENT_CBMC \
62  " --refine-strings use string refinement (experimental)\n" \
63  " --string-printable restrict to printable strings (experimental)\n" /* NOLINT(*) */
64 // clang-format on
65 
66 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
67 
68 class string_refinementt final : public bv_refinementt
69 {
70 private:
71  struct configt
72  {
73  std::size_t refinement_bound = 0;
74  bool use_counter_example = true;
75  };
76 
77 public:
79  struct infot : public bv_refinementt::infot, public configt
80  {
81  };
82 
83  explicit string_refinementt(const infot &);
84 
85  std::string decision_procedure_text() const override
86  {
87  return "string refinement loop with " + prop.solver_text();
88  }
89 
90  exprt get(const exprt &expr) const override;
91  void set_to(const exprt &expr, bool value) override;
93 
94 private:
95  // Base class
97 
98  string_refinementt(const infot &, bool);
99 
101  std::size_t loop_bound_;
103 
104  // Simple constraints that have been given to the solver
105  std::set<exprt> seen_instances;
106 
108 
109  // Unquantified lemmas that have newly been added
110  std::vector<exprt> current_constraints;
111 
112  // See the definition in the PASS article
113  // Warning: this is indexed by array_expressions and not string expressions
114 
117 
118  std::vector<exprt> equations;
119 
121 
122  void add_lemma(const exprt &lemma, bool simplify_lemma = true);
123 };
124 
125 exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
126 
127 // Declaration required for unit-test:
129  const std::vector<equal_exprt> &equations,
130  const namespacet &ns,
131  messaget::mstreamt &stream);
132 
133 // Declaration required for unit-test:
135  exprt expr,
136  symbol_generatort &symbol_generator,
137  const bool left_propagate);
138 
139 #endif
string_refinementt::loop_bound_
std::size_t loop_bound_
Definition: string_refinement.h:101
string_refinementt::generator
string_constraint_generatort generator
Definition: string_refinement.h:102
propt::solver_text
virtual const std::string solver_text()=0
union_find_replace.h
string_refinementt::current_constraints
std::vector< exprt > current_constraints
Definition: string_refinement.h:110
bv_refinementt::infot
Definition: bv_refinement.h:34
index_set_pairt
Definition: string_refinement_util.h:61
string_refinementt::configt::refinement_bound
std::size_t refinement_bound
Definition: string_refinement.h:73
string_refinement_invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
string_refinementt::index_sets
index_set_pairt index_sets
Definition: string_refinement.h:115
string_axiomst
Definition: string_refinement_util.h:67
string_dependencies.h
Keeps track of dependencies between strings.
magic.h
Magic numbers used throughout the codebase.
string_constraint_generatort
Definition: string_constraint_generator.h:45
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
symbol_generatort
Generation of fresh symbols of a given type.
Definition: array_pool.h:23
string_refinement_util.h
string_refinementt::get
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
Definition: string_refinement.cpp:1814
string_refinementt::supert
bv_refinementt supert
Definition: string_refinement.h:96
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' expr...
Definition: string_refinement.cpp:1267
substitute_array_lists
exprt substitute_array_lists(exprt expr, std::size_t string_max_length)
string_refinementt::axioms
string_axiomst axioms
Definition: string_refinement.h:107
bv_refinementt
Definition: bv_refinement.h:20
string_refinementt::symbol_resolve
union_find_replacet symbol_resolve
Definition: string_refinement.h:116
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
string_refinementt::dec_solve
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
Definition: string_refinement.cpp:606
string_refinementt::dependencies
string_dependenciest dependencies
Definition: string_refinement.h:120
string_refinementt::configt
Definition: string_refinement.h:72
string_refinementt
Definition: string_refinement.h:69
string_constraint.h
Defines string constraints.
union_find_replacet
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Definition: union_find_replace.h:17
string_dependenciest
Keep track of dependencies between strings.
Definition: string_dependencies.h:25
string_refinementt::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: string_refinement.h:85
messaget::mstreamt
Definition: message.h:224
string_refinementt::equations
std::vector< exprt > equations
Definition: string_refinement.h:118
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.
Definition: string_refinement.cpp:462
string_refinementt::add_lemma
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Definition: string_refinement.cpp:895
string_refinementt::infot
string_refinementt constructor arguments
Definition: string_refinement.h:80
replace_expr.h
string_refinementt::config_
const configt config_
Definition: string_refinement.h:100
string_refinementt::set_to
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 other...
Definition: string_refinement.cpp:282
string_refinementt::configt::use_counter_example
bool use_counter_example
Definition: string_refinement.h:74
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
string_expr.h
String expressions for the string solver.
string_refinementt::string_refinementt
string_refinementt(const infot &)
Definition: string_refinement.cpp:164
string_refinementt::seen_instances
std::set< exprt > seen_instances
Definition: string_refinement.h:105
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131