cprover
arrays.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "arrays.h"
10 
11 #include <cassert>
12 #include <iostream>
13 
14 #include <langapi/language_util.h>
15 
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 #include <util/arith_tools.h>
19 #include <util/base_type.h>
20 #include <util/namespace.h>
21 
22 #include <solvers/prop/prop.h>
23 
25  const namespacet &_ns,
26  propt &_prop):equalityt(_ns, _prop)
27 {
28  lazy_arrays = false; // will be set to true when --refine is used
29  incremental_cache = false; // for incremental solving
30 }
31 
33 {
34  // we are not allowed to put the index directly in the
35  // entry for the root of the equivalence class
36  // because this map is accessed during building the error trace
37  std::size_t number=arrays.number(index.array());
38  index_map[number].insert(index.index());
39  update_indices.insert(number);
40 }
41 
43  const equal_exprt &equality)
44 {
45  const exprt &op0=equality.op0();
46  const exprt &op1=equality.op1();
47 
48  // check types
49  if(!base_type_eq(op0.type(), op1.type(), ns))
50  {
51  std::cout << equality.pretty() << '\n';
52  throw "record_array_equality got equality without matching types";
53  }
54 
55  assert(ns.follow(op0.type()).id()==ID_array);
56 
57  array_equalities.push_back(array_equalityt());
58 
59  array_equalities.back().f1=op0;
60  array_equalities.back().f2=op1;
61  array_equalities.back().l=SUB::equality(op0, op1);
62 
63  arrays.make_union(op0, op1);
64  collect_arrays(op0);
65  collect_arrays(op1);
66 
67  return array_equalities.back().l;
68 }
69 
71 {
72  for(std::size_t i=0; i<arrays.size(); i++)
73  {
75  }
76 }
77 
79 {
80  if(expr.id()!=ID_index)
81  {
82  forall_operands(op, expr) collect_indices(*op);
83  }
84  else
85  {
86  const index_exprt &e = to_index_expr(expr);
87  collect_indices(e.index()); // necessary?
88 
89  const typet &array_op_type=ns.follow(e.array().type());
90 
91  if(array_op_type.id()==ID_array)
92  {
93  const array_typet &array_type=
94  to_array_type(array_op_type);
95 
96  if(is_unbounded_array(array_type))
97  {
99  }
100  }
101  }
102 }
103 
105 {
106  const array_typet &array_type=
107  to_array_type(ns.follow(a.type()));
108 
109  if(a.id()==ID_with)
110  {
111  const with_exprt &with_expr=to_with_expr(a);
112 
113  // check types
114  if(!base_type_eq(array_type, with_expr.old().type(), ns))
115  {
116  std::cout << a.pretty() << '\n';
117  throw "collect_arrays got 'with' without matching types";
118  }
119 
120  arrays.make_union(a, with_expr.old());
121  collect_arrays(with_expr.old());
122 
123  // make sure this shows as an application
124  index_exprt index_expr(with_expr.old(), with_expr.where());
125  record_array_index(index_expr);
126  }
127  else if(a.id()==ID_update)
128  {
129  const update_exprt &update_expr=to_update_expr(a);
130 
131  // check types
132  if(!base_type_eq(array_type, update_expr.old().type(), ns))
133  {
134  std::cout << a.pretty() << '\n';
135  throw "collect_arrays got 'update' without matching types";
136  }
137 
138  arrays.make_union(a, update_expr.old());
139  collect_arrays(update_expr.old());
140 
141 #if 0
142  // make sure this shows as an application
143  index_exprt index_expr(update_expr.old(), update_expr.index());
144  record_array_index(index_expr);
145 #endif
146  }
147  else if(a.id()==ID_if)
148  {
149  const if_exprt &if_expr=to_if_expr(a);
150 
151  // check types
152  if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
153  {
154  std::cout << a.pretty() << '\n';
155  throw "collect_arrays got if without matching types";
156  }
157 
158  // check types
159  if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
160  {
161  std::cout << a.pretty() << '\n';
162  throw "collect_arrays got if without matching types";
163  }
164 
165  arrays.make_union(a, if_expr.true_case());
166  arrays.make_union(a, if_expr.false_case());
167  collect_arrays(if_expr.true_case());
168  collect_arrays(if_expr.false_case());
169  }
170  else if(a.id()==ID_symbol)
171  {
172  }
173  else if(a.id()==ID_nondet_symbol)
174  {
175  }
176  else if(a.id()==ID_member)
177  {
178  if(to_member_expr(a).struct_op().id()!=ID_symbol)
179  throw
180  "unexpected array expression: member with `"+a.op0().id_string()+"'";
181  }
182  else if(a.id()==ID_constant ||
183  a.id()==ID_array ||
184  a.id()==ID_string_constant)
185  {
186  }
187  else if(a.id()==ID_array_of)
188  {
189  }
190  else if(a.id()==ID_byte_update_little_endian ||
191  a.id()==ID_byte_update_big_endian)
192  {
193  assert(0);
194  }
195  else if(a.id()==ID_typecast)
196  {
197  // cast between array types?
198  assert(a.operands().size()==1);
199 
200  if(a.op0().type().id()==ID_array)
201  {
202  arrays.make_union(a, a.op0());
203  collect_arrays(a.op0());
204  }
205  else
206  throw "unexpected array type cast from "+a.op0().type().id_string();
207  }
208  else if(a.id()==ID_index)
209  {
210  // nested unbounded arrays
211  arrays.make_union(a, a.op0());
212  collect_arrays(a.op0());
213  }
214  else
215  throw "unexpected array expression (collect_arrays): `"+a.id_string()+"'";
216 }
217 
219 void arrayst::add_array_constraint(const lazy_constraintt &lazy, bool refine)
220 {
221  if(lazy_arrays && refine)
222  {
223  // lazily add the constraint
225  {
226  if(expr_map.find(lazy.lazy) == expr_map.end())
227  {
228  lazy_array_constraints.push_back(lazy);
229  expr_map[lazy.lazy] = true;
230  }
231  }
232  else
233  {
234  lazy_array_constraints.push_back(lazy);
235  }
236  }
237  else
238  {
239  // add the constraint eagerly
241  }
242 }
243 
245 {
246  collect_indices();
247  // at this point all indices should in the index set
248 
249  // reduce initial index map
250  update_index_map(true);
251 
252  // add constraints for if, with, array_of
253  for(std::size_t i=0; i<arrays.size(); i++)
254  {
255  // take a copy as arrays may get modified by add_array_constraints
256  // in case of nested unbounded arrays
257  exprt a=arrays[i];
258 
260 
261  // we have to update before it gets used in the next add_* call
262  update_index_map(false);
263  }
264 
265  // add constraints for equalities
266  for(const auto &equality : array_equalities)
267  {
270  equality);
271 
272  // update_index_map should not be necessary here
273  }
274 
275  // add the Ackermann constraints
277 }
278 
280 {
281  // this is quadratic!
282 
283 #if 0
284  std::cout << "arrays.size(): " << arrays.size() << '\n';
285 #endif
286 
287  // iterate over arrays
288  for(std::size_t i=0; i<arrays.size(); i++)
289  {
290  const index_sett &index_set=index_map[arrays.find_number(i)];
291 
292 #if 0
293  std::cout << "index_set.size(): " << index_set.size() << '\n';
294 #endif
295 
296  // iterate over indices, 2x!
297  for(index_sett::const_iterator
298  i1=index_set.begin();
299  i1!=index_set.end();
300  i1++)
301  for(index_sett::const_iterator
302  i2=index_set.begin();
303  i2!=index_set.end();
304  i2++)
305  if(i1!=i2)
306  {
307  if(i1->is_constant() && i2->is_constant())
308  continue;
309 
310  // index equality
311  equal_exprt indices_equal(*i1, *i2);
312 
313  if(indices_equal.op0().type()!=
314  indices_equal.op1().type())
315  {
316  indices_equal.op1().
317  make_typecast(indices_equal.op0().type());
318  }
319 
320  literalt indices_equal_lit=convert(indices_equal);
321 
322  if(indices_equal_lit!=const_literal(false))
323  {
324  const typet &subtype=ns.follow(arrays[i].type()).subtype();
325  index_exprt index_expr1(arrays[i], *i1, subtype);
326 
327  index_exprt index_expr2=index_expr1;
328  index_expr2.index()=*i2;
329 
330  equal_exprt values_equal(index_expr1, index_expr2);
331 
332  // add constraint
334  or_exprt(literal_exprt(!indices_equal_lit), values_equal));
335  add_array_constraint(lazy, true); // added lazily
336 
337 #if 0 // old code for adding, not significantly faster
338  prop.lcnf(!indices_equal_lit, convert(values_equal));
339 #endif
340  }
341  }
342  }
343 }
344 
346 void arrayst::update_index_map(std::size_t i)
347 {
348  if(arrays.is_root_number(i))
349  return;
350 
351  std::size_t root_number=arrays.find_number(i);
352  assert(root_number!=i);
353 
354  index_sett &root_index_set=index_map[root_number];
355  index_sett &index_set=index_map[i];
356 
357  root_index_set.insert(index_set.begin(), index_set.end());
358 }
359 
360 void arrayst::update_index_map(bool update_all)
361 {
362  // iterate over non-roots
363  // possible reasons why update is needed:
364  // -- there are new equivalence classes in arrays
365  // -- there are new indices for arrays that are not the root
366  // of an equivalence class
367  // (and we cannot do that in record_array_index())
368  // -- equivalence classes have been merged
369  if(update_all)
370  {
371  for(std::size_t i=0; i<arrays.size(); i++)
372  update_index_map(i);
373  }
374  else
375  {
376  for(const auto &index : update_indices)
377  update_index_map(index);
378 
379  update_indices.clear();
380  }
381 
382 #ifdef DEBUG
383  // print index sets
384  for(const auto &index_entry : index_map)
385  for(const auto &index : index_entry.second)
386  std::cout << "Index set (" << index_entry.first << " = "
387  << arrays.find_number(index_entry.first) << " = "
388  << from_expr(ns, "",
389  arrays[arrays.find_number(index_entry.first)])
390  << "): "
391  << from_expr(ns, "", index) << '\n';
392  std::cout << "-----\n";
393 #endif
394 }
395 
397  const index_sett &index_set,
398  const array_equalityt &array_equality)
399 {
400  // add constraints x=y => x[i]=y[i]
401 
402  for(const auto &index : index_set)
403  {
404  const typet &subtype1=ns.follow(array_equality.f1.type()).subtype();
405  index_exprt index_expr1(array_equality.f1, index, subtype1);
406 
407  const typet &subtype2=ns.follow(array_equality.f2.type()).subtype();
408  index_exprt index_expr2(array_equality.f2, index, subtype2);
409 
410  assert(index_expr1.type()==index_expr2.type());
411 
412  array_equalityt equal;
413  equal.f1 = index_expr1;
414  equal.f2 = index_expr2;
415  equal.l = array_equality.l;
416  equal_exprt equality_expr(index_expr1, index_expr2);
417 
418  // add constraint
419  // equality constraints are not added lazily
420  // convert must be done to guarantee correct update of the index_set
421  prop.lcnf(!array_equality.l, convert(equality_expr));
422  }
423 }
424 
426  const index_sett &index_set,
427  const exprt &expr)
428 {
429  if(expr.id()==ID_with)
430  return add_array_constraints_with(index_set, to_with_expr(expr));
431  else if(expr.id()==ID_update)
432  return add_array_constraints_update(index_set, to_update_expr(expr));
433  else if(expr.id()==ID_if)
434  return add_array_constraints_if(index_set, to_if_expr(expr));
435  else if(expr.id()==ID_array_of)
436  return add_array_constraints_array_of(index_set, to_array_of_expr(expr));
437  else if(expr.id()==ID_symbol ||
438  expr.id()==ID_nondet_symbol ||
439  expr.id()==ID_constant ||
440  expr.id()=="zero_string" ||
441  expr.id()==ID_array ||
442  expr.id()==ID_string_constant)
443  {
444  }
445  else if(expr.id()==ID_member &&
446  to_member_expr(expr).struct_op().id()==ID_symbol)
447  {
448  }
449  else if(expr.id()==ID_byte_update_little_endian ||
450  expr.id()==ID_byte_update_big_endian)
451  {
452  assert(0);
453  }
454  else if(expr.id()==ID_typecast)
455  {
456  // we got a=(type[])b
457  assert(expr.operands().size()==1);
458 
459  // add a[i]=b[i]
460  for(const auto &index : index_set)
461  {
462  const typet &subtype=ns.follow(expr.type()).subtype();
463  index_exprt index_expr1(expr, index, subtype);
464  index_exprt index_expr2(expr.op0(), index, subtype);
465 
466  assert(index_expr1.type()==index_expr2.type());
467 
468  // add constraint
470  equal_exprt(index_expr1, index_expr2));
471  add_array_constraint(lazy, false); // added immediately
472  }
473  }
474  else if(expr.id()==ID_index)
475  {
476  }
477  else
478  throw
479  "unexpected array expression (add_array_constraints): `"+
480  expr.id_string()+"'";
481 }
482 
484  const index_sett &index_set,
485  const with_exprt &expr)
486 {
487  // we got x=(y with [i:=v])
488  // add constraint x[i]=v
489 
490  const exprt &index=expr.where();
491  const exprt &value=expr.new_value();
492 
493  {
494  index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
495 
496  if(index_expr.type()!=value.type())
497  {
498  std::cout << expr.pretty() << '\n';
499  assert(false);
500  }
501 
502  lazy_constraintt lazy(
503  lazy_typet::ARRAY_WITH, equal_exprt(index_expr, value));
504  add_array_constraint(lazy, false); // added immediately
505  }
506 
507  // use other array index applications for "else" case
508  // add constraint x[I]=y[I] for I!=i
509 
510  for(auto other_index : index_set)
511  {
512  if(other_index!=index)
513  {
514  // we first build the guard
515 
516  if(other_index.type()!=index.type())
517  other_index.make_typecast(index.type());
518 
519  literalt guard_lit=convert(equal_exprt(index, other_index));
520 
521  if(guard_lit!=const_literal(true))
522  {
523  const typet &subtype=ns.follow(expr.type()).subtype();
524  index_exprt index_expr1(expr, other_index, subtype);
525  index_exprt index_expr2(expr.op0(), other_index, subtype);
526 
527  equal_exprt equality_expr(index_expr1, index_expr2);
528 
529  // add constraint
531  literal_exprt(guard_lit)));
532  add_array_constraint(lazy, false); // added immediately
533 
534 #if 0 // old code for adding, not significantly faster
535  {
536  literalt equality_lit=convert(equality_expr);
537 
538  bvt bv;
539  bv.reserve(2);
540  bv.push_back(equality_lit);
541  bv.push_back(guard_lit);
542  prop.lcnf(bv);
543  }
544 #endif
545  }
546  }
547  }
548 }
549 
551  const index_sett &index_set,
552  const update_exprt &expr)
553 {
554  // we got x=UPDATE(y, [i], v)
555  // add constaint x[i]=v
556 
557 #if 0
558  const exprt &index=expr.where();
559  const exprt &value=expr.new_value();
560 
561  {
562  index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
563 
564  if(index_expr.type()!=value.type())
565  {
566  std::cout << expr.pretty() << '\n';
567  assert(false);
568  }
569 
570  set_to_true(equal_exprt(index_expr, value));
571  }
572 
573  // use other array index applications for "else" case
574  // add constraint x[I]=y[I] for I!=i
575 
576  for(auto other_index : index_set)
577  {
578  if(other_index!=index)
579  {
580  // we first build the guard
581 
582  if(other_index.type()!=index.type())
583  other_index.make_typecast(index.type());
584 
585  literalt guard_lit=convert(equal_exprt(index, other_index));
586 
587  if(guard_lit!=const_literal(true))
588  {
589  const typet &subtype=ns.follow(expr.type()).subtype();
590  index_exprt index_expr1(expr, other_index, subtype);
591  index_exprt index_expr2(expr.op0(), other_index, subtype);
592 
593  equal_exprt equality_expr(index_expr1, index_expr2);
594 
595  literalt equality_lit=convert(equality_expr);
596 
597  // add constraint
598  bvt bv;
599  bv.reserve(2);
600  bv.push_back(equality_lit);
601  bv.push_back(guard_lit);
602  prop.lcnf(bv);
603  }
604  }
605  }
606 #endif
607 }
608 
610  const index_sett &index_set,
611  const array_of_exprt &expr)
612 {
613  // we got x=array_of[v]
614  // get other array index applications
615  // and add constraint x[i]=v
616 
617  for(const auto &index : index_set)
618  {
619  const typet &subtype=ns.follow(expr.type()).subtype();
620  index_exprt index_expr(expr, index, subtype);
621 
622  assert(base_type_eq(index_expr.type(), expr.op0().type(), ns));
623 
624  // add constraint
625  lazy_constraintt lazy(
626  lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.op0()));
627  add_array_constraint(lazy, false); // added immediately
628  }
629 }
630 
632  const index_sett &index_set,
633  const if_exprt &expr)
634 {
635  // we got x=(c?a:b)
636  literalt cond_lit=convert(expr.cond());
637 
638  // get other array index applications
639  // and add c => x[i]=a[i]
640  // !c => x[i]=b[i]
641 
642  // first do true case
643 
644  for(const auto &index : index_set)
645  {
646  const typet subtype=ns.follow(expr.type()).subtype();
647  index_exprt index_expr1(expr, index, subtype);
648  index_exprt index_expr2(expr.true_case(), index, subtype);
649 
650  // add implication
652  or_exprt(literal_exprt(!cond_lit),
653  equal_exprt(index_expr1, index_expr2)));
654  add_array_constraint(lazy, false); // added immediately
655 
656 #if 0 // old code for adding, not significantly faster
657  prop.lcnf(!cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
658 #endif
659  }
660 
661  // now the false case
662  for(const auto &index : index_set)
663  {
664  const typet subtype=ns.follow(expr.type()).subtype();
665  index_exprt index_expr1(expr, index, subtype);
666  index_exprt index_expr2(expr.false_case(), index, subtype);
667 
668  // add implication
669  lazy_constraintt lazy(
671  or_exprt(literal_exprt(cond_lit),
672  equal_exprt(index_expr1, index_expr2)));
673  add_array_constraint(lazy, false); // added immediately
674 
675 #if 0 // old code for adding, not significantly faster
676  prop.lcnf(cond_lit, convert(equal_exprt(index_expr1, index_expr2)));
677 #endif
678  }
679 }
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:2919
The type of an expression.
Definition: type.h:20
void add_array_constraint(const lazy_constraintt &lazy, bool refine=true)
adds array constraints (refine=true...lazily for the refinement loop)
Definition: arrays.cpp:219
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & true_case()
Definition: std_expr.h:2805
void collect_arrays(const exprt &a)
Definition: arrays.cpp:104
bool lazy_arrays
Definition: arrays.h:95
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
Definition: std_expr.h:1286
union_find< exprt > arrays
Definition: arrays.h:64
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
index_mapt index_map
Definition: arrays.h:71
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
size_type find_number(typename numbering< T >::const_iterator it) const
Definition: union_find.h:191
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
void add_array_constraints()
Definition: arrays.cpp:244
Operator to update elements in structs and arrays.
Definition: std_expr.h:3039
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
std::set< exprt > index_sett
Definition: arrays.h:67
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
exprt & old()
Definition: std_expr.h:2878
exprt & new_value()
Definition: std_expr.h:2898
typet & type()
Definition: expr.h:60
void add_array_constraints_with(const index_sett &index_set, const with_exprt &expr)
Definition: arrays.cpp:483
void l_set_to_true(literalt a)
Definition: prop.h:47
equality
Definition: std_expr.h:1082
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
void add_array_constraints_equality(const index_sett &index_set, const array_equalityt &array_equality)
Definition: arrays.cpp:396
arrayst(const namespacet &_ns, propt &_prop)
Definition: arrays.cpp:24
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
bool incremental_cache
Definition: arrays.h:96
size_type number(const T &a)
Definition: union_find.h:226
exprt & old()
Definition: std_expr.h:3063
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
Theory of Arrays with Extensionality.
const update_exprt & to_update_expr(const exprt &expr)
Cast a generic exprt to an update_exprt.
Definition: std_expr.h:3108
void update_index_map(bool update_all)
Definition: arrays.cpp:360
API to expression classes.
exprt & op1()
Definition: expr.h:87
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void collect_indices()
Definition: arrays.cpp:70
#define forall_operands(it, expr)
Definition: expr.h:17
const namespacet & ns
array constructor from single element
Definition: std_expr.h:1252
literalt record_array_equality(const equal_exprt &expr)
Definition: arrays.cpp:42
exprt & false_case()
Definition: std_expr.h:2815
TO_BE_DOCUMENTED.
Definition: prop.h:22
std::set< std::size_t > update_indices
Definition: arrays.h:119
array_equalitiest array_equalities
Definition: arrays.h:61
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
literalt const_literal(bool value)
Definition: literal.h:187
API to type classes.
void add_array_constraints_array_of(const index_sett &index_set, const array_of_exprt &exprt)
Definition: arrays.cpp:609
exprt & index()
Definition: std_expr.h:1208
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:32
Base class for all expressions.
Definition: expr.h:46
void add_array_constraints_update(const index_sett &index_set, const update_exprt &expr)
Definition: arrays.cpp:550
const exprt & struct_op() const
Definition: std_expr.h:3270
std::list< lazy_constraintt > lazy_array_constraints
Definition: arrays.h:97
void set_to_true(const exprt &expr)
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
virtual bool is_unbounded_array(const typet &type) const =0
const std::string & id_string() const
Definition: irep.h:192
arrays with given size
Definition: std_types.h:901
bool make_union(const T &a, const T &b)
Definition: union_find.h:140
exprt & new_value()
Definition: std_expr.h:3087
exprt & where()
Definition: std_expr.h:2888
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
exprt & array()
Definition: std_expr.h:1198
void add_array_Ackermann_constraints()
Definition: arrays.cpp:279
std::vector< literalt > bvt
Definition: literal.h:197
void add_array_constraints_if(const index_sett &index_set, const if_exprt &exprt)
Definition: arrays.cpp:631
std::map< exprt, bool > expr_map
Definition: arrays.h:99
array index operator
Definition: std_expr.h:1170
bool is_root_number(size_type a) const
Definition: union_find.h:206