bounded_loop_unroller Class Reference

This goes through every loop of the program and tries to check if it is a bounded loop, if it is, it will be unrolled all times needed. More...

#include <loop_unroll.h>

Inheritance diagram for bounded_loop_unroller:

Public Member Functions
	bounded_loop_unroller (size_t unroll_limit=1000)
	Note: the default value for unroll_limit is based on testing.
unsigned	get_number_of_bounded_loops ()
	Get the number of bounded loops that were detected after the algorithm has run.
Public Member Functions inherited from unsound_loop_unroller
	unsound_loop_unroller ()
Public Member Functions inherited from goto_functions_algorithm
	goto_functions_algorithm (bool sideffect)
unsigned	get_number_of_functions ()
unsigned	get_number_of_loops ()
bool	run (goto_functionst &) override
	Executes the algorithm over a T object.
void	setTarget (const std::string &_tgt)
Public Member Functions inherited from algorithm< goto_functionst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Member Functions
int	get_loop_bounds (loopst &loop) override
	Get the number of iteractions to unroll the loop.
Protected Member Functions inherited from unsound_loop_unroller
bool	runOnLoop (loopst &loop, goto_programt &goto_program) override
Protected Member Functions inherited from goto_functions_algorithm
virtual bool	runOnFunction (std::pair< const irep_idt, goto_functiont > &F)
virtual bool	runOnProgram (goto_functionst &)

Protected Attributes
const size_t	unroll_limit
Protected Attributes inherited from goto_functions_algorithm
std::string	target_function = ""
Protected Attributes inherited from algorithm< goto_functionst >
const bool	sideeffect

Detailed Description

This goes through every loop of the program and tries to check if it is a bounded loop, if it is, it will be unrolled all times needed.

The intention is to simplify structures such as:

SYMBOL = K0 1: IF !(SYMBOL < K) THEN GOTO 2 P SYMBOL = SYMBOL + 1 GOTO 1 2: Q

If K > K0 and P does not contain assignments over SYMBOL, then this is converted into:

P SYMBOL = SYMBOL + 1 ... // K - K0 times P SYMBOL = SYMBOL + 1 Q

Constructor & Destructor Documentation

bounded_loop_unroller()

bounded_loop_unroller::bounded_loop_unroller ( size_t unroll_limit = 1000 )

inlineexplicit

Note: the default value for unroll_limit is based on testing.

Member Function Documentation

get_loop_bounds()

int bounded_loop_unroller::get_loop_bounds ( loopst & loop )

overrideprotectedvirtual

Get the number of iteractions to unroll the loop.

Parameters

loop

Returns

int negative means error, positive is the quantity to unroll

This looks for the following template

z: symbol = k0

a: IF !(symbol < k) GOTO [...] b: ... // code that only reads symbol b: symbol++

If this is matched properly then set bound as k - k0 and return true

Implements unsound_loop_unroller.

get_number_of_bounded_loops()

unsigned bounded_loop_unroller::get_number_of_bounded_loops ( )

inline

Get the number of bounded loops that were detected after the algorithm has run.

Returns

number of bounded loops

Member Data Documentation

unroll_limit

const size_t bounded_loop_unroller::unroll_limit

protected

---

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

• src/goto-programs/loop_unroll.h
• src/goto-programs/loop_unroll.cpp