41 if(expr.
id()==ID_symbol ||
42 expr.
id()==ID_index ||
43 expr.
id()==ID_member ||
44 expr.
id()==ID_dereference)
69 for(goto_programt::instructionst::const_iterator
70 it=instructions.begin();
71 it!=instructions.end();
80 for(
const auto &step : path)
88 for(
const auto &step : loop)
97 modified.insert(t->assign_lhs());
101 std::map<exprt, polynomialt> polynomials,
117 std::vector<exprt> polynomials_hold;
122 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
123 it!=polynomials.end();
126 const equal_exprt holds(it->first, it->second.to_expr());
129 polynomials_hold.push_back(holds);
142 for(
const auto &p : polynomials_hold)
146 std::cout <<
"Checking following program for inductiveness:\n";
156 std::cout <<
"Not inductive!\n";
165 catch(
const std::string &s)
167 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
170 catch (
const char *s)
172 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
179 std::map<exprt, polynomialt> &polynomials,
188 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
189 it!=polynomials.end();
192 it->second.substitute(substitution);
205 vars.erase(loop_counter_name);
228 for(patht::reverse_iterator r_it=path.rbegin();
237 const exprt &lhs = t->assign_lhs();
238 const exprt &rhs = t->assign_rhs();
240 if(lhs.
id()==ID_symbol ||
241 lhs.
id()==ID_index ||
242 lhs.
id()==ID_dereference)
251 else if(t->is_assume() || t->is_assert())
260 if(!r_it->guard.is_true() && !r_it->guard.is_nil())
280 if(expr.
id()==ID_index ||
281 expr.
id()==ID_dereference)
283 expr_mapt::iterator it=abstractions.find(expr);
285 if(it==abstractions.end())
312 if(expr.
id() == ID_not &&
to_not_expr(expr).op().
id() == ID_nondet)
316 else if(expr.
id()==ID_equal ||
323 if(rel_expr.lhs().id() == ID_nondet || rel_expr.rhs().id() == ID_nondet)
331 std::map<exprt, polynomialt> polynomials,
366 std::vector<exprt> polynomials_hold;
368 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
369 it!=polynomials.end();
373 exprt rhs=it->second.to_expr();
380 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
381 it!=polynomials_hold.end();
393 for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
394 p_it!=polynomials.end();
397 program.
assign(p_it->first, p_it->second.to_expr());
400 program.
assume(condition);
405 for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
406 p_it!=polynomials.end();
409 program.
assign(p_it->first, p_it->second.to_expr());
420 std::cout <<
"Checking following program for monotonicity:\n";
429 std::cout <<
"Path is not monotone\n";
435 catch(
const std::string &s)
437 std::cout <<
"Error in monotonicity SAT check: " << s <<
'\n';
442 std::cout <<
"Error in monotonicity SAT check: " << s <<
'\n';
447 std::cout <<
"Path is monotone\n";
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);
470 std::cout <<
"Adding overflow checks at " << now <<
"...\n";
483 std::cout <<
"Done at " << now <<
".\n";
493 for(goto_programt::instructionst::reverse_iterator r_it=loop_body.rbegin();
494 r_it!=loop_body.rend();
497 if(r_it->is_assign())
500 exprt assignment_lhs = r_it->assign_lhs();
501 exprt assignment_rhs = r_it->assign_rhs();
503 if(assignment_lhs.
id() == ID_index)
506 assignments.push_back(std::make_pair(assignment_lhs, assignment_rhs));
510 arrays_written.insert(index_expr.
array());
516 for(expr_pairst::iterator a_it=assignments.begin();
517 a_it!=assignments.end();
520 replace_expr(assignment_lhs, assignment_rhs, a_it->first);
521 replace_expr(assignment_lhs, assignment_rhs, a_it->second);
532 std::map<exprt, polynomialt> &polynomials,
537 std::cout <<
"Doing arrays...\n";
546 std::cout <<
"Found " << array_assignments.size()
547 <<
" array assignments\n";
550 if(array_assignments.empty())
560 array_assignments, polynomials, poly_assignments, nondet_indices))
565 std::cout <<
"Couldn't model an array assignment :-(\n";
571 for(expr_sett::iterator it=arrays_written.begin();
572 it!=arrays_written.end();
582 for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
583 it!=poly_assignments.end();
614 for(expr_sett::iterator a_it=arrays_written.begin();
615 a_it!=arrays_written.end();
619 exprt old_array=substitution[array];
620 std::vector<polynomialt> indices;
621 bool nonlinear_index=
false;
623 for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
624 it!=poly_assignments.end();
631 indices.push_back(index);
639 nonlinear_index=
true;
661 pos_eliminator=neg_eliminator;
662 pos_eliminator.
mult(-1);
666 for(std::vector<polynomialt>::iterator it=indices.begin();
671 exprt max_idx, min_idx;
679 index.
add(pos_eliminator);
688 index.
add(neg_eliminator);
693 assert(!
"ITSALLGONEWRONG");
699 unchanged_operands.push_back(unchanged_by_this_one);
712 for(std::vector<polynomialt>::iterator it=indices.begin();
716 idx_touched_operands.push_back(
734 implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
736 idx_never_touched=
exprt(ID_forall);
751 implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
759 program.
assume(array_unchanged);
767 std::map<exprt, polynomialt> &polynomials,
771 for(expr_pairst::iterator it=array_assignments.begin();
772 it!=array_assignments.end();
784 std::cout <<
"Couldn't convert index: "
791 std::cout <<
"Converted index to: "
796 if(it->second.id()==ID_nondet)
798 nondet_indices.push_back(poly_assignment.
index);
800 else if(!
expr2poly(it->second, polynomials, poly_assignment.
value))
804 std::cout <<
"Couldn't convert RHS: " <<
expr2c(it->second,
ns)
812 std::cout <<
"Converted RHS to: "
817 array_polynomials.push_back(poly_assignment);
826 std::map<exprt, polynomialt> &polynomials,
829 exprt subbed_expr=expr;
831 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
832 it!=polynomials.end();
835 replace_expr(it->first, it->second.to_expr(), subbed_expr);
839 std::cout <<
"expr2poly(" <<
expr2c(subbed_expr,
ns) <<
")\n";
856 std::map<exprt, polynomialt> &polynomials,
867 std::unordered_set<index_exprt, irep_hash> array_writes;
871 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
872 it!=polynomials.end();
875 const exprt &var=it->first;
890 for(expr_sett::iterator it=nonrecursive.begin();
891 it!=nonrecursive.end();
898 for(goto_programt::instructionst::iterator it=body.begin();
904 exprt lhs = it->assign_lhs();
905 exprt rhs = it->assign_rhs();
907 if(lhs.
id()==ID_dereference)
911 std::cout <<
"Bailing out on write-through-pointer\n";
916 if(lhs.
id()==ID_index)
920 array_writes.insert(lhs_index_expr);
922 if(arrays_written.find(lhs_index_expr.array()) != arrays_written.end())
927 std::cout <<
"Bailing out on array written to twice in loop: "
928 <<
expr2c(lhs_index_expr.array(),
ns) <<
'\n';
933 arrays_written.insert(lhs_index_expr.array());
944 for(expr_sett::iterator it=arrays_written.begin();
945 it!=arrays_written.end();
948 if(arrays_read.find(*it)!=arrays_read.end())
951 std::cout <<
"Bailing out on array read and written on same path\n";
957 for(expr_sett::iterator it=nonrecursive.begin();
958 it!=nonrecursive.end();
961 if(it->id()==ID_symbol)
963 exprt &val=state[*it];
967 std::cout <<
"Fitted nonrecursive: " <<
expr2c(*it,
ns) <<
"=" <<
973 for(
const auto &write : array_writes)
975 const auto &lhs = write;
976 const auto &rhs = state[write];
981 std::cout <<
"Failed to assign a nonrecursive array: " <<
997 std::cout <<
"Modelling array assignment " <<
expr2c(lhs,
ns) <<
"=" <<
1001 if(lhs.
id()==ID_dereference)
1005 std::cout <<
"Bailing out on write-through-pointer\n";
1023 const exprt &fresh_array =
1051 std::cout <<
"Trying to polynomialize " <<
expr2c(idx,
ns) <<
'\n';
1058 if(idx.
id()==ID_pointer_offset)
1071 std::cout <<
"Failed to polynomialize\n";
1085 std::cout <<
"Bailing out on nonlinear index: "
1093 exprt lower_bound=idx;
1094 exprt upper_bound=idx;
1115 std::cout <<
"Bailing out on write to constant array index: " <<
1120 else if(stride == 1 || stride == -1)
1158 exprt fresh_lhs=lhs;
1169 forall.
where() = implies;
1174 program.
assign(arr, fresh_array);
1183 if(e.
id() == ID_index)
1187 else if(e.
id() == ID_dereference)
1200 std::set<std::pair<expr_listt, exprt> > &coefficients,
1203 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1204 it!=coefficients.end();
1209 exprt coefficient=it->second;
1211 std::map<exprt, int> degrees;
1214 monomial.
coeff = numeric_cast_v<int>(mp);
1216 if(monomial.
coeff==0)
1221 for(
const auto &term : terms)
1223 if(degrees.find(term)!=degrees.end())
1233 for(std::map<exprt, int>::iterator it=degrees.begin();
1239 term.
exp=it->second;
1240 monomial.
terms.push_back(term);
1243 polynomial.
monomials.push_back(monomial);
1249 static int num_symbols=0;
1251 std::string name=base +
"_" + std::to_string(num_symbols++);
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
std::list< exprt > expr_listt
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)
A base class for relations, i.e., binary predicates whose two operands have the same type.
A codet representing an assignment in the program.
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The Boolean constant false.
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())
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
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.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
std::vector< termt > terms
parentt::loopt natural_loopt
void set_option(const std::string &option, const bool value)
void add_overflow_checks()
The plus expression Associativity is not specified.
void substitute(substitutiont &substitution)
void from_expr(const exprt &expr)
std::vector< monomialt > monomials
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.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
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.
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
The type of an expression, extends irept.
std::unordered_set< exprt, irep_hash > expr_sett
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
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
#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
std::list< path_nodet > patht
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::vector< polynomialt > polynomialst
std::map< exprt, exprt > substitutiont
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
This is unused by this implementation of guards, but can be used by other implementations of the same...
unsignedbv_typet unsigned_poly_type()
signedbv_typet signed_poly_type()