cprover
acceleration_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "acceleration_utils.h"
13 
14 #include <iostream>
15 #include <map>
16 #include <set>
17 #include <string>
18 #include <algorithm>
19 
21 
22 #include <ansi-c/expr2c.h>
23 
24 #include <util/symbol_table.h>
25 #include <util/options.h>
26 #include <util/std_code.h>
27 #include <util/find_symbols.h>
28 #include <util/simplify_expr.h>
29 #include <util/replace_expr.h>
30 #include <util/arith_tools.h>
31 
32 #include "cone_of_influence.h"
33 #include "overflow_instrumenter.h"
34 #include "scratch_program.h"
35 #include "util.h"
36 
38  const exprt &expr,
39  expr_sett &rvalues)
40 {
41  if(expr.id()==ID_symbol ||
42  expr.id()==ID_index ||
43  expr.id()==ID_member ||
44  expr.id()==ID_dereference)
45  {
46  rvalues.insert(expr);
47  }
48  else
49  {
50  forall_operands(it, expr)
51  {
52  gather_rvalues(*it, rvalues);
53  }
54  }
55 }
56 
58  const goto_programt &body,
59  expr_sett &modified)
60 {
62  find_modified(it, modified);
63 }
64 
66  const goto_programt::instructionst &instructions,
67  expr_sett &modified)
68 {
69  for(goto_programt::instructionst::const_iterator
70  it=instructions.begin();
71  it!=instructions.end();
72  ++it)
73  find_modified(it, modified);
74 }
75 
77  const patht &path,
78  expr_sett &modified)
79 {
80  for(const auto &step : path)
81  find_modified(step.loc, modified);
82 }
83 
86  expr_sett &modified)
87 {
88  for(const auto &step : loop)
89  find_modified(step, modified);
90 }
91 
94  expr_sett &modified)
95 {
96  if(t->is_assign())
97  {
98  code_assignt assignment = t->get_assign();
99  modified.insert(assignment.lhs());
100  }
101 }
102 
104  std::map<exprt, polynomialt> polynomials,
105  patht &path,
106  guard_managert &guard_manager)
107 {
108  // Checking that our polynomial is inductive with respect to the loop body is
109  // equivalent to checking safety of the following program:
110  //
111  // assume (target1==polynomial1);
112  // assume (target2==polynomial2)
113  // ...
114  // loop_body;
115  // loop_counter++;
116  // assert (target1==polynomial1);
117  // assert (target2==polynomial2);
118  // ...
119  scratch_programt program(symbol_table, message_handler, guard_manager);
120  std::vector<exprt> polynomials_hold;
121  substitutiont substitution;
122 
123  stash_polynomials(program, polynomials, substitution, path);
124 
125  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
126  it!=polynomials.end();
127  ++it)
128  {
129  const equal_exprt holds(it->first, it->second.to_expr());
130  program.add(goto_programt::make_assumption(holds));
131 
132  polynomials_hold.push_back(holds);
133  }
134 
135  program.append_path(path);
136 
137  auto inc_loop_counter = code_assignt(
138  loop_counter,
140 
141  program.add(goto_programt::make_assignment(inc_loop_counter));
142 
143  ensure_no_overflows(program);
144 
145  for(const auto &p : polynomials_hold)
147 
148 #ifdef DEBUG
149  std::cout << "Checking following program for inductiveness:\n";
150  program.output(ns, irep_idt(), std::cout);
151 #endif
152 
153  try
154  {
155  if(program.check_sat(guard_manager))
156  {
157  // We found a counterexample to inductiveness... :-(
158  #ifdef DEBUG
159  std::cout << "Not inductive!\n";
160  #endif
161  return false;
162  }
163  else
164  {
165  return true;
166  }
167  }
168  catch(const std::string &s)
169  {
170  std::cout << "Error in inductiveness SAT check: " << s << '\n';
171  return false;
172  }
173  catch (const char *s)
174  {
175  std::cout << "Error in inductiveness SAT check: " << s << '\n';
176  return false;
177  }
178 }
179 
181  scratch_programt &program,
182  std::map<exprt, polynomialt> &polynomials,
183  substitutiont &substitution,
184  patht &path)
185 {
186  expr_sett modified;
187 
188  find_modified(path, modified);
189  stash_variables(program, modified, substitution);
190 
191  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
192  it!=polynomials.end();
193  ++it)
194  {
195  it->second.substitute(substitution);
196  }
197 }
198 
200  scratch_programt &program,
201  expr_sett modified,
202  substitutiont &substitution)
203 {
204  find_symbols_sett vars =
205  find_symbols_or_nexts(modified.begin(), modified.end());
206  const irep_idt &loop_counter_name =
208  vars.erase(loop_counter_name);
209 
210  for(const irep_idt &symbol : vars)
211  {
212  const symbolt &orig = symbol_table.lookup_ref(symbol);
213  symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
214  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
215  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
216  }
217 }
218 
219 /*
220  * Finds a precondition which guarantees that all the assumptions and assertions
221  * along this path hold.
222  *
223  * This is not the weakest precondition, since we make underapproximations due
224  * to aliasing.
225  */
226 
228 {
229  exprt ret=false_exprt();
230 
231  for(patht::reverse_iterator r_it=path.rbegin();
232  r_it!=path.rend();
233  ++r_it)
234  {
235  goto_programt::const_targett t=r_it->loc;
236 
237  if(t->is_assign())
238  {
239  // XXX Need to check for aliasing...
240  const code_assignt &assignment = t->get_assign();
241  const exprt &lhs=assignment.lhs();
242  const exprt &rhs=assignment.rhs();
243 
244  if(lhs.id()==ID_symbol ||
245  lhs.id()==ID_index ||
246  lhs.id()==ID_dereference)
247  {
248  replace_expr(lhs, rhs, ret);
249  }
250  else
251  {
252  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
253  }
254  }
255  else if(t->is_assume() || t->is_assert())
256  {
257  ret = implies_exprt(t->get_condition(), ret);
258  }
259  else
260  {
261  // Ignore.
262  }
263 
264  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
265  {
266  // The guard isn't constant true, so we need to accumulate that too.
267  ret=implies_exprt(r_it->guard, ret);
268  }
269  }
270 
271  // Hack: replace array accesses with nondet.
272  expr_mapt array_abstractions;
273  // abstract_arrays(ret, array_abstractions);
274 
275  simplify(ret, ns);
276 
277  return ret;
278 }
279 
281  exprt &expr,
282  expr_mapt &abstractions)
283 {
284  if(expr.id()==ID_index ||
285  expr.id()==ID_dereference)
286  {
287  expr_mapt::iterator it=abstractions.find(expr);
288 
289  if(it==abstractions.end())
290  {
291  symbolt sym=fresh_symbol("accelerate::array_abstraction", expr.type());
292  abstractions[expr]=sym.symbol_expr();
293  expr=sym.symbol_expr();
294  }
295  else
296  {
297  expr=it->second;
298  }
299  }
300  else
301  {
302  Forall_operands(it, expr)
303  {
304  abstract_arrays(*it, abstractions);
305  }
306  }
307 }
308 
310 {
311  Forall_operands(it, expr)
312  {
313  push_nondet(*it);
314  }
315 
316  if(expr.id() == ID_not && to_not_expr(expr).op().id() == ID_nondet)
317  {
318  expr = side_effect_expr_nondett(expr.type(), expr.source_location());
319  }
320  else if(expr.id()==ID_equal ||
321  expr.id()==ID_lt ||
322  expr.id()==ID_gt ||
323  expr.id()==ID_le ||
324  expr.id()==ID_ge)
325  {
326  const auto &rel_expr = to_binary_relation_expr(expr);
327  if(rel_expr.lhs().id() == ID_nondet || rel_expr.rhs().id() == ID_nondet)
328  {
329  expr = side_effect_expr_nondett(expr.type(), expr.source_location());
330  }
331  }
332 }
333 
335  std::map<exprt, polynomialt> polynomials,
336  patht &path,
337  exprt &guard,
338  guard_managert &guard_manager)
339 {
340  // We want to check that if an assumption fails, the next iteration can't be
341  // feasible again. To do this we check the following program for safety:
342  //
343  // loop_counter=1;
344  // assume(target1==polynomial1);
345  // assume(target2==polynomial2);
346  // ...
347  // assume(precondition);
348  //
349  // loop_counter=*;
350  // target1=polynomial1);
351  // target2=polynomial2);
352  // ...
353  // assume(!precondition);
354  //
355  // loop_counter++;
356  //
357  // target1=polynomial1;
358  // target2=polynomial2;
359  // ...
360  //
361  // assume(no overflows in above program)
362  // assert(!precondition);
363 
364  exprt condition=precondition(path);
365  scratch_programt program(symbol_table, message_handler, guard_manager);
366 
367  substitutiont substitution;
368  stash_polynomials(program, polynomials, substitution, path);
369 
370  std::vector<exprt> polynomials_hold;
371 
372  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
373  it!=polynomials.end();
374  ++it)
375  {
376  exprt lhs=it->first;
377  exprt rhs=it->second.to_expr();
378 
379  polynomials_hold.push_back(equal_exprt(lhs, rhs));
380  }
381 
383 
384  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
385  it!=polynomials_hold.end();
386  ++it)
387  {
388  program.assume(*it);
389  }
390 
391  program.assume(not_exprt(condition));
392 
393  program.assign(
394  loop_counter,
396 
397  for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
398  p_it!=polynomials.end();
399  ++p_it)
400  {
401  program.assign(p_it->first, p_it->second.to_expr());
402  }
403 
404  program.assume(condition);
405  program.assign(
406  loop_counter,
408 
409  for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
410  p_it!=polynomials.end();
411  ++p_it)
412  {
413  program.assign(p_it->first, p_it->second.to_expr());
414  }
415 
416  ensure_no_overflows(program);
417 
418  program.add(goto_programt::make_assertion(condition));
419 
420  guard=not_exprt(condition);
421  simplify(guard, ns);
422 
423 #ifdef DEBUG
424  std::cout << "Checking following program for monotonicity:\n";
425  program.output(ns, irep_idt(), std::cout);
426 #endif
427 
428  try
429  {
430  if(program.check_sat(guard_manager))
431  {
432  #ifdef DEBUG
433  std::cout << "Path is not monotone\n";
434  #endif
435 
436  return false;
437  }
438  }
439  catch(const std::string &s)
440  {
441  std::cout << "Error in monotonicity SAT check: " << s << '\n';
442  return false;
443  }
444  catch(const char *s)
445  {
446  std::cout << "Error in monotonicity SAT check: " << s << '\n';
447  return false;
448  }
449 
450 #ifdef DEBUG
451  std::cout << "Path is monotone\n";
452 #endif
453 
454  return true;
455 }
456 
458 {
459  symbolt overflow_sym=fresh_symbol("polynomial::overflow", bool_typet());
460  const exprt &overflow_var=overflow_sym.symbol_expr();
461  overflow_instrumentert instrumenter(program, overflow_var, symbol_table);
462 
463  optionst checker_options;
464 
465  checker_options.set_option("signed-overflow-check", true);
466  checker_options.set_option("unsigned-overflow-check", true);
467  checker_options.set_option("assert-to-assume", true);
468  checker_options.set_option("assumptions", true);
469  checker_options.set_option("simplify", true);
470 
471 
472 #ifdef DEBUG
473  time_t now=time(0);
474  std::cout << "Adding overflow checks at " << now << "...\n";
475 #endif
476 
477  instrumenter.add_overflow_checks();
478  program.add(goto_programt::make_assumption(not_exprt(overflow_var)));
479 
480  // goto_functionst::goto_functiont fn;
481  // fn.body.instructions.swap(program.instructions);
482  // goto_check(ns, checker_options, fn);
483  // fn.body.instructions.swap(program.instructions);
484 
485 #ifdef DEBUG
486  now=time(0);
487  std::cout << "Done at " << now << ".\n";
488 #endif
489 }
490 
492  goto_programt::instructionst &loop_body,
493  expr_sett &arrays_written)
494 {
495  expr_pairst assignments;
496 
497  for(goto_programt::instructionst::reverse_iterator r_it=loop_body.rbegin();
498  r_it!=loop_body.rend();
499  ++r_it)
500  {
501  if(r_it->is_assign())
502  {
503  // Is this an array assignment?
504  code_assignt assignment = r_it->get_assign();
505 
506  if(assignment.lhs().id()==ID_index)
507  {
508  // This is an array assignment -- accumulate it in our list.
509  assignments.push_back(
510  std::make_pair(assignment.lhs(), assignment.rhs()));
511 
512  // Also add this array to the set of arrays written to.
513  index_exprt index_expr=to_index_expr(assignment.lhs());
514  arrays_written.insert(index_expr.array());
515  }
516  else
517  {
518  // This is a regular assignment. Do weakest precondition on all our
519  // array expressions with respect to this assignment.
520  for(expr_pairst::iterator a_it=assignments.begin();
521  a_it!=assignments.end();
522  ++a_it)
523  {
524  replace_expr(assignment.lhs(), assignment.rhs(), a_it->first);
525  replace_expr(assignment.lhs(), assignment.rhs(), a_it->second);
526  }
527  }
528  }
529  }
530 
531  return assignments;
532 }
533 
535  goto_programt::instructionst &loop_body,
536  std::map<exprt, polynomialt> &polynomials,
537  substitutiont &substitution,
538  scratch_programt &program)
539 {
540 #ifdef DEBUG
541  std::cout << "Doing arrays...\n";
542 #endif
543 
544  expr_sett arrays_written;
545  expr_pairst array_assignments;
546 
547  array_assignments=gather_array_assignments(loop_body, arrays_written);
548 
549 #ifdef DEBUG
550  std::cout << "Found " << array_assignments.size()
551  << " array assignments\n";
552 #endif
553 
554  if(array_assignments.empty())
555  {
556  // The loop doesn't write to any arrays. We're done!
557  return true;
558  }
559 
560  polynomial_array_assignmentst poly_assignments;
561  polynomialst nondet_indices;
562 
564  array_assignments, polynomials, poly_assignments, nondet_indices))
565  {
566  // We weren't able to model some array assignment. That means we need to
567  // bail out altogether :-(
568 #ifdef DEBUG
569  std::cout << "Couldn't model an array assignment :-(\n";
570 #endif
571  return false;
572  }
573 
574  // First make all written-to arrays nondeterministic.
575  for(expr_sett::iterator it=arrays_written.begin();
576  it!=arrays_written.end();
577  ++it)
578  {
579  program.assign(
580  *it, side_effect_expr_nondett(it->type(), source_locationt()));
581  }
582 
583  // Now add in all the effects of this loop on the arrays.
584  exprt::operandst array_operands;
585 
586  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
587  it!=poly_assignments.end();
588  ++it)
589  {
590  polynomialt stashed_index=it->index;
591  polynomialt stashed_value=it->value;
592 
593  stashed_index.substitute(substitution);
594  stashed_value.substitute(substitution);
595 
596  array_operands.push_back(equal_exprt(
597  index_exprt(it->array, stashed_index.to_expr()),
598  stashed_value.to_expr()));
599  }
600 
601  exprt arrays_expr=conjunction(array_operands);
602 
603  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
604  const symbol_exprt k = k_sym.symbol_expr();
605 
606  const and_exprt k_bound(
607  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
609  replace_expr(loop_counter, k, arrays_expr);
610 
611  implies_exprt implies(k_bound, arrays_expr);
612 
613  const forall_exprt forall(k, implies);
614  program.assume(forall);
615 
616  // Now have to encode that the array doesn't change at indices we didn't
617  // touch.
618  for(expr_sett::iterator a_it=arrays_written.begin();
619  a_it!=arrays_written.end();
620  ++a_it)
621  {
622  exprt array=*a_it;
623  exprt old_array=substitution[array];
624  std::vector<polynomialt> indices;
625  bool nonlinear_index=false;
626 
627  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
628  it!=poly_assignments.end();
629  ++it)
630  {
631  if(it->array==array)
632  {
633  polynomialt index=it->index;
634  index.substitute(substitution);
635  indices.push_back(index);
636 
637  if(index.max_degree(loop_counter) > 1 ||
638  (index.coeff(loop_counter)!=1 && index.coeff(loop_counter)!=-1))
639  {
640 #ifdef DEBUG
641  std::cout << expr2c(index.to_expr(), ns) << " is nonlinear\n";
642 #endif
643  nonlinear_index=true;
644  }
645  }
646  }
647 
648  exprt idx_never_touched=nil_exprt();
649  symbolt idx_sym=fresh_symbol("polynomial::idx", signed_poly_type());
650  const symbol_exprt idx = idx_sym.symbol_expr();
651 
652  // Optimization: if all the assignments to a particular array A are of the
653  // form:
654  // A[loop_counter + e]=f
655  // where e does not contain loop_counter, we don't need quantifier
656  // alternation to encode the non-changedness. We can get away
657  // with the expression:
658  // forall k; k < e || k > loop_counter+e => A[k]=old_A[k]
659 
660  if(!nonlinear_index)
661  {
662  polynomialt pos_eliminator, neg_eliminator;
663 
664  neg_eliminator.from_expr(loop_counter);
665  pos_eliminator=neg_eliminator;
666  pos_eliminator.mult(-1);
667 
668  exprt::operandst unchanged_operands;
669 
670  for(std::vector<polynomialt>::iterator it=indices.begin();
671  it!=indices.end();
672  ++it)
673  {
674  polynomialt index=*it;
675  exprt max_idx, min_idx;
676 
677  if(index.coeff(loop_counter)==1)
678  {
679  max_idx=
680  minus_exprt(
681  index.to_expr(),
682  from_integer(1, index.to_expr().type()));
683  index.add(pos_eliminator);
684  min_idx=index.to_expr();
685  }
686  else if(index.coeff(loop_counter)==-1)
687  {
688  min_idx=
689  plus_exprt(
690  index.to_expr(),
691  from_integer(1, index.to_expr().type()));
692  index.add(neg_eliminator);
693  max_idx=index.to_expr();
694  }
695  else
696  {
697  assert(!"ITSALLGONEWRONG");
698  }
699 
700  or_exprt unchanged_by_this_one(
701  binary_relation_exprt(idx, ID_lt, min_idx),
702  binary_relation_exprt(idx, ID_gt, max_idx));
703  unchanged_operands.push_back(unchanged_by_this_one);
704  }
705 
706  idx_never_touched=conjunction(unchanged_operands);
707  }
708  else
709  {
710  // The vector `indices' now contains all of the indices written
711  // to for the current array, each with the free variable
712  // loop_counter. Now let's build an expression saying that the
713  // fresh variable idx is none of these indices.
714  exprt::operandst idx_touched_operands;
715 
716  for(std::vector<polynomialt>::iterator it=indices.begin();
717  it!=indices.end();
718  ++it)
719  {
720  idx_touched_operands.push_back(
721  not_exprt(equal_exprt(idx, it->to_expr())));
722  }
723 
724  exprt idx_not_touched=conjunction(idx_touched_operands);
725 
726  // OK, we have an expression saying idx is not touched by the
727  // loop_counter'th iteration. Let's quantify that to say that
728  // idx is not touched at all.
729  symbolt l_sym=fresh_symbol("polynomial::l", signed_poly_type());
730  exprt l=l_sym.symbol_expr();
731 
732  replace_expr(loop_counter, l, idx_not_touched);
733 
734  // 0 < l <= loop_counter => idx_not_touched
735  and_exprt l_bound(
736  binary_relation_exprt(from_integer(0, l.type()), ID_lt, l),
738  implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
739 
740  idx_never_touched=exprt(ID_forall);
741  idx_never_touched.type()=bool_typet();
742  idx_never_touched.copy_to_operands(l);
743  idx_never_touched.copy_to_operands(idx_not_touched_bound);
744  }
745 
746  // We now have an expression saying idx is never touched. It is the
747  // following:
748  // forall l . 0 < l <= loop_counter => idx!=index_1 && ... && idx!=index_N
749  //
750  // Now let's build an expression saying that such an idx doesn't get
751  // updated by this loop, i.e.
752  // idx_never_touched => A[idx]==A_old[idx]
753  equal_exprt value_unchanged(
754  index_exprt(array, idx), index_exprt(old_array, idx));
755  implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
756 
757  // Cool. Finally, we want to quantify over idx to say that every idx that
758  // is never touched has its value unchanged. So our expression is:
759  // forall idx . idx_never_touched => A[idx]==A_old[idx]
760  const forall_exprt array_unchanged(idx, idx_unchanged);
761 
762  // And we're done!
763  program.assume(array_unchanged);
764  }
765 
766  return true;
767 }
768 
770  expr_pairst &array_assignments,
771  std::map<exprt, polynomialt> &polynomials,
772  polynomial_array_assignmentst &array_polynomials,
773  polynomialst &nondet_indices)
774 {
775  for(expr_pairst::iterator it=array_assignments.begin();
776  it!=array_assignments.end();
777  ++it)
778  {
779  polynomial_array_assignmentt poly_assignment;
780  index_exprt index_expr=to_index_expr(it->first);
781 
782  poly_assignment.array=index_expr.array();
783 
784  if(!expr2poly(index_expr.index(), polynomials, poly_assignment.index))
785  {
786  // Couldn't convert the index -- bail out.
787 #ifdef DEBUG
788  std::cout << "Couldn't convert index: "
789  << expr2c(index_expr.index(), ns) << '\n';
790 #endif
791  return false;
792  }
793 
794 #ifdef DEBUG
795  std::cout << "Converted index to: "
796  << expr2c(poly_assignment.index.to_expr(), ns)
797  << '\n';
798 #endif
799 
800  if(it->second.id()==ID_nondet)
801  {
802  nondet_indices.push_back(poly_assignment.index);
803  }
804  else if(!expr2poly(it->second, polynomials, poly_assignment.value))
805  {
806  // Couldn't conver the RHS -- bail out.
807 #ifdef DEBUG
808  std::cout << "Couldn't convert RHS: " << expr2c(it->second, ns)
809  << '\n';
810 #endif
811  return false;
812  }
813  else
814  {
815 #ifdef DEBUG
816  std::cout << "Converted RHS to: "
817  << expr2c(poly_assignment.value.to_expr(), ns)
818  << '\n';
819 #endif
820 
821  array_polynomials.push_back(poly_assignment);
822  }
823  }
824 
825  return true;
826 }
827 
829  exprt &expr,
830  std::map<exprt, polynomialt> &polynomials,
831  polynomialt &poly)
832 {
833  exprt subbed_expr=expr;
834 
835  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
836  it!=polynomials.end();
837  ++it)
838  {
839  replace_expr(it->first, it->second.to_expr(), subbed_expr);
840  }
841 
842 #ifdef DEBUG
843  std::cout << "expr2poly(" << expr2c(subbed_expr, ns) << ")\n";
844 #endif
845 
846  try
847  {
848  poly.from_expr(subbed_expr);
849  }
850  catch(...)
851  {
852  return false;
853  }
854 
855  return true;
856 }
857 
860  std::map<exprt, polynomialt> &polynomials,
861  substitutiont &substitution,
862  expr_sett &nonrecursive,
863  scratch_programt &program)
864 {
865  // We have some variables that are defined non-recursively -- that
866  // is to say, their value at the end of a loop iteration does not
867  // depend on their value at the previous iteration. We can solve
868  // for these variables by just forward simulating the path and
869  // taking the expressions we get at the end.
870  replace_mapt state;
871  std::unordered_set<index_exprt, irep_hash> array_writes;
872  expr_sett arrays_written;
873  expr_sett arrays_read;
874 
875  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
876  it!=polynomials.end();
877  ++it)
878  {
879  const exprt &var=it->first;
880  polynomialt poly=it->second;
881  poly.substitute(substitution);
882  exprt e=poly.to_expr();
883 
884 #if 0
885  replace_expr(
886  loop_counter,
888  e);
889 #endif
890 
891  state[var]=e;
892  }
893 
894  for(expr_sett::iterator it=nonrecursive.begin();
895  it!=nonrecursive.end();
896  ++it)
897  {
898  exprt e=*it;
899  state[e]=e;
900  }
901 
902  for(goto_programt::instructionst::iterator it=body.begin();
903  it!=body.end();
904  ++it)
905  {
906  if(it->is_assign())
907  {
908  exprt lhs = it->assign_lhs();
909  exprt rhs = it->assign_rhs();
910 
911  if(lhs.id()==ID_dereference)
912  {
913  // Not handling pointer dereferences yet...
914 #ifdef DEBUG
915  std::cout << "Bailing out on write-through-pointer\n";
916 #endif
917  return false;
918  }
919 
920  if(lhs.id()==ID_index)
921  {
922  auto &lhs_index_expr = to_index_expr(lhs);
923  replace_expr(state, lhs_index_expr.index());
924  array_writes.insert(lhs_index_expr);
925 
926  if(arrays_written.find(lhs_index_expr.array()) != arrays_written.end())
927  {
928  // We've written to this array before -- be conservative and bail
929  // out now.
930 #ifdef DEBUG
931  std::cout << "Bailing out on array written to twice in loop: "
932  << expr2c(lhs_index_expr.array(), ns) << '\n';
933 #endif
934  return false;
935  }
936 
937  arrays_written.insert(lhs_index_expr.array());
938  }
939 
940  replace_expr(state, rhs);
941  state[lhs]=rhs;
942 
943  gather_array_accesses(rhs, arrays_read);
944  }
945  }
946 
947  // Be conservative: if we read and write from the same array, bail out.
948  for(expr_sett::iterator it=arrays_written.begin();
949  it!=arrays_written.end();
950  ++it)
951  {
952  if(arrays_read.find(*it)!=arrays_read.end())
953  {
954 #ifdef DEBUG
955  std::cout << "Bailing out on array read and written on same path\n";
956 #endif
957  return false;
958  }
959  }
960 
961  for(expr_sett::iterator it=nonrecursive.begin();
962  it!=nonrecursive.end();
963  ++it)
964  {
965  if(it->id()==ID_symbol)
966  {
967  exprt &val=state[*it];
968  program.assign(*it, val);
969 
970 #ifdef DEBUG
971  std::cout << "Fitted nonrecursive: " << expr2c(*it, ns) << "=" <<
972  expr2c(val, ns) << '\n';
973 #endif
974  }
975  }
976 
977  for(const auto &write : array_writes)
978  {
979  const auto &lhs = write;
980  const auto &rhs = state[write];
981 
982  if(!assign_array(lhs, rhs, program))
983  {
984 #ifdef DEBUG
985  std::cout << "Failed to assign a nonrecursive array: " <<
986  expr2c(lhs, ns) << "=" << expr2c(rhs, ns) << '\n';
987 #endif
988  return false;
989  }
990  }
991 
992  return true;
993 }
994 
996  const index_exprt &lhs,
997  const exprt &rhs,
998  scratch_programt &program)
999 {
1000 #ifdef DEBUG
1001  std::cout << "Modelling array assignment " << expr2c(lhs, ns) << "=" <<
1002  expr2c(rhs, ns) << '\n';
1003 #endif
1004 
1005  if(lhs.id()==ID_dereference)
1006  {
1007  // Don't handle writes through pointers for now...
1008 #ifdef DEBUG
1009  std::cout << "Bailing out on write-through-pointer\n";
1010 #endif
1011  return false;
1012  }
1013 
1014  // We handle N iterations of the array write:
1015  //
1016  // A[i]=e
1017  //
1018  // by the following sequence:
1019  //
1020  // A'=nondet()
1021  // assume(forall 0 <= k < N . A'[i(k/loop_counter)]=e(k/loop_counter));
1022  // assume(forall j . notwritten(j) ==> A'[j]=A[j]);
1023  // A=A'
1024 
1025  const exprt &arr=lhs.op0();
1026  exprt idx=lhs.op1();
1027  const exprt &fresh_array =
1028  fresh_symbol("polynomial::array", arr.type()).symbol_expr();
1029 
1030  // First make the fresh nondet array.
1031  program.assign(
1032  fresh_array, side_effect_expr_nondett(arr.type(), lhs.source_location()));
1033 
1034  // Then assume that the fresh array has the appropriate values at the indices
1035  // the loop updated.
1036  equal_exprt changed(lhs, rhs);
1037  replace_expr(arr, fresh_array, changed);
1038 
1039  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
1040  const symbol_exprt k = k_sym.symbol_expr();
1041 
1042  const and_exprt k_bound(
1043  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
1044  binary_relation_exprt(k, ID_lt, loop_counter));
1045  replace_expr(loop_counter, k, changed);
1046 
1047  implies_exprt implies(k_bound, changed);
1048 
1049  forall_exprt forall(k, implies);
1050  program.assume(forall);
1051 
1052  // Now let's ensure that the array did not change at the indices we
1053  // didn't touch.
1054 #ifdef DEBUG
1055  std::cout << "Trying to polynomialize " << expr2c(idx, ns) << '\n';
1056 #endif
1057 
1058  polynomialt poly;
1059 
1060  try
1061  {
1062  if(idx.id()==ID_pointer_offset)
1063  {
1064  poly.from_expr(to_unary_expr(idx).op());
1065  }
1066  else
1067  {
1068  poly.from_expr(idx);
1069  }
1070  }
1071  catch(...)
1072  {
1073  // idx is probably nonlinear... bail out.
1074 #ifdef DEBUG
1075  std::cout << "Failed to polynomialize\n";
1076 #endif
1077  return false;
1078  }
1079 
1080  if(poly.max_degree(loop_counter) > 1)
1081  {
1082  // The index expression is nonlinear, e.g. it's something like:
1083  //
1084  // A[x*loop_counter]=0;
1085  //
1086  // where x changes inside the loop. Modelling this requires quantifier
1087  // alternation, and that's too expensive. Bail out.
1088 #ifdef DEBUG
1089  std::cout << "Bailing out on nonlinear index: "
1090  << expr2c(idx, ns) << '\n';
1091 #endif
1092  return false;
1093  }
1094 
1095  int stride=poly.coeff(loop_counter);
1096  exprt not_touched;
1097  exprt lower_bound=idx;
1098  exprt upper_bound=idx;
1099 
1100  if(stride > 0)
1101  {
1102  replace_expr(
1103  loop_counter, from_integer(0, loop_counter.type()), lower_bound);
1104  lower_bound = simplify_expr(std::move(lower_bound), ns);
1105  }
1106  else
1107  {
1108  replace_expr(
1109  loop_counter, from_integer(0, loop_counter.type()), upper_bound);
1110  upper_bound = simplify_expr(std::move(upper_bound), ns);
1111  }
1112 
1113  if(stride==0)
1114  {
1115  // The index we write to doesn't depend on the loop counter....
1116  // We could optimise for this, but I suspect it's not going to
1117  // happen to much so just bail out.
1118 #ifdef DEBUG
1119  std::cout << "Bailing out on write to constant array index: " <<
1120  expr2c(idx, ns) << '\n';
1121 #endif
1122  return false;
1123  }
1124  else if(stride == 1 || stride == -1)
1125  {
1126  // This is the simplest case -- we have an assignment like:
1127  //
1128  // A[c + loop_counter]=e;
1129  //
1130  // where c doesn't change in the loop. The expression to say it doesn't
1131  // change at unexpected places is:
1132  //
1133  // forall k . (k < c || k >= loop_counter + c) ==> A'[k]==A[k]
1134 
1135  not_touched = or_exprt(
1136  binary_relation_exprt(k, ID_lt, lower_bound),
1137  binary_relation_exprt(k, ID_ge, upper_bound));
1138  }
1139  else
1140  {
1141  // A more complex case -- our assignment is:
1142  //
1143  // A[c + s*loop_counter]=e;
1144  //
1145  // where c and s are constants. Now our condition for an index i
1146  // to be unchanged is:
1147  //
1148  // i < c || i >= (c + s*loop_counter) || (i - c) % s!=0
1149 
1150  const minus_exprt step(k, lower_bound);
1151 
1152  not_touched = or_exprt(
1153  or_exprt(
1154  binary_relation_exprt(k, ID_lt, lower_bound),
1155  binary_relation_exprt(k, ID_ge, lower_bound)),
1157  mod_exprt(step, from_integer(stride, step.type())),
1158  from_integer(0, step.type())));
1159  }
1160 
1161  // OK now do the assumption.
1162  exprt fresh_lhs=lhs;
1163  exprt old_lhs=lhs;
1164 
1165  replace_expr(arr, fresh_array, fresh_lhs);
1166  replace_expr(loop_counter, k, fresh_lhs);
1167 
1168  replace_expr(loop_counter, k, old_lhs);
1169 
1170  equal_exprt idx_unchanged(fresh_lhs, old_lhs);
1171 
1172  implies=implies_exprt(not_touched, idx_unchanged);
1173  forall.where() = implies;
1174 
1175  program.assume(forall);
1176 
1177  // Finally, assign the array to the fresh one we've just build.
1178  program.assign(arr, fresh_array);
1179 
1180  return true;
1181 }
1182 
1184  const exprt &e,
1185  expr_sett &arrays)
1186 {
1187  if(e.id() == ID_index)
1188  {
1189  arrays.insert(to_index_expr(e).array());
1190  }
1191  else if(e.id() == ID_dereference)
1192  {
1193  arrays.insert(to_dereference_expr(e).pointer());
1194  }
1195 
1196  forall_operands(it, e)
1197  {
1198  gather_array_accesses(*it, arrays);
1199  }
1200 }
1201 
1203  scratch_programt &program,
1204  std::set<std::pair<expr_listt, exprt> > &coefficients,
1205  polynomialt &polynomial)
1206 {
1207  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1208  it!=coefficients.end();
1209  ++it)
1210  {
1211  monomialt monomial;
1212  expr_listt terms=it->first;
1213  exprt coefficient=it->second;
1214  constant_exprt concrete_term=to_constant_expr(program.eval(coefficient));
1215  std::map<exprt, int> degrees;
1216 
1217  mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true);
1218  monomial.coeff = numeric_cast_v<int>(mp);
1219 
1220  if(monomial.coeff==0)
1221  {
1222  continue;
1223  }
1224 
1225  for(const auto &term : terms)
1226  {
1227  if(degrees.find(term)!=degrees.end())
1228  {
1229  degrees[term]++;
1230  }
1231  else
1232  {
1233  degrees[term]=1;
1234  }
1235  }
1236 
1237  for(std::map<exprt, int>::iterator it=degrees.begin();
1238  it!=degrees.end();
1239  ++it)
1240  {
1241  monomialt::termt term;
1242  term.var=it->first;
1243  term.exp=it->second;
1244  monomial.terms.push_back(term);
1245  }
1246 
1247  polynomial.monomials.push_back(monomial);
1248  }
1249 }
1250 
1252 {
1253  static int num_symbols=0;
1254 
1255  std::string name=base + "_" + std::to_string(num_symbols++);
1256  symbolt ret;
1257  ret.module="scratch";
1258  ret.name=name;
1259  ret.base_name=name;
1260  ret.pretty_name=name;
1261  ret.type=type;
1262 
1263  symbol_table.add(ret);
1264 
1265  return ret;
1266 }
Loop Acceleration.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
std::list< exprt > expr_listt
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
void push_nondet(exprt &expr)
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
void find_modified(const patht &path, expr_sett &modified)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
message_handlert & message_handler
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
bool assign_array(const index_exprt &lhs, const exprt &rhs, scratch_programt &program)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
symbolt fresh_symbol(std::string base, typet type)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
std::vector< expr_pairt > expr_pairst
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)
symbol_tablet & symbol_table
void ensure_no_overflows(scratch_programt &program)
exprt precondition(patht &path)
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
Boolean AND.
Definition: std_expr.h:1920
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
exprt & where()
Definition: std_expr.h:2877
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
exprt & lhs()
Definition: std_code.h:310
A constant literal expression.
Definition: std_expr.h:2753
const irep_idt & get_value() const
Definition: std_expr.h:2761
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const char * c_str() const
Definition: dstring.h:99
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2811
A forall expression.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
instructionst::const_iterator const_targett
Definition: goto_program.h:647
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
Definition: goto_program.h:644
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
Boolean implication.
Definition: std_expr.h:1983
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:407
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
int coeff
Definition: polynomial.h:31
std::vector< termt > terms
Definition: polynomial.h:30
The NIL expression.
Definition: std_expr.h:2820
Boolean negation.
Definition: std_expr.h:2127
Disequality.
Definition: std_expr.h:1283
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
Boolean OR.
Definition: std_expr.h:2028
The plus expression Associativity is not specified.
Definition: std_expr.h:914
void substitute(substitutiont &substitution)
Definition: polynomial.cpp:160
void from_expr(const exprt &expr)
Definition: polynomial.cpp:100
std::vector< monomialt > monomials
Definition: polynomial.h:46
void mult(int scalar)
Definition: polynomial.cpp:252
exprt to_expr()
Definition: polynomial.cpp:22
int coeff(const exprt &expr)
Definition: polynomial.cpp:426
void add(polynomialt &other)
Definition: polynomial.cpp:178
int max_degree(const exprt &var)
Definition: polynomial.cpp:408
bool check_sat(bool do_slice, guard_managert &guard_manager)
targett assume(const exprt &guard)
targett assign(const exprt &lhs, const exprt &rhs)
exprt eval(const exprt &e)
void append_path(patht &path)
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
The type of an expression, extends irept.
Definition: type.h:28
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
std::string expr2c(const exprt &expr, const namespacet &ns)
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
Concrete Goto Program.
#define forall_goto_program_instructions(it, program)
dstringt irep_idt
Definition: irep.h:37
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:117
Options.
Loop Acceleration.
std::list< path_nodet > patht
Definition: path.h:44
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
Loop Acceleration.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
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:34
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
unsigned int exp
Definition: polynomial.h:26
Author: Diffblue Ltd.
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
signedbv_typet signed_poly_type()
Definition: util.cpp:20
Loop Acceleration.