Symex complexity module. More...

#include <complexity_limiter.h>

Collaboration diagram for complexity_limitert:

Public Member Functions
	complexity_limitert (message_handlert &logger, const optionst &options)

bool	complexity_limits_active ()
	Is the complexity module active? More...

complexity_violationt	check_complexity (goto_symex_statet &state)
	Checks the passed-in state to see if its become too complex for us to deal with, and if so set its guard to false. More...

void	run_transformations (complexity_violationt complexity_violation, goto_symex_statet &current_state)
	Runs a suite of transformations on the state and symex executable, performing whatever transformations are required depending on the modules that have been loaded. More...

Static Public Member Functions
static std::size_t	bounded_expr_size (const exprt &expr, std::size_t limit)
	Amount of nodes in `expr` approximately bounded by limit. More...

Protected Member Functions
bool	are_loop_children_too_complicated (call_stackt &current_call_stack)
	Checks whether the current loop execution stack has violated max_loops_complexity. More...

Static Protected Member Functions
static bool	in_blacklisted_loop (const call_stackt &current_call_stack, const goto_programt::const_targett &instr)
	Checks whether we're in a loop that is currently considered blacklisted, and shouldn't be executed. More...

static framet::active_loop_infot *	get_current_active_loop (call_stackt &current_call_stack)
	Returns inner-most currently active loop. More...

Protected Attributes
messaget	log

bool	complexity_active = false
	Is the complexity module active, usually coincides with a max_complexity value above 0. More...

std::vector< symex_complexity_limit_exceeded_actiont >	violation_transformations
	Functions called when the heuristic has been violated. More...

symex_complexity_limit_exceeded_actiont	default_transformation
	Default heuristic transformation. Sets state as unreachable. More...

std::size_t	max_complexity = 0
	The max complexity rating that a branch can be before it's abandoned. More...

std::size_t	max_loops_complexity = 0
	The amount of branches that can fail within the scope of a loops execution before the entire loop is abandoned. More...

Detailed Description

Symex complexity module.

Dynamically sets branches as unreachable symex considers them too complex. A branch is too complex when runtime may be beyond reasonable bounds due to internal structures becoming too large or solving conditions becoming too big for the SAT solver to deal with.

On top of the branch cancelling there is special consideration for loops. As branches get cancelled it keeps track of what loops are currently active up through the stack. If a loop has too many of its child branches killed (including additional loops or recursion) it won't do any more unwinds of that particular loop and will blacklist it.

This blacklist is only held for as long as any loop is still active. As soon as the loop iteration ends and the context in which the code is being executed changes it'll be able to be run again.

Example of loop blacklisting:

loop A: (complexity: 5070)
    loop B: (complexity: 5000)
    loop C: (complexity: 70)

In the above loop B will be blacklisted if we have a complexity limitation < 5000, but loop A and C will still be run, because when loop B is removed the complexity of the loop as a whole is acceptable.

Definition at line 48 of file complexity_limiter.h.

Constructor & Destructor Documentation

◆ complexity_limitert()

complexity_limitert::complexity_limitert	(	message_handlert &	logger,
		const optionst &	options
	)

Definition at line 17 of file complexity_limiter.cpp.

Member Function Documentation

◆ are_loop_children_too_complicated()

bool complexity_limitert::are_loop_children_too_complicated ( call_stackt & current_call_stack )

protected

Checks whether the current loop execution stack has violated max_loops_complexity.

Definition at line 88 of file complexity_limiter.cpp.

◆ bounded_expr_size()

std::size_t complexity_limitert::bounded_expr_size	(	const exprt &	expr,
		std::size_t	limit
	)

static

Amount of nodes in expr approximately bounded by limit.

This is the size of the actual tree, ignoring memory/sub-tree sharing. Expressions that make substantial use of sharing may result in excessive run time.

Definition at line 243 of file complexity_limiter.cpp.

◆ check_complexity()

complexity_violationt complexity_limitert::check_complexity ( goto_symex_statet & state )

Checks the passed-in state to see if its become too complex for us to deal with, and if so set its guard to false.

Parameters

state goto_symex_statet you want to check the complexity of.

Returns: True/false depending on whether this branch should be abandoned.

Definition at line 138 of file complexity_limiter.cpp.

◆ complexity_limits_active()

bool complexity_limitert::complexity_limits_active ( )

inline

Is the complexity module active?

Returns: Whether complexity limits are active or not.

Definition at line 55 of file complexity_limiter.h.

◆ get_current_active_loop()

framet::active_loop_infot * complexity_limitert::get_current_active_loop ( call_stackt & current_call_stack )

staticprotected

Returns inner-most currently active loop.

This is frame-agnostic, so if we're in a loop further up the stack that will still be returned as the 'active' one.

Definition at line 48 of file complexity_limiter.cpp.

◆ in_blacklisted_loop()

bool complexity_limitert::in_blacklisted_loop	(	const call_stackt &	current_call_stack,
		const goto_programt::const_targett &	instr
	)

staticprotected

Checks whether we're in a loop that is currently considered blacklisted, and shouldn't be executed.

Definition at line 65 of file complexity_limiter.cpp.

◆ run_transformations()

void complexity_limitert::run_transformations	(	complexity_violationt	complexity_violation,
		goto_symex_statet &	current_state
	)

Runs a suite of transformations on the state and symex executable, performing whatever transformations are required depending on the modules that have been loaded.

Definition at line 211 of file complexity_limiter.cpp.

Member Data Documentation

◆ complexity_active

bool complexity_limitert::complexity_active = false

protected

Is the complexity module active, usually coincides with a max_complexity value above 0.

Definition at line 84 of file complexity_limiter.h.

◆ default_transformation

symex_complexity_limit_exceeded_actiont complexity_limitert::default_transformation

protected

Default heuristic transformation. Sets state as unreachable.

Definition at line 92 of file complexity_limiter.h.

◆ log

messaget complexity_limitert::log

mutableprotected

Definition at line 80 of file complexity_limiter.h.

◆ max_complexity

std::size_t complexity_limitert::max_complexity = 0

protected

The max complexity rating that a branch can be before it's abandoned.

The internal representation for computing complexity, has no relation to the argument passed in via options.

Definition at line 97 of file complexity_limiter.h.

◆ max_loops_complexity

std::size_t complexity_limitert::max_loops_complexity = 0

protected

The amount of branches that can fail within the scope of a loops execution before the entire loop is abandoned.

Definition at line 101 of file complexity_limiter.h.

◆ violation_transformations

std::vector<symex_complexity_limit_exceeded_actiont> complexity_limitert::violation_transformations

protected

Functions called when the heuristic has been violated.

Can perform any form of branch, state or full-program transformation.

Definition at line 89 of file complexity_limiter.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/complexity_limiter.h
/home/runner/work/cbmc/cbmc/src/goto-symex/complexity_limiter.cpp

Public Member Functions

Static Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ complexity_limitert()

Member Function Documentation

◆ are_loop_children_too_complicated()

◆ bounded_expr_size()

◆ check_complexity()

◆ complexity_limits_active()

◆ get_current_active_loop()

◆ in_blacklisted_loop()

◆ run_transformations()

Member Data Documentation

◆ complexity_active

◆ default_transformation

◆ log

◆ max_complexity

◆ max_loops_complexity

◆ violation_transformations