cprover
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 #include <algorithm>
14 #include <unordered_set>
15 #include <util/expr_iterator.h>
16 
19 static bool contains(const exprt &index, const symbol_exprt &qvar)
20 {
21  return std::find(index.depth_begin(), index.depth_end(), qvar) !=
22  index.depth_end();
23 }
24 
32 static std::unordered_set<exprt, irep_hash>
33 find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
34 {
35  decltype(find_indexes(expr, str, qvar)) result;
36  auto index_str_containing_qvar = [&](const exprt &e) {
37  if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
38  {
39  const auto &arr = index_expr->array();
40  const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
41  return str_it != arr.depth_end() && contains(index_expr->index(), qvar);
42  }
43  return false;
44  };
45 
46  std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) {
47  if(index_str_containing_qvar(e))
48  result.insert(to_index_expr(e).index());
49  });
50  return result;
51 }
52 
54 {
55  type = f.type();
56  // list of expressions to process with a boolean flag telling whether they
57  // appear positively or negatively (true is for positive)
58  std::list<std::pair<exprt, bool>> to_process;
59  to_process.emplace_back(f, true);
60 
61  while(!to_process.empty())
62  {
63  const exprt cur = to_process.back().first;
64  bool positive = to_process.back().second;
65  to_process.pop_back();
66  if(auto integer = numeric_cast<mp_integer>(cur))
67  {
68  constant_coefficient += positive ? integer.value() : -integer.value();
69  }
70  else if(cur.id() == ID_plus)
71  {
72  for(const auto &op : cur.operands())
73  to_process.emplace_back(op, positive);
74  }
75  else if(cur.id() == ID_minus)
76  {
77  to_process.emplace_back(to_minus_expr(cur).op1(), !positive);
78  to_process.emplace_back(to_minus_expr(cur).op0(), positive);
79  }
80  else if(cur.id() == ID_unary_minus)
81  {
82  to_process.emplace_back(to_unary_minus_expr(cur).op(), !positive);
83  }
84  else
85  {
86  if(positive)
87  ++coefficients[cur];
88  else
89  --coefficients[cur];
90  }
91  }
92 }
93 
95 {
96  PRECONDITION(type == other.type);
98  for(auto pair : other.coefficients)
99  coefficients[pair.first] += pair.second;
100 }
101 
102 exprt linear_functiont::to_expr(bool negated) const
103 {
104  exprt sum = nil_exprt{};
105  const exprt constant_expr = from_integer(constant_coefficient, type);
106  if(constant_coefficient != 0)
107  sum = negated ? (exprt)unary_minus_exprt{constant_expr} : constant_expr;
108 
109  for(const auto &term : coefficients)
110  {
111  const exprt &t = term.first;
112  const mp_integer factor = negated ? (-term.second) : term.second;
113  if(factor == -1)
114  {
115  if(sum.is_nil())
116  sum = unary_minus_exprt(t);
117  else
118  sum = minus_exprt(sum, t);
119  }
120  else if(factor == 1)
121  {
122  if(sum.is_nil())
123  sum = t;
124  else
125  sum = plus_exprt(sum, t);
126  }
127  else if(factor != 0)
128  {
129  const mult_exprt to_add{t, from_integer(factor, t.type())};
130  if(sum.is_nil())
131  sum = to_add;
132  else
133  sum = plus_exprt(sum, to_add);
134  }
135  }
136  return sum.is_nil() ? from_integer(0, type) : sum;
137 }
138 
141  const exprt &var,
142  const exprt &val)
143 {
144  auto it = f.coefficients.find(var);
145  PRECONDITION(it != f.coefficients.end());
146  PRECONDITION(it->second == 1 || it->second == -1);
147  const bool positive = it->second == 1;
148 
149  // Transform `f` into `f(var <- 0)`
150  f.coefficients.erase(it);
151  // Transform `f(var <- 0)` into `f(var <- 0) - val`
153 
154  // If the coefficient of var is 1 then solution `val - f(var <- 0),
155  // otherwise `f(var <- 0) - val`
156  return f.to_expr(positive);
157 }
158 
160 {
161  std::ostringstream stream;
162  stream << constant_coefficient;
163  for(const auto &pair : coefficients)
164  stream << " + " << pair.second << " * " << ::format(pair.first);
165  return stream.str();
166 }
167 
184  const string_constraintt &axiom,
185  const exprt &str,
186  const exprt &val)
187 {
188  exprt::operandst conjuncts;
189  for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var))
190  {
191  const exprt univ_var_value =
193  implies_exprt instance(
194  and_exprt(
195  binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
196  binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
197  axiom.body);
198  replace_expr(axiom.univ_var, univ_var_value, instance);
199  conjuncts.push_back(instance);
200  }
201  return conjunction(conjuncts);
202 }
203 
211 std::vector<exprt> instantiate_not_contains(
212  const string_not_contains_constraintt &axiom,
213  const std::set<std::pair<exprt, exprt>> &index_pairs,
214  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
215  &witnesses)
216 {
217  std::vector<exprt> lemmas;
218 
219  const array_string_exprt s0 = axiom.s0;
220  const array_string_exprt s1 = axiom.s1;
221 
222  for(const auto &pair : index_pairs)
223  {
224  // We have s0[x+f(x)] and s1[f(x)], so to have i0 indexing s0 and i1
225  // indexing s1, we need x = i0 - i1 and f(i0 - i1) = f(x) = i1.
226  const exprt &i0 = pair.first;
227  const exprt &i1 = pair.second;
228  const minus_exprt val(i0, i1);
229  const and_exprt universal_bound(
230  binary_relation_exprt(axiom.univ_lower_bound, ID_le, val),
231  binary_relation_exprt(axiom.univ_upper_bound, ID_gt, val));
232  const exprt f = index_exprt(witnesses.at(axiom), val);
233  const equal_exprt relevancy(f, i1);
234  const and_exprt premise(relevancy, axiom.premise, universal_bound);
235 
236  const notequal_exprt differ(s0[i0], s1[i1]);
237  const and_exprt existential_bound(
238  binary_relation_exprt(axiom.exists_lower_bound, ID_le, i1),
239  binary_relation_exprt(axiom.exists_upper_bound, ID_gt, i1));
240  const and_exprt body(differ, existential_bound);
241 
242  const implies_exprt lemma(premise, body);
243  lemmas.push_back(lemma);
244  }
245 
246  return lemmas;
247 }
conjunction
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:51
linear_functiont::constant_coefficient
mp_integer constant_coefficient
Definition: string_constraint_instantiation.h:65
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
linear_functiont::format
std::string format()
Format the linear function as a string, can be used for debugging.
Definition: string_constraint_instantiation.cpp:159
string_not_contains_constraintt::univ_upper_bound
exprt univ_upper_bound
Definition: string_constraint.h:129
linear_functiont::add
void add(const linear_functiont &other)
Make this function the sum of the current function with other.
Definition: string_constraint_instantiation.cpp:94
string_constraintt
Definition: string_constraint.h:60
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
linear_functiont::coefficients
std::unordered_map< exprt, mp_integer, irep_hash > coefficients
Definition: string_constraint_instantiation.h:66
and_exprt
Boolean AND.
Definition: std_expr.h:2137
s1
int8_t s1
Definition: bytecode_info.h:59
linear_functiont::linear_functiont
linear_functiont(const exprt &f)
Put an expression f composed of additions and subtractions into its cannonical representation.
Definition: string_constraint_instantiation.cpp:53
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
linear_functiont
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
Definition: string_constraint_instantiation.h:42
string_not_contains_constraintt::exists_upper_bound
exprt exists_upper_bound
Definition: string_constraint.h:132
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
instantiate
exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Instantiates a string constraint by substituting the quantifiers.
Definition: string_constraint_instantiation.cpp:183
equal_exprt
Equality.
Definition: std_expr.h:1190
string_constraintt::univ_var
symbol_exprt univ_var
Definition: string_constraint.h:64
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
string_not_contains_constraintt::premise
exprt premise
Definition: string_constraint.h:130
notequal_exprt
Disequality.
Definition: std_expr.h:1248
string_constraintt::upper_bound
exprt upper_bound
Definition: string_constraint.h:66
string_constraintt::body
exprt body
Definition: string_constraint.h:67
string_constraintt::lower_bound
exprt lower_bound
Definition: string_constraint.h:65
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
find_indexes
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'),...
Definition: string_constraint_instantiation.cpp:33
linear_functiont::to_expr
exprt to_expr(bool negated=false) const
Definition: string_constraint_instantiation.cpp:102
linear_functiont::solve
static exprt solve(linear_functiont f, const exprt &var, const exprt &val)
Return an expression y such that f(var <- y) = val.
Definition: string_constraint_instantiation.cpp:139
string_not_contains_constraintt::exists_lower_bound
exprt exists_lower_bound
Definition: string_constraint.h:131
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
minus_exprt
Binary minus.
Definition: std_expr.h:940
string_not_contains_constraintt::univ_lower_bound
exprt univ_lower_bound
Definition: string_constraint.h:128
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
string_refinementt::instantiate_not_contains
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...
Definition: string_constraint_instantiation.cpp:211
string_constraint_instantiation.h
Defines related function for string constraints.
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
string_not_contains_constraintt::s0
array_string_exprt s0
Definition: string_constraint.h:133
contains
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
Definition: string_constraint_instantiation.cpp:19
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:127
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1293
string_not_contains_constraintt::s1
array_string_exprt s1
Definition: string_constraint.h:134
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
linear_functiont::type
typet type
Definition: string_constraint_instantiation.h:67
array_string_exprt
Definition: string_expr.h:67