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  substitutiont &substitution,
560  scratch_programt &program)
561 {
562 #ifdef DEBUG
563  std::cout << "Doing arrays...\n";
564 #endif
565 
566  expr_sett arrays_written;
567  expr_pairst array_assignments;
568 
569  array_assignments=gather_array_assignments(loop_body, arrays_written);
570 
571 #ifdef DEBUG
572  std::cout << "Found " << array_assignments.size()
573  << " array assignments\n";
574 #endif
575 
576  if(array_assignments.empty())
577  {
578  // The loop doesn't write to any arrays. We're done!
579  return true;
580  }
581 
582  polynomial_array_assignmentst poly_assignments;
583  polynomialst nondet_indices;
584 
586  array_assignments, polynomials, poly_assignments, nondet_indices))
587  {
588  // We weren't able to model some array assignment. That means we need to
589  // bail out altogether :-(
590 #ifdef DEBUG
591  std::cout << "Couldn't model an array assignment :-(\n";
592 #endif
593  return false;
594  }
595 
596  // First make all written-to arrays nondeterministic.
597  for(expr_sett::iterator it=arrays_written.begin();
598  it!=arrays_written.end();
599  ++it)
600  {
601  program.assign(
602  *it, side_effect_expr_nondett(it->type(), source_locationt()));
603  }
604 
605  // Now add in all the effects of this loop on the arrays.
606  exprt::operandst array_operands;
607 
608  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
609  it!=poly_assignments.end();
610  ++it)
611  {
612  polynomialt stashed_index=it->index;
613  polynomialt stashed_value=it->value;
614 
615  stashed_index.substitute(substitution);
616  stashed_value.substitute(substitution);
617 
618  array_operands.push_back(equal_exprt(
619  index_exprt(it->array, stashed_index.to_expr()),
620  stashed_value.to_expr()));
621  }
622 
623  exprt arrays_expr=conjunction(array_operands);
624 
625  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
626  const symbol_exprt k = k_sym.symbol_expr();
627 
628  const and_exprt k_bound(
629  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
631  replace_expr(loop_counter, k, arrays_expr);
632 
633  implies_exprt implies(k_bound, arrays_expr);
634 
635  const forall_exprt forall(k, implies);
636  program.assume(forall);
637 
638  // Now have to encode that the array doesn't change at indices we didn't
639  // touch.
640  for(expr_sett::iterator a_it=arrays_written.begin();
641  a_it!=arrays_written.end();
642  ++a_it)
643  {
644  exprt array=*a_it;
645  exprt old_array=substitution[array];
646  std::vector<polynomialt> indices;
647  bool nonlinear_index=false;
648 
649  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
650  it!=poly_assignments.end();
651  ++it)
652  {
653  if(it->array==array)
654  {
655  polynomialt index=it->index;
656  index.substitute(substitution);
657  indices.push_back(index);
658 
659  if(index.max_degree(loop_counter) > 1 ||
660  (index.coeff(loop_counter)!=1 && index.coeff(loop_counter)!=-1))
661  {
662 #ifdef DEBUG
663  std::cout << expr2c(index.to_expr(), ns) << " is nonlinear\n";
664 #endif
665  nonlinear_index=true;
666  }
667  }
668  }
669 
670  exprt idx_never_touched=nil_exprt();
671  symbolt idx_sym=fresh_symbol("polynomial::idx", signed_poly_type());
672  const symbol_exprt idx = idx_sym.symbol_expr();
673 
674  // Optimization: if all the assignments to a particular array A are of the
675  // form:
676  // A[loop_counter + e]=f
677  // where e does not contain loop_counter, we don't need quantifier
678  // alternation to encode the non-changedness. We can get away
679  // with the expression:
680  // forall k; k < e || k > loop_counter+e => A[k]=old_A[k]
681 
682  if(!nonlinear_index)
683  {
684  polynomialt pos_eliminator, neg_eliminator;
685 
686  neg_eliminator.from_expr(loop_counter);
687  pos_eliminator=neg_eliminator;
688  pos_eliminator.mult(-1);
689 
690  exprt::operandst unchanged_operands;
691 
692  for(std::vector<polynomialt>::iterator it=indices.begin();
693  it!=indices.end();
694  ++it)
695  {
696  polynomialt index=*it;
697  exprt max_idx, min_idx;
698 
699  if(index.coeff(loop_counter)==1)
700  {
701  max_idx=
702  minus_exprt(
703  index.to_expr(),
704  from_integer(1, index.to_expr().type()));
705  index.add(pos_eliminator);
706  min_idx=index.to_expr();
707  }
708  else if(index.coeff(loop_counter)==-1)
709  {
710  min_idx=
711  plus_exprt(
712  index.to_expr(),
713  from_integer(1, index.to_expr().type()));
714  index.add(neg_eliminator);
715  max_idx=index.to_expr();
716  }
717  else
718  {
719  assert(!"ITSALLGONEWRONG");
720  }
721 
722  or_exprt unchanged_by_this_one(
723  binary_relation_exprt(idx, ID_lt, min_idx),
724  binary_relation_exprt(idx, ID_gt, max_idx));
725  unchanged_operands.push_back(unchanged_by_this_one);
726  }
727 
728  idx_never_touched=conjunction(unchanged_operands);
729  }
730  else
731  {
732  // The vector `indices' now contains all of the indices written
733  // to for the current array, each with the free variable
734  // loop_counter. Now let's build an expression saying that the
735  // fresh variable idx is none of these indices.
736  exprt::operandst idx_touched_operands;
737 
738  for(std::vector<polynomialt>::iterator it=indices.begin();
739  it!=indices.end();
740  ++it)
741  {
742  idx_touched_operands.push_back(
743  not_exprt(equal_exprt(idx, it->to_expr())));
744  }
745 
746  exprt idx_not_touched=conjunction(idx_touched_operands);
747 
748  // OK, we have an expression saying idx is not touched by the
749  // loop_counter'th iteration. Let's quantify that to say that
750  // idx is not touched at all.
751  symbolt l_sym=fresh_symbol("polynomial::l", signed_poly_type());
752  exprt l=l_sym.symbol_expr();
753 
754  replace_expr(loop_counter, l, idx_not_touched);
755 
756  // 0 < l <= loop_counter => idx_not_touched
757  and_exprt l_bound(
758  binary_relation_exprt(from_integer(0, l.type()), ID_lt, l),
760  implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
761 
762  idx_never_touched=exprt(ID_forall);
763  idx_never_touched.type()=bool_typet();
764  idx_never_touched.copy_to_operands(l);
765  idx_never_touched.copy_to_operands(idx_not_touched_bound);
766  }
767 
768  // We now have an expression saying idx is never touched. It is the
769  // following:
770  // forall l . 0 < l <= loop_counter => idx!=index_1 && ... && idx!=index_N
771  //
772  // Now let's build an expression saying that such an idx doesn't get
773  // updated by this loop, i.e.
774  // idx_never_touched => A[idx]==A_old[idx]
775  equal_exprt value_unchanged(
776  index_exprt(array, idx), index_exprt(old_array, idx));
777  implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
778 
779  // Cool. Finally, we want to quantify over idx to say that every idx that
780  // is never touched has its value unchanged. So our expression is:
781  // forall idx . idx_never_touched => A[idx]==A_old[idx]
782  const forall_exprt array_unchanged(idx, idx_unchanged);
783 
784  // And we're done!
785  program.assume(array_unchanged);
786  }
787 
788  return true;
789 }
790 
792  expr_pairst &array_assignments,
793  std::map<exprt, polynomialt> &polynomials,
794  polynomial_array_assignmentst &array_polynomials,
795  polynomialst &nondet_indices)
796 {
797  for(expr_pairst::iterator it=array_assignments.begin();
798  it!=array_assignments.end();
799  ++it)
800  {
801  polynomial_array_assignmentt poly_assignment;
802  index_exprt index_expr=to_index_expr(it->first);
803 
804  poly_assignment.array=index_expr.array();
805 
806  if(!expr2poly(index_expr.index(), polynomials, poly_assignment.index))
807  {
808  // Couldn't convert the index -- bail out.
809 #ifdef DEBUG
810  std::cout << "Couldn't convert index: "
811  << expr2c(index_expr.index(), ns) << '\n';
812 #endif
813  return false;
814  }
815 
816 #ifdef DEBUG
817  std::cout << "Converted index to: "
818  << expr2c(poly_assignment.index.to_expr(), ns)
819  << '\n';
820 #endif
821 
822  if(it->second.id()==ID_nondet)
823  {
824  nondet_indices.push_back(poly_assignment.index);
825  }
826  else if(!expr2poly(it->second, polynomials, poly_assignment.value))
827  {
828  // Couldn't conver the RHS -- bail out.
829 #ifdef DEBUG
830  std::cout << "Couldn't convert RHS: " << expr2c(it->second, ns)
831  << '\n';
832 #endif
833  return false;
834  }
835  else
836  {
837 #ifdef DEBUG
838  std::cout << "Converted RHS to: "
839  << expr2c(poly_assignment.value.to_expr(), ns)
840  << '\n';
841 #endif
842 
843  array_polynomials.push_back(poly_assignment);
844  }
845  }
846 
847  return true;
848 }
849 
851  exprt &expr,
852  std::map<exprt, polynomialt> &polynomials,
853  polynomialt &poly)
854 {
855  exprt subbed_expr=expr;
856 
857  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
858  it!=polynomials.end();
859  ++it)
860  {
861  replace_expr(it->first, it->second.to_expr(), subbed_expr);
862  }
863 
864 #ifdef DEBUG
865  std::cout << "expr2poly(" << expr2c(subbed_expr, ns) << ")\n";
866 #endif
867 
868  try
869  {
870  poly.from_expr(subbed_expr);
871  }
872  catch(...)
873  {
874  return false;
875  }
876 
877  return true;
878 }
879 
882  std::map<exprt, polynomialt> &polynomials,
883  substitutiont &substitution,
884  expr_sett &nonrecursive,
885  scratch_programt &program)
886 {
887  // We have some variables that are defined non-recursively -- that
888  // is to say, their value at the end of a loop iteration does not
889  // depend on their value at the previous iteration. We can solve
890  // for these variables by just forward simulating the path and
891  // taking the expressions we get at the end.
892  replace_mapt state;
893  expr_sett array_writes;
894  expr_sett arrays_written;
895  expr_sett arrays_read;
896 
897  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
898  it!=polynomials.end();
899  ++it)
900  {
901  const exprt &var=it->first;
902  polynomialt poly=it->second;
903  poly.substitute(substitution);
904  exprt e=poly.to_expr();
905 
906 #if 0
907  replace_expr(
908  loop_counter,
910  e);
911 #endif
912 
913  state[var]=e;
914  }
915 
916  for(expr_sett::iterator it=nonrecursive.begin();
917  it!=nonrecursive.end();
918  ++it)
919  {
920  exprt e=*it;
921  state[e]=e;
922  }
923 
924  for(goto_programt::instructionst::iterator it=body.begin();
925  it!=body.end();
926  ++it)
927  {
928  if(it->is_assign())
929  {
930  exprt lhs=it->code.op0();
931  exprt rhs=it->code.op1();
932 
933  if(lhs.id()==ID_dereference)
934  {
935  // Not handling pointer dereferences yet...
936 #ifdef DEBUG
937  std::cout << "Bailing out on write-through-pointer\n";
938 #endif
939  return false;
940  }
941 
942  if(lhs.id()==ID_index)
943  {
944  replace_expr(state, lhs.op1());
945  array_writes.insert(lhs);
946 
947  if(arrays_written.find(lhs.op0())!=arrays_written.end())
948  {
949  // We've written to this array before -- be conservative and bail
950  // out now.
951 #ifdef DEBUG
952  std::cout << "Bailing out on array written to twice in loop: " <<
953  expr2c(lhs.op0(), ns) << '\n';
954 #endif
955  return false;
956  }
957 
958  arrays_written.insert(lhs.op0());
959  }
960 
961  replace_expr(state, rhs);
962  state[lhs]=rhs;
963 
964  gather_array_accesses(rhs, arrays_read);
965  }
966  }
967 
968  // Be conservative: if we read and write from the same array, bail out.
969  for(expr_sett::iterator it=arrays_written.begin();
970  it!=arrays_written.end();
971  ++it)
972  {
973  if(arrays_read.find(*it)!=arrays_read.end())
974  {
975 #ifdef DEBUG
976  std::cout << "Bailing out on array read and written on same path\n";
977 #endif
978  return false;
979  }
980  }
981 
982  for(expr_sett::iterator it=nonrecursive.begin();
983  it!=nonrecursive.end();
984  ++it)
985  {
986  if(it->id()==ID_symbol)
987  {
988  exprt &val=state[*it];
989  program.assign(*it, val);
990 
991 #ifdef DEBUG
992  std::cout << "Fitted nonrecursive: " << expr2c(*it, ns) << "=" <<
993  expr2c(val, ns) << '\n';
994 #endif
995  }
996  }
997 
998  for(expr_sett::iterator it=array_writes.begin();
999  it!=array_writes.end();
1000  ++it)
1001  {
1002  const exprt &lhs=*it;
1003  const exprt &rhs=state[*it];
1004 
1005  if(!assign_array(lhs, rhs, program))
1006  {
1007 #ifdef DEBUG
1008  std::cout << "Failed to assign a nonrecursive array: " <<
1009  expr2c(lhs, ns) << "=" << expr2c(rhs, ns) << '\n';
1010 #endif
1011  return false;
1012  }
1013  }
1014 
1015  return true;
1016 }
1017 
1019  const exprt &lhs,
1020  const exprt &rhs,
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(
1055  fresh_array, side_effect_expr_nondett(arr.type(), lhs.source_location()));
1056 
1057  // Then assume that the fresh array has the appropriate values at the indices
1058  // the loop updated.
1059  equal_exprt changed(lhs, rhs);
1060  replace_expr(arr, fresh_array, changed);
1061 
1062  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
1063  const symbol_exprt k = k_sym.symbol_expr();
1064 
1065  const and_exprt k_bound(
1066  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
1067  binary_relation_exprt(k, ID_lt, loop_counter));
1068  replace_expr(loop_counter, k, changed);
1069 
1070  implies_exprt implies(k_bound, changed);
1071 
1072  forall_exprt forall(k, implies);
1073  program.assume(forall);
1074 
1075  // Now let's ensure that the array did not change at the indices we
1076  // didn't touch.
1077 #ifdef DEBUG
1078  std::cout << "Trying to polynomialize " << expr2c(idx, ns) << '\n';
1079 #endif
1080 
1081  polynomialt poly;
1082 
1083  try
1084  {
1085  if(idx.id()==ID_pointer_offset)
1086  {
1087  poly.from_expr(idx.op0());
1088  }
1089  else
1090  {
1091  poly.from_expr(idx);
1092  }
1093  }
1094  catch(...)
1095  {
1096  // idx is probably nonlinear... bail out.
1097 #ifdef DEBUG
1098  std::cout << "Failed to polynomialize\n";
1099 #endif
1100  return false;
1101  }
1102 
1103  if(poly.max_degree(loop_counter) > 1)
1104  {
1105  // The index expression is nonlinear, e.g. it's something like:
1106  //
1107  // A[x*loop_counter]=0;
1108  //
1109  // where x changes inside the loop. Modelling this requires quantifier
1110  // alternation, and that's too expensive. Bail out.
1111 #ifdef DEBUG
1112  std::cout << "Bailing out on nonlinear index: "
1113  << expr2c(idx, ns) << '\n';
1114 #endif
1115  return false;
1116  }
1117 
1118  int stride=poly.coeff(loop_counter);
1119  exprt not_touched;
1120  exprt lower_bound=idx;
1121  exprt upper_bound=idx;
1122 
1123  if(stride > 0)
1124  {
1125  replace_expr(
1126  loop_counter, from_integer(0, loop_counter.type()), lower_bound);
1127  simplify_expr(lower_bound, ns);
1128  }
1129  else
1130  {
1131  replace_expr(
1132  loop_counter, from_integer(0, loop_counter.type()), upper_bound);
1133  simplify_expr(upper_bound, ns);
1134  }
1135 
1136  if(stride==0)
1137  {
1138  // The index we write to doesn't depend on the loop counter....
1139  // We could optimise for this, but I suspect it's not going to
1140  // happen to much so just bail out.
1141 #ifdef DEBUG
1142  std::cout << "Bailing out on write to constant array index: " <<
1143  expr2c(idx, ns) << '\n';
1144 #endif
1145  return false;
1146  }
1147  else if(stride == 1 || stride == -1)
1148  {
1149  // This is the simplest case -- we have an assignment like:
1150  //
1151  // A[c + loop_counter]=e;
1152  //
1153  // where c doesn't change in the loop. The expression to say it doesn't
1154  // change at unexpected places is:
1155  //
1156  // forall k . (k < c || k >= loop_counter + c) ==> A'[k]==A[k]
1157 
1158  not_touched = or_exprt(
1159  binary_relation_exprt(k, ID_lt, lower_bound),
1160  binary_relation_exprt(k, ID_ge, upper_bound));
1161  }
1162  else
1163  {
1164  // A more complex case -- our assignment is:
1165  //
1166  // A[c + s*loop_counter]=e;
1167  //
1168  // where c and s are constants. Now our condition for an index i
1169  // to be unchanged is:
1170  //
1171  // i < c || i >= (c + s*loop_counter) || (i - c) % s!=0
1172 
1173  const minus_exprt step(k, lower_bound);
1174 
1175  not_touched = or_exprt(
1176  or_exprt(
1177  binary_relation_exprt(k, ID_lt, lower_bound),
1178  binary_relation_exprt(k, ID_ge, lower_bound)),
1180  mod_exprt(step, from_integer(stride, step.type())),
1181  from_integer(0, step.type())));
1182  }
1183 
1184  // OK now do the assumption.
1185  exprt fresh_lhs=lhs;
1186  exprt old_lhs=lhs;
1187 
1188  replace_expr(arr, fresh_array, fresh_lhs);
1189  replace_expr(loop_counter, k, fresh_lhs);
1190 
1191  replace_expr(loop_counter, k, old_lhs);
1192 
1193  equal_exprt idx_unchanged(fresh_lhs, old_lhs);
1194 
1195  implies=implies_exprt(not_touched, idx_unchanged);
1196  forall.where() = implies;
1197 
1198  program.assume(forall);
1199 
1200  // Finally, assign the array to the fresh one we've just build.
1201  program.assign(arr, fresh_array);
1202 
1203  return true;
1204 }
1205 
1207  const exprt &e,
1208  expr_sett &arrays)
1209 {
1210  if(e.id()==ID_index ||
1211  e.id()==ID_dereference)
1212  {
1213  arrays.insert(e.op0());
1214  }
1215 
1216  forall_operands(it, e)
1217  {
1218  gather_array_accesses(*it, arrays);
1219  }
1220 }
1221 
1223  scratch_programt &program,
1224  std::set<std::pair<expr_listt, exprt> > &coefficients,
1225  polynomialt &polynomial)
1226 {
1227  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1228  it!=coefficients.end();
1229  ++it)
1230  {
1231  monomialt monomial;
1232  expr_listt terms=it->first;
1233  exprt coefficient=it->second;
1234  constant_exprt concrete_term=to_constant_expr(program.eval(coefficient));
1235  std::map<exprt, int> degrees;
1236 
1237  mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true);
1238  monomial.coeff=mp.to_long();
1239 
1240  if(monomial.coeff==0)
1241  {
1242  continue;
1243  }
1244 
1245  for(const auto &term : terms)
1246  {
1247  if(degrees.find(term)!=degrees.end())
1248  {
1249  degrees[term]++;
1250  }
1251  else
1252  {
1253  degrees[term]=1;
1254  }
1255  }
1256 
1257  for(std::map<exprt, int>::iterator it=degrees.begin();
1258  it!=degrees.end();
1259  ++it)
1260  {
1261  monomialt::termt term;
1262  term.var=it->first;
1263  term.exp=it->second;
1264  monomial.terms.push_back(term);
1265  }
1266 
1267  polynomial.monomials.push_back(monomial);
1268  }
1269 }
1270 
1272 {
1273  static int num_symbols=0;
1274 
1275  std::string name=base + "_" + std::to_string(num_symbols++);
1276  symbolt ret;
1277  ret.module="scratch";
1278  ret.name=name;
1279  ret.base_name=name;
1280  ret.pretty_name=name;
1281  ret.type=type;
1282 
1283  symbol_table.add(ret);
1284 
1285  return ret;
1286 }
std::list< exprt > expr_listt
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
void substitute(substitutiont &substitution)
Definition: polynomial.cpp:160
Boolean negation.
Definition: std_expr.h:3308
BigInt mp_integer
Definition: mp_arith.h:22
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
Boolean OR.
Definition: std_expr.h:2531
exprt & op0()
Definition: expr.h:84
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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
const irep_idt & get_identifier() const
Definition: std_expr.h:176
Goto Programs with Functions.
const irep_idt & get_value() const
Definition: std_expr.h:4403
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:43
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
typet & type()
Return the type of the expression.
Definition: expr.h:68
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
A constant literal expression.
Definition: std_expr.h:4384
std::vector< termt > terms
Definition: polynomial.h:30
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
Boolean implication.
Definition: std_expr.h:2485
signedbv_typet signed_poly_type()
Definition: util.cpp:20
Equality.
Definition: std_expr.h:1484
bool assign_array(const exprt &lhs, const exprt &rhs, scratch_programt &program)
std::list< instructiont > instructionst
Definition: goto_program.h:412
int coeff
Definition: polynomial.h:31
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:50
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
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:269
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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:4461
symbolt fresh_symbol(std::string base, typet type)
exprt & rhs()
Definition: std_code.h:274
exprt eval(const exprt &e)
Symbolic Execution.
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
Boolean AND.
Definition: std_expr.h:2409
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
Loop Acceleration.
API to expression classes.
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
exprt & op1()
Definition: expr.h:87
std::list< path_nodet > patht
Definition: path.h:45
instructionst::const_iterator const_targett
Definition: goto_program.h:415
Disequality.
Definition: std_expr.h:1545
Weakest Preconditions.
void find_modified(const patht &path, expr_sett &modified)
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
A forall expression.
Definition: std_expr.h:4777
#define forall_operands(it, expr)
Definition: expr.h:20
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
Program Transformation.
exprt & where()
Definition: std_expr.h:4729
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:35
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 an exprt to a constant_exprt.
Definition: std_expr.h:4423
The Boolean constant false.
Definition: std_expr.h:4452
int max_degree(const exprt &var)
Definition: polynomial.cpp:408
std::vector< exprt > operandst
Definition: expr.h:57
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:72
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
typet type
Type of symbol.
Definition: symbol.h:31
Loop Acceleration.
void append_path(patht &path)
Loop Acceleration.
exprt & index()
Definition: std_expr.h:1631
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:541
Base class for all expressions.
Definition: expr.h:54
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:46
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3955
const source_locationt & source_location() const
Definition: expr.h:228
void add(polynomialt &other)
Definition: polynomial.cpp:178
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:26
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
Binary minus.
Definition: std_expr.h:1106
void push_nondet(exprt &expr)
symbol_tablet & symbol_table
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Options.
const char * c_str() const
Definition: dstring.h:86
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:26
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
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:804
exprt & array()
Definition: std_expr.h:1621
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
void find_symbols(const exprt &src, find_symbols_sett &dest)
Concrete Goto Program.
Modulo.
Definition: std_expr.h:1287
void mult(int scalar)
Definition: polynomial.cpp:252
A codet representing an assignment in the program.
Definition: std_code.h:256
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:1595
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)