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