cprover
complexity_limiter.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: 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 "complexity_violation.h"
16 #include "goto_symex_state.h"
18 
46 {
47 public:
48  complexity_limitert() = default;
49 
50  complexity_limitert(message_handlert &logger, const optionst &options);
51 
55  {
56  return this->complexity_active;
57  }
58 
64 
69  complexity_violationt complexity_violation,
70  goto_symex_statet &current_state);
71 
72 protected:
73  mutable messaget log;
74 
77  bool complexity_active = false;
78 
81  std::vector<symex_complexity_limit_exceeded_actiont>
83 
86 
90  std::size_t max_complexity = 0;
91 
94  std::size_t max_loops_complexity = 0;
95 
98  bool are_loop_children_too_complicated(call_stackt &current_call_stack);
99 
102  static bool in_blacklisted_loop(
103  const call_stackt &current_call_stack,
104  const goto_programt::const_targett &instr);
105 
110  get_current_active_loop(call_stackt &current_call_stack);
111 };
112 
113 #endif // CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
complexity_limitert::complexity_active
bool complexity_active
Is the complexity module active, usually coincides with a max_complexity value above 0.
Definition: complexity_limiter.h:77
optionst
Definition: options.h:23
framet::active_loop_infot
Definition: frame.h:51
complexity_limitert::complexity_limits_active
bool complexity_limits_active()
Is the complexity module active?
Definition: complexity_limiter.h:54
complexity_limitert::violation_transformations
std::vector< symex_complexity_limit_exceeded_actiont > violation_transformations
Functions called when the heuristic has been violated.
Definition: complexity_limiter.h:82
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
complexity_limitert::max_complexity
std::size_t max_complexity
The max complexity rating that a branch can be before it's abandoned.
Definition: complexity_limiter.h:90
symex_complexity_limit_exceeded_action.h
complexity_violationt
complexity_violationt
What sort of symex-complexity violation has taken place.
Definition: complexity_violation.h:18
call_stackt
Definition: call_stack.h:15
complexity_limitert::complexity_limitert
complexity_limitert()=default
complexity_limitert::run_transformations
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...
Definition: complexity_limiter.cpp:204
message_handlert
Definition: message.h:28
goto_symex_state.h
Symbolic Execution.
complexity_limitert::max_loops_complexity
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 ...
Definition: complexity_limiter.h:94
complexity_limitert::log
messaget log
Definition: complexity_limiter.h:73
symex_complexity_limit_exceeded_actiont
Default heuristic transformation that cancels branches when complexity has been breached.
Definition: symex_complexity_limit_exceeded_action.h:13
complexity_limitert::are_loop_children_too_complicated
bool are_loop_children_too_complicated(call_stackt &current_call_stack)
Checks whether the current loop execution stack has violated max_loops_complexity.
Definition: complexity_limiter.cpp:84
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
complexity_limitert::get_current_active_loop
static framet::active_loop_infot * get_current_active_loop(call_stackt &current_call_stack)
Returns inner-most currently active loop.
Definition: complexity_limiter.cpp:44
complexity_limitert::default_transformation
symex_complexity_limit_exceeded_actiont default_transformation
Default heuristic transformation. Sets state as unreachable.
Definition: complexity_limiter.h:85
complexity_violation.h
complexity_limitert::check_complexity
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...
Definition: complexity_limiter.cpp:134
complexity_limitert
Symex complexity module.
Definition: complexity_limiter.h:46
complexity_limitert::in_blacklisted_loop
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.
Definition: complexity_limiter.cpp:61