cprover
|
#include <accelerate.h>
Public Member Functions | |
acceleratet (goto_programt &_program, goto_functionst &_goto_functions, symbol_tablet &_symbol_table, 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 29 of file accelerate.h.
|
protected |
Definition at line 111 of file accelerate.h.
|
inline |
Definition at line 32 of file accelerate.h.
References accelerate_loop(), accelerate_loops(), accelerate_path(), natural_loops, program, and restrict_traces().
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_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, is_underapproximate(), natural_loops_templatet< P, T >::loop_map, make_overflow_loc(), natural_loops, ns, output_path(), path_acceleratort::path, program, path_acceleratort::pure_accelerator, SKIP, subsumed, symbol_table, and goto_program_templatet< codeT, guardT >::update().
Referenced by accelerate_loops(), and acceleratet().
int acceleratet::accelerate_loops | ( | ) |
Definition at line 622 of file accelerate.cpp.
References accelerate_loop(), natural_loops_templatet< P, T >::loop_map, natural_loops, program, restrict_traces(), and goto_program_templatet< codeT, guardT >::update().
Referenced by accelerate_functions(), and acceleratet().
bool acceleratet::accelerate_path | ( | patht & | path, |
path_acceleratort & | accelerator | ||
) |
Referenced by acceleratet().
|
protected |
Definition at line 356 of file accelerate.cpp.
References ASSIGN, ASSUME, dirty_vars_map, find_symbols(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, namespacet::lookup(), ns, exprt::op0(), and program.
|
protected |
Definition at line 525 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 462 of file accelerate.cpp.
References goto_program_templatet< codeT, guardT >::insert_before(), and program.
Referenced by decl(), and insert_automaton().
|
protected |
Definition at line 473 of file accelerate.cpp.
References decl(), goto_program_templatet< codeT, guardT >::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 subsumed_patht::accelerator, insert_looping_path(), goto_program_templatet< codeT, guardT >::instructions, path_acceleratort::overflow_path, path_acceleratort::pure_accelerator, and subsumed_patht::residue.
Referenced by accelerate_loop().
|
protected |
Definition at line 484 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_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, make_symbol(), 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_program_templatet< codeT, guardT >::destructive_insert(), goto_program_templatet< codeT, guardT >::insert_before(), and program.
Referenced by insert_accelerator().
|
protected |
Definition at line 422 of file accelerate.cpp.
References path_acceleratort::dirty_vars, expr2c(), symbol_exprt::get_identifier(), symbol_tablet::lookup(), symbolt::module, ns, symbol_table, and to_symbol_expr().
Referenced by accelerate_loop().
|
protected |
Definition at line 236 of file accelerate.cpp.
References overflow_instrumentert::add_overflow_checks(), acceleration_utilst::fresh_symbol(), GOTO, goto_program_templatet< codeT, guardT >::insert_after(), natural_loops_templatet< P, T >::loop_map, natural_loops, overflow_locs, program, SKIP, symbolt::symbol_expr(), symbol_table, and utils.
Referenced by accelerate_loop().
Definition at line 448 of file accelerate.cpp.
References symbol_tablet::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 285 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(), and acceleratet().
|
protected |
Definition at line 325 of file accelerate.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSIGN, path_acceleratort::dirty_vars, dirty_vars_map, expr2c(), acceleration_utilst::fresh_symbol(), ns, path_acceleratort::pure_accelerator, symbolt::symbol_expr(), symbol_table, and utils.
|
static |
Definition at line 53 of file accelerate.h.
Referenced by accelerate_loop().
|
protected |
Definition at line 114 of file accelerate.h.
Referenced by add_dirty_checks(), and set_dirty_vars().
|
protected |
Definition at line 103 of file accelerate.h.
Referenced by accelerate_loop().
|
protected |
Definition at line 106 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 105 of file accelerate.h.
Referenced by accelerate_loop(), add_dirty_checks(), is_underapproximate(), restrict_traces(), and set_dirty_vars().
|
protected |
Definition at line 112 of file accelerate.h.
Referenced by make_overflow_loc().
|
protected |
Definition at line 102 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 107 of file accelerate.h.
Referenced by accelerate_loop(), and restrict_traces().
|
protected |
Definition at line 104 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 116 of file accelerate.h.
|
protected |
Definition at line 108 of file accelerate.h.
Referenced by make_overflow_loc(), and set_dirty_vars().