CBMC
string_constraint_instantiation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Defines functions related to string constraints.
4 
5 Author: Jesse Sigal, jesse.sigal@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/arith_tools.h>
15 #include <util/expr_iterator.h>
16 #include <util/format_expr.h>
17 
18 #include "string_constraint.h"
19 
20 #include <algorithm>
21 #include <list>
22 #include <unordered_set>
23 
26 static bool contains(const exprt &index, const symbol_exprt &qvar)
27 {
28  return std::find(index.depth_begin(), index.depth_end(), qvar) !=
29  index.depth_end();
30 }
31 
39 static std::unordered_set<exprt, irep_hash>
40 find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
41 {
42  decltype(find_indexes(expr, str, qvar)) result;
43  auto index_str_containing_qvar = [&](const exprt &e) {
44  if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
45  {
46  const auto &arr = index_expr->array();
47  const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
48  return str_it != arr.depth_end() && contains(index_expr->index(), qvar);
49  }
50  return false;
51  };
52 
53  std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) {
54  if(index_str_containing_qvar(e))
55  result.insert(to_index_expr(e).index());
56  });
57  return result;
58 }
59 
61 {
62  type = f.type();
63  // list of expressions to process with a boolean flag telling whether they
64  // appear positively or negatively (true is for positive)
65  std::list<std::pair<exprt, bool>> to_process;
66  to_process.emplace_back(f, true);
67 
68  while(!to_process.empty())
69  {
70  const exprt cur = to_process.back().first;
71  bool positive = to_process.back().second;
72  to_process.pop_back();
73  if(auto integer = numeric_cast<mp_integer>(cur))
74  {
75  constant_coefficient += positive ? integer.value() : -integer.value();
76  }
77  else if(cur.id() == ID_plus)
78  {
79  for(const auto &op : cur.operands())
80  to_process.emplace_back(op, positive);
81  }
82  else if(cur.id() == ID_minus)
83  {
84  to_process.emplace_back(to_minus_expr(cur).op1(), !positive);
85  to_process.emplace_back(to_minus_expr(cur).op0(), positive);
86  }
87  else if(cur.id() == ID_unary_minus)
88  {
89  to_process.emplace_back(to_unary_minus_expr(cur).op(), !positive);
90  }
91  else
92  {
93  if(positive)
94  ++coefficients[cur];
95  else
96  --coefficients[cur];
97  }
98  }
99 }
100 
102 {
103  PRECONDITION(type == other.type);
105  for(auto pair : other.coefficients)
106  coefficients[pair.first] += pair.second;
107 }
108 
109 exprt linear_functiont::to_expr(bool negated) const
110 {
111  exprt sum = nil_exprt{};
112  const exprt constant_expr = from_integer(constant_coefficient, type);
113  if(constant_coefficient != 0)
114  sum = negated ? (exprt)unary_minus_exprt{constant_expr} : constant_expr;
115 
116  for(const auto &term : coefficients)
117  {
118  const exprt &t = term.first;
119  const mp_integer factor = negated ? (-term.second) : term.second;
120  if(factor == -1)
121  {
122  if(sum.is_nil())
123  sum = unary_minus_exprt(t);
124  else
125  sum = minus_exprt(sum, t);
126  }
127  else if(factor == 1)
128  {
129  if(sum.is_nil())
130  sum = t;
131  else
132  sum = plus_exprt(sum, t);
133  }
134  else if(factor != 0)
135  {
136  const mult_exprt to_add{t, from_integer(factor, t.type())};
137  if(sum.is_nil())
138  sum = to_add;
139  else
140  sum = plus_exprt(sum, to_add);
141  }
142  }
143  return sum.is_nil() ? from_integer(0, type) : sum;
144 }
145 
148  const exprt &var,
149  const exprt &val)
150 {
151  auto it = f.coefficients.find(var);
152  PRECONDITION(it != f.coefficients.end());
153  PRECONDITION(it->second == 1 || it->second == -1);
154  const bool positive = it->second == 1;
155 
156  // Transform `f` into `f(var <- 0)`
157  f.coefficients.erase(it);
158  // Transform `f(var <- 0)` into `f(var <- 0) - val`
160 
161  // If the coefficient of var is 1 then solution `val - f(var <- 0),
162  // otherwise `f(var <- 0) - val`
163  return f.to_expr(positive);
164 }
165 
167 {
168  std::ostringstream stream;
169  stream << constant_coefficient;
170  for(const auto &pair : coefficients)
171  stream << " + " << pair.second << " * " << ::format(pair.first);
172  return stream.str();
173 }
174 
176  const string_constraintt &axiom,
177  const exprt &str,
178  const exprt &val)
179 {
180  exprt::operandst conjuncts;
181  for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var))
182  {
183  const exprt univ_var_value =
185  implies_exprt instance(
186  and_exprt(
187  binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
188  binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
189  axiom.body);
190  replace_expr(axiom.univ_var, univ_var_value, instance);
191  conjuncts.push_back(instance);
192  }
193  return conjunction(conjuncts);
194 }
195 
203 std::vector<exprt> instantiate_not_contains(
204  const string_not_contains_constraintt &axiom,
205  const std::set<std::pair<exprt, exprt>> &index_pairs,
206  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
207  &witnesses)
208 {
209  std::vector<exprt> lemmas;
210 
211  const array_string_exprt s0 = axiom.s0;
212  const array_string_exprt s1 = axiom.s1;
213 
214  for(const auto &pair : index_pairs)
215  {
216  // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
217  // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
218  const exprt &i0 = pair.first;
219  const exprt &i1 = pair.second;
220  const minus_exprt val(i0, i1);
221  const and_exprt universal_bound(
222  binary_relation_exprt(axiom.univ_lower_bound, ID_le, val),
223  binary_relation_exprt(axiom.univ_upper_bound, ID_gt, val));
224  const exprt f = index_exprt(witnesses.at(axiom), val);
225  const equal_exprt relevancy(f, i1);
226  const and_exprt premise(relevancy, axiom.premise, universal_bound);
227 
228  const notequal_exprt differ(s0[i0], s1[i1]);
229  const and_exprt existential_bound(
230  binary_relation_exprt(axiom.exists_lower_bound, ID_le, i1),
231  binary_relation_exprt(axiom.exists_upper_bound, ID_gt, i1));
232  const and_exprt body(differ, existential_bound);
233 
234  const implies_exprt lemma(premise, body);
235  lemmas.push_back(lemma);
236  }
237 
238  return lemmas;
239 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
int8_t s1
Definition: bytecode_info.h:59
Boolean AND.
Definition: std_expr.h:2120
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
depth_iteratort depth_end()
Definition: expr.cpp:249
depth_iteratort depth_begin()
Definition: expr.cpp:247
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
Boolean implication.
Definition: std_expr.h:2183
Array index operator.
Definition: std_expr.h:1465
const irep_idt & id() const
Definition: irep.h:384
bool is_nil() const
Definition: irep.h:364
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
exprt to_expr(bool negated=false) const
static exprt solve(linear_functiont f, const exprt &var, const exprt &val)
Return an expression y such that f(var <- y) = val.
linear_functiont(const exprt &f)
Put an expression f composed of additions and subtractions into its cannonical representation.
std::unordered_map< exprt, mp_integer, irep_hash > coefficients
std::string format()
Format the linear function as a string, can be used for debugging.
void add(const linear_functiont &other)
Make this function the sum of the current function with other.
Binary minus.
Definition: std_expr.h:1061
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1107
The NIL expression.
Definition: std_expr.h:3073
Disequality.
Definition: std_expr.h:1420
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The unary minus expression.
Definition: std_expr.h:484
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:66
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:514
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:1086
Defines string constraints.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Instantiates a string constraint by substituting the quantifiers.
static std::unordered_set< exprt, irep_hash > find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
Find indexes of str used in expr that contains qvar, for instance with arguments (str[k+1]=='a'),...
Defines related function for string constraints.
Constraints to encode non containement of strings.