cprover
acceleratet Class Reference

#include <accelerate.h>

Collaboration diagram for acceleratet:
[legend]

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

message_handlertmessage_handler
 
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 30 of file accelerate.h.

Member Typedef Documentation

◆ overflow_mapt

Definition at line 122 of file accelerate.h.

Constructor & Destructor Documentation

◆ acceleratet()

acceleratet::acceleratet ( goto_programt _program,
goto_modelt _goto_model,
message_handlert message_handler,
bool  _use_z3 
)
inline

Definition at line 33 of file accelerate.h.

References natural_loops, and program.

Member Function Documentation

◆ accelerate_loop()

◆ accelerate_loops()

int acceleratet::accelerate_loops ( )

◆ accelerate_path()

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

◆ 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 460 of file accelerate.cpp.

References goto_programt::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

Definition at line 471 of file accelerate.cpp.

References decl(), goto_programt::insert_before(), and program.

◆ 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()

void acceleratet::insert_accelerator ( goto_programt::targett loop_header,
goto_programt::targett back_jump,
path_acceleratort accelerator,
subsumed_patht subsumed 
)
protected

◆ 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 56 of file accelerate.h.

Referenced by accelerate_loop().

◆ dirty_vars_map

expr_mapt acceleratet::dirty_vars_map
protected

Definition at line 125 of file accelerate.h.

Referenced by add_dirty_checks(), and set_dirty_vars().

◆ goto_functions

goto_functionst& acceleratet::goto_functions
protected

Definition at line 114 of file accelerate.h.

Referenced by accelerate_loop().

◆ message_handler

message_handlert& acceleratet::message_handler
protected

Definition at line 59 of file accelerate.h.

Referenced by accelerate_loop(), insert_automaton(), and set_dirty_vars().

◆ 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 123 of file accelerate.h.

Referenced by make_overflow_loc().

◆ program

◆ subsumed

subsumed_pathst acceleratet::subsumed
protected

Definition at line 118 of file accelerate.h.

Referenced by accelerate_loop(), insert_accelerator(), and restrict_traces().

◆ symbol_table

symbol_tablet& acceleratet::symbol_table
protected

◆ use_z3

bool acceleratet::use_z3
protected

Definition at line 127 of file accelerate.h.

◆ utils

acceleration_utilst acceleratet::utils
protected

Definition at line 119 of file accelerate.h.

Referenced by make_overflow_loc(), and set_dirty_vars().


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