Go to the documentation of this file.
41 for(
const auto &t : loop)
44 t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
45 t->targets.front() == loop_header &&
46 t->location_number > back_jump->location_number)
60 for(
const auto &t : loop)
62 if(t->is_backwards_goto())
64 if(t->targets.size()!=1 ||
65 t->get_target()!=loop_header)
83 pathst loop_paths, exit_paths;
85 int num_accelerated=0;
86 std::list<path_acceleratort> accelerators;
94 std::cout <<
"Not accelerating an outer loop\n";
130 std::cout <<
"Not inserting accelerator because of underapproximation\n";
136 accelerators.push_back(accelerator);
140 std::cout <<
"Accelerated path:\n";
143 std::cout <<
"Accelerator has "
145 <<
" instructions\n";
157 std::cout <<
"Overflow loc is " << overflow_loc->location_number <<
'\n';
158 std::cout <<
"Back jump is " << back_jump->location_number <<
'\n';
160 for(std::list<path_acceleratort>::iterator it=accelerators.begin();
161 it!=accelerators.end();
171 return num_accelerated;
204 patht &inserted_path)
228 inserted_path.push_back(
path_nodet(back_jump));
242 for(
const auto &loop_instruction : loop)
248 for(
const auto &new_instruction : added)
249 loop.insert_instruction(new_instruction);
255 t->swap(*loop_header);
256 loop.insert_instruction(t);
260 overflow_loc->swap(*loop_end);
261 loop.insert_instruction(overflow_loc);
267 loop.insert_instruction(t2);
270 overflow_loc=loop_end;
278 for(subsumed_pathst::iterator it=
subsumed.begin();
282 if(!it->subsumed.empty())
286 std::cout <<
"Restricting path:\n";
293 patht double_accelerator;
294 patht::iterator jt=double_accelerator.begin();
295 double_accelerator.insert(
296 jt, it->accelerator.begin(), it->accelerator.end());
297 double_accelerator.insert(
298 jt, it->accelerator.begin(), it->accelerator.end());
302 std::cout <<
"Restricting path:\n";
305 automaton.
add_path(double_accelerator);
308 std::cout <<
"Building trace automaton...\n";
316 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
332 dirty_var=jt->second;
336 std::cout <<
"Setting dirty flag " <<
expr2c(dirty_var,
ns)
337 <<
" for " <<
expr2c(*it,
ns) <<
'\n';
370 const exprt &lhs = it->get_assign().lhs();
385 if(it->has_condition())
393 for(find_symbols_sett::iterator jt=read.begin();
414 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
418 if(it->id()==ID_symbol && it->type() ==
bool_typet())
430 std::cout <<
"Underapproximate variable: " <<
expr2c(*it,
ns) <<
'\n';
487 <<
"Inserting trace automaton with "
489 << accept_states.size() <<
" accepting states and "
490 << transitions.size() <<
" transitions\n";
500 for(
const auto &sym : automaton.
alphabet)
514 trace_automatont::sym_mapt::iterator begin,
515 trace_automatont::sym_mapt::iterator end,
521 std::map<unsigned int, unsigned int> successor_counts;
522 unsigned int max_count=0;
523 unsigned int likely_next=0;
528 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
531 unsigned int to=state_pair.second;
532 unsigned int count=0;
534 if(successor_counts.find(to)==successor_counts.end())
540 count=successor_counts[to] + 1;
543 successor_counts[to]=count;
545 if(count > max_count)
554 if(successor_counts.size()==1)
556 if(accept_states.find(likely_next)!=accept_states.end())
563 state_machine.
assign(state,
570 state_machine.
assign(next_state,
573 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
576 unsigned int from=state_pair.first;
577 unsigned int to=state_pair.second;
595 state_machine.
assign(next_state, rhs);
599 state_machine.
assign(state, next_state);
601 for(state_sett::iterator it=accept_states.begin();
602 it!=accept_states.end();
612 int num_accelerated=0;
614 for(natural_loops_mutablet::loop_mapt::iterator it =
625 if(num_accelerated > 0)
627 std::cout <<
"Engaging crush mode...\n";
633 std::cout <<
"Crush mode engaged.\n";
636 return num_accelerated;
647 std::cout <<
"Accelerating function " << it->first <<
'\n';
649 it->second.body, goto_model, message_handler, use_z3, guard_manager);
653 if(num_accelerated > 0)
655 std::cout <<
"Added " << num_accelerated
656 <<
" accelerator(s)\n";
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static const int accelerate_limit
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
acceleration_utilst utils
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
void accept_states(state_sett &states)
guard_managert & guard_manager
The type of an expression, extends irept.
symbolt fresh_symbol(std::string base, typet type)
std::list< patht > pathst
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.
typet type
Type of symbol.
symbol_tablet & symbol_table
void get_transitions(sym_mapt &transitions)
The trinary if-then-else operator.
void update()
Update all indices.
A codet representing the declaration of a local variable.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Base class for all expressions.
message_handlert & message_handler
std::pair< statet, statet > state_pairt
irep_idt base_name
Base (non-scoped) name.
std::set< exprt > dirty_vars
Expression to hold a symbol (variable)
void set_dirty_vars(path_acceleratort &accelerator)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
unsignedbv_typet unsigned_poly_type()
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool is_underapproximate(path_acceleratort &accelerator)
irep_idt pretty_name
Language-specific display name.
int accelerate_loop(goto_programt::targett &loop_header)
std::list< targett > targetst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
This is unused by this implementation of guards, but can be used by other implementations of the same...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void add_path(patht &path)
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
const source_locationt & source_location() const
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
goto_programt overflow_path
A loop, specified as a set of instructions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
targett assume(const exprt &guard)
goto_programt pure_accelerator
The Boolean constant false.
bool accelerate(path_acceleratort &accelerator)
void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)
#define Forall_goto_functions(it, functions)
std::multimap< goto_programt::targett, state_pairt > sym_mapt
symbolt make_symbol(std::string name, typet type)
A side_effect_exprt that returns a non-deterministically chosen value.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
instructionst instructions
The list of instructions in the goto program.
overflow_mapt overflow_locs
goto_functionst goto_functions
GOTO functions.
std::unordered_set< irep_idt > find_symbols_sett
std::list< path_nodet > patht
Compute natural loops in a goto_function.
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
void decl(symbol_exprt &sym, goto_programt::targett t)
bool insert_instruction(const T instruction)
Adds instruction to this loop.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
void insert_automaton(trace_automatont &automaton)
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 insert_before_swap(targett target)
Insertion that preserves jumps to "target".
A codet representing an assignment in the program.
The Boolean constant true.
irep_idt module
Name of module the symbol belongs to.
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
targett assign(const exprt &lhs, const exprt &rhs)
natural_loops_mutablet natural_loops
const source_locationt & source_location() const
irep_idt name
The unique identifier.
goto_functionst & goto_functions
void add_overflow_checks()
instructionst::iterator targett
std::set< statet > state_sett
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
bool contains_nested_loops(goto_programt::targett &loop_header)