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
resultt
Result of running the decision procedure.
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
virtual const std::string solver_text()=0
Keep track of dependencies between strings.
string_constraint_generatort generator
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
union_find_replacet symbol_resolve
bv_refinementt supert
std::vector< exprt > equations
string_axiomst axioms
string_refinementt(const infot &)
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
std::set< exprt > seen_instances
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...
string_dependenciest dependencies
index_set_pairt index_sets
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::vector< exprt > current_constraints
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Generation of fresh symbols of a given type.
Definition: array_pool.h:23
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Magic numbers used throughout the codebase.
Defines string constraints.
Generates string constraints to link results from string functions with their arguments.
Keeps track of dependencies between strings.
String expressions for the string solver.
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...
exprt substitute_array_lists(exprt expr, std::size_t string_max_length)
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.
string_refinementt constructor arguments