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/string_expr.h>
25 #include <util/replace_expr.h>
31 
32 // clang-format off
33 #define OPT_STRING_REFINEMENT \
34  "(no-refine-strings)" \
35  "(string-printable)" \
36  "(string-input-value):" \
37  "(string-non-empty)" \
38  "(max-nondet-string-length):"
39 
40 #define HELP_STRING_REFINEMENT \
41  " --no-refine-strings turn off string refinement\n" \
42  " --string-printable restrict to printable strings (experimental)\n" /* NOLINT(*) */ \
43  " --string-non-empty restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
44  " --string-printable st restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \
45  " the switch can be used multiple times to give\n" /* NOLINT(*) */ \
46  " several strings\n" /* NOLINT(*) */ \
47  " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */
48 
49 // The integration of the string solver into CBMC is incomplete. Therefore,
50 // it is not turned on by default and not all options are available.
51 #define OPT_STRING_REFINEMENT_CBMC \
52  "(refine-strings)" \
53  "(string-printable)"
54 
55 #define HELP_STRING_REFINEMENT_CBMC \
56  " --refine-strings use string refinement (experimental)\n" \
57  " --string-printable restrict to printable strings (experimental)\n" /* NOLINT(*) */
58 // clang-format on
59 
60 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
61 
63 {
64 private:
65  struct configt
66  {
67  std::size_t refinement_bound=0;
69  };
70 public:
72  struct infot : public bv_refinementt::infot,
73  public configt
74  {
75  };
76 
77  explicit string_refinementt(const infot &);
78 
79  std::string decision_procedure_text() const override
80  { return "string refinement loop with "+prop.solver_text(); }
81 
82  exprt get(const exprt &expr) const override;
83  void set_to(const exprt &expr, bool value) override;
85 
86 private:
87  // Base class
89 
90  string_refinementt(const infot &, bool);
91 
93  std::size_t loop_bound_;
95 
96  // Simple constraints that have been given to the solver
97  std::set<exprt> seen_instances;
98 
100 
101  // Unquantified lemmas that have newly been added
102  std::vector<exprt> current_constraints;
103 
104  // See the definition in the PASS article
105  // Warning: this is indexed by array_expressions and not string expressions
106 
109 
110  std::vector<equal_exprt> equations;
111 
113 
114  void add_lemma(const exprt &lemma, bool simplify_lemma = true);
115 };
116 
117 exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
118 
119 // Declaration required for unit-test:
121  std::vector<equal_exprt> &equations,
122  const namespacet &ns,
123  messaget::mstreamt &stream);
124 
125 // Declaration required for unit-test:
127  exprt expr,
128  const std::function<symbol_exprt(const irep_idt &, const typet &)>
129  &symbol_generator,
130  const bool left_propagate);
131 
132 #endif
The type of an expression, extends irept.
Definition: type.h:27
Generates string constraints to link results from string functions with their arguments.
std::vector< equal_exprt > equations
virtual const std::string solver_text()=0
string_refinementt constructor arguments
bv_refinementt supert
string_dependenciest dependencies
string_refinementt(const infot &)
exprt substitute_array_lists(exprt expr, std::size_t string_max_length)
Defines string constraints.
union_find_replacet symbol_resolve
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
Keep track of dependencies between strings.
string_constraint_generatort generator
String expressions for the string solver.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
const configt config_
Base class for all expressions.
Definition: expr.h:54
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...
std::set< exprt > seen_instances
std::string decision_procedure_text() const override
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.
string_axiomst axioms
Expression to hold a symbol (variable)
Definition: std_expr.h:143
std::vector< exprt > current_constraints
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 &#39;with&#39; expressions are replaced by &#39;if&#39; expr...
index_set_pairt index_sets
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.