41 for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
48 t->targets.size()==1 &&
49 t->targets.front()==loop_header &&
50 t->location_number > back_jump->location_number)
64 for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
70 if(t->is_backwards_goto())
72 if(t->targets.size()!=1 ||
73 t->get_target()!=loop_header)
91 pathst loop_paths, exit_paths;
93 int num_accelerated=0;
94 std::list<path_acceleratort> accelerators;
102 std::cout <<
"Not accelerating an outer loop\n";
137 std::cout <<
"Not inserting accelerator because of underapproximation\n";
143 accelerators.push_back(accelerator);
147 std::cout <<
"Accelerated path:\n";
150 std::cout <<
"Accelerator has " 152 <<
" instructions\n";
156 goto_programt::instructiont skip(
SKIP);
162 loop.insert(new_inst);
165 std::cout <<
"Overflow loc is " << overflow_loc->location_number <<
'\n';
166 std::cout <<
"Back jump is " << back_jump->location_number <<
'\n';
168 for(std::list<path_acceleratort>::iterator it=accelerators.begin();
169 it!=accelerators.end();
179 return num_accelerated;
209 patht &inserted_path)
217 jump->targets.push_back(loop_body);
224 jump->targets.push_back(back_jump);
233 inserted_path.push_back(
path_nodet(back_jump));
247 for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
255 loop.insert(added.begin(), added.end());
259 t->make_assignment();
261 t->swap(*loop_header);
265 goto_programt::instructiont s(
SKIP);
268 overflow_loc->swap(*loop_end);
269 loop.insert(overflow_loc);
271 goto_programt::instructiont g(
GOTO);
273 g.targets.push_back(overflow_loc);
281 overflow_loc=loop_end;
289 for(subsumed_pathst::iterator it=
subsumed.begin();
293 if(!it->subsumed.empty())
297 std::cout <<
"Restricting path:\n";
304 patht double_accelerator;
305 patht::iterator jt=double_accelerator.begin();
306 double_accelerator.insert(
307 jt, it->accelerator.begin(), it->accelerator.end());
308 double_accelerator.insert(
309 jt, it->accelerator.begin(), it->accelerator.end());
313 std::cout <<
"Restricting path:\n";
316 automaton.
add_path(double_accelerator);
319 std::cout <<
"Building trace automaton...\n";
327 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
343 dirty_var=jt->second;
347 std::cout <<
"Setting dirty flag " <<
expr2c(dirty_var,
ns)
348 <<
" for " <<
expr2c(*it,
ns) <<
'\n';
362 goto_programt::instructiont assign(
ASSIGN);
386 goto_programt::instructiont clear_flag(
ASSIGN);
403 for(find_symbols_sett::iterator jt=read.begin();
415 goto_programt::instructiont not_dirty(
ASSUME);
416 not_dirty.guard=
not_exprt(dirty_var->second);
424 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
428 if(it->id()==ID_symbol && it->type() ==
bool_typet())
440 std::cout <<
"Underapproximate variable: " <<
expr2c(*it,
ns) <<
'\n';
480 assign->make_assignment();
500 <<
"Inserting trace automaton with " 502 << accept_states.size() <<
" accepting states and " 503 << transitions.size() <<
" transitions\n";
513 for(
const auto &sym : automaton.
alphabet)
526 trace_automatont::sym_mapt::iterator begin,
527 trace_automatont::sym_mapt::iterator end,
533 std::map<unsigned int, unsigned int> successor_counts;
534 unsigned int max_count=0;
535 unsigned int likely_next=0;
540 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
543 unsigned int to=state_pair.second;
544 unsigned int count=0;
546 if(successor_counts.find(to)==successor_counts.end())
552 count=successor_counts[to] + 1;
555 successor_counts[to]=count;
557 if(count > max_count)
566 if(successor_counts.size()==1)
568 if(accept_states.find(likely_next)!=accept_states.end())
575 state_machine.
assign(state,
582 state_machine.
assign(next_state,
585 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
588 unsigned int from=state_pair.first;
589 unsigned int to=state_pair.second;
607 state_machine.
assign(next_state, rhs);
611 state_machine.
assign(state, next_state);
613 for(state_sett::iterator it=accept_states.begin();
614 it!=accept_states.end();
624 int num_accelerated=0;
626 for(natural_loops_mutablet::loop_mapt::iterator it =
637 if(num_accelerated > 0)
639 std::cout <<
"Engaging crush mode...\n";
645 std::cout <<
"Crush mode engaged.\n";
648 return num_accelerated;
659 std::cout <<
"Accelerating function " << it->first <<
'\n';
660 acceleratet accelerate(it->second.body, functions, symbol_table, use_z3);
664 if(num_accelerated > 0)
666 std::cout <<
"Added " << num_accelerated
667 <<
" accelerator(s)\n";
void get_transitions(sym_mapt &transitions)
The type of an expression.
irep_idt name
The unique identifier.
void insert_automaton(trace_automatont &automaton)
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
void update()
Update all indices.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
targett add_instruction()
Adds an instruction at the end.
targett assign(const exprt &lhs, const exprt &rhs)
natural_loops_mutablet natural_loops
static const int accelerate_limit
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
goto_functionst & goto_functions
bool contains_nested_loops(goto_programt::targett &loop_header)
instructionst instructions
The list of instructions in the goto program.
void add_overflow_checks()
const irep_idt & get_identifier() const
Goto Programs with Functions.
std::set< goto_programt::targett > natural_loopt
int accelerate_loop(goto_programt::targett &loop_header)
The trinary if-then-else operator.
irep_idt module
Name of module the symbol belongs to.
irep_idt pretty_name
Language-specific display name.
void accept_states(state_sett &states)
void set_dirty_vars(path_acceleratort &accelerator)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::pair< statet, statet > state_pairt
symbol_tablet & symbol_table
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
goto_programt overflow_path
virtual bool accelerate(path_acceleratort &accelerator)
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
The boolean constant true.
unsignedbv_typet unsigned_poly_type()
A declaration of a local variable.
targett assume(const exprt &guard)
symbolt fresh_symbol(std::string base, typet type)
API to expression classes.
std::list< path_nodet > patht
bool is_underapproximate(path_acceleratort &accelerator)
std::list< targett > targetst
A side effect that returns a non-deterministically chosen value.
std::list< patht > pathst
void add_path(patht &path)
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed)
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
std::set< statet > state_sett
The boolean constant false.
symbolt make_symbol(std::string name, typet type)
targett insert_before(const_targett target)
Insertion before the given target.
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void decl(symbol_exprt &sym, goto_programt::targett t)
void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)
typet type
Type of symbol.
std::multimap< goto_programt::targett, state_pairt > sym_mapt
std::set< exprt > dirty_vars
Base class for all expressions.
overflow_mapt overflow_locs
irep_idt base_name
Base (non-scoped) name.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
goto_programt pure_accelerator
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
std::string expr2c(const exprt &expr, const namespacet &ns)
void accelerate_functions(goto_functionst &functions, symbol_tablet &symbol_table, bool use_z3)
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 destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
Compute natural loops in a goto_function.
acceleration_utilst utils
void find_symbols(const exprt &src, find_symbols_sett &dest)
instructionst::iterator targett