#include <acceleration_utils.h>

Collaboration diagram for acceleration_utilst:

Classes
struct	polynomial_array_assignmentt

Public Types
typedef std::pair< exprt, exprt >	expr_pairt

typedef std::vector< expr_pairt >	expr_pairst

typedef std::vector< polynomial_array_assignmentt >	polynomial_array_assignmentst

Public Member Functions
	acceleration_utilst (symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter)

	acceleration_utilst (symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions)

void	extract_polynomial (scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)

bool	check_inductive (std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)

void	stash_variables (scratch_programt &program, expr_sett modified, substitutiont &substitution)

void	stash_polynomials (scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)

exprt	precondition (patht &path)

void	abstract_arrays (exprt &expr, expr_mapt &abstractions)

void	push_nondet (exprt &expr)

bool	do_assumptions (std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)

bool	do_arrays (goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)

expr_pairst	gather_array_assignments (goto_programt::instructionst &loop_body, expr_sett &arrays_written)

bool	array_assignments2polys (expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)

bool	expr2poly (exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)

bool	do_nonrecursive (goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)

bool	assign_array (const index_exprt &lhs, const exprt &rhs, scratch_programt &program)

void	gather_array_accesses (const exprt &expr, expr_sett &arrays)

void	gather_rvalues (const exprt &expr, expr_sett &rvalues)

void	ensure_no_overflows (scratch_programt &program)

void	find_modified (const patht &path, expr_sett &modified)

void	find_modified (const goto_programt &program, expr_sett &modified)

void	find_modified (const goto_programt::instructionst &instructions, expr_sett &modified)

void	find_modified (const natural_loops_mutablet::natural_loopt &loop, expr_sett &modified)

void	find_modified (goto_programt::const_targett t, expr_sett &modified)

symbolt	fresh_symbol (std::string base, typet type)

Public Attributes
symbol_table_baset &	symbol_table

namespacet	ns

const goto_functionst &	goto_functions

exprt &	loop_counter

nil_exprt	nil

Protected Attributes
message_handlert &	message_handler

Detailed Description

Definition at line 34 of file acceleration_utils.h.

Member Typedef Documentation

◆ expr_pairst

typedef std::vector<expr_pairt> acceleration_utilst::expr_pairst

Definition at line 93 of file acceleration_utils.h.

◆ expr_pairt

typedef std::pair<exprt, exprt> acceleration_utilst::expr_pairt

Definition at line 92 of file acceleration_utils.h.

◆ polynomial_array_assignmentst

typedef std::vector<polynomial_array_assignmentt> acceleration_utilst::polynomial_array_assignmentst

Definition at line 103 of file acceleration_utils.h.

Constructor & Destructor Documentation

◆ acceleration_utilst() [1/2]

acceleration_utilst::acceleration_utilst	(	symbol_table_baset &	_symbol_table,
		message_handlert &	message_handler,
		const goto_functionst &	_goto_functions,
		exprt &	_loop_counter
	)

inline

Definition at line 40 of file acceleration_utils.h.

◆ acceleration_utilst() [2/2]

acceleration_utilst::acceleration_utilst	(	symbol_table_baset &	_symbol_table,
		message_handlert &	message_handler,
		const goto_functionst &	_goto_functions
	)

inline

Definition at line 53 of file acceleration_utils.h.

Member Function Documentation

◆ abstract_arrays()

void acceleration_utilst::abstract_arrays	(	exprt &	expr,
		expr_mapt &	abstractions
	)

Definition at line 275 of file acceleration_utils.cpp.

◆ array_assignments2polys()

bool acceleration_utilst::array_assignments2polys	(	expr_pairst &	array_assignments,
		std::map< exprt, polynomialt > &	polynomials,
		polynomial_array_assignmentst &	array_polynomials,
		polynomialst &	nondet_indices
	)

Definition at line 764 of file acceleration_utils.cpp.

◆ assign_array()

bool acceleration_utilst::assign_array	(	const index_exprt &	lhs,
		const exprt &	rhs,
		scratch_programt &	program
	)

Definition at line 990 of file acceleration_utils.cpp.

◆ check_inductive()

bool acceleration_utilst::check_inductive	(	std::map< exprt, polynomialt >	polynomials,
		patht &	path,
		guard_managert &	guard_manager
	)

Definition at line 98 of file acceleration_utils.cpp.

◆ do_arrays()

bool acceleration_utilst::do_arrays	(	goto_programt::instructionst &	loop_body,
		std::map< exprt, polynomialt > &	polynomials,
		substitutiont &	substitution,
		scratch_programt &	program
	)

Definition at line 529 of file acceleration_utils.cpp.

◆ do_assumptions()

bool acceleration_utilst::do_assumptions	(	std::map< exprt, polynomialt >	polynomials,
		patht &	body,
		exprt &	guard,
		guard_managert &	guard_manager
	)

Definition at line 329 of file acceleration_utils.cpp.

◆ do_nonrecursive()

bool acceleration_utilst::do_nonrecursive	(	goto_programt::instructionst &	loop_body,
		std::map< exprt, polynomialt > &	polynomials,
		substitutiont &	substitution,
		expr_sett &	nonrecursive,
		scratch_programt &	program
	)

Definition at line 853 of file acceleration_utils.cpp.

◆ ensure_no_overflows()

void acceleration_utilst::ensure_no_overflows ( scratch_programt & program )

Definition at line 452 of file acceleration_utils.cpp.

◆ expr2poly()

bool acceleration_utilst::expr2poly	(	exprt &	expr,
		std::map< exprt, polynomialt > &	polynomials,
		polynomialt &	poly
	)

Definition at line 823 of file acceleration_utils.cpp.

◆ extract_polynomial()

void acceleration_utilst::extract_polynomial	(	scratch_programt &	program,
		std::set< std::pair< expr_listt, exprt >> &	coefficients,
		polynomialt &	polynomial
	)

Definition at line 1197 of file acceleration_utils.cpp.

◆ find_modified() [1/5]

void acceleration_utilst::find_modified	(	const goto_programt &	program,
		expr_sett &	modified
	)

Definition at line 55 of file acceleration_utils.cpp.

◆ find_modified() [2/5]

void acceleration_utilst::find_modified	(	const goto_programt::instructionst &	instructions,
		expr_sett &	modified
	)

Definition at line 63 of file acceleration_utils.cpp.

◆ find_modified() [3/5]

void acceleration_utilst::find_modified	(	const natural_loops_mutablet::natural_loopt &	loop,
		expr_sett &	modified
	)

Definition at line 82 of file acceleration_utils.cpp.

◆ find_modified() [4/5]

void acceleration_utilst::find_modified	(	const patht &	path,
		expr_sett &	modified
	)

Definition at line 74 of file acceleration_utils.cpp.

◆ find_modified() [5/5]

void acceleration_utilst::find_modified	(	goto_programt::const_targett	t,
		expr_sett &	modified
	)

Definition at line 90 of file acceleration_utils.cpp.

◆ fresh_symbol()

symbolt acceleration_utilst::fresh_symbol	(	std::string	base,
		typet	type
	)

Definition at line 1246 of file acceleration_utils.cpp.

◆ gather_array_accesses()

void acceleration_utilst::gather_array_accesses	(	const exprt &	expr,
		expr_sett &	arrays
	)

Definition at line 1178 of file acceleration_utils.cpp.

◆ gather_array_assignments()

acceleration_utilst::expr_pairst acceleration_utilst::gather_array_assignments	(	goto_programt::instructionst &	loop_body,
		expr_sett &	arrays_written
	)

Definition at line 486 of file acceleration_utils.cpp.

◆ gather_rvalues()

void acceleration_utilst::gather_rvalues	(	const exprt &	expr,
		expr_sett &	rvalues
	)

Definition at line 35 of file acceleration_utils.cpp.

◆ precondition()

exprt acceleration_utilst::precondition ( patht & path )

Definition at line 223 of file acceleration_utils.cpp.

◆ push_nondet()

void acceleration_utilst::push_nondet ( exprt & expr )

Definition at line 304 of file acceleration_utils.cpp.

◆ stash_polynomials()

void acceleration_utilst::stash_polynomials	(	scratch_programt &	program,
		std::map< exprt, polynomialt > &	polynomials,
		std::map< exprt, exprt > &	stashed,
		patht &	path
	)

Definition at line 175 of file acceleration_utils.cpp.

◆ stash_variables()

void acceleration_utilst::stash_variables	(	scratch_programt &	program,
		expr_sett	modified,
		substitutiont &	substitution
	)

Definition at line 194 of file acceleration_utils.cpp.

Member Data Documentation

◆ goto_functions

const goto_functionst& acceleration_utilst::goto_functions

Definition at line 157 of file acceleration_utils.h.

◆ loop_counter

exprt& acceleration_utilst::loop_counter

Definition at line 158 of file acceleration_utils.h.

◆ message_handler

message_handlert& acceleration_utilst::message_handler

protected

Definition at line 37 of file acceleration_utils.h.

◆ nil

nil_exprt acceleration_utilst::nil

Definition at line 159 of file acceleration_utils.h.

◆ ns

namespacet acceleration_utilst::ns

Definition at line 156 of file acceleration_utils.h.

◆ symbol_table

symbol_table_baset& acceleration_utilst::symbol_table

Definition at line 155 of file acceleration_utils.h.

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

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

Classes

Public Types

Public Member Functions

Public Attributes

Protected Attributes