53 std::map<exprt, polynomialt> polynomials;
59 std::cout <<
"Polynomial accelerating program:\n";
61 for(goto_programt::instructionst::iterator
72 std::cout <<
"Modified:\n";
74 for(expr_sett::iterator it=
modified.begin();
78 std::cout <<
expr2c(*it,
ns) <<
'\n';
99 for(expr_sett::iterator it=
modified.begin();
106 if(it->type().id()==ID_bool)
112 if(target.
id()==ID_index ||
113 target.
id()==ID_dereference)
121 std::map<exprt, polynomialt> this_poly;
122 this_poly[target]=poly;
127 std::cout <<
"Fitted a polynomial for " <<
expr2c(target,
ns)
130 polynomials[target]=poly;
137 if(polynomials.empty())
150 for(patht::iterator it=accelerator.
path.begin();
151 it!=accelerator.
path.end();
154 if(it->loc->is_assign() || it->loc->is_decl())
156 assigns.push_back(*(it->loc));
160 for(expr_sett::iterator it=dirty.begin();
165 std::cout <<
"Trying to accelerate " <<
expr2c(*it,
ns) <<
'\n';
168 if(it->type().id()==ID_bool)
173 std::cout <<
"Ignoring boolean\n";
178 if(it->id()==ID_index ||
179 it->id()==ID_dereference)
182 std::cout <<
"Ignoring array reference\n";
191 std::cout <<
"We've accelerated it already\n";
202 std::cout <<
"Ignoring because it depends on an array\n";
213 std::map<exprt, polynomialt> this_poly;
214 this_poly[target]=poly;
218 polynomials[target]=poly;
225 std::cout <<
"Failed to accelerate " <<
expr2c(*it,
ns) <<
'\n';
245 bool path_is_monotone;
254 std::cout <<
"Assumptions error: " << s <<
'\n';
258 exprt pre_guard(guard);
260 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
261 it!=polynomials.end();
293 exprt forall(ID_forall);
314 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
315 it!=polynomials.end();
318 program.
assign(it->first, it->second.to_expr());
357 for(distinguish_valuest::iterator jt=it->begin();
361 exprt distinguisher=jt->first;
362 bool taken=jt->second;
367 distinguisher.
swap(negated);
370 or_exprt disjunct(new_path, distinguisher);
371 new_path.
swap(disjunct);
384 std::cout <<
"Found a path\n";
394 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
398 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
410 std::vector<expr_listt> parameters;
411 std::set<std::pair<expr_listt, exprt> > coefficients;
419 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
420 <<
", which depends on:\n";
422 for(expr_sett::iterator it=influence.begin();
426 std::cout <<
expr2c(*it,
ns) <<
'\n';
430 for(expr_sett::iterator it=influence.begin();
434 if(it->id()==ID_index ||
435 it->id()==ID_dereference)
444 exprs.push_back(*it);
445 parameters.push_back(exprs);
448 parameters.push_back(exprs);
454 parameters.push_back(exprs);
458 parameters.push_back(exprs);
462 parameters.push_back(exprs);
464 for(std::vector<expr_listt>::iterator it=parameters.begin();
465 it!=parameters.end();
469 coefficients.insert(make_pair(*it, coeff.
symbol_expr()));
490 std::map<exprt, exprt> ivals1;
491 std::map<exprt, exprt> ivals2;
492 std::map<exprt, exprt> ivals3;
494 for(expr_sett::iterator it=influence.begin();
543 std::map<exprt, exprt> values;
545 for(expr_sett::iterator it=influence.begin();
549 values[*it]=ivals1[*it];
564 for(
int n=0; n <= 1; n++)
566 for(expr_sett::iterator it=influence.begin();
570 values[*it]=ivals2[*it];
573 values[*it]=ivals3[*it];
576 values[*it]=ivals1[*it];
580 for(expr_sett::iterator it=influence.begin();
584 values[*it]=ivals3[*it];
598 for(distinguish_valuest::iterator jt=it->begin();
602 exprt distinguisher=jt->first;
603 bool taken=jt->second;
608 distinguisher.
swap(negated);
611 or_exprt disjunct(new_path, distinguisher);
612 new_path.
swap(disjunct);
630 std::cout <<
"Found a polynomial\n";
642 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
646 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
654 std::map<exprt, exprt> &values,
655 std::set<std::pair<expr_listt, exprt> > &coefficients,
663 for(std::map<exprt, exprt>::iterator it=values.begin();
669 expr_type=it->first.type();
673 expr_type=
join_types(expr_type, it->first.type());
678 for(std::map<exprt, exprt>::iterator it=values.begin();
682 program.
assign(it->first, it->second);
686 for(
int i=0; i<num_unwindings; i++)
688 program.
append(loop_body);
694 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
695 it!=coefficients.end();
700 for(expr_listt::const_iterator e_it=it->first.begin();
701 e_it!=it->first.end();
709 from_integer(num_unwindings, expr_type), concrete_value);
710 mult.
swap(concrete_value);
714 std::map<exprt, exprt>::iterator v_it=values.find(e);
716 assert(v_it!=values.end());
718 mult_exprt mult(concrete_value, v_it->second);
719 mult.swap(concrete_value);
747 assumption->guard=polynomial_holds;
760 for(natural_loops_mutablet::natural_loopt::iterator it=
loop.begin();
770 for(
const auto &jt : succs)
796 assert(succs.size() > 0);
808 bool found_branch=
false;
810 for(
const auto &succ : succs)
813 bool taken=scratch_program.
eval(distinguisher).
is_true();
818 (succ->location_number < next->location_number))
827 assert(found_branch);
838 for(goto_programt::targetst::iterator it=t->targets.begin();
839 it!=t->targets.end();
865 std::map<exprt, exprt> shadow_distinguishers;
900 exprt &distinguisher=*it;
904 shadow_distinguishers[distinguisher]=shadow;
907 assign->make_assignment();
931 exprt &distinguisher=d->second;
932 exprt &shadow=shadow_distinguishers[distinguisher];
935 assign->make_assignment();
938 assign->swap(*fixedt);
944 assert(fixedt->is_goto());
954 for(
const auto &target : t->targets)
956 if(target->location_number > t->location_number)
967 fixedt->targets.clear();
968 fixedt->targets.push_back(kill);
978 fixedt->targets.clear();
979 fixedt->targets.push_back(end);
984 fixedt->targets.clear();
985 fixedt->targets.push_back(kill);
998 const exprt &shadow=shadow_distinguishers[expr];
1032 for(expr_sett::iterator it=influence.begin();
1033 it!=influence.end();
1036 if(it->id()==ID_index ||
1037 it->id()==ID_dereference)
The type of an expression.
goto_programt::targett loop_header
void update()
Update all indices.
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
void build_path(scratch_programt &scratch_program, patht &path)
instructionst instructions
The list of instructions in the goto program.
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
void copy_to_operands(const exprt &expr)
Goto Programs with Functions.
void record_path(scratch_programt &scratch_program)
bool depends_on_array(const exprt &e, exprt &array)
std::set< exprt > changed_vars
void assert_for_values(scratch_programt &program, std::map< exprt, exprt > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt &loop_body, exprt &target)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
signedbv_typet signed_poly_type()
std::list< Target > get_successors(Target target) const
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual bool accelerate(path_acceleratort &accelerator)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
unsignedbv_typet unsigned_poly_type()
void ensure_no_overflows(scratch_programt &program)
std::unordered_set< exprt, irep_hash > expr_sett
A declaration of a local variable.
goto_functionst & goto_functions
targett assume(const exprt &guard)
symbolt fresh_symbol(std::string base, typet type)
exprt eval(const exprt &e)
Fixed-width bit-vector with two's complement interpretation.
symbol_tablet & symbol_table
API to expression classes.
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
void find_modified(const patht &path, expr_sett &modified)
A side effect that returns a non-deterministically chosen value.
std::map< exprt, bool > distinguish_valuest
targett insert_after(const_targett target)
Insertion after the given target.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
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.
std::list< exprt > expr_listt
The boolean constant false.
targett insert_before(const_targett target)
Insertion before the given target.
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
acceleration_utilst utils
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
std::set< exprt > dirty_vars
Base class for all expressions.
std::map< exprt, exprt > substitutiont
natural_loops_mutablet::natural_loopt & loop
goto_programt pure_accelerator
std::string expr2c(const exprt &expr, const namespacet &ns)
std::list< exprt > distinguishers
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
distinguish_mapt distinguishing_points
bool find_path(patht &path)
#define Forall_goto_program_instructions(it, program)
std::list< distinguish_valuest > accelerated_paths
void cone_of_influence(const exprt &target, expr_sett &cone)
Expression to hold a symbol (variable)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
goto_programt & goto_program
void find_distinguishing_points()
bool simplify(exprt &expr, const namespacet &ns)
instructionst::iterator targett
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)