cprover
|
#include <accelerate.h>
Public Member Functions | |
acceleratet (goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3) | |
int | accelerate_loop (goto_programt::targett &loop_header) |
int | accelerate_loops () |
bool | accelerate_path (patht &path, path_acceleratort &accelerator) |
void | restrict_traces () |
Static Public Attributes | |
static const int | accelerate_limit = -1 |
Protected Types | |
typedef std::map< goto_programt::targett, goto_programt::targetst > | overflow_mapt |
Definition at line 30 of file accelerate.h.
|
protected |
Definition at line 122 of file accelerate.h.
|
inline |
Definition at line 33 of file accelerate.h.
References natural_loops, and program.
int acceleratet::accelerate_loop | ( | goto_programt::targett & | loop_header | ) |
Definition at line 89 of file accelerate.cpp.
References disjunctive_polynomial_accelerationt::accelerate(), accelerate_limit, contains_nested_loops(), find_back_jump(), goto_functions, insert_accelerator(), goto_programt::insert_before_swap(), goto_programt::instructions, is_underapproximate(), natural_loops_templatet< P, T >::loop_map, make_overflow_loc(), message_handler, natural_loops, ns, output_path(), path_acceleratort::path, program, path_acceleratort::pure_accelerator, SKIP, subsumed, symbol_table, and goto_programt::update().
Referenced by accelerate_loops().
int acceleratet::accelerate_loops | ( | ) |
Definition at line 618 of file accelerate.cpp.
References accelerate_loop(), natural_loops_templatet< P, T >::loop_map, natural_loops, program, restrict_traces(), and goto_programt::update().
Referenced by accelerate_functions().
bool acceleratet::accelerate_path | ( | patht & | path, |
path_acceleratort & | accelerator | ||
) |
|
protected |
Definition at line 352 of file accelerate.cpp.
References ASSIGN, ASSUME, goto_programt::instructiont::code, dirty_vars_map, find_symbols(), goto_programt::instructiont::guard, goto_programt::insert_before_swap(), goto_programt::instructions, namespacet::lookup(), ns, exprt::op0(), and program.
|
protected |
Definition at line 521 of file accelerate.cpp.
References scratch_programt::assign(), scratch_programt::assume(), from_integer(), and exprt::type().
Referenced by insert_automaton().
|
protected |
Definition at line 59 of file accelerate.cpp.
References natural_loops_templatet< P, T >::loop_map, and natural_loops.
Referenced by accelerate_loop().
|
protected |
Definition at line 458 of file accelerate.cpp.
References goto_programt::insert_before(), and program.
Referenced by decl(), and insert_automaton().
|
protected |
Definition at line 469 of file accelerate.cpp.
References decl(), goto_programt::insert_before(), and program.
|
protected |
|
protected |
Definition at line 34 of file accelerate.cpp.
References natural_loops_templatet< P, T >::loop_map, and natural_loops.
Referenced by accelerate_loop().
|
protected |
|
protected |
Definition at line 182 of file accelerate.cpp.
References insert_looping_path(), goto_programt::instructions, path_acceleratort::overflow_path, path_acceleratort::pure_accelerator, and subsumed.
Referenced by accelerate_loop().
|
protected |
Definition at line 480 of file accelerate.cpp.
References trace_automatont::accept_states(), trace_automatont::alphabet, build_state_machine(), decl(), from_integer(), trace_automatont::get_transitions(), trace_automatont::init_state(), goto_programt::insert_before_swap(), goto_programt::instructions, make_symbol(), message_handler, trace_automatont::num_states(), program, symbolt::symbol_expr(), symbol_table, exprt::type(), and unsigned_poly_type().
Referenced by restrict_traces().
|
protected |
Definition at line 205 of file accelerate.cpp.
References goto_programt::destructive_insert(), goto_programt::insert_before(), and program.
Referenced by insert_accelerator().
|
protected |
Definition at line 418 of file accelerate.cpp.
References path_acceleratort::dirty_vars, expr2c(), symbol_exprt::get_identifier(), symbol_table_baset::lookup(), symbolt::module, ns, symbol_table, and to_symbol_expr().
Referenced by accelerate_loop().
|
protected |
Definition at line 232 of file accelerate.cpp.
References overflow_instrumentert::add_overflow_checks(), acceleration_utilst::fresh_symbol(), GOTO, goto_programt::instructiont::guard, goto_programt::insert_after(), natural_loops_templatet< P, T >::loop_map, natural_loops, overflow_locs, program, SKIP, goto_programt::instructiont::swap(), symbolt::symbol_expr(), symbol_table, goto_programt::instructiont::targets, and utils.
Referenced by accelerate_loop().
Definition at line 444 of file accelerate.cpp.
References symbol_table_baset::add(), symbolt::base_name, symbolt::module, symbolt::name, symbolt::pretty_name, symbol_table, and symbolt::type.
Referenced by insert_automaton().
void acceleratet::restrict_traces | ( | ) |
Definition at line 281 of file accelerate.cpp.
References trace_automatont::add_path(), trace_automatont::build(), insert_automaton(), ns, output_path(), program, subsumed, and symbol_table.
Referenced by accelerate_loops().
|
protected |
Definition at line 321 of file accelerate.cpp.
References goto_programt::add_instruction(), ASSIGN, path_acceleratort::dirty_vars, dirty_vars_map, expr2c(), acceleration_utilst::fresh_symbol(), message_handler, ns, path_acceleratort::pure_accelerator, symbolt::symbol_expr(), symbol_table, and utils.
|
static |
Definition at line 56 of file accelerate.h.
Referenced by accelerate_loop().
|
protected |
Definition at line 125 of file accelerate.h.
Referenced by add_dirty_checks(), and set_dirty_vars().
|
protected |
Definition at line 114 of file accelerate.h.
Referenced by accelerate_loop().
|
protected |
Definition at line 59 of file accelerate.h.
Referenced by accelerate_loop(), insert_automaton(), and set_dirty_vars().
|
protected |
Definition at line 117 of file accelerate.h.
Referenced by accelerate_loop(), accelerate_loops(), acceleratet(), contains_nested_loops(), find_back_jump(), and make_overflow_loc().
|
protected |
Definition at line 116 of file accelerate.h.
Referenced by accelerate_loop(), add_dirty_checks(), is_underapproximate(), restrict_traces(), and set_dirty_vars().
|
protected |
Definition at line 123 of file accelerate.h.
Referenced by make_overflow_loc().
|
protected |
Definition at line 113 of file accelerate.h.
Referenced by accelerate_loop(), accelerate_loops(), acceleratet(), add_dirty_checks(), decl(), insert_automaton(), insert_looping_path(), make_overflow_loc(), and restrict_traces().
|
protected |
Definition at line 118 of file accelerate.h.
Referenced by accelerate_loop(), insert_accelerator(), and restrict_traces().
|
protected |
Definition at line 115 of file accelerate.h.
Referenced by accelerate_loop(), insert_automaton(), is_underapproximate(), make_overflow_loc(), make_symbol(), restrict_traces(), and set_dirty_vars().
|
protected |
Definition at line 127 of file accelerate.h.
|
protected |
Definition at line 119 of file accelerate.h.
Referenced by make_overflow_loc(), and set_dirty_vars().