cprover
acceleratet Class Reference

#include <accelerate.h>

Collaboration diagram for acceleratet:
[legend]

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::targetstoverflow_mapt
 

Protected Member Functions

void find_paths (goto_programt::targett &loop_header, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
 
void extend_path (goto_programt::targett &t, goto_programt::targett &loop_header, natural_loops_mutablet::natural_loopt &loop, patht &prefix, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
 
goto_programt::targett find_back_jump (goto_programt::targett loop_header)
 
void insert_looping_path (goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
 
void insert_accelerator (goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed)
 
void set_dirty_vars (path_acceleratort &accelerator)
 
void add_dirty_checks ()
 
bool is_underapproximate (path_acceleratort &accelerator)
 
void make_overflow_loc (goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
 
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)
 
symbolt make_symbol (std::string name, typet type)
 
void decl (symbol_exprt &sym, goto_programt::targett t)
 
void decl (symbol_exprt &sym, goto_programt::targett t, exprt init)
 
bool contains_nested_loops (goto_programt::targett &loop_header)
 

Protected Attributes

goto_programtprogram
 
goto_functionstgoto_functions
 
symbol_tabletsymbol_table
 
namespacet ns
 
natural_loops_mutablet natural_loops
 
subsumed_pathst subsumed
 
acceleration_utilst utils
 
overflow_mapt overflow_locs
 
expr_mapt dirty_vars_map
 
bool use_z3
 

Detailed Description

Definition at line 29 of file accelerate.h.

Member Typedef Documentation

§ overflow_mapt

Definition at line 111 of file accelerate.h.

Constructor & Destructor Documentation

§ acceleratet()

acceleratet::acceleratet ( goto_programt _program,
goto_functionst _goto_functions,
symbol_tablet _symbol_table,
bool  _use_z3 
)
inline

Member Function Documentation

§ accelerate_loop()

§ accelerate_loops()

§ accelerate_path()

bool acceleratet::accelerate_path ( patht path,
path_acceleratort accelerator 
)

Referenced by acceleratet().

§ add_dirty_checks()

§ build_state_machine()

void acceleratet::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 
)
protected

§ contains_nested_loops()

bool acceleratet::contains_nested_loops ( goto_programt::targett loop_header)
protected

Definition at line 59 of file accelerate.cpp.

References natural_loops_templatet< P, T >::loop_map, and natural_loops.

Referenced by accelerate_loop().

§ decl() [1/2]

void acceleratet::decl ( symbol_exprt sym,
goto_programt::targett  t 
)
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().

§ decl() [2/2]

void acceleratet::decl ( symbol_exprt sym,
goto_programt::targett  t,
exprt  init 
)
protected

§ extend_path()

void acceleratet::extend_path ( goto_programt::targett t,
goto_programt::targett loop_header,
natural_loops_mutablet::natural_loopt loop,
patht prefix,
pathst loop_paths,
pathst exit_paths,
goto_programt::targett back_jump 
)
protected

§ find_back_jump()

goto_programt::targett acceleratet::find_back_jump ( goto_programt::targett  loop_header)
protected

Definition at line 34 of file accelerate.cpp.

References natural_loops_templatet< P, T >::loop_map, and natural_loops.

Referenced by accelerate_loop().

§ find_paths()

void acceleratet::find_paths ( goto_programt::targett loop_header,
pathst loop_paths,
pathst exit_paths,
goto_programt::targett back_jump 
)
protected

§ insert_accelerator()

§ insert_automaton()

§ insert_looping_path()

void acceleratet::insert_looping_path ( goto_programt::targett loop_header,
goto_programt::targett back_jump,
goto_programt looping_path,
patht inserted_path 
)
protected

§ is_underapproximate()

bool acceleratet::is_underapproximate ( path_acceleratort accelerator)
protected

§ make_overflow_loc()

§ make_symbol()

symbolt acceleratet::make_symbol ( std::string  name,
typet  type 
)
protected

§ restrict_traces()

void acceleratet::restrict_traces ( )

§ set_dirty_vars()

Member Data Documentation

§ accelerate_limit

const int acceleratet::accelerate_limit = -1
static

Definition at line 53 of file accelerate.h.

Referenced by accelerate_loop().

§ dirty_vars_map

expr_mapt acceleratet::dirty_vars_map
protected

Definition at line 114 of file accelerate.h.

Referenced by add_dirty_checks(), and set_dirty_vars().

§ goto_functions

goto_functionst& acceleratet::goto_functions
protected

Definition at line 103 of file accelerate.h.

Referenced by accelerate_loop().

§ natural_loops

natural_loops_mutablet acceleratet::natural_loops
protected

§ ns

namespacet acceleratet::ns
protected

§ overflow_locs

overflow_mapt acceleratet::overflow_locs
protected

Definition at line 112 of file accelerate.h.

Referenced by make_overflow_loc().

§ program

§ subsumed

subsumed_pathst acceleratet::subsumed
protected

Definition at line 107 of file accelerate.h.

Referenced by accelerate_loop(), and restrict_traces().

§ symbol_table

symbol_tablet& acceleratet::symbol_table
protected

§ use_z3

bool acceleratet::use_z3
protected

Definition at line 116 of file accelerate.h.

§ utils

acceleration_utilst acceleratet::utils
protected

Definition at line 108 of file accelerate.h.

Referenced by make_overflow_loc(), and set_dirty_vars().


The documentation for this class was generated from the following files: