44 for(patht::iterator it=loop.begin();
48 body.push_back(*(it->loc));
59 std::cout <<
"Polynomial accelerating program:\n";
61 for(goto_programt::instructionst::iterator it=body.begin();
65 program.output_instruction(
ns,
"scratch", std::cout, *it);
68 std::cout <<
"Modified:\n";
70 for(expr_sett::iterator it=targets.begin();
74 std::cout <<
expr2c(*it,
ns) <<
'\n';
78 for(goto_programt::instructionst::iterator it=body.begin();
82 if(it->is_assign() || it->is_decl())
84 assigns.push_back(*it);
95 for(expr_sett::iterator it=targets.begin();
115 std::cout <<
"Found nonrecursive expression: "
144 std::cout <<
"Failed to fit a polynomial for "
176 catch(
const std::string &s)
179 std::cout <<
"Assumptions error: " << s <<
'\n';
185 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
238 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
242 program.assign(it->first, it->second.to_expr());
252 std::cout <<
"Failed to accelerate a nonrecursive expression\n";
277 std::vector<expr_listt> parameters;
278 std::set<std::pair<expr_listt, exprt> > coefficients;
286 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
287 <<
", which depends on:\n";
289 for(expr_sett::iterator it=
influence.begin();
293 std::cout <<
expr2c(*it,
ns) <<
'\n';
297 for(expr_sett::iterator it=
influence.begin();
310 exprs.push_back(*it);
311 parameters.push_back(
exprs);
314 parameters.push_back(
exprs);
320 parameters.push_back(
exprs);
328 parameters.push_back(
exprs);
339 for(std::vector<expr_listt>::iterator it=parameters.begin();
340 it!=parameters.end();
345 coefficients.insert(std::make_pair(*it, coeff.
symbol_expr()));
357 std::map<exprt, int> values;
359 for(expr_sett::iterator it=
influence.begin();
367 std::cout <<
"Fitting polynomial over " << values.size()
371 for(
int n=0;
n<=2;
n++)
373 for(expr_sett::iterator it=
influence.begin();
387 for(expr_sett::iterator it=
influence.begin();
397 std::cout <<
"Fitting polynomial with program:\n";
414 catch(
const std::string &s)
416 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
420 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
461 std::cout <<
"Fitting constant, eval'd to: "
471 mon.terms.push_back(term);
472 mon.coeff=
mp.to_long();
479 catch(
const std::string &s)
481 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
485 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
494 std::map<exprt, int> &values,
495 std::set<std::pair<expr_listt, exprt> > &coefficients,
504 for(std::map<exprt, int>::iterator it=values.begin();
512 std::cout <<
"Overriding pointer type\n";
529 "joined types must be non-empty bitvector types");
532 for(std::map<exprt, int>::iterator it=values.begin();
548 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
549 it!=coefficients.end();
554 for(expr_listt::const_iterator
e_it=it->first.begin();
555 e_it!=it->first.end();
566 std::map<exprt, int>::iterator
v_it=values.find(e);
568 if(
v_it!=values.end())
592 overflow.overflow_expr(rhs, overflow_expr);
614 for(goto_programt::instructionst::reverse_iterator
r_it=
orig_body.rbegin();
618 if(
r_it->is_assign())
638 body.push_front(*
r_it);
669 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
679 program.append(body);
694 std::cout <<
"Checking following program for inductiveness:\n";
704 std::cout <<
"Not inductive!\n";
713 catch(
const std::string &s)
715 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
720 std::cout <<
"Error in inductiveness SAT check: " << s <<
'\n';
735 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
774 for(patht::reverse_iterator
r_it=path.rbegin();
783 const exprt &lhs = t->assign_lhs();
784 const exprt &rhs = t->assign_rhs();
800 else if(t->is_assume() || t->is_assert())
809 if(!
r_it->guard.is_true() && !
r_it->guard.is_nil())
std::list< exprt > expr_listt
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
unsignedbv_typet size_type()
void find_modified(const patht &path, expr_sett &modified)
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
symbolt fresh_symbol(std::string base, typet type)
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)
virtual void clear()
Reset the abstract state.
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.
std::size_t get_width() const
A 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.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The Boolean constant false.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
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
Binary multiplication Associativity is not specified.
std::set< exprt > dirty_vars
goto_programt pure_accelerator
The plus expression Associativity is not specified.
acceleration_utilst utils
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)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
bool accelerate(patht &loop, path_acceleratort &accelerator)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
symbol_tablet & symbol_table
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
guard_managert & guard_manager
exprt precondition(patht &path)
message_handlert & message_handler
bool check_sat(bool do_slice, guard_managert &guard_manager)
targett assign(const exprt &lhs, const exprt &rhs)
void append(goto_programt::instructionst &instructions)
exprt eval(const exprt &e)
A side_effect_exprt that returns a non-deterministically chosen value.
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Semantic type conversion.
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)
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
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
std::list< path_nodet > patht
std::map< exprt, exprt > substitutiont
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.
unsignedbv_typet unsigned_poly_type()
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?