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(), expr.source_location());
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(), expr.source_location());
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 
415  program.assign(
416  loop_counter,
418 
419  for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
420  p_it!=polynomials.end();
421  ++p_it)
422  {
423  program.assign(p_it->first, p_it->second.to_expr());
424  }
425 
426  program.assume(condition);
427  program.assign(
428  loop_counter,
430 
431  for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
432  p_it!=polynomials.end();
433  ++p_it)
434  {
435  program.assign(p_it->first, p_it->second.to_expr());
436  }
437 
438  ensure_no_overflows(program);
439 
440  program.add_instruction(ASSERT)->guard=condition;
441 
442  guard=not_exprt(condition);
443  simplify(guard, ns);
444 
445 #ifdef DEBUG
446  std::cout << "Checking following program for monotonicity:\n";
447  program.output(ns, "", std::cout);
448 #endif
449 
450  try
451  {
452  if(program.check_sat())
453  {
454  #ifdef DEBUG
455  std::cout << "Path is not monotone\n";
456  #endif
457 
458  return false;
459  }
460  }
461  catch(const std::string &s)
462  {
463  std::cout << "Error in monotonicity SAT check: " << s << '\n';
464  return false;
465  }
466  catch(const char *s)
467  {
468  std::cout << "Error in monotonicity SAT check: " << s << '\n';
469  return false;
470  }
471 
472 #ifdef DEBUG
473  std::cout << "Path is monotone\n";
474 #endif
475 
476  return true;
477 }
478 
480 {
481  symbolt overflow_sym=fresh_symbol("polynomial::overflow", bool_typet());
482  const exprt &overflow_var=overflow_sym.symbol_expr();
483  overflow_instrumentert instrumenter(program, overflow_var, symbol_table);
484 
485  optionst checker_options;
486 
487  checker_options.set_option("signed-overflow-check", true);
488  checker_options.set_option("unsigned-overflow-check", true);
489  checker_options.set_option("assert-to-assume", true);
490  checker_options.set_option("assumptions", true);
491  checker_options.set_option("simplify", true);
492 
493 
494 #ifdef DEBUG
495  time_t now=time(0);
496  std::cout << "Adding overflow checks at " << now << "...\n";
497 #endif
498 
499  instrumenter.add_overflow_checks();
500  program.add_instruction(ASSUME)->guard=not_exprt(overflow_var);
501 
502  // goto_functionst::goto_functiont fn;
503  // fn.body.instructions.swap(program.instructions);
504  // goto_check(ns, checker_options, fn);
505  // fn.body.instructions.swap(program.instructions);
506 
507 #ifdef DEBUG
508  now=time(0);
509  std::cout << "Done at " << now << ".\n";
510 #endif
511 }
512 
514  goto_programt::instructionst &loop_body,
515  expr_sett &arrays_written)
516 {
517  expr_pairst assignments;
518 
519  for(goto_programt::instructionst::reverse_iterator r_it=loop_body.rbegin();
520  r_it!=loop_body.rend();
521  ++r_it)
522  {
523  if(r_it->is_assign())
524  {
525  // Is this an array assignment?
526  code_assignt assignment=to_code_assign(r_it->code);
527 
528  if(assignment.lhs().id()==ID_index)
529  {
530  // This is an array assignment -- accumulate it in our list.
531  assignments.push_back(
532  std::make_pair(assignment.lhs(), assignment.rhs()));
533 
534  // Also add this array to the set of arrays written to.
535  index_exprt index_expr=to_index_expr(assignment.lhs());
536  arrays_written.insert(index_expr.array());
537  }
538  else
539  {
540  // This is a regular assignment. Do weakest precondition on all our
541  // array expressions with respect to this assignment.
542  for(expr_pairst::iterator a_it=assignments.begin();
543  a_it!=assignments.end();
544  ++a_it)
545  {
546  replace_expr(assignment.lhs(), assignment.rhs(), a_it->first);
547  replace_expr(assignment.lhs(), assignment.rhs(), a_it->second);
548  }
549  }
550  }
551  }
552 
553  return assignments;
554 }
555 
557  goto_programt::instructionst &loop_body,
558  std::map<exprt, polynomialt> &polynomials,
559  exprt &loop_counter,
560  substitutiont &substitution,
561  scratch_programt &program)
562 {
563 #ifdef DEBUG
564  std::cout << "Doing arrays...\n";
565 #endif
566 
567  expr_sett arrays_written;
568  expr_pairst array_assignments;
569 
570  array_assignments=gather_array_assignments(loop_body, arrays_written);
571 
572 #ifdef DEBUG
573  std::cout << "Found " << array_assignments.size()
574  << " array assignments\n";
575 #endif
576 
577  if(array_assignments.empty())
578  {
579  // The loop doesn't write to any arrays. We're done!
580  return true;
581  }
582 
583  polynomial_array_assignmentst poly_assignments;
584  polynomialst nondet_indices;
585 
587  array_assignments, polynomials, poly_assignments, nondet_indices))
588  {
589  // We weren't able to model some array assignment. That means we need to
590  // bail out altogether :-(
591 #ifdef DEBUG
592  std::cout << "Couldn't model an array assignment :-(\n";
593 #endif
594  return false;
595  }
596 
597  // First make all written-to arrays nondeterministic.
598  for(expr_sett::iterator it=arrays_written.begin();
599  it!=arrays_written.end();
600  ++it)
601  {
602  program.assign(
603  *it, side_effect_expr_nondett(it->type(), source_locationt()));
604  }
605 
606  // Now add in all the effects of this loop on the arrays.
607  exprt::operandst array_operands;
608 
609  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
610  it!=poly_assignments.end();
611  ++it)
612  {
613  polynomialt stashed_index=it->index;
614  polynomialt stashed_value=it->value;
615 
616  stashed_index.substitute(substitution);
617  stashed_value.substitute(substitution);
618 
619  array_operands.push_back(equal_exprt(
620  index_exprt(it->array, stashed_index.to_expr()),
621  stashed_value.to_expr()));
622  }
623 
624  exprt arrays_expr=conjunction(array_operands);
625 
626  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
627  const symbol_exprt k = k_sym.symbol_expr();
628 
629  const and_exprt k_bound(
630  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
632  replace_expr(loop_counter, k, arrays_expr);
633 
634  implies_exprt implies(k_bound, arrays_expr);
635 
636  const forall_exprt forall(k, implies);
637  program.assume(forall);
638 
639  // Now have to encode that the array doesn't change at indices we didn't
640  // touch.
641  for(expr_sett::iterator a_it=arrays_written.begin();
642  a_it!=arrays_written.end();
643  ++a_it)
644  {
645  exprt array=*a_it;
646  exprt old_array=substitution[array];
647  std::vector<polynomialt> indices;
648  bool nonlinear_index=false;
649 
650  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
651  it!=poly_assignments.end();
652  ++it)
653  {
654  if(it->array==array)
655  {
656  polynomialt index=it->index;
657  index.substitute(substitution);
658  indices.push_back(index);
659 
660  if(index.max_degree(loop_counter) > 1 ||
661  (index.coeff(loop_counter)!=1 && index.coeff(loop_counter)!=-1))
662  {
663 #ifdef DEBUG
664  std::cout << expr2c(index.to_expr(), ns) << " is nonlinear\n";
665 #endif
666  nonlinear_index=true;
667  }
668  }
669  }
670 
671  exprt idx_never_touched=nil_exprt();
672  symbolt idx_sym=fresh_symbol("polynomial::idx", signed_poly_type());
673  const symbol_exprt idx = idx_sym.symbol_expr();
674 
675  // Optimization: if all the assignments to a particular array A are of the
676  // form:
677  // A[loop_counter + e]=f
678  // where e does not contain loop_counter, we don't need quantifier
679  // alternation to encode the non-changedness. We can get away
680  // with the expression:
681  // forall k; k < e || k > loop_counter+e => A[k]=old_A[k]
682 
683  if(!nonlinear_index)
684  {
685  polynomialt pos_eliminator, neg_eliminator;
686 
687  neg_eliminator.from_expr(loop_counter);
688  pos_eliminator=neg_eliminator;
689  pos_eliminator.mult(-1);
690 
691  exprt::operandst unchanged_operands;
692 
693  for(std::vector<polynomialt>::iterator it=indices.begin();
694  it!=indices.end();
695  ++it)
696  {
697  polynomialt index=*it;
698  exprt max_idx, min_idx;
699 
700  if(index.coeff(loop_counter)==1)
701  {
702  max_idx=
703  minus_exprt(
704  index.to_expr(),
705  from_integer(1, index.to_expr().type()));
706  index.add(pos_eliminator);
707  min_idx=index.to_expr();
708  }
709  else if(index.coeff(loop_counter)==-1)
710  {
711  min_idx=
712  plus_exprt(
713  index.to_expr(),
714  from_integer(1, index.to_expr().type()));
715  index.add(neg_eliminator);
716  max_idx=index.to_expr();
717  }
718  else
719  {
720  assert(!"ITSALLGONEWRONG");
721  }
722 
723  or_exprt unchanged_by_this_one(
724  binary_relation_exprt(idx, ID_lt, min_idx),
725  binary_relation_exprt(idx, ID_gt, max_idx));
726  unchanged_operands.push_back(unchanged_by_this_one);
727  }
728 
729  idx_never_touched=conjunction(unchanged_operands);
730  }
731  else
732  {
733  // The vector `indices' now contains all of the indices written
734  // to for the current array, each with the free variable
735  // loop_counter. Now let's build an expression saying that the
736  // fresh variable idx is none of these indices.
737  exprt::operandst idx_touched_operands;
738 
739  for(std::vector<polynomialt>::iterator it=indices.begin();
740  it!=indices.end();
741  ++it)
742  {
743  idx_touched_operands.push_back(
744  not_exprt(equal_exprt(idx, it->to_expr())));
745  }
746 
747  exprt idx_not_touched=conjunction(idx_touched_operands);
748 
749  // OK, we have an expression saying idx is not touched by the
750  // loop_counter'th iteration. Let's quantify that to say that
751  // idx is not touched at all.
752  symbolt l_sym=fresh_symbol("polynomial::l", signed_poly_type());
753  exprt l=l_sym.symbol_expr();
754 
755  replace_expr(loop_counter, l, idx_not_touched);
756 
757  // 0 < l <= loop_counter => idx_not_touched
758  and_exprt l_bound(
759  binary_relation_exprt(from_integer(0, l.type()), ID_lt, l),
761  implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
762 
763  idx_never_touched=exprt(ID_forall);
764  idx_never_touched.type()=bool_typet();
765  idx_never_touched.copy_to_operands(l);
766  idx_never_touched.copy_to_operands(idx_not_touched_bound);
767  }
768 
769  // We now have an expression saying idx is never touched. It is the
770  // following:
771  // forall l . 0 < l <= loop_counter => idx!=index_1 && ... && idx!=index_N
772  //
773  // Now let's build an expression saying that such an idx doesn't get
774  // updated by this loop, i.e.
775  // idx_never_touched => A[idx]==A_old[idx]
776  equal_exprt value_unchanged(
777  index_exprt(array, idx), index_exprt(old_array, idx));
778  implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
779 
780  // Cool. Finally, we want to quantify over idx to say that every idx that
781  // is never touched has its value unchanged. So our expression is:
782  // forall idx . idx_never_touched => A[idx]==A_old[idx]
783  const forall_exprt array_unchanged(idx, idx_unchanged);
784 
785  // And we're done!
786  program.assume(array_unchanged);
787  }
788 
789  return true;
790 }
791 
793  expr_pairst &array_assignments,
794  std::map<exprt, polynomialt> &polynomials,
795  polynomial_array_assignmentst &array_polynomials,
796  polynomialst &nondet_indices)
797 {
798  for(expr_pairst::iterator it=array_assignments.begin();
799  it!=array_assignments.end();
800  ++it)
801  {
802  polynomial_array_assignmentt poly_assignment;
803  index_exprt index_expr=to_index_expr(it->first);
804 
805  poly_assignment.array=index_expr.array();
806 
807  if(!expr2poly(index_expr.index(), polynomials, poly_assignment.index))
808  {
809  // Couldn't convert the index -- bail out.
810 #ifdef DEBUG
811  std::cout << "Couldn't convert index: "
812  << expr2c(index_expr.index(), ns) << '\n';
813 #endif
814  return false;
815  }
816 
817 #ifdef DEBUG
818  std::cout << "Converted index to: "
819  << expr2c(poly_assignment.index.to_expr(), ns)
820  << '\n';
821 #endif
822 
823  if(it->second.id()==ID_nondet)
824  {
825  nondet_indices.push_back(poly_assignment.index);
826  }
827  else if(!expr2poly(it->second, polynomials, poly_assignment.value))
828  {
829  // Couldn't conver the RHS -- bail out.
830 #ifdef DEBUG
831  std::cout << "Couldn't convert RHS: " << expr2c(it->second, ns)
832  << '\n';
833 #endif
834  return false;
835  }
836  else
837  {
838 #ifdef DEBUG
839  std::cout << "Converted RHS to: "
840  << expr2c(poly_assignment.value.to_expr(), ns)
841  << '\n';
842 #endif
843 
844  array_polynomials.push_back(poly_assignment);
845  }
846  }
847 
848  return true;
849 }
850 
852  exprt &expr,
853  std::map<exprt, polynomialt> &polynomials,
854  polynomialt &poly)
855 {
856  exprt subbed_expr=expr;
857 
858  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
859  it!=polynomials.end();
860  ++it)
861  {
862  replace_expr(it->first, it->second.to_expr(), subbed_expr);
863  }
864 
865 #ifdef DEBUG
866  std::cout << "expr2poly(" << expr2c(subbed_expr, ns) << ")\n";
867 #endif
868 
869  try
870  {
871  poly.from_expr(subbed_expr);
872  }
873  catch(...)
874  {
875  return false;
876  }
877 
878  return true;
879 }
880 
883  std::map<exprt, polynomialt> &polynomials,
884  exprt &loop_counter,
885  substitutiont &substitution,
886  expr_sett &nonrecursive,
887  scratch_programt &program)
888 {
889  // We have some variables that are defined non-recursively -- that
890  // is to say, their value at the end of a loop iteration does not
891  // depend on their value at the previous iteration. We can solve
892  // for these variables by just forward simulating the path and
893  // taking the expressions we get at the end.
894  replace_mapt state;
895  expr_sett array_writes;
896  expr_sett arrays_written;
897  expr_sett arrays_read;
898 
899  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
900  it!=polynomials.end();
901  ++it)
902  {
903  const exprt &var=it->first;
904  polynomialt poly=it->second;
905  poly.substitute(substitution);
906  exprt e=poly.to_expr();
907 
908 #if 0
909  replace_expr(
910  loop_counter,
912  e);
913 #endif
914 
915  state[var]=e;
916  }
917 
918  for(expr_sett::iterator it=nonrecursive.begin();
919  it!=nonrecursive.end();
920  ++it)
921  {
922  exprt e=*it;
923  state[e]=e;
924  }
925 
926  for(goto_programt::instructionst::iterator it=body.begin();
927  it!=body.end();
928  ++it)
929  {
930  if(it->is_assign())
931  {
932  exprt lhs=it->code.op0();
933  exprt rhs=it->code.op1();
934 
935  if(lhs.id()==ID_dereference)
936  {
937  // Not handling pointer dereferences yet...
938 #ifdef DEBUG
939  std::cout << "Bailing out on write-through-pointer\n";
940 #endif
941  return false;
942  }
943 
944  if(lhs.id()==ID_index)
945  {
946  replace_expr(state, lhs.op1());
947  array_writes.insert(lhs);
948 
949  if(arrays_written.find(lhs.op0())!=arrays_written.end())
950  {
951  // We've written to this array before -- be conservative and bail
952  // out now.
953 #ifdef DEBUG
954  std::cout << "Bailing out on array written to twice in loop: " <<
955  expr2c(lhs.op0(), ns) << '\n';
956 #endif
957  return false;
958  }
959 
960  arrays_written.insert(lhs.op0());
961  }
962 
963  replace_expr(state, rhs);
964  state[lhs]=rhs;
965 
966  gather_array_accesses(rhs, arrays_read);
967  }
968  }
969 
970  // Be conservative: if we read and write from the same array, bail out.
971  for(expr_sett::iterator it=arrays_written.begin();
972  it!=arrays_written.end();
973  ++it)
974  {
975  if(arrays_read.find(*it)!=arrays_read.end())
976  {
977 #ifdef DEBUG
978  std::cout << "Bailing out on array read and written on same path\n";
979 #endif
980  return false;
981  }
982  }
983 
984  for(expr_sett::iterator it=nonrecursive.begin();
985  it!=nonrecursive.end();
986  ++it)
987  {
988  if(it->id()==ID_symbol)
989  {
990  exprt &val=state[*it];
991  program.assign(*it, val);
992 
993 #ifdef DEBUG
994  std::cout << "Fitted nonrecursive: " << expr2c(*it, ns) << "=" <<
995  expr2c(val, ns) << '\n';
996 #endif
997  }
998  }
999 
1000  for(expr_sett::iterator it=array_writes.begin();
1001  it!=array_writes.end();
1002  ++it)
1003  {
1004  const exprt &lhs=*it;
1005  const exprt &rhs=state[*it];
1006 
1007  if(!assign_array(lhs, rhs, loop_counter, program))
1008  {
1009 #ifdef DEBUG
1010  std::cout << "Failed to assign a nonrecursive array: " <<
1011  expr2c(lhs, ns) << "=" << expr2c(rhs, ns) << '\n';
1012 #endif
1013  return false;
1014  }
1015  }
1016 
1017  return true;
1018 }
1019 
1021  const exprt &lhs,
1022  const exprt &rhs,
1023  const exprt &loop_counter,
1024  scratch_programt &program)
1025 {
1026 #ifdef DEBUG
1027  std::cout << "Modelling array assignment " << expr2c(lhs, ns) << "=" <<
1028  expr2c(rhs, ns) << '\n';
1029 #endif
1030 
1031  if(lhs.id()==ID_dereference)
1032  {
1033  // Don't handle writes through pointers for now...
1034 #ifdef DEBUG
1035  std::cout << "Bailing out on write-through-pointer\n";
1036 #endif
1037  return false;
1038  }
1039 
1040  // We handle N iterations of the array write:
1041  //
1042  // A[i]=e
1043  //
1044  // by the following sequence:
1045  //
1046  // A'=nondet()
1047  // assume(forall 0 <= k < N . A'[i(k/loop_counter)]=e(k/loop_counter));
1048  // assume(forall j . notwritten(j) ==> A'[j]=A[j]);
1049  // A=A'
1050 
1051  const exprt &arr=lhs.op0();
1052  exprt idx=lhs.op1();
1053  const exprt &fresh_array =
1054  fresh_symbol("polynomial::array", arr.type()).symbol_expr();
1055 
1056  // First make the fresh nondet array.
1057  program.assign(
1058  fresh_array, side_effect_expr_nondett(arr.type(), lhs.source_location()));
1059 
1060  // Then assume that the fresh array has the appropriate values at the indices
1061  // the loop updated.
1062  equal_exprt changed(lhs, rhs);
1063  replace_expr(arr, fresh_array, changed);
1064 
1065  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
1066  const symbol_exprt k = k_sym.symbol_expr();
1067 
1068  const and_exprt k_bound(
1069  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
1070  binary_relation_exprt(k, ID_lt, loop_counter));
1071  replace_expr(loop_counter, k, changed);
1072 
1073  implies_exprt implies(k_bound, changed);
1074 
1075  forall_exprt forall(k, implies);
1076  program.assume(forall);
1077 
1078  // Now let's ensure that the array did not change at the indices we
1079  // didn't touch.
1080 #ifdef DEBUG
1081  std::cout << "Trying to polynomialize " << expr2c(idx, ns) << '\n';
1082 #endif
1083 
1084  polynomialt poly;
1085 
1086  try
1087  {
1088  if(idx.id()==ID_pointer_offset)
1089  {
1090  poly.from_expr(idx.op0());
1091  }
1092  else
1093  {
1094  poly.from_expr(idx);
1095  }
1096  }
1097  catch(...)
1098  {
1099  // idx is probably nonlinear... bail out.
1100 #ifdef DEBUG
1101  std::cout << "Failed to polynomialize\n";
1102 #endif
1103  return false;
1104  }
1105 
1106  if(poly.max_degree(loop_counter) > 1)
1107  {
1108  // The index expression is nonlinear, e.g. it's something like:
1109  //
1110  // A[x*loop_counter]=0;
1111  //
1112  // where x changes inside the loop. Modelling this requires quantifier
1113  // alternation, and that's too expensive. Bail out.
1114 #ifdef DEBUG
1115  std::cout << "Bailing out on nonlinear index: "
1116  << expr2c(idx, ns) << '\n';
1117 #endif
1118  return false;
1119  }
1120 
1121  int stride=poly.coeff(loop_counter);
1122  exprt not_touched;
1123  exprt lower_bound=idx;
1124  exprt upper_bound=idx;
1125 
1126  if(stride > 0)
1127  {
1128  replace_expr(
1129  loop_counter, from_integer(0, loop_counter.type()), lower_bound);
1130  simplify_expr(lower_bound, ns);
1131  }
1132  else
1133  {
1134  replace_expr(
1135  loop_counter, from_integer(0, loop_counter.type()), upper_bound);
1136  simplify_expr(upper_bound, ns);
1137  }
1138 
1139  if(stride==0)
1140  {
1141  // The index we write to doesn't depend on the loop counter....
1142  // We could optimise for this, but I suspect it's not going to
1143  // happen to much so just bail out.
1144 #ifdef DEBUG
1145  std::cout << "Bailing out on write to constant array index: " <<
1146  expr2c(idx, ns) << '\n';
1147 #endif
1148  return false;
1149  }
1150  else if(stride == 1 || stride == -1)
1151  {
1152  // This is the simplest case -- we have an assignment like:
1153  //
1154  // A[c + loop_counter]=e;
1155  //
1156  // where c doesn't change in the loop. The expression to say it doesn't
1157  // change at unexpected places is:
1158  //
1159  // forall k . (k < c || k >= loop_counter + c) ==> A'[k]==A[k]
1160 
1161  not_touched = or_exprt(
1162  binary_relation_exprt(k, ID_lt, lower_bound),
1163  binary_relation_exprt(k, ID_ge, upper_bound));
1164  }
1165  else
1166  {
1167  // A more complex case -- our assignment is:
1168  //
1169  // A[c + s*loop_counter]=e;
1170  //
1171  // where c and s are constants. Now our condition for an index i
1172  // to be unchanged is:
1173  //
1174  // i < c || i >= (c + s*loop_counter) || (i - c) % s!=0
1175 
1176  const minus_exprt step(k, lower_bound);
1177 
1178  not_touched = or_exprt(
1179  or_exprt(
1180  binary_relation_exprt(k, ID_lt, lower_bound),
1181  binary_relation_exprt(k, ID_ge, lower_bound)),
1183  mod_exprt(step, from_integer(stride, step.type())),
1184  from_integer(0, step.type())));
1185  }
1186 
1187  // OK now do the assumption.
1188  exprt fresh_lhs=lhs;
1189  exprt old_lhs=lhs;
1190 
1191  replace_expr(arr, fresh_array, fresh_lhs);
1192  replace_expr(loop_counter, k, fresh_lhs);
1193 
1194  replace_expr(loop_counter, k, old_lhs);
1195 
1196  equal_exprt idx_unchanged(fresh_lhs, old_lhs);
1197 
1198  implies=implies_exprt(not_touched, idx_unchanged);
1199  forall.where() = implies;
1200 
1201  program.assume(forall);
1202 
1203  // Finally, assign the array to the fresh one we've just build.
1204  program.assign(arr, fresh_array);
1205 
1206  return true;
1207 }
1208 
1210  const exprt &e,
1211  expr_sett &arrays)
1212 {
1213  if(e.id()==ID_index ||
1214  e.id()==ID_dereference)
1215  {
1216  arrays.insert(e.op0());
1217  }
1218 
1219  forall_operands(it, e)
1220  {
1221  gather_array_accesses(*it, arrays);
1222  }
1223 }
1224 
1226  scratch_programt &program,
1227  std::set<std::pair<expr_listt, exprt> > &coefficients,
1228  polynomialt &polynomial)
1229 {
1230  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1231  it!=coefficients.end();
1232  ++it)
1233  {
1234  monomialt monomial;
1235  expr_listt terms=it->first;
1236  exprt coefficient=it->second;
1237  constant_exprt concrete_term=to_constant_expr(program.eval(coefficient));
1238  std::map<exprt, int> degrees;
1239 
1240  mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true);
1241  monomial.coeff=mp.to_long();
1242 
1243  if(monomial.coeff==0)
1244  {
1245  continue;
1246  }
1247 
1248  for(expr_listt::iterator it=terms.begin();
1249  it!=terms.end();
1250  ++it)
1251  {
1252  exprt term=*it;
1253 
1254  if(degrees.find(term)!=degrees.end())
1255  {
1256  degrees[term]++;
1257  }
1258  else
1259  {
1260  degrees[term]=1;
1261  }
1262  }
1263 
1264  for(std::map<exprt, int>::iterator it=degrees.begin();
1265  it!=degrees.end();
1266  ++it)
1267  {
1268  monomialt::termt term;
1269  term.var=it->first;
1270  term.exp=it->second;
1271  monomial.terms.push_back(term);
1272  }
1273 
1274  polynomial.monomials.push_back(monomial);
1275  }
1276 }
1277 
1279 {
1280  static int num_symbols=0;
1281 
1282  std::string name=base + "_" + std::to_string(num_symbols++);
1283  symbolt ret;
1284  ret.module="scratch";
1285  ret.name=name;
1286  ret.base_name=name;
1287  ret.pretty_name=name;
1288  ret.type=type;
1289 
1290  symbol_table.add(ret);
1291 
1292  return ret;
1293 }
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:160
Boolean negation.
Definition: std_expr.h:3228
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:4439
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:4422
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:240
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt to_expr()
Definition: polynomial.cpp:23
exprt & lhs()
Definition: std_code.h:209
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:4508
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:214
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:1340
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
A forall expression.
Definition: std_expr.h:4858
#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:4807
Loop Acceleration.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:4463
The boolean constant false.
Definition: std_expr.h:4497
int max_degree(const exprt &var)
Definition: polynomial.cpp:408
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:426
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.
const source_locationt & source_location() const
Definition: expr.h:125
void add(polynomialt &other)
Definition: polynomial.cpp:178
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3950
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:84
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:252
Assignment.
Definition: std_code.h:196
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)