cprover
complexity_limiter.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: John Dumbell
6 
7 \*******************************************************************/
8 
9 #include "complexity_limiter.h"
10 #include "goto_symex_state.h"
11 #include <cmath>
12 
14  message_handlert &message_handler,
15  const optionst &options)
16  : log(message_handler)
17 {
18  std::size_t limit = options.get_signed_int_option("symex-complexity-limit");
19  if((complexity_active = limit > 0))
20  {
21  // This gives a curve that allows low limits to be rightly restrictive,
22  // while larger numbers are very large.
23  max_complexity = static_cast<std::size_t>((limit * limit) * 25);
24 
25  const std::size_t failed_child_loops_limit = options.get_signed_int_option(
26  "symex-complexity-failed-child-loops-limit");
27  const std::size_t unwind = options.get_signed_int_option("unwind");
28 
29  // If we have complexity enabled, try to work out a failed_children_limit.
30  // In order of priority:
31  // * explicit limit
32  // * inferred limit from unwind
33  // * best limit we can apply with very little information.
34  if(failed_child_loops_limit > 0)
35  max_loops_complexity = failed_child_loops_limit;
36  else if(unwind > 0)
37  max_loops_complexity = std::max(static_cast<int>(floor(unwind / 3)), 1);
38  else
39  max_loops_complexity = limit;
40  }
41 }
42 
45 {
46  for(auto frame_iter = current_call_stack.rbegin();
47  frame_iter != current_call_stack.rend();
48  ++frame_iter)
49  {
50  // As we're walking bottom-up, the first frame we find with active loops
51  // is our closest active one.
52  if(!frame_iter->active_loops.empty())
53  {
54  return &frame_iter->active_loops.back();
55  }
56  }
57 
58  return {};
59 }
60 
62  const call_stackt &current_call_stack,
63  const goto_programt::const_targett &instr)
64 {
65  for(auto frame_iter = current_call_stack.rbegin();
66  frame_iter != current_call_stack.rend();
67  ++frame_iter)
68  {
69  for(auto &loop_iter : frame_iter->active_loops)
70  {
71  for(auto &blacklisted_loop : loop_iter.blacklisted_loops)
72  {
73  if(blacklisted_loop.get().contains(instr))
74  {
75  return true;
76  }
77  }
78  }
79  }
80 
81  return false;
82 }
83 
85  call_stackt &current_call_stack)
86 {
87  std::size_t sum_complexity = 0;
88 
89  // This will walk all currently active loops, from inner-most to outer-most,
90  // and sum the times their branches have failed.
91  //
92  // If we find that this sum is higher than our max_loops_complexity we take
93  // note of the loop that happens in and then cause every parent still
94  // executing that loop to blacklist it.
95  //
96  // This acts as a context-sensitive loop cancel, so if we've got unwind 20
97  // and find out at the 3rd iteration a particular nested loop is too
98  // complicated, we make sure we don't execute it the other 17 times. But as
99  // soon as we're running the loop again via a different context it gets a
100  // chance to redeem itself.
101  lexical_loopst::loopt *loop_to_blacklist = nullptr;
102  for(auto frame_iter = current_call_stack.rbegin();
103  frame_iter != current_call_stack.rend();
104  ++frame_iter)
105  {
106  for(auto it = frame_iter->active_loops.rbegin();
107  it != frame_iter->active_loops.rend();
108  it++)
109  {
110  auto &loop_info = *it;
111 
112  // Because we're walking in reverse this will only be non-empty for
113  // parents of the loop that's been blacklisted. We then add that to their
114  // internal lists of blacklisted children.
115  if(loop_to_blacklist)
116  {
117  loop_info.blacklisted_loops.emplace_back(*loop_to_blacklist);
118  }
119  else
120  {
121  sum_complexity += loop_info.children_too_complex;
122  if(sum_complexity > max_loops_complexity)
123  {
124  loop_to_blacklist = &loop_info.loop;
125  }
126  }
127  }
128  }
129 
130  return !loop_to_blacklist;
131 }
132 
135 {
136  if(!complexity_limits_active() || !state.reachable)
138 
139  std::size_t complexity = state.complexity();
140  if(complexity == 0)
142 
143  auto &current_call_stack = state.call_stack();
144 
145  // Check if this branch is too complicated to continue.
146  auto active_loop = get_current_active_loop(current_call_stack);
147  if(complexity >= max_complexity)
148  {
149  // If we're too complex, add a counter to the current loop we're in and
150  // check if we've violated child-loop complexity limits.
151  if(active_loop != nullptr)
152  {
153  active_loop->children_too_complex++;
154 
155  // If we're considered too complex, cancel branch.
156  if(are_loop_children_too_complicated(current_call_stack))
157  {
158  log.warning()
159  << "[symex-complexity] Loop operations considered too complex"
160  << (state.source.pc->source_location.is_not_nil()
161  ? " at: " + state.source.pc->source_location.as_string()
162  : ", location number: " +
163  std::to_string(state.source.pc->location_number) + ".")
164  << messaget::eom;
165 
167  }
168  }
169 
170  log.warning() << "[symex-complexity] Branch considered too complex"
171  << (state.source.pc->source_location.is_not_nil()
172  ? " at: " + state.source.pc->source_location.as_string()
173  : ", location number: " +
174  std::to_string(state.source.pc->location_number) +
175  ".")
176  << messaget::eom;
177 
178  // Then kill this branch.
180  }
181 
182  // If we're not in any loop, return with no violation.
183  if(!active_loop)
185 
186  // Check if we've entered a loop that has been previously black-listed, and
187  // if so then cancel before we go any further.
188  if(in_blacklisted_loop(current_call_stack, state.source.pc))
189  {
190  log.warning() << "[symex-complexity] Trying to enter blacklisted loop"
191  << (state.source.pc->source_location.is_not_nil()
192  ? " at: " + state.source.pc->source_location.as_string()
193  : ", location number: " +
194  std::to_string(state.source.pc->location_number) +
195  ".")
196  << messaget::eom;
197 
199  }
200 
202 }
203 
205  complexity_violationt complexity_violation,
206  goto_symex_statet &current_state)
207 {
208  if(violation_transformations.empty())
209  default_transformation.transform(complexity_violation, current_state);
210  else
211  for(auto transform_lambda : violation_transformations)
212  transform_lambda.transform(complexity_violation, current_state);
213 }
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
std::size_t complexity()
Get the complexity for this state.
Definition: goto_state.h:76
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:58
Central data structure: state.
call_stackt & call_stack()
symex_targett::sourcet source
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
signed int get_signed_int_option(const std::string &option) const
Definition: options.cpp:50
virtual void transform(const complexity_violationt heuristic_result, goto_symex_statet &current_state)
Symbolic Execution.
complexity_violationt
What sort of symex-complexity violation has taken place.
Symbolic Execution.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
goto_programt::const_targett pc
Definition: symex_target.h:43