51 if(expr.
id()==ID_symbol ||
52 expr.
id()==ID_index ||
53 expr.
id()==ID_member ||
54 expr.
id()==ID_dereference)
79 for(goto_programt::instructionst::const_iterator
80 it=instructions.begin();
81 it!=instructions.end();
90 for(
const auto &step : path)
98 for(
const auto &step : loop)
109 modified.insert(assignment.
lhs());
115 std::map<exprt, polynomialt> polynomials,
130 std::vector<exprt> polynomials_hold;
135 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
136 it!=polynomials.end();
139 const equal_exprt holds(it->first, it->second.to_expr());
142 polynomials_hold.push_back(holds);
147 codet inc_loop_counter=
155 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
156 it!=polynomials_hold.end();
163 std::cout <<
"Checking following program for inductiveness:\n";
173 std::cout <<
"Not inductive!\n";
182 catch(
const std::string &s)
184 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
187 catch (
const char *s)
189 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
196 std::map<exprt, polynomialt> &polynomials,
205 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
206 it!=polynomials.end();
209 it->second.substitute(substitution);
220 for(expr_sett::iterator it=modified.begin();
228 vars.erase(loop_counter_name);
230 for(find_symbols_sett::iterator it=vars.begin();
253 for(patht::reverse_iterator r_it=path.rbegin();
266 if(lhs.
id()==ID_symbol ||
267 lhs.
id()==ID_index ||
268 lhs.
id()==ID_dereference)
277 else if(t->is_assume() || t->is_assert())
286 if(!r_it->guard.is_true() && !r_it->guard.is_nil())
306 if(expr.
id()==ID_index ||
307 expr.
id()==ID_dereference)
309 expr_mapt::iterator it=abstractions.find(expr);
311 if(it==abstractions.end())
338 if(expr.
id()==ID_not &&
339 expr.
op0().
id()==ID_nondet)
343 else if(expr.
id()==ID_equal ||
349 if(expr.
op0().
id()==ID_nondet ||
350 expr.
op1().
id()==ID_nondet)
358 std::map<exprt, polynomialt> polynomials,
392 std::vector<exprt> polynomials_hold;
394 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
395 it!=polynomials.end();
399 exprt rhs=it->second.to_expr();
406 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
407 it!=polynomials_hold.end();
419 for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
420 p_it!=polynomials.end();
423 program.
assign(p_it->first, p_it->second.to_expr());
426 program.
assume(condition);
431 for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
432 p_it!=polynomials.end();
435 program.
assign(p_it->first, p_it->second.to_expr());
446 std::cout <<
"Checking following program for monotonicity:\n";
455 std::cout <<
"Path is not monotone\n";
461 catch(
const std::string &s)
463 std::cout <<
"Error in monotonicity SAT check: " << s <<
'\n';
468 std::cout <<
"Error in monotonicity SAT check: " << s <<
'\n';
473 std::cout <<
"Path is monotone\n";
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);
496 std::cout <<
"Adding overflow checks at " << now <<
"...\n";
509 std::cout <<
"Done at " << now <<
".\n";
519 for(goto_programt::instructionst::reverse_iterator r_it=loop_body.rbegin();
520 r_it!=loop_body.rend();
523 if(r_it->is_assign())
528 if(assignment.
lhs().
id()==ID_index)
531 assignments.push_back(
532 std::make_pair(assignment.
lhs(), assignment.
rhs()));
536 arrays_written.insert(index_expr.
array());
542 for(expr_pairst::iterator a_it=assignments.begin();
543 a_it!=assignments.end();
558 std::map<exprt, polynomialt> &polynomials,
563 std::cout <<
"Doing arrays...\n";
572 std::cout <<
"Found " << array_assignments.size()
573 <<
" array assignments\n";
576 if(array_assignments.empty())
586 array_assignments, polynomials, poly_assignments, nondet_indices))
591 std::cout <<
"Couldn't model an array assignment :-(\n";
597 for(expr_sett::iterator it=arrays_written.begin();
598 it!=arrays_written.end();
608 for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
609 it!=poly_assignments.end();
640 for(expr_sett::iterator a_it=arrays_written.begin();
641 a_it!=arrays_written.end();
645 exprt old_array=substitution[array];
646 std::vector<polynomialt> indices;
647 bool nonlinear_index=
false;
649 for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
650 it!=poly_assignments.end();
657 indices.push_back(index);
665 nonlinear_index=
true;
687 pos_eliminator=neg_eliminator;
688 pos_eliminator.
mult(-1);
692 for(std::vector<polynomialt>::iterator it=indices.begin();
697 exprt max_idx, min_idx;
705 index.
add(pos_eliminator);
714 index.
add(neg_eliminator);
719 assert(!
"ITSALLGONEWRONG");
725 unchanged_operands.push_back(unchanged_by_this_one);
738 for(std::vector<polynomialt>::iterator it=indices.begin();
742 idx_touched_operands.push_back(
760 implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
762 idx_never_touched=
exprt(ID_forall);
777 implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
785 program.
assume(array_unchanged);
793 std::map<exprt, polynomialt> &polynomials,
797 for(expr_pairst::iterator it=array_assignments.begin();
798 it!=array_assignments.end();
810 std::cout <<
"Couldn't convert index: "
817 std::cout <<
"Converted index to: "
822 if(it->second.id()==ID_nondet)
824 nondet_indices.push_back(poly_assignment.
index);
826 else if(!
expr2poly(it->second, polynomials, poly_assignment.
value))
830 std::cout <<
"Couldn't convert RHS: " <<
expr2c(it->second,
ns)
838 std::cout <<
"Converted RHS to: "
843 array_polynomials.push_back(poly_assignment);
852 std::map<exprt, polynomialt> &polynomials,
855 exprt subbed_expr=expr;
857 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
858 it!=polynomials.end();
861 replace_expr(it->first, it->second.to_expr(), subbed_expr);
865 std::cout <<
"expr2poly(" <<
expr2c(subbed_expr,
ns) <<
")\n";
882 std::map<exprt, polynomialt> &polynomials,
897 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
898 it!=polynomials.end();
901 const exprt &var=it->first;
916 for(expr_sett::iterator it=nonrecursive.begin();
917 it!=nonrecursive.end();
924 for(goto_programt::instructionst::iterator it=body.begin();
933 if(lhs.
id()==ID_dereference)
937 std::cout <<
"Bailing out on write-through-pointer\n";
942 if(lhs.
id()==ID_index)
945 array_writes.insert(lhs);
947 if(arrays_written.find(lhs.
op0())!=arrays_written.end())
952 std::cout <<
"Bailing out on array written to twice in loop: " <<
958 arrays_written.insert(lhs.
op0());
969 for(expr_sett::iterator it=arrays_written.begin();
970 it!=arrays_written.end();
973 if(arrays_read.find(*it)!=arrays_read.end())
976 std::cout <<
"Bailing out on array read and written on same path\n";
982 for(expr_sett::iterator it=nonrecursive.begin();
983 it!=nonrecursive.end();
986 if(it->id()==ID_symbol)
988 exprt &val=state[*it];
992 std::cout <<
"Fitted nonrecursive: " <<
expr2c(*it,
ns) <<
"=" <<
998 for(expr_sett::iterator it=array_writes.begin();
999 it!=array_writes.end();
1002 const exprt &lhs=*it;
1003 const exprt &rhs=state[*it];
1008 std::cout <<
"Failed to assign a nonrecursive array: " <<
1024 std::cout <<
"Modelling array assignment " <<
expr2c(lhs,
ns) <<
"=" <<
1028 if(lhs.
id()==ID_dereference)
1032 std::cout <<
"Bailing out on write-through-pointer\n";
1050 const exprt &fresh_array =
1078 std::cout <<
"Trying to polynomialize " <<
expr2c(idx,
ns) <<
'\n';
1085 if(idx.
id()==ID_pointer_offset)
1098 std::cout <<
"Failed to polynomialize\n";
1112 std::cout <<
"Bailing out on nonlinear index: "
1120 exprt lower_bound=idx;
1121 exprt upper_bound=idx;
1142 std::cout <<
"Bailing out on write to constant array index: " <<
1147 else if(stride == 1 || stride == -1)
1185 exprt fresh_lhs=lhs;
1196 forall.
where() = implies;
1201 program.
assign(arr, fresh_array);
1210 if(e.
id()==ID_index ||
1211 e.
id()==ID_dereference)
1213 arrays.insert(e.
op0());
1224 std::set<std::pair<expr_listt, exprt> > &coefficients,
1227 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1228 it!=coefficients.end();
1233 exprt coefficient=it->second;
1235 std::map<exprt, int> degrees;
1238 monomial.
coeff=mp.to_long();
1240 if(monomial.
coeff==0)
1245 for(
const auto &term : terms)
1247 if(degrees.find(term)!=degrees.end())
1257 for(std::map<exprt, int>::iterator it=degrees.begin();
1263 term.
exp=it->second;
1264 monomial.
terms.push_back(term);
1267 polynomial.
monomials.push_back(monomial);
1273 static int num_symbols=0;