Go to the documentation of this file.
39 for(
const auto &t : loop)
42 t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
43 t->targets.front() == loop_header &&
44 t->location_number > back_jump->location_number)
58 for(
const auto &t : loop)
60 if(t->is_backwards_goto())
62 if(t->targets.size()!=1 ||
63 t->get_target()!=loop_header)
81 pathst loop_paths, exit_paths;
83 int num_accelerated=0;
84 std::list<path_acceleratort> accelerators;
92 std::cout <<
"Not accelerating an outer loop\n";
128 std::cout <<
"Not inserting accelerator because of underapproximation\n";
134 accelerators.push_back(accelerator);
138 std::cout <<
"Accelerated path:\n";
141 std::cout <<
"Accelerator has "
143 <<
" instructions\n";
155 std::cout <<
"Overflow loc is " << overflow_loc->location_number <<
'\n';
156 std::cout <<
"Back jump is " << back_jump->location_number <<
'\n';
158 for(std::list<path_acceleratort>::iterator it=accelerators.begin();
159 it!=accelerators.end();
169 return num_accelerated;
202 patht &inserted_path)
226 inserted_path.push_back(
path_nodet(back_jump));
240 for(
const auto &loop_instruction : loop)
246 for(
const auto &new_instruction : added)
247 loop.insert_instruction(new_instruction);
253 t->swap(*loop_header);
254 loop.insert_instruction(t);
258 overflow_loc->swap(*loop_end);
259 loop.insert_instruction(overflow_loc);
265 loop.insert_instruction(t2);
268 overflow_loc=loop_end;
276 for(subsumed_pathst::iterator it=
subsumed.begin();
280 if(!it->subsumed.empty())
284 std::cout <<
"Restricting path:\n";
291 patht double_accelerator;
292 patht::iterator jt=double_accelerator.begin();
293 double_accelerator.insert(
294 jt, it->accelerator.begin(), it->accelerator.end());
295 double_accelerator.insert(
296 jt, it->accelerator.begin(), it->accelerator.end());
300 std::cout <<
"Restricting path:\n";
303 automaton.
add_path(double_accelerator);
306 std::cout <<
"Building trace automaton...\n";
314 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
330 dirty_var=jt->second;
334 std::cout <<
"Setting dirty flag " <<
expr2c(dirty_var,
ns)
335 <<
" for " <<
expr2c(*it,
ns) <<
'\n';
368 const exprt &lhs = it->assign_lhs();
383 if(it->has_condition())
391 for(find_symbols_sett::iterator jt=read.begin();
412 for(std::set<exprt>::iterator it=accelerator.
dirty_vars.begin();
416 if(it->id()==ID_symbol && it->type() ==
bool_typet())
428 std::cout <<
"Underapproximate variable: " <<
expr2c(*it,
ns) <<
'\n';
485 <<
"Inserting trace automaton with "
487 << accept_states.size() <<
" accepting states and "
488 << transitions.size() <<
" transitions\n";
498 for(
const auto &sym : automaton.
alphabet)
512 trace_automatont::sym_mapt::iterator begin,
513 trace_automatont::sym_mapt::iterator end,
519 std::map<unsigned int, unsigned int> successor_counts;
520 unsigned int max_count=0;
521 unsigned int likely_next=0;
526 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
529 unsigned int to=state_pair.second;
530 unsigned int count=0;
532 if(successor_counts.find(to)==successor_counts.end())
538 count=successor_counts[to] + 1;
541 successor_counts[to]=count;
543 if(count > max_count)
552 if(successor_counts.size()==1)
554 if(accept_states.find(likely_next)!=accept_states.end())
561 state_machine.
assign(state,
568 state_machine.
assign(next_state,
571 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
574 unsigned int from=state_pair.first;
575 unsigned int to=state_pair.second;
593 state_machine.
assign(next_state, rhs);
597 state_machine.
assign(state, next_state);
599 for(state_sett::iterator it=accept_states.begin();
600 it!=accept_states.end();
610 int num_accelerated=0;
612 for(natural_loops_mutablet::loop_mapt::iterator it =
623 if(num_accelerated > 0)
625 std::cout <<
"Engaging crush mode...\n";
631 std::cout <<
"Crush mode engaged.\n";
634 return num_accelerated;
645 std::cout <<
"Accelerating function " << gf_entry.first <<
'\n';
647 gf_entry.second.body, goto_model, message_handler, use_z3, guard_manager);
651 if(num_accelerated > 0)
653 std::cout <<
"Added " << num_accelerated
654 <<
" 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.
std::string expr2c(const exprt &expr, const namespacet &ns)
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
function_mapt function_map
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())
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)
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)