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
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?
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.
instructionst::const_iterator const_targett
Definition: goto_program.h:551
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.
Symbolic Execution.