42 std::cout <<
"Polynomial accelerating program:\n";
44 for(goto_programt::instructionst::iterator
55 std::cout <<
"Modified:\n";
57 for(expr_sett::iterator it=
modified.begin();
61 std::cout <<
expr2c(*it,
ns) <<
'\n';
82 for(expr_sett::iterator it=
modified.begin();
110 std::cout <<
"Fitted a polynomial for " <<
expr2c(target,
ns)
133 for(patht::iterator it=accelerator.
path.begin();
134 it!=accelerator.
path.end();
137 if(it->loc->is_assign() || it->loc->is_decl())
139 assigns.push_back(*(it->loc));
143 for(expr_sett::iterator it=dirty.begin();
148 std::cout <<
"Trying to accelerate " <<
expr2c(*it,
ns) <<
'\n';
156 std::cout <<
"Ignoring boolean\n";
165 std::cout <<
"Ignoring array reference\n";
174 std::cout <<
"We've accelerated it already\n";
185 std::cout <<
"Ignoring because it depends on an array\n";
208 std::cout <<
"Failed to accelerate " <<
expr2c(*it,
ns) <<
'\n';
235 catch(
const std::string &s)
238 std::cout <<
"Assumptions error: " << s <<
'\n';
244 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
294 for(std::map<exprt, polynomialt>::iterator it=
polynomials.begin();
298 program.assign(it->first, it->second.to_expr());
327 program.append(
fixed);
328 program.append(
fixed);
337 for(distinguish_valuest::iterator
jt=it->begin();
364 std::cout <<
"Found a path\n";
372 catch(
const std::string &s)
374 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
378 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
390 std::vector<expr_listt> parameters;
391 std::set<std::pair<expr_listt, exprt> > coefficients;
399 std::cout <<
"Fitting a polynomial for " <<
expr2c(var,
ns)
400 <<
", which depends on:\n";
402 for(expr_sett::iterator it=
influence.begin();
406 std::cout <<
expr2c(*it,
ns) <<
'\n';
410 for(expr_sett::iterator it=
influence.begin();
424 exprs.push_back(*it);
425 parameters.push_back(
exprs);
428 parameters.push_back(
exprs);
434 parameters.push_back(
exprs);
438 parameters.push_back(
exprs);
442 parameters.push_back(
exprs);
444 for(std::vector<expr_listt>::iterator it=parameters.begin();
445 it!=parameters.end();
470 std::map<exprt, exprt>
ivals1;
471 std::map<exprt, exprt>
ivals2;
472 std::map<exprt, exprt>
ivals3;
474 for(expr_sett::iterator it=
influence.begin();
486 ival2.symbol_expr()));
488 ival3.symbol_expr()));
523 std::map<exprt, exprt> values;
525 for(expr_sett::iterator it=
influence.begin();
534 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
544 for(
int n=0;
n <= 1;
n++)
546 for(expr_sett::iterator it=
influence.begin();
560 for(expr_sett::iterator it=
influence.begin();
578 for(distinguish_valuest::iterator
jt=it->begin();
610 std::cout <<
"Found a polynomial\n";
620 catch(
const std::string &s)
622 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
626 std::cout <<
"Error in fitting polynomial SAT check: " << s <<
'\n';
634 std::map<exprt, exprt> &values,
635 std::set<std::pair<expr_listt, exprt> > &coefficients,
643 for(std::map<exprt, exprt>::iterator it=values.begin();
658 for(std::map<exprt, exprt>::iterator it=values.begin();
662 program.
assign(it->first, it->second);
674 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
675 it!=coefficients.end();
680 for(expr_listt::const_iterator
e_it=it->first.begin();
681 e_it!=it->first.end();
694 std::map<exprt, exprt>::iterator
v_it=values.find(e);
772 "we should have a looping path, so we should never hit a location "
773 "with no successors.");
787 for(
const auto &succ :
succs)
795 (succ->location_number < next->location_number))
815 for(goto_programt::targetst::iterator it=t->targets.begin();
816 it!=t->targets.end();
821 cond = t->get_condition();
847 if(instruction.is_assert())
848 instruction.turn_into_assume();
870 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
894 if(!
loop.contains(t))
928 for(
const auto &target : t->targets)
930 if(target->location_number > t->location_number)
933 if(
loop.contains(target))
942 fixedt->targets.push_back(kill);
953 fixedt->targets.push_back(end);
959 fixedt->targets.push_back(kill);
989 for(std::list<symbol_exprt>::iterator it =
distinguishers.begin();
1007 for(expr_sett::iterator it=
influence.begin();
std::list< exprt > expr_listt
void find_modified(const patht &path, expr_sett &modified)
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 check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
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.
A codet representing an assignment in the program.
goto_functionst & goto_functions
symbol_tablet & symbol_table
std::list< distinguish_valuest > accelerated_paths
guard_managert & guard_manager
std::list< symbol_exprt > distinguishers
bool depends_on_array(const exprt &e, exprt &array)
message_handlert & message_handler
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)
natural_loops_mutablet::natural_loopt & loop
void record_path(scratch_programt &scratch_program)
goto_programt::targett loop_header
goto_programt & goto_program
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
bool accelerate(path_acceleratort &accelerator)
bool find_path(patht &path)
distinguish_mapt distinguishing_points
void cone_of_influence(const exprt &target, expr_sett &cone)
void find_distinguishing_points()
void build_path(scratch_programt &scratch_program, patht &path)
acceleration_utilst utils
std::map< exprt, bool > distinguish_valuest
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
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())
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void update()
Update all indices.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
const irep_idt & id() const
Binary multiplication Associativity is not specified.
std::set< exprt > changed_vars
std::set< exprt > dirty_vars
goto_programt pure_accelerator
The plus expression Associativity is not specified.
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)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
Semantic type conversion.
std::unordered_set< exprt, irep_hash > expr_sett
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::list< path_nodet > patht
std::map< exprt, exprt > substitutiont
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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()
signedbv_typet signed_poly_type()