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