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::NONE
@ NONE
goto_statet::complexity
std::size_t complexity()
Get the complexity for this state.
Definition: goto_state.h:72
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
goto_statet::reachable
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:54
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
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
complexity_violationt
complexity_violationt
What sort of symex-complexity violation has taken place.
Definition: complexity_violation.h:18
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:64
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
call_stackt
Definition: call_stack.h:15
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:147
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
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
optionst::get_signed_int_option
signed int get_signed_int_option(const std::string &option) const
Definition: options.cpp:50
message_handlert
Definition: message.h:28
symex_complexity_limit_exceeded_actiont::transform
virtual void transform(const complexity_violationt heuristic_result, goto_symex_statet &current_state)
Definition: symex_complexity_limit_exceeded_action.h:15
complexity_violationt::LOOP
@ LOOP
complexity_violationt::BRANCH
@ BRANCH
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
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_limiter.h
Symbolic Execution.
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_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::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
messaget::warning
mstreamt & warning() const
Definition: message.h:404