48 for(
const auto &op : expr.
operands())
67 for(goto_programt::instructionst::const_iterator
68 it=instructions.begin();
69 it!=instructions.end();
78 for(
const auto &step : path)
86 for(
const auto &step : loop)
95 modified.insert(t->assign_lhs());
120 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
144 std::cout <<
"Checking following program for inductiveness:\n";
154 std::cout <<
"Not inductive!\n";
163 catch(
const std::string &s)
165 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
168 catch (
const char *s)
170 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
186 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
201 std::set<symbol_exprt>
vars;
202 for(
const exprt &expr : modified)
227 for(patht::reverse_iterator
r_it=path.rbegin();
236 const exprt &lhs = t->assign_lhs();
237 const exprt &rhs = t->assign_rhs();
250 else if(t->is_assume() || t->is_assert())
259 if(!
r_it->guard.is_true() && !
r_it->guard.is_nil())
288 expr=
sym.symbol_expr();
367 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
372 exprt rhs=it->second.to_expr();
399 program.
assume(condition);
419 std::cout <<
"Checking following program for monotonicity:\n";
428 std::cout <<
"Path is not monotone\n";
434 catch(
const std::string &s)
436 std::cout <<
"Error in monotonicity SAT check: " << s <<
'\n';
441 std::cout <<
"Error in monotonicity SAT check: " << s <<
'\n';
446 std::cout <<
"Path is monotone\n";
469 std::cout <<
"Adding overflow checks at " <<
now <<
"...\n";
482 std::cout <<
"Done at " <<
now <<
".\n";
492 for(goto_programt::instructionst::reverse_iterator
r_it=
loop_body.rbegin();
496 if(
r_it->is_assign())
515 for(expr_pairst::iterator
a_it=assignments.begin();
516 a_it!=assignments.end();
536 std::cout <<
"Doing arrays...\n";
546 <<
" array assignments\n";
564 std::cout <<
"Couldn't model an array assignment :-(\n";
619 std::vector<polynomialt> indices;
630 indices.push_back(index);
665 for(std::vector<polynomialt>::iterator it=indices.begin();
711 for(std::vector<polynomialt>::iterator it=indices.begin();
783 std::cout <<
"Couldn't convert index: "
790 std::cout <<
"Converted index to: "
803 std::cout <<
"Couldn't convert RHS: " <<
expr2c(it->second,
ns)
811 std::cout <<
"Converted RHS to: "
830 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
866 std::unordered_set<index_exprt, irep_hash>
array_writes;
870 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
874 const exprt &var=it->first;
889 for(expr_sett::iterator it=nonrecursive.begin();
890 it!=nonrecursive.end();
897 for(goto_programt::instructionst::iterator it=body.begin();
903 exprt lhs = it->assign_lhs();
904 exprt rhs = it->assign_rhs();
910 std::cout <<
"Bailing out on write-through-pointer\n";
926 std::cout <<
"Bailing out on array written to twice in loop: "
950 std::cout <<
"Bailing out on array read and written on same path\n";
956 for(expr_sett::iterator it=nonrecursive.begin();
957 it!=nonrecursive.end();
966 std::cout <<
"Fitted nonrecursive: " <<
expr2c(*it,
ns) <<
"=" <<
974 const auto &lhs =
write;
975 const auto &rhs = state[
write];
980 std::cout <<
"Failed to assign a nonrecursive array: " <<
996 std::cout <<
"Modelling array assignment " <<
expr2c(lhs,
ns) <<
"=" <<
1004 std::cout <<
"Bailing out on write-through-pointer\n";
1050 std::cout <<
"Trying to polynomialize " <<
expr2c(idx,
ns) <<
'\n';
1063 poly.from_expr(idx);
1070 std::cout <<
"Failed to polynomialize\n";
1084 std::cout <<
"Bailing out on nonlinear index: "
1092 exprt lower_bound=idx;
1093 exprt upper_bound=idx;
1114 std::cout <<
"Bailing out on write to constant array index: " <<
1168 forall.where() = implies;
1199 std::set<std::pair<expr_listt, exprt> > &coefficients,
1202 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1203 it!=coefficients.end();
1220 for(
const auto &term : terms)
1232 for(std::map<exprt, int>::iterator it=
degrees.begin();
1238 term.
exp=it->second;
1250 std::string name=base +
"_" + std::to_string(
num_symbols++);
1252 ret.module=
"scratch";
1254 ret.pretty_name=name;
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
std::list< exprt > expr_listt
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...
A base class for relations, i.e., binary predicates whose two operands have the same type.
A goto_instruction_codet representing an assignment in the program.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
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())
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())
const irep_idt & id() const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
parentt::loopt natural_loopt
void add_overflow_checks()
The plus expression Associativity is not specified.
void substitute(substitutiont &substitution)
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)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
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)
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...
#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.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_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)
#define UNREACHABLE
This should be used to mark dead code.
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 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...
time_t time(time_t *tloc)
ssize_t write(int fildes, const void *buf, size_t nbyte)
unsignedbv_typet unsigned_poly_type()
signedbv_typet signed_poly_type()