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