52 for(patht::iterator it=loop.begin();
56 body.push_back(*(it->loc));
60 std::map<exprt, polynomialt> polynomials;
67 std::cout <<
"Polynomial accelerating program:\n";
69 for(goto_programt::instructionst::iterator it=body.begin();
76 std::cout <<
"Modified:\n";
78 for(expr_sett::iterator it=targets.begin();
82 std::cout <<
expr2c(*it,
ns) <<
'\n';
86 for(goto_programt::instructionst::iterator it=body.begin();
90 if(it->is_assign() || it->is_decl())
92 assigns.push_back(*it);
103 for(expr_sett::iterator it=targets.begin();
120 if(influence.find(target)==influence.end())
123 std::cout <<
"Found nonrecursive expression: " 131 if(target.
id()==ID_index ||
132 target.
id()==ID_dereference)
141 std::map<exprt, polynomialt> this_poly;
142 this_poly[target]=poly;
146 polynomials.insert(std::make_pair(target, poly));
152 std::cout <<
"Failed to fit a polynomial for " 160 if(polynomials.empty())
177 bool path_is_monotone;
183 catch(
const std::string &s)
186 std::cout <<
"Assumptions error: " << s <<
'\n';
192 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
193 it!=polynomials.end();
196 replace_expr(it->first, it->second.to_expr(), guard_last);
245 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
246 it!=polynomials.end();
249 program.
assign(it->first, it->second.to_expr());
259 std::cout <<
"Failed to accelerate a nonrecursive expression\n";
284 std::vector<expr_listt> parameters;
285 std::set<std::pair<expr_listt, exprt> > coefficients;
293 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
294 <<
", which depends on:\n";
296 for(expr_sett::iterator it=influence.begin();
300 std::cout <<
expr2c(*it,
ns) <<
'\n';
304 for(expr_sett::iterator it=influence.begin();
308 if(it->id()==ID_index ||
309 it->id()==ID_dereference)
317 exprs.push_back(*it);
318 parameters.push_back(exprs);
321 parameters.push_back(exprs);
327 parameters.push_back(exprs);
335 parameters.push_back(exprs);
346 for(std::vector<expr_listt>::iterator it=parameters.begin();
347 it!=parameters.end();
352 coefficients.insert(std::make_pair(*it, coeff.
symbol_expr()));
364 std::map<exprt, int> values;
366 for(expr_sett::iterator it=influence.begin();
374 std::cout <<
"Fitting polynomial over " << values.size()
378 for(
int n=0; n<=2; n++)
380 for(expr_sett::iterator it=influence.begin();
394 for(expr_sett::iterator it=influence.begin();
404 std::cout <<
"Fitting polynomial with program:\n";
423 catch(
const std::string &s)
425 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
429 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
466 std::cout <<
"Fitting constant, eval'd to: " 476 mon.terms.push_back(term);
477 mon.coeff=mp.to_long();
484 catch(
const std::string &s)
486 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
490 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
499 std::map<exprt, int> &values,
500 std::set<std::pair<expr_listt, exprt> > &coefficients,
509 for(std::map<exprt, int>::iterator it=values.begin();
513 typet this_type=it->first.type();
514 if(this_type.
id()==ID_pointer)
517 std::cout <<
"Overriding pointer type\n";
536 for(std::map<exprt, int>::iterator it=values.begin();
544 for(
int i=0; i < num_unwindings; i++)
546 program.
append(loop_body);
552 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
553 it!=coefficients.end();
556 int concrete_value=1;
558 for(expr_listt::const_iterator e_it=it->first.begin();
559 e_it!=it->first.end();
566 concrete_value *= num_unwindings;
570 std::map<exprt, int>::iterator v_it=values.find(e);
572 if(v_it!=values.end())
574 concrete_value *= v_it->second;
608 assumption->guard=polynomial_holds;
619 for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
620 r_it!=orig_body.rend();
623 if(r_it->is_assign())
634 for(expr_sett::iterator s_it=lhs_syms.begin();
635 s_it!=lhs_syms.end();
638 if(cone.find(*s_it)!=cone.end())
642 body.push_front(*r_it);
643 cone.erase(assignment.
lhs());
653 std::map<exprt, polynomialt> polynomials,
668 std::vector<exprt> polynomials_hold;
673 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
674 it!=polynomials.end();
677 const equal_exprt holds(it->first, it->second.to_expr());
680 polynomials_hold.push_back(holds);
685 codet inc_loop_counter=
691 for(std::vector<exprt>::iterator it=polynomials_hold.begin();
692 it!=polynomials_hold.end();
699 std::cout <<
"Checking following program for inductiveness:\n";
709 std::cout <<
"Not inductive!\n";
718 catch(
const std::string &s)
720 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
725 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
732 std::map<exprt, polynomialt> &polynomials,
740 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
741 it!=polynomials.end();
744 it->second.substitute(substitution);
755 for(expr_sett::iterator it=modified.begin();
763 vars.erase(loop_counter_name);
765 for(find_symbols_sett::iterator it=vars.begin();
788 for(patht::reverse_iterator r_it=path.rbegin();
801 if(lhs.
id()==ID_symbol)
805 else if(lhs.
id()==ID_index ||
806 lhs.
id()==ID_dereference)
815 else if(t->is_assume() || t->is_assert())
824 if(!r_it->guard.is_true() && !r_it->guard.is_nil())
std::list< exprt > expr_listt
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
The type of an expression.
exprt precondition(patht &path)
A generic base class for relations, i.e., binary predicates.
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
const irep_idt & get_identifier() const
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
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::list< instructiont > instructionst
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)
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
instructionst::iterator targett
symbolt fresh_symbol(std::string base, typet type)
exprt eval(const exprt &e)
Fixed-width bit-vector with two's complement interpretation.
bool accelerate(patht &loop, path_acceleratort &accelerator)
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
instructionst::const_iterator const_targett
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.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
message_handlert & message_handler
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
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.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
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::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
std::set< exprt > dirty_vars
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
std::map< exprt, exprt > substitutiont
const source_locationt & source_location() const
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)
Expression to hold a symbol (variable)
acceleration_utilst utils
A statement in a programming language.
std::unordered_set< irep_idt > find_symbols_sett
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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)