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