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>
26 
27 #include <goto-symex/goto_symex.h>
29 
30 #include <analyses/goto_check.h>
31 
32 #include <ansi-c/expr2c.h>
33 
34 #include <util/symbol_table.h>
35 #include <util/options.h>
36 #include <util/std_expr.h>
37 #include <util/std_code.h>
38 #include <util/find_symbols.h>
39 #include <util/rename.h>
40 #include <util/simplify_expr.h>
41 #include <util/replace_expr.h>
42 #include <util/arith_tools.h>
43 
44 #include "accelerator.h"
45 #include "util.h"
46 #include "cone_of_influence.h"
47 #include "overflow_instrumenter.h"
48 
50  const exprt &expr,
51  expr_sett &rvalues)
52 {
53  if(expr.id()==ID_symbol ||
54  expr.id()==ID_index ||
55  expr.id()==ID_member ||
56  expr.id()==ID_dereference)
57  {
58  rvalues.insert(expr);
59  }
60  else
61  {
62  forall_operands(it, expr)
63  {
64  gather_rvalues(*it, rvalues);
65  }
66  }
67 }
68 
70  const goto_programt &body,
71  expr_sett &modified)
72 {
74  find_modified(it, modified);
75 }
76 
78  const goto_programt::instructionst &instructions,
79  expr_sett &modified)
80 {
81  for(goto_programt::instructionst::const_iterator
82  it=instructions.begin();
83  it!=instructions.end();
84  ++it)
85  find_modified(it, modified);
86 }
87 
89  const patht &path,
90  expr_sett &modified)
91 {
92  for(const auto &step : path)
93  find_modified(step.loc, modified);
94 }
95 
98  expr_sett &modified)
99 {
100  for(const auto &step : loop)
101  find_modified(step, modified);
102 }
103 
106  expr_sett &modified)
107 {
108  if(t->is_assign())
109  {
110  code_assignt assignment=to_code_assign(t->code);
111  modified.insert(assignment.lhs());
112  }
113 }
114 
115 
117  std::map<exprt, polynomialt> polynomials,
118  patht &path)
119 {
120  // Checking that our polynomial is inductive with respect to the loop body is
121  // equivalent to checking safety of the following program:
122  //
123  // assume (target1==polynomial1);
124  // assume (target2==polynomial2)
125  // ...
126  // loop_body;
127  // loop_counter++;
128  // assert (target1==polynomial1);
129  // assert (target2==polynomial2);
130  // ...
132  std::vector<exprt> polynomials_hold;
133  substitutiont substitution;
134 
135  stash_polynomials(program, polynomials, substitution, path);
136 
137  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
138  it!=polynomials.end();
139  ++it)
140  {
141  exprt holds=equal_exprt(it->first, it->second.to_expr());
142  program.add_instruction(ASSUME)->guard=holds;
143 
144  polynomials_hold.push_back(holds);
145  }
146 
147  program.append_path(path);
148 
149  codet inc_loop_counter=
150  code_assignt(
151  loop_counter,
153  program.add_instruction(ASSIGN)->code=inc_loop_counter;
154 
155  ensure_no_overflows(program);
156 
157  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
158  it!=polynomials_hold.end();
159  ++it)
160  {
161  program.add_instruction(ASSERT)->guard=*it;
162  }
163 
164 #ifdef DEBUG
165  std::cout << "Checking following program for inductiveness:\n";
166  program.output(ns, "", std::cout);
167 #endif
168 
169  try
170  {
171  if(program.check_sat())
172  {
173  // We found a counterexample to inductiveness... :-(
174  #ifdef DEBUG
175  std::cout << "Not inductive!\n";
176  #endif
177  return false;
178  }
179  else
180  {
181  return true;
182  }
183  }
184  catch(std::string s)
185  {
186  std::cout << "Error in inductiveness SAT check: " << s << '\n';
187  return false;
188  }
189  catch (const char *s)
190  {
191  std::cout << "Error in inductiveness SAT check: " << s << '\n';
192  return false;
193  }
194 }
195 
197  scratch_programt &program,
198  std::map<exprt, polynomialt> &polynomials,
199  substitutiont &substitution,
200  patht &path)
201 {
202  expr_sett modified;
203 
204  find_modified(path, modified);
205  stash_variables(program, modified, substitution);
206 
207  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
208  it!=polynomials.end();
209  ++it)
210  {
211  it->second.substitute(substitution);
212  }
213 }
214 
216  scratch_programt &program,
217  expr_sett modified,
218  substitutiont &substitution)
219 {
220  find_symbols_sett vars;
221 
222  for(expr_sett::iterator it=modified.begin();
223  it!=modified.end();
224  ++it)
225  {
226  find_symbols(*it, vars);
227  }
228 
229  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
230  vars.erase(loop_counter_name);
231 
232  for(find_symbols_sett::iterator it=vars.begin();
233  it!=vars.end();
234  ++it)
235  {
236  symbolt orig=symbol_table.lookup(*it);
237  symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
238  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
239  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
240  }
241 }
242 
243 /*
244  * Finds a precondition which guarantees that all the assumptions and assertions
245  * along this path hold.
246  *
247  * This is not the weakest precondition, since we make underapproximations due
248  * to aliasing.
249  */
250 
252 {
253  exprt ret=false_exprt();
254 
255  for(patht::reverse_iterator r_it=path.rbegin();
256  r_it!=path.rend();
257  ++r_it)
258  {
259  goto_programt::const_targett t=r_it->loc;
260 
261  if(t->is_assign())
262  {
263  // XXX Need to check for aliasing...
264  const code_assignt &assignment=to_code_assign(t->code);
265  const exprt &lhs=assignment.lhs();
266  const exprt &rhs=assignment.rhs();
267 
268  if(lhs.id()==ID_symbol ||
269  lhs.id()==ID_index ||
270  lhs.id()==ID_dereference)
271  {
272  replace_expr(lhs, rhs, ret);
273  }
274  else
275  {
276  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
277  }
278  }
279  else if(t->is_assume() || t->is_assert())
280  {
281  ret=implies_exprt(t->guard, ret);
282  }
283  else
284  {
285  // Ignore.
286  }
287 
288  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
289  {
290  // The guard isn't constant true, so we need to accumulate that too.
291  ret=implies_exprt(r_it->guard, ret);
292  }
293  }
294 
295  // Hack: replace array accesses with nondet.
296  expr_mapt array_abstractions;
297  // abstract_arrays(ret, array_abstractions);
298 
299  simplify(ret, ns);
300 
301  return ret;
302 }
303 
305  exprt &expr,
306  expr_mapt &abstractions)
307 {
308  if(expr.id()==ID_index ||
309  expr.id()==ID_dereference)
310  {
311  expr_mapt::iterator it=abstractions.find(expr);
312 
313  if(it==abstractions.end())
314  {
315  symbolt sym=fresh_symbol("accelerate::array_abstraction", expr.type());
316  abstractions[expr]=sym.symbol_expr();
317  expr=sym.symbol_expr();
318  }
319  else
320  {
321  expr=it->second;
322  }
323  }
324  else
325  {
326  Forall_operands(it, expr)
327  {
328  abstract_arrays(*it, abstractions);
329  }
330  }
331 }
332 
334 {
335  Forall_operands(it, expr)
336  {
337  push_nondet(*it);
338  }
339 
340  if(expr.id()==ID_not &&
341  expr.op0().id()==ID_nondet)
342  {
343  expr=side_effect_expr_nondett(expr.type());
344  }
345  else if(expr.id()==ID_equal ||
346  expr.id()==ID_lt ||
347  expr.id()==ID_gt ||
348  expr.id()==ID_le ||
349  expr.id()==ID_ge)
350  {
351  if(expr.op0().id()==ID_nondet ||
352  expr.op1().id()==ID_nondet)
353  {
354  expr=side_effect_expr_nondett(expr.type());
355  }
356  }
357 }
358 
360  std::map<exprt, polynomialt> polynomials,
361  patht &path,
362  exprt &guard)
363 {
364  // We want to check that if an assumption fails, the next iteration can't be
365  // feasible again. To do this we check the following program for safety:
366  //
367  // loop_counter=1;
368  // assume(target1==polynomial1);
369  // assume(target2==polynomial2);
370  // ...
371  // assume(precondition);
372  //
373  // loop_counter=*;
374  // target1=polynomial1);
375  // target2=polynomial2);
376  // ...
377  // assume(!precondition);
378  //
379  // loop_counter++;
380  //
381  // target1=polynomial1;
382  // target2=polynomial2;
383  // ...
384  //
385  // assume(no overflows in above program)
386  // assert(!precondition);
387 
388  exprt condition=precondition(path);
390 
391  substitutiont substitution;
392  stash_polynomials(program, polynomials, substitution, path);
393 
394  std::vector<exprt> polynomials_hold;
395 
396  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
397  it!=polynomials.end();
398  ++it)
399  {
400  exprt lhs=it->first;
401  exprt rhs=it->second.to_expr();
402 
403  polynomials_hold.push_back(equal_exprt(lhs, rhs));
404  }
405 
407 
408  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
409  it!=polynomials_hold.end();
410  ++it)
411  {
412  program.assume(*it);
413  }
414 
415  program.assume(not_exprt(condition));
416 
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(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(*it, side_effect_expr_nondett(it->type()));
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  exprt k=k_sym.symbol_expr();
627 
628  exprt k_bound=
629  and_exprt(
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  exprt forall(ID_forall);
637  forall.type()=bool_typet();
638  forall.copy_to_operands(k);
639  forall.copy_to_operands(implies);
640 
641  program.assume(forall);
642 
643  // Now have to encode that the array doesn't change at indices we didn't
644  // touch.
645  for(expr_sett::iterator a_it=arrays_written.begin();
646  a_it!=arrays_written.end();
647  ++a_it)
648  {
649  exprt array=*a_it;
650  exprt old_array=substitution[array];
651  std::vector<polynomialt> indices;
652  bool nonlinear_index=false;
653 
654  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
655  it!=poly_assignments.end();
656  ++it)
657  {
658  if(it->array==array)
659  {
660  polynomialt index=it->index;
661  index.substitute(substitution);
662  indices.push_back(index);
663 
664  if(index.max_degree(loop_counter) > 1 ||
665  (index.coeff(loop_counter)!=1 && index.coeff(loop_counter)!=-1))
666  {
667 #ifdef DEBUG
668  std::cout << expr2c(index.to_expr(), ns) << " is nonlinear\n";
669 #endif
670  nonlinear_index=true;
671  }
672  }
673  }
674 
675  exprt idx_never_touched=nil_exprt();
676  symbolt idx_sym=fresh_symbol("polynomial::idx", signed_poly_type());
677  exprt idx=idx_sym.symbol_expr();
678 
679 
680  // Optimization: if all the assignments to a particular array A are of the
681  // form:
682  // A[loop_counter + e]=f
683  // where e does not contain loop_counter, we don't need quantifier
684  // alternation to encode the non-changedness. We can get away
685  // with the expression:
686  // forall k; k < e || k > loop_counter+e => A[k]=old_A[k]
687 
688  if(!nonlinear_index)
689  {
690  polynomialt pos_eliminator, neg_eliminator;
691 
692  neg_eliminator.from_expr(loop_counter);
693  pos_eliminator=neg_eliminator;
694  pos_eliminator.mult(-1);
695 
696  exprt::operandst unchanged_operands;
697 
698  for(std::vector<polynomialt>::iterator it=indices.begin();
699  it!=indices.end();
700  ++it)
701  {
702  polynomialt index=*it;
703  exprt max_idx, min_idx;
704 
705  if(index.coeff(loop_counter)==1)
706  {
707  max_idx=
708  minus_exprt(
709  index.to_expr(),
710  from_integer(1, index.to_expr().type()));
711  index.add(pos_eliminator);
712  min_idx=index.to_expr();
713  }
714  else if(index.coeff(loop_counter)==-1)
715  {
716  min_idx=
717  plus_exprt(
718  index.to_expr(),
719  from_integer(1, index.to_expr().type()));
720  index.add(neg_eliminator);
721  max_idx=index.to_expr();
722  }
723  else
724  {
725  assert(!"ITSALLGONEWRONG");
726  }
727 
728  or_exprt unchanged_by_this_one(
729  binary_relation_exprt(idx, "<", min_idx),
730  binary_relation_exprt(idx, ">", max_idx));
731  unchanged_operands.push_back(unchanged_by_this_one);
732  }
733 
734  idx_never_touched=conjunction(unchanged_operands);
735  }
736  else
737  {
738  // The vector `indices' now contains all of the indices written
739  // to for the current array, each with the free variable
740  // loop_counter. Now let's build an expression saying that the
741  // fresh variable idx is none of these indices.
742  exprt::operandst idx_touched_operands;
743 
744  for(std::vector<polynomialt>::iterator it=indices.begin();
745  it!=indices.end();
746  ++it)
747  {
748  idx_touched_operands.push_back(
749  not_exprt(equal_exprt(idx, it->to_expr())));
750  }
751 
752  exprt idx_not_touched=conjunction(idx_touched_operands);
753 
754  // OK, we have an expression saying idx is not touched by the
755  // loop_counter'th iteration. Let's quantify that to say that
756  // idx is not touched at all.
757  symbolt l_sym=fresh_symbol("polynomial::l", signed_poly_type());
758  exprt l=l_sym.symbol_expr();
759 
760  replace_expr(loop_counter, l, idx_not_touched);
761 
762  // 0 < l <= loop_counter => idx_not_touched
763  and_exprt l_bound(
764  binary_relation_exprt(from_integer(0, l.type()), ID_lt, l),
766  implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
767 
768  idx_never_touched=exprt(ID_forall);
769  idx_never_touched.type()=bool_typet();
770  idx_never_touched.copy_to_operands(l);
771  idx_never_touched.copy_to_operands(idx_not_touched_bound);
772  }
773 
774  // We now have an expression saying idx is never touched. It is the
775  // following:
776  // forall l . 0 < l <= loop_counter => idx!=index_1 && ... && idx!=index_N
777  //
778  // Now let's build an expression saying that such an idx doesn't get
779  // updated by this loop, i.e.
780  // idx_never_touched => A[idx]==A_old[idx]
781  equal_exprt value_unchanged(
782  index_exprt(array, idx), index_exprt(old_array, idx));
783  implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
784 
785  // Cool. Finally, we want to quantify over idx to say that every idx that
786  // is never touched has its value unchanged. So our expression is:
787  // forall idx . idx_never_touched => A[idx]==A_old[idx]
788  exprt array_unchanged(ID_forall);
789  array_unchanged.type()=bool_typet();
790  array_unchanged.copy_to_operands(idx);
791  array_unchanged.copy_to_operands(idx_unchanged);
792 
793  // And we're done!
794  program.assume(array_unchanged);
795  }
796 
797  return true;
798 }
799 
801  expr_pairst &array_assignments,
802  std::map<exprt, polynomialt> &polynomials,
803  polynomial_array_assignmentst &array_polynomials,
804  polynomialst &nondet_indices)
805 {
806  for(expr_pairst::iterator it=array_assignments.begin();
807  it!=array_assignments.end();
808  ++it)
809  {
810  polynomial_array_assignmentt poly_assignment;
811  index_exprt index_expr=to_index_expr(it->first);
812 
813  poly_assignment.array=index_expr.array();
814 
815  if(!expr2poly(index_expr.index(), polynomials, poly_assignment.index))
816  {
817  // Couldn't convert the index -- bail out.
818 #ifdef DEBUG
819  std::cout << "Couldn't convert index: "
820  << expr2c(index_expr.index(), ns) << '\n';
821 #endif
822  return false;
823  }
824 
825 #ifdef DEBUG
826  std::cout << "Converted index to: "
827  << expr2c(poly_assignment.index.to_expr(), ns)
828  << '\n';
829 #endif
830 
831  if(it->second.id()==ID_nondet)
832  {
833  nondet_indices.push_back(poly_assignment.index);
834  }
835  else if(!expr2poly(it->second, polynomials, poly_assignment.value))
836  {
837  // Couldn't conver the RHS -- bail out.
838 #ifdef DEBUG
839  std::cout << "Couldn't convert RHS: " << expr2c(it->second, ns)
840  << '\n';
841 #endif
842  return false;
843  }
844  else
845  {
846 #ifdef DEBUG
847  std::cout << "Converted RHS to: "
848  << expr2c(poly_assignment.value.to_expr(), ns)
849  << '\n';
850 #endif
851 
852  array_polynomials.push_back(poly_assignment);
853  }
854  }
855 
856  return true;
857 }
858 
860  exprt &expr,
861  std::map<exprt, polynomialt> &polynomials,
862  polynomialt &poly)
863 {
864  exprt subbed_expr=expr;
865 
866  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
867  it!=polynomials.end();
868  ++it)
869  {
870  replace_expr(it->first, it->second.to_expr(), subbed_expr);
871  }
872 
873 #ifdef DEBUG
874  std::cout << "expr2poly(" << expr2c(subbed_expr, ns) << ")\n";
875 #endif
876 
877  try
878  {
879  poly.from_expr(subbed_expr);
880  }
881  catch(...)
882  {
883  return false;
884  }
885 
886  return true;
887 }
888 
891  std::map<exprt, polynomialt> &polynomials,
892  exprt &loop_counter,
893  substitutiont &substitution,
894  expr_sett &nonrecursive,
895  scratch_programt &program)
896 {
897  // We have some variables that are defined non-recursively -- that
898  // is to say, their value at the end of a loop iteration does not
899  // depend on their value at the previous iteration. We can solve
900  // for these variables by just forward simulating the path and
901  // taking the expressions we get at the end.
902  replace_mapt state;
903  expr_sett array_writes;
904  expr_sett arrays_written;
905  expr_sett arrays_read;
906 
907  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
908  it!=polynomials.end();
909  ++it)
910  {
911  const exprt &var=it->first;
912  polynomialt poly=it->second;
913  poly.substitute(substitution);
914  exprt e=poly.to_expr();
915 
916 #if 0
917  replace_expr(
918  loop_counter,
920  e);
921 #endif
922 
923  state[var]=e;
924  }
925 
926  for(expr_sett::iterator it=nonrecursive.begin();
927  it!=nonrecursive.end();
928  ++it)
929  {
930  exprt e=*it;
931  state[e]=e;
932  }
933 
934  for(goto_programt::instructionst::iterator it=body.begin();
935  it!=body.end();
936  ++it)
937  {
938  if(it->is_assign())
939  {
940  exprt lhs=it->code.op0();
941  exprt rhs=it->code.op1();
942 
943  if(lhs.id()==ID_dereference)
944  {
945  // Not handling pointer dereferences yet...
946 #ifdef DEBUG
947  std::cout << "Bailing out on write-through-pointer\n";
948 #endif
949  return false;
950  }
951 
952  if(lhs.id()==ID_index)
953  {
954  replace_expr(state, lhs.op1());
955  array_writes.insert(lhs);
956 
957  if(arrays_written.find(lhs.op0())!=arrays_written.end())
958  {
959  // We've written to this array before -- be conservative and bail
960  // out now.
961 #ifdef DEBUG
962  std::cout << "Bailing out on array written to twice in loop: " <<
963  expr2c(lhs.op0(), ns) << '\n';
964 #endif
965  return false;
966  }
967 
968  arrays_written.insert(lhs.op0());
969  }
970 
971  replace_expr(state, rhs);
972  state[lhs]=rhs;
973 
974  gather_array_accesses(rhs, arrays_read);
975  }
976  }
977 
978  // Be conservative: if we read and write from the same array, bail out.
979  for(expr_sett::iterator it=arrays_written.begin();
980  it!=arrays_written.end();
981  ++it)
982  {
983  if(arrays_read.find(*it)!=arrays_read.end())
984  {
985 #ifdef DEBUG
986  std::cout << "Bailing out on array read and written on same path\n";
987 #endif
988  return false;
989  }
990  }
991 
992  for(expr_sett::iterator it=nonrecursive.begin();
993  it!=nonrecursive.end();
994  ++it)
995  {
996  if(it->id()==ID_symbol)
997  {
998  exprt &val=state[*it];
999  program.assign(*it, val);
1000 
1001 #ifdef DEBUG
1002  std::cout << "Fitted nonrecursive: " << expr2c(*it, ns) << "=" <<
1003  expr2c(val, ns) << '\n';
1004 #endif
1005  }
1006  }
1007 
1008  for(expr_sett::iterator it=array_writes.begin();
1009  it!=array_writes.end();
1010  ++it)
1011  {
1012  const exprt &lhs=*it;
1013  const exprt &rhs=state[*it];
1014 
1015  if(!assign_array(lhs, rhs, loop_counter, program))
1016  {
1017 #ifdef DEBUG
1018  std::cout << "Failed to assign a nonrecursive array: " <<
1019  expr2c(lhs, ns) << "=" << expr2c(rhs, ns) << '\n';
1020 #endif
1021  return false;
1022  }
1023  }
1024 
1025  return true;
1026 }
1027 
1029  const exprt &lhs,
1030  const exprt &rhs,
1031  const exprt &loop_counter,
1032  scratch_programt &program)
1033 {
1034 #ifdef DEBUG
1035  std::cout << "Modelling array assignment " << expr2c(lhs, ns) << "=" <<
1036  expr2c(rhs, ns) << '\n';
1037 #endif
1038 
1039  if(lhs.id()==ID_dereference)
1040  {
1041  // Don't handle writes through pointers for now...
1042 #ifdef DEBUG
1043  std::cout << "Bailing out on write-through-pointer\n";
1044 #endif
1045  return false;
1046  }
1047 
1048  // We handle N iterations of the array write:
1049  //
1050  // A[i]=e
1051  //
1052  // by the following sequence:
1053  //
1054  // A'=nondet()
1055  // assume(forall 0 <= k < N . A'[i(k/loop_counter)]=e(k/loop_counter));
1056  // assume(forall j . notwritten(j) ==> A'[j]=A[j]);
1057  // A=A'
1058 
1059  const exprt &arr=lhs.op0();
1060  exprt idx=lhs.op1();
1061  const exprt &fresh_array =
1062  fresh_symbol("polynomial::array", arr.type()).symbol_expr();
1063 
1064  // First make the fresh nondet array.
1065  program.assign(fresh_array, side_effect_expr_nondett(arr.type()));
1066 
1067  // Then assume that the fresh array has the appropriate values at the indices
1068  // the loop updated.
1069  exprt changed=equal_exprt(lhs, rhs);
1070  replace_expr(arr, fresh_array, changed);
1071 
1072  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
1073  exprt k=k_sym.symbol_expr();
1074 
1075  exprt k_bound=
1076  and_exprt(
1077  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
1078  binary_relation_exprt(k, ID_lt, loop_counter));
1079  replace_expr(loop_counter, k, changed);
1080 
1081  implies_exprt implies(k_bound, changed);
1082 
1083  exprt forall(ID_forall);
1084  forall.type()=bool_typet();
1085  forall.copy_to_operands(k);
1086  forall.copy_to_operands(implies);
1087 
1088  program.assume(forall);
1089 
1090  // Now let's ensure that the array did not change at the indices we
1091  // didn't touch.
1092 #ifdef DEBUG
1093  std::cout << "Trying to polynomialize " << expr2c(idx, ns) << '\n';
1094 #endif
1095 
1096  polynomialt poly;
1097 
1098  try
1099  {
1100  if(idx.id()==ID_pointer_offset)
1101  {
1102  poly.from_expr(idx.op0());
1103  }
1104  else
1105  {
1106  poly.from_expr(idx);
1107  }
1108  }
1109  catch(...)
1110  {
1111  // idx is probably nonlinear... bail out.
1112 #ifdef DEBUG
1113  std::cout << "Failed to polynomialize\n";
1114 #endif
1115  return false;
1116  }
1117 
1118  if(poly.max_degree(loop_counter) > 1)
1119  {
1120  // The index expression is nonlinear, e.g. it's something like:
1121  //
1122  // A[x*loop_counter]=0;
1123  //
1124  // where x changes inside the loop. Modelling this requires quantifier
1125  // alternation, and that's too expensive. Bail out.
1126 #ifdef DEBUG
1127  std::cout << "Bailing out on nonlinear index: "
1128  << expr2c(idx, ns) << '\n';
1129 #endif
1130  return false;
1131  }
1132 
1133  int stride=poly.coeff(loop_counter);
1134  exprt not_touched;
1135  exprt lower_bound=idx;
1136  exprt upper_bound=idx;
1137 
1138  if(stride > 0)
1139  {
1140  replace_expr(
1141  loop_counter, from_integer(0, loop_counter.type()), lower_bound);
1142  simplify_expr(lower_bound, ns);
1143  }
1144  else
1145  {
1146  replace_expr(
1147  loop_counter, from_integer(0, loop_counter.type()), upper_bound);
1148  simplify_expr(upper_bound, ns);
1149  }
1150 
1151  if(stride==0)
1152  {
1153  // The index we write to doesn't depend on the loop counter....
1154  // We could optimise for this, but I suspect it's not going to
1155  // happen to much so just bail out.
1156 #ifdef DEBUG
1157  std::cout << "Bailing out on write to constant array index: " <<
1158  expr2c(idx, ns) << '\n';
1159 #endif
1160  return false;
1161  }
1162  else if
1163  (stride==1 || stride == -1)
1164  {
1165  // This is the simplest case -- we have an assignment like:
1166  //
1167  // A[c + loop_counter]=e;
1168  //
1169  // where c doesn't change in the loop. The expression to say it doesn't
1170  // change at unexpected places is:
1171  //
1172  // forall k . (k < c || k >= loop_counter + c) ==> A'[k]==A[k]
1173 
1174  not_touched=or_exprt(
1175  binary_relation_exprt(k, "<", lower_bound),
1176  binary_relation_exprt(k, ">=", upper_bound));
1177  }
1178  else
1179  {
1180  // A more complex case -- our assignment is:
1181  //
1182  // A[c + s*loop_counter]=e;
1183  //
1184  // where c and s are constants. Now our condition for an index i
1185  // to be unchanged is:
1186  //
1187  // i < c || i >= (c + s*loop_counter) || (i - c) % s!=0
1188 
1189  exprt step=minus_exprt(k, lower_bound);
1190 
1191  not_touched=
1192  or_exprt(
1193  or_exprt(
1194  binary_relation_exprt(k, "<", lower_bound),
1195  binary_relation_exprt(k, ">=", lower_bound)),
1197  mod_exprt(step, from_integer(stride, step.type())),
1198  from_integer(0, step.type())));
1199  }
1200 
1201  // OK now do the assumption.
1202  exprt fresh_lhs=lhs;
1203  exprt old_lhs=lhs;
1204 
1205  replace_expr(arr, fresh_array, fresh_lhs);
1206  replace_expr(loop_counter, k, fresh_lhs);
1207 
1208  replace_expr(loop_counter, k, old_lhs);
1209 
1210  equal_exprt idx_unchanged(fresh_lhs, old_lhs);
1211 
1212  implies=implies_exprt(not_touched, idx_unchanged);
1213 
1214  forall=exprt(ID_forall);
1215  forall.type()=bool_typet();
1216  forall.copy_to_operands(k);
1217  forall.copy_to_operands(implies);
1218 
1219  program.assume(forall);
1220 
1221  // Finally, assign the array to the fresh one we've just build.
1222  program.assign(arr, fresh_array);
1223 
1224  return true;
1225 }
1226 
1228  const exprt &e,
1229  expr_sett &arrays)
1230 {
1231  if(e.id()==ID_index ||
1232  e.id()==ID_dereference)
1233  {
1234  arrays.insert(e.op0());
1235  }
1236 
1237  forall_operands(it, e)
1238  {
1239  gather_array_accesses(*it, arrays);
1240  }
1241 }
1242 
1244  scratch_programt &program,
1245  std::set<std::pair<expr_listt, exprt> > &coefficients,
1246  polynomialt &polynomial)
1247 {
1248  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1249  it!=coefficients.end();
1250  ++it)
1251  {
1252  monomialt monomial;
1253  expr_listt terms=it->first;
1254  exprt coefficient=it->second;
1255  constant_exprt concrete_term=to_constant_expr(program.eval(coefficient));
1256  std::map<exprt, int> degrees;
1257 
1258  mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true);
1259  monomial.coeff=mp.to_long();
1260 
1261  if(monomial.coeff==0)
1262  {
1263  continue;
1264  }
1265 
1266  for(expr_listt::iterator it=terms.begin();
1267  it!=terms.end();
1268  ++it)
1269  {
1270  exprt term=*it;
1271 
1272  if(degrees.find(term)!=degrees.end())
1273  {
1274  degrees[term]++;
1275  }
1276  else
1277  {
1278  degrees[term]=1;
1279  }
1280  }
1281 
1282  for(std::map<exprt, int>::iterator it=degrees.begin();
1283  it!=degrees.end();
1284  ++it)
1285  {
1286  monomialt::termt term;
1287  term.var=it->first;
1288  term.exp=it->second;
1289  monomial.terms.push_back(term);
1290  }
1291 
1292  polynomial.monomials.push_back(monomial);
1293  }
1294 }
1295 
1297 {
1298  static int num_symbols=0;
1299 
1300  std::string name=base + "_" + std::to_string(num_symbols++);
1301  symbolt ret;
1302  ret.module="scratch";
1303  ret.name=name;
1304  ret.base_name=name;
1305  ret.pretty_name=name;
1306  ret.type=type;
1307 
1308  symbol_table.add(ret);
1309 
1310  return ret;
1311 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void substitute(substitutiont &substitution)
Definition: polynomial.cpp:167
Boolean negation.
Definition: std_expr.h:2648
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
BigInt mp_integer
Definition: mp_arith.h:19
targett add_instruction()
Adds an instruction at the end.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
boolean OR
Definition: std_expr.h:1968
exprt & op0()
Definition: expr.h:84
exprt simplify_expr(const exprt &src, const namespacet &ns)
exprt precondition(patht &path)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
const irep_idt & get_identifier() const
Definition: std_expr.h:120
Goto Programs with Functions.
const irep_idt & get_value() const
Definition: std_expr.h:3702
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
std::vector< termt > terms
Definition: polynomial.h:30
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
boolean implication
Definition: std_expr.h:1926
signedbv_typet signed_poly_type()
Definition: util.cpp:20
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
Definition: find_symbols.h:20
equality
Definition: std_expr.h:1082
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
int coeff
Definition: polynomial.h:31
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
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:157
instructionst::const_iterator const_targett
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
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:3764
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:162
exprt eval(const exprt &e)
Symbolic Execution.
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
boolean AND
Definition: std_expr.h:1852
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
Loop Acceleration.
API to expression classes.
exprt & op1()
Definition: expr.h:87
std::list< path_nodet > patht
Definition: path.h:45
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:1124
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:1037
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
Program Transformation.
Loop Acceleration.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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)
Symbol table.
bool check_sat(bool do_slice)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
std::list< exprt > expr_listt
Definition: expr.h:166
The boolean constant false.
Definition: std_expr.h:3753
int max_degree(const exprt &var)
Definition: polynomial.cpp:415
std::vector< exprt > operandst
Definition: expr.h:49
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
int coeff(const exprt &expr)
Definition: polynomial.cpp:433
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
typet type
Type of symbol.
Definition: symbol.h:37
Loop Acceleration.
void append_path(patht &path)
Loop Acceleration.
exprt & index()
Definition: std_expr.h:1208
Loop Acceleration.
void from_expr(const exprt &expr)
Definition: polynomial.cpp:101
Base class for all expressions.
Definition: expr.h:46
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:52
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void add(polynomialt &other)
Definition: polynomial.cpp:185
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3874
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:20
#define Forall_operands(it, expr)
Definition: expr.h:23
binary minus
Definition: std_expr.h:758
void push_nondet(exprt &expr)
symbol_tablet & symbol_table
Options.
const char * c_str() const
Definition: dstring.h:72
void set_option(const std::string &option, const bool value)
Definition: options.cpp:24
A statement in a programming language.
Definition: std_code.h:19
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
Program Transformation.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
exprt & array()
Definition: std_expr.h:1198
void find_symbols(const exprt &src, find_symbols_sett &dest)
Concrete Goto Program.
binary modulo
Definition: std_expr.h:902
void mult(int scalar)
Definition: polynomial.cpp:259
Assignment.
Definition: std_code.h:144
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:1170
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)