54 for(patht::iterator it=loop.begin();
58 body.push_back(*(it->loc));
62 std::map<exprt, polynomialt> polynomials;
69 std::cout <<
"Polynomial accelerating program:\n";
71 for(goto_programt::instructionst::iterator it=body.begin();
78 std::cout <<
"Modified:\n";
80 for(expr_sett::iterator it=targets.begin();
84 std::cout <<
expr2c(*it,
ns) <<
'\n';
88 for(goto_programt::instructionst::iterator it=body.begin();
92 if(it->is_assign() || it->is_decl())
94 assigns.push_back(*it);
105 for(expr_sett::iterator it=targets.begin();
122 if(influence.find(target)==influence.end())
125 std::cout <<
"Found nonrecursive expression: " 133 if(target.
id()==ID_index ||
134 target.
id()==ID_dereference)
143 std::map<exprt, polynomialt> this_poly;
144 this_poly[target]=poly;
148 polynomials.insert(std::make_pair(target, poly));
154 std::cout <<
"Failed to fit a polynomial for " 161 if(polynomials.empty())
179 bool path_is_monotone;
185 catch (std::string s)
188 std::cout <<
"Assumptions error: " << s <<
'\n';
194 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
195 it!=polynomials.end();
198 replace_expr(it->first, it->second.to_expr(), guard_last);
227 exprt forall(ID_forall);
250 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
251 it!=polynomials.end();
254 program.
assign(it->first, it->second.to_expr());
264 std::cout <<
"Failed to accelerate a nonrecursive expression\n";
289 std::vector<expr_listt> parameters;
290 std::set<std::pair<expr_listt, exprt> > coefficients;
298 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
299 <<
", which depends on:\n";
301 for(expr_sett::iterator it=influence.begin();
305 std::cout <<
expr2c(*it,
ns) <<
'\n';
309 for(expr_sett::iterator it=influence.begin();
313 if(it->id()==ID_index ||
314 it->id()==ID_dereference)
322 exprs.push_back(*it);
323 parameters.push_back(exprs);
326 parameters.push_back(exprs);
332 parameters.push_back(exprs);
340 parameters.push_back(exprs);
349 if(var.
type().
id()==ID_pointer)
353 for(std::vector<expr_listt>::iterator it=parameters.begin();
354 it!=parameters.end();
359 coefficients.insert(std::make_pair(*it, coeff.
symbol_expr()));
371 std::map<exprt, int> values;
373 for(expr_sett::iterator it=influence.begin();
381 std::cout <<
"Fitting polynomial over " << values.size()
385 for(
int n=0; n<=2; n++)
387 for(expr_sett::iterator it=influence.begin();
401 for(expr_sett::iterator it=influence.begin();
411 std::cout <<
"Fitting polynomial with program:\n";
432 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
436 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
472 std::cout <<
"Fitting constant, eval'd to: " 482 mon.terms.push_back(term);
483 mon.coeff=mp.to_long();
492 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
496 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
504 std::map<exprt, int> &values,
505 std::set<std::pair<expr_listt, exprt> > &coefficients,
514 for(std::map<exprt, int>::iterator it=values.begin();
518 typet this_type=it->first.type();
519 if(this_type.
id()==ID_pointer)
522 std::cout <<
"Overriding pointer type\n";
541 for(std::map<exprt, int>::iterator it=values.begin();
549 for(
int i=0; i < num_unwindings; i++)
551 program.
append(loop_body);
557 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
558 it!=coefficients.end();
561 int concrete_value=1;
563 for(expr_listt::const_iterator e_it=it->first.begin();
564 e_it!=it->first.end();
571 concrete_value *= num_unwindings;
575 std::map<exprt, int>::iterator v_it=values.find(e);
577 if(v_it!=values.end())
579 concrete_value *= v_it->second;
613 assumption->guard=polynomial_holds;
624 for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
625 r_it!=orig_body.rend();
628 if(r_it->is_assign())
639 for(expr_sett::iterator s_it=lhs_syms.begin();
640 s_it!=lhs_syms.end();
643 if(cone.find(*s_it)!=cone.end())
647 body.push_front(*r_it);
648 cone.erase(assignment.
lhs());
658 std::map<exprt, polynomialt> polynomials,
673 std::vector<exprt> polynomials_hold;
678 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
679 it!=polynomials.end();
685 polynomials_hold.push_back(holds);
690 codet inc_loop_counter=
696 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
697 it!=polynomials_hold.end();
704 std::cout <<
"Checking following program for inductiveness:\n";
714 std::cout <<
"Not inductive!\n";
725 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
730 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
737 std::map<exprt, polynomialt> &polynomials,
745 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
746 it!=polynomials.end();
749 it->second.substitute(substitution);
760 for(expr_sett::iterator it=modified.begin();
768 vars.erase(loop_counter_name);
770 for(find_symbols_sett::iterator it=vars.begin();
793 for(patht::reverse_iterator r_it=path.rbegin();
806 if(lhs.
id()==ID_symbol)
810 else if(lhs.
id()==ID_index ||
811 lhs.
id()==ID_dereference)
820 else if(t->is_assume() || t->is_assert())
829 if(!r_it->guard.is_true() && !r_it->guard.is_nil())
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
The type of an expression.
struct configt::ansi_ct ansi_c
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
exprt precondition(patht &path)
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
instructionst instructions
The list of instructions in the goto program.
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
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.
unsignedbv_typet size_type()
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
void assert_for_values(scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt >> &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
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
unsignedbv_typet unsigned_poly_type()
void ensure_no_overflows(scratch_programt &program)
std::unordered_set< exprt, irep_hash > expr_sett
symbolt fresh_symbol(std::string base, typet type)
exprt eval(const exprt &e)
Fixed-width bit-vector with two's complement interpretation.
virtual bool accelerate(patht &loop, path_acceleratort &accelerator)
API to expression classes.
void append(goto_programt::instructionst &instructions)
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)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
void find_modified(const patht &path, expr_sett &modified)
A side effect that returns a non-deterministically chosen value.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
void overflow_expr(const exprt &expr, expr_sett &cases)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool check_sat(bool do_slice)
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
std::list< exprt > expr_listt
The boolean constant false.
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
typet type
Type of symbol.
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
std::set< exprt > dirty_vars
Base class for all expressions.
std::map< exprt, exprt > substitutiont
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
goto_programt pure_accelerator
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
std::string expr2c(const exprt &expr, const namespacet &ns)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
acceleration_utilst utils
A statement in a programming language.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
void find_symbols(const exprt &src, find_symbols_sett &dest)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
symbol_tablet & symbol_table
std::vector< monomialt > monomials
bool simplify(exprt &expr, const namespacet &ns)
instructionst::iterator targett
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.