#include <accelerate.h>

Collaboration diagram for acceleratet:

Public Member Functions
	acceleratet (goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3, guard_managert &guard_manager)

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, goto_programt::target_less_than >	overflow_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_path)

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)

Detailed Description

Definition at line 26 of file accelerate.h.

Member Typedef Documentation

◆ overflow_mapt

typedef std::map< goto_programt::targett, goto_programt::targetst, goto_programt::target_less_than> acceleratet::overflow_mapt

protected

Definition at line 124 of file accelerate.h.

Constructor & Destructor Documentation

◆ acceleratet()

acceleratet::acceleratet	(	goto_programt &	_program,
		goto_modelt &	_goto_model,
		message_handlert &	message_handler,
		bool	_use_z3,
		guard_managert &	guard_manager
	)

inline

Definition at line 29 of file accelerate.h.

Member Function Documentation

◆ accelerate_loop()

int acceleratet::accelerate_loop ( goto_programt::targett & loop_header )

Definition at line 84 of file accelerate.cpp.

◆ accelerate_loops()

int acceleratet::accelerate_loops ( )

Definition at line 606 of file accelerate.cpp.

◆ accelerate_path()

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

◆ add_dirty_checks()

void acceleratet::add_dirty_checks ( )

protected

Definition at line 348 of file accelerate.cpp.

◆ 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

Definition at line 509 of file accelerate.cpp.

◆ contains_nested_loops()

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

protected

Definition at line 58 of file accelerate.cpp.

◆ decl() [1/2]

void acceleratet::decl	(	symbol_exprt &	sym,
		goto_programt::targett	t
	)

protected

Definition at line 448 of file accelerate.cpp.

◆ decl() [2/2]

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

protected

Definition at line 459 of file accelerate.cpp.

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

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

protected

Definition at line 177 of file accelerate.cpp.

◆ insert_automaton()

void acceleratet::insert_automaton ( trace_automatont & automaton )

protected

Definition at line 467 of file accelerate.cpp.

◆ 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

Definition at line 203 of file accelerate.cpp.

◆ is_underapproximate()

bool acceleratet::is_underapproximate ( path_acceleratort & accelerator )

protected

Definition at line 410 of file accelerate.cpp.

◆ make_overflow_loc()

void acceleratet::make_overflow_loc	(	goto_programt::targett	loop_header,
		goto_programt::targett &	loop_end,
		goto_programt::targett &	overflow_loc
	)

protected

Definition at line 234 of file accelerate.cpp.

◆ make_symbol()

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

protected

Definition at line 436 of file accelerate.cpp.

◆ restrict_traces()

void acceleratet::restrict_traces ( )

Definition at line 277 of file accelerate.cpp.

◆ set_dirty_vars()

void acceleratet::set_dirty_vars ( path_acceleratort & accelerator )

protected

Definition at line 317 of file accelerate.cpp.

Member Data Documentation

◆ accelerate_limit

const int acceleratet::accelerate_limit = -1

static

Definition at line 54 of file accelerate.h.

◆ dirty_vars_map

expr_mapt acceleratet::dirty_vars_map

protected

Definition at line 127 of file accelerate.h.

◆ goto_functions

goto_functionst& acceleratet::goto_functions

protected

Definition at line 112 of file accelerate.h.

◆ guard_manager

guard_managert& acceleratet::guard_manager

protected

Definition at line 114 of file accelerate.h.

◆ message_handler

message_handlert& acceleratet::message_handler

protected

Definition at line 57 of file accelerate.h.

◆ natural_loops

natural_loops_mutablet acceleratet::natural_loops

protected

Definition at line 116 of file accelerate.h.

◆ ns

namespacet acceleratet::ns

protected

Definition at line 115 of file accelerate.h.

◆ overflow_locs

overflow_mapt acceleratet::overflow_locs

protected

Definition at line 125 of file accelerate.h.

◆ program

goto_programt& acceleratet::program

protected

Definition at line 111 of file accelerate.h.

◆ subsumed

subsumed_pathst acceleratet::subsumed

protected

Definition at line 117 of file accelerate.h.

◆ symbol_table

symbol_tablet& acceleratet::symbol_table

protected

Definition at line 113 of file accelerate.h.

◆ use_z3

bool acceleratet::use_z3

protected

Definition at line 129 of file accelerate.h.

◆ utils

acceleration_utilst acceleratet::utils

protected

Definition at line 118 of file accelerate.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/accelerate/accelerate.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/accelerate/accelerate.cpp

Protected Attributes
message_handlert &	message_handler

goto_programt &	program

goto_functionst &	goto_functions

symbol_tablet &	symbol_table

guard_managert &	guard_manager

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

Public Member Functions

Static Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ overflow_mapt

Constructor & Destructor Documentation

◆ acceleratet()

Member Function Documentation

◆ accelerate_loop()

◆ accelerate_loops()

◆ accelerate_path()

◆ add_dirty_checks()

◆ build_state_machine()

◆ contains_nested_loops()

◆ decl() [1/2]

◆ decl() [2/2]

◆ extend_path()

◆ find_back_jump()

◆ find_paths()

◆ insert_accelerator()

◆ insert_automaton()

◆ insert_looping_path()

◆ is_underapproximate()

◆ make_overflow_loc()

◆ make_symbol()

◆ restrict_traces()

◆ set_dirty_vars()

Member Data Documentation

◆ accelerate_limit

◆ dirty_vars_map

◆ goto_functions

◆ guard_manager

◆ message_handler

◆ natural_loops

◆ ns

◆ overflow_locs

◆ program

◆ subsumed

◆ symbol_table

◆ use_z3

◆ utils