40 for(
const auto &t : loop)
43 t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
44 t->targets.front() == loop_header &&
45 t->location_number >
back_jump->location_number)
59 for(
const auto &t : loop)
61 if(t->is_backwards_goto())
63 if(t->targets.size()!=1 ||
64 t->get_target()!=loop_header)
93 std::cout <<
"Not accelerating an outer loop\n";
129 std::cout <<
"Not inserting accelerator because of underapproximation\n";
139 std::cout <<
"Accelerated path:\n";
142 std::cout <<
"Accelerator has "
144 <<
" instructions\n";
156 std::cout <<
"Overflow loc is " <<
overflow_loc->location_number <<
'\n';
157 std::cout <<
"Back jump is " <<
back_jump->location_number <<
'\n';
159 for(std::list<path_acceleratort>::iterator it=
accelerators.begin();
247 for(
const auto &new_instruction :
added)
248 loop.insert_instruction(new_instruction);
254 t->swap(*loop_header);
255 loop.insert_instruction(t);
266 loop.insert_instruction(
t2);
277 for(subsumed_pathst::iterator it=
subsumed.begin();
281 if(!it->subsumed.empty())
285 std::cout <<
"Restricting path:\n";
295 jt, it->accelerator.begin(), it->accelerator.end());
297 jt, it->accelerator.begin(), it->accelerator.end());
301 std::cout <<
"Restricting path:\n";
307 std::cout <<
"Building trace automaton...\n";
315 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
336 <<
" for " <<
expr2c(*it,
ns) <<
'\n';
369 const exprt &lhs = it->assign_lhs();
384 if(it->has_condition())
392 for(find_symbols_sett::iterator
jt=read.begin();
413 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
422 if(
sym.module==
"scratch")
429 std::cout <<
"Underapproximate variable: " <<
expr2c(*it,
ns) <<
'\n';
440 ret.module=
"accelerate";
443 ret.pretty_name=name;
486 <<
"Inserting trace automaton with "
488 << accept_states.size() <<
" accepting states and "
489 << transitions.size() <<
" transitions\n";
513 trace_automatont::sym_mapt::iterator begin,
514 trace_automatont::sym_mapt::iterator end,
527 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
531 unsigned int count=0;
555 if(accept_states.find(
likely_next)!=accept_states.end())
572 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
600 for(state_sett::iterator it=accept_states.begin();
601 it!=accept_states.end();
613 for(natural_loops_mutablet::loop_mapt::iterator it =
626 std::cout <<
"Engaging crush mode...\n";
632 std::cout <<
"Crush mode engaged.\n";
646 std::cout <<
"Accelerating function " <<
gf_entry.first <<
'\n';
648 gf_entry.second.body, goto_model, message_handler, use_z3, guard_manager);
655 <<
" accelerator(s)\n";
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
void insert_automaton(trace_automatont &automaton)
acceleration_utilst utils
symbolt make_symbol(std::string name, typet type)
natural_loops_mutablet natural_loops
message_handlert & message_handler
void decl(symbol_exprt &sym, goto_programt::targett t)
symbol_tablet & symbol_table
bool contains_nested_loops(goto_programt::targett &loop_header)
void build_state_machine(trace_automatont::sym_mapt::iterator p, trace_automatont::sym_mapt::iterator end, state_sett &accept_states, symbol_exprt state, symbol_exprt next_state, scratch_programt &state_machine)
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
overflow_mapt overflow_locs
void set_dirty_vars(path_acceleratort &accelerator)
goto_functionst & goto_functions
bool is_underapproximate(path_acceleratort &accelerator)
static const int accelerate_limit
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
guard_managert & guard_manager
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
int accelerate_loop(goto_programt::targett &loop_header)
symbolt fresh_symbol(std::string base, typet type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
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.
The Boolean constant false.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
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 update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment 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.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, 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.
std::list< targett > targetst
The trinary if-then-else operator.
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void add_overflow_checks()
goto_programt overflow_path
std::set< exprt > dirty_vars
goto_programt pure_accelerator
A side_effect_exprt that returns a non-deterministically chosen value.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
std::multimap< goto_programt::targett, state_pairt > sym_mapt
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
std::pair< statet, statet > state_pairt
The Boolean constant true.
The type of an expression, extends irept.
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
Goto Programs with Functions.
Compute natural loops in a goto_function.
void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)
std::list< patht > pathst
std::list< path_nodet > patht
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
This is unused by this implementation of guards, but can be used by other implementations of the same...
std::set< statet > state_sett
unsignedbv_typet unsigned_poly_type()