53 if(expr.
id()==ID_symbol ||
54 expr.
id()==ID_index ||
55 expr.
id()==ID_member ||
56 expr.
id()==ID_dereference)
81 for(goto_programt::instructionst::const_iterator
82 it=instructions.begin();
83 it!=instructions.end();
92 for(
const auto &step : path)
100 for(
const auto &step : loop)
111 modified.insert(assignment.
lhs());
117 std::map<exprt, polynomialt> polynomials,
132 std::vector<exprt> polynomials_hold;
137 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
138 it!=polynomials.end();
144 polynomials_hold.push_back(holds);
149 codet inc_loop_counter=
157 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
158 it!=polynomials_hold.end();
165 std::cout <<
"Checking following program for inductiveness:\n";
175 std::cout <<
"Not inductive!\n";
186 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
189 catch (
const char *s)
191 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
198 std::map<exprt, polynomialt> &polynomials,
207 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
208 it!=polynomials.end();
211 it->second.substitute(substitution);
222 for(expr_sett::iterator it=modified.begin();
230 vars.erase(loop_counter_name);
232 for(find_symbols_sett::iterator it=vars.begin();
255 for(patht::reverse_iterator r_it=path.rbegin();
268 if(lhs.
id()==ID_symbol ||
269 lhs.
id()==ID_index ||
270 lhs.
id()==ID_dereference)
279 else if(t->is_assume() || t->is_assert())
288 if(!r_it->guard.is_true() && !r_it->guard.is_nil())
308 if(expr.
id()==ID_index ||
309 expr.
id()==ID_dereference)
311 expr_mapt::iterator it=abstractions.find(expr);
313 if(it==abstractions.end())
340 if(expr.
id()==ID_not &&
341 expr.
op0().
id()==ID_nondet)
345 else if(expr.
id()==ID_equal ||
351 if(expr.
op0().
id()==ID_nondet ||
352 expr.
op1().
id()==ID_nondet)
360 std::map<exprt, polynomialt> polynomials,
394 std::vector<exprt> polynomials_hold;
396 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
397 it!=polynomials.end();
401 exprt rhs=it->second.to_expr();
408 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
409 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";
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,
564 std::cout <<
"Doing arrays...\n";
573 std::cout <<
"Found " << array_assignments.size()
574 <<
" array assignments\n";
577 if(array_assignments.empty())
587 array_assignments, polynomials, poly_assignments, nondet_indices))
592 std::cout <<
"Couldn't model an array assignment :-(\n";
598 for(expr_sett::iterator it=arrays_written.begin();
599 it!=arrays_written.end();
608 for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
609 it!=poly_assignments.end();
636 exprt forall(ID_forall);
645 for(expr_sett::iterator a_it=arrays_written.begin();
646 a_it!=arrays_written.end();
650 exprt old_array=substitution[array];
651 std::vector<polynomialt> indices;
652 bool nonlinear_index=
false;
654 for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
655 it!=poly_assignments.end();
662 indices.push_back(index);
670 nonlinear_index=
true;
693 pos_eliminator=neg_eliminator;
694 pos_eliminator.
mult(-1);
698 for(std::vector<polynomialt>::iterator it=indices.begin();
703 exprt max_idx, min_idx;
711 index.
add(pos_eliminator);
720 index.
add(neg_eliminator);
725 assert(!
"ITSALLGONEWRONG");
731 unchanged_operands.push_back(unchanged_by_this_one);
744 for(std::vector<polynomialt>::iterator it=indices.begin();
748 idx_touched_operands.push_back(
766 implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
768 idx_never_touched=
exprt(ID_forall);
783 implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
788 exprt array_unchanged(ID_forall);
794 program.
assume(array_unchanged);
802 std::map<exprt, polynomialt> &polynomials,
806 for(expr_pairst::iterator it=array_assignments.begin();
807 it!=array_assignments.end();
819 std::cout <<
"Couldn't convert index: " 826 std::cout <<
"Converted index to: " 831 if(it->second.id()==ID_nondet)
833 nondet_indices.push_back(poly_assignment.
index);
835 else if(!
expr2poly(it->second, polynomials, poly_assignment.
value))
839 std::cout <<
"Couldn't convert RHS: " <<
expr2c(it->second,
ns)
847 std::cout <<
"Converted RHS to: " 852 array_polynomials.push_back(poly_assignment);
861 std::map<exprt, polynomialt> &polynomials,
864 exprt subbed_expr=expr;
866 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
867 it!=polynomials.end();
870 replace_expr(it->first, it->second.to_expr(), subbed_expr);
874 std::cout <<
"expr2poly(" <<
expr2c(subbed_expr,
ns) <<
")\n";
891 std::map<exprt, polynomialt> &polynomials,
907 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
908 it!=polynomials.end();
911 const exprt &var=it->first;
926 for(expr_sett::iterator it=nonrecursive.begin();
927 it!=nonrecursive.end();
934 for(goto_programt::instructionst::iterator it=body.begin();
943 if(lhs.
id()==ID_dereference)
947 std::cout <<
"Bailing out on write-through-pointer\n";
952 if(lhs.
id()==ID_index)
955 array_writes.insert(lhs);
957 if(arrays_written.find(lhs.
op0())!=arrays_written.end())
962 std::cout <<
"Bailing out on array written to twice in loop: " <<
968 arrays_written.insert(lhs.
op0());
979 for(expr_sett::iterator it=arrays_written.begin();
980 it!=arrays_written.end();
983 if(arrays_read.find(*it)!=arrays_read.end())
986 std::cout <<
"Bailing out on array read and written on same path\n";
992 for(expr_sett::iterator it=nonrecursive.begin();
993 it!=nonrecursive.end();
996 if(it->id()==ID_symbol)
998 exprt &val=state[*it];
1002 std::cout <<
"Fitted nonrecursive: " <<
expr2c(*it,
ns) <<
"=" <<
1008 for(expr_sett::iterator it=array_writes.begin();
1009 it!=array_writes.end();
1012 const exprt &lhs=*it;
1013 const exprt &rhs=state[*it];
1018 std::cout <<
"Failed to assign a nonrecursive array: " <<
1031 const exprt &loop_counter,
1035 std::cout <<
"Modelling array assignment " <<
expr2c(lhs,
ns) <<
"=" <<
1039 if(lhs.
id()==ID_dereference)
1043 std::cout <<
"Bailing out on write-through-pointer\n";
1061 const exprt &fresh_array =
1083 exprt forall(ID_forall);
1093 std::cout <<
"Trying to polynomialize " <<
expr2c(idx,
ns) <<
'\n';
1100 if(idx.
id()==ID_pointer_offset)
1113 std::cout <<
"Failed to polynomialize\n";
1127 std::cout <<
"Bailing out on nonlinear index: " 1135 exprt lower_bound=idx;
1136 exprt upper_bound=idx;
1157 std::cout <<
"Bailing out on write to constant array index: " <<
1163 (stride==1 || stride == -1)
1202 exprt fresh_lhs=lhs;
1214 forall=
exprt(ID_forall);
1222 program.
assign(arr, fresh_array);
1231 if(e.
id()==ID_index ||
1232 e.
id()==ID_dereference)
1234 arrays.insert(e.
op0());
1245 std::set<std::pair<expr_listt, exprt> > &coefficients,
1248 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1249 it!=coefficients.end();
1254 exprt coefficient=it->second;
1256 std::map<exprt, int> degrees;
1259 monomial.
coeff=mp.to_long();
1261 if(monomial.
coeff==0)
1266 for(expr_listt::iterator it=terms.begin();
1272 if(degrees.find(term)!=degrees.end())
1282 for(std::map<exprt, int>::iterator it=degrees.begin();
1288 term.
exp=it->second;
1289 monomial.
terms.push_back(term);
1292 polynomial.
monomials.push_back(monomial);
1300 std::string name=base +
"_" + std::to_string(
num_symbols++);
The type of an expression.
irep_idt name
The unique identifier.
void substitute(substitutiont &substitution)
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
targett add_instruction()
Adds an instruction at the end.
A generic base class for relations, i.e., binary predicates.
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
std::list< instructiont > instructionst
exprt simplify_expr(const exprt &src, const namespacet &ns)
exprt precondition(patht &path)
void add_overflow_checks()
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
Goto Programs with Functions.
const irep_idt & get_value() const
std::set< goto_programt::targett > natural_loopt
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
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.
std::vector< polynomialt > polynomialst
irep_idt pretty_name
Language-specific display name.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
std::vector< termt > terms
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
signedbv_typet signed_poly_type()
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
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.
exprt conjunction(const exprt::operandst &op)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
instructionst::const_iterator const_targett
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
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()
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)
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 eval(const exprt &e)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
API to expression classes.
std::list< path_nodet > patht
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
void find_modified(const patht &path, expr_sett &modified)
A side effect that returns a non-deterministically chosen value.
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
#define forall_operands(it, expr)
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)
bool check_sat(bool do_slice)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
std::list< exprt > expr_listt
The boolean constant false.
int max_degree(const exprt &var)
std::vector< exprt > operandst
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
int coeff(const exprt &expr)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
typet type
Type of symbol.
void append_path(patht &path)
void from_expr(const exprt &expr)
Base class for all expressions.
std::map< exprt, exprt > substitutiont
irep_idt base_name
Base (non-scoped) name.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void add(polynomialt &other)
std::string expr2c(const exprt &expr, const namespacet &ns)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
#define Forall_operands(it, expr)
void push_nondet(exprt &expr)
symbol_tablet & symbol_table
const char * c_str() const
void set_option(const std::string &option, const bool value)
A statement in a programming language.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
#define forall_goto_program_instructions(it, program)
void find_symbols(const exprt &src, find_symbols_sett &dest)
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
bool simplify(exprt &expr, const namespacet &ns)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)