cprover
Loading...
Searching...
No Matches
complexity_limiter.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: John Dumbell
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
13#define CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
14
15#include <util/message.h>
16
19
20class optionst;
21
49{
50public:
52
54
58 {
59 return this->complexity_active;
60 }
61
67
74
79 static std::size_t bounded_expr_size(const exprt &expr, std::size_t limit);
80
81protected:
82 mutable messaget log;
83
86 bool complexity_active = false;
87
90 std::vector<symex_complexity_limit_exceeded_actiont>
92
95
99 std::size_t max_complexity = 0;
100
103 std::size_t max_loops_complexity = 0;
104
108
111 static bool in_blacklisted_loop(
114
120};
121
122#endif // CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Symex complexity module.
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 gu...
bool complexity_limits_active()
Is the complexity module active?
static std::size_t bounded_expr_size(const exprt &expr, std::size_t limit)
Amount of nodes in expr approximately bounded by limit.
bool complexity_active
Is the complexity module active, usually coincides with a max_complexity value above 0.
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.
std::size_t max_complexity
The max complexity rating that a branch can be before it's abandoned.
std::vector< symex_complexity_limit_exceeded_actiont > violation_transformations
Functions called when the heuristic has been violated.
std::size_t max_loops_complexity
The amount of branches that can fail within the scope of a loops execution before the entire loop is ...
static framet::active_loop_infot * get_current_active_loop(call_stackt &current_call_stack)
Returns inner-most currently active loop.
complexity_limitert()=default
symex_complexity_limit_exceeded_actiont default_transformation
Default heuristic transformation. Sets state as unreachable.
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 transformation...
bool are_loop_children_too_complicated(call_stackt &current_call_stack)
Checks whether the current loop execution stack has violated max_loops_complexity.
Base class for all expressions.
Definition expr.h:56
instructionst::const_iterator const_targett
Central data structure: state.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
Default heuristic transformation that cancels branches when complexity has been breached.
complexity_violationt
What sort of symex-complexity violation has taken place.