cprover
Loading...
Searching...
No Matches
string_refinement.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: 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
9Author: 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
24
26
28#include "string_dependencies.h"
30
31// clang-format off
32#define OPT_STRING_REFINEMENT \
33 "(no-refine-strings)" \
34 "(string-printable)" \
35 "(string-input-value):" \
36 "(string-non-empty)" \
37 "(max-nondet-string-length):"
38
39#define HELP_STRING_REFINEMENT \
40 " --no-refine-strings turn off string refinement\n" \
41 " --string-printable restrict to printable strings and characters\n" /* NOLINT(*) */ \
42 " --string-non-empty restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \
43 " --string-input-value st restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \
44 " the switch can be used multiple times to give\n" /* NOLINT(*) */ \
45 " several strings\n" /* NOLINT(*) */ \
46 " --max-nondet-string-length n bound the length of nondet (e.g. input) strings.\n" /* NOLINT(*) */ \
47 " Default is " + std::to_string(MAX_CONCRETE_STRING_SIZE - 1) + "; note that\n" /* NOLINT(*) */ \
48 " setting the value higher than this does not work\n" /* NOLINT(*) */ \
49 " with --trace or --validate-trace.\n" /* NOLINT(*) */
50
51// The integration of the string solver into CBMC is incomplete. Therefore,
52// it is not turned on by default and not all options are available.
53#define OPT_STRING_REFINEMENT_CBMC \
54 "(refine-strings)" \
55 "(string-printable)"
56
57#define HELP_STRING_REFINEMENT_CBMC \
58 " --refine-strings use string refinement (experimental)\n" \
59 " --string-printable restrict to printable strings (experimental)\n" /* NOLINT(*) */
60// clang-format on
61
62#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
63
65{
66private:
67 struct configt
68 {
69 std::size_t refinement_bound = 0;
71 };
72
73public:
75 struct infot : public bv_refinementt::infot, public configt
76 {
77 };
78
79 explicit string_refinementt(const infot &);
80
81 std::string decision_procedure_text() const override
82 {
83 return "string refinement loop with " + prop.solver_text();
84 }
85
86 exprt get(const exprt &expr) const override;
87 void set_to(const exprt &expr, bool value) override;
89
90private:
91 // Base class
93
94 string_refinementt(const infot &, bool);
95
97 std::size_t loop_bound_;
99
100 // Simple constraints that have been given to the solver
101 std::set<exprt> seen_instances;
102
104
105 // Unquantified lemmas that have newly been added
106 std::vector<exprt> current_constraints;
107
108 // See the definition in the PASS article
109 // Warning: this is indexed by array_expressions and not string expressions
110
113
114 std::vector<exprt> equations;
115
117
118 void add_lemma(const exprt &lemma, bool simplify_lemma = true);
119};
120
122
123// Declaration required for unit-test:
125 const std::vector<equal_exprt> &equations,
126 const namespacet &ns,
128
129// Declaration required for unit-test:
131 exprt expr,
133 const bool left_propagate);
134
135#endif
Abstraction Refinement Loop.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:91
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
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:22
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Generates string constraints to link results from string functions with their arguments.
Keeps track of dependencies between strings.
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