cprover
Loading...
Searching...
No Matches
complexity_limiter.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: John Dumbell
6
7\*******************************************************************/
8
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
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,
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 =
141 if(complexity == 1)
143
144 auto &current_call_stack = state.call_stack();
145
146 // Check if this branch is too complicated to continue.
147 auto active_loop = get_current_active_loop(current_call_stack);
148 if(complexity >= max_complexity)
149 {
150 // If we're too complex, add a counter to the current loop we're in and
151 // check if we've violated child-loop complexity limits.
152 if(active_loop != nullptr)
153 {
154 active_loop->children_too_complex++;
155
156 // If we're considered too complex, cancel branch.
157 if(are_loop_children_too_complicated(current_call_stack))
158 {
159 log.warning()
160 << "[symex-complexity] Loop operations considered too complex"
161 << (state.source.pc->source_location().is_not_nil()
162 ? " at: " + state.source.pc->source_location().as_string()
163 : ", location number: " +
164 std::to_string(state.source.pc->location_number) + ".")
165 << messaget::eom;
166
168 }
169 }
170
171 log.warning() << "[symex-complexity] Branch considered too complex"
172 << (state.source.pc->source_location().is_not_nil()
173 ? " at: " +
174 state.source.pc->source_location().as_string()
175 : ", location number: " +
176 std::to_string(state.source.pc->location_number) +
177 ".")
178 << messaget::eom;
179
180 // Then kill this branch.
182 }
183
184 // If we're not in any loop, return with no violation.
185 if(!active_loop)
187
188 // Check if we've entered a loop that has been previously black-listed, and
189 // if so then cancel before we go any further.
190 if(in_blacklisted_loop(current_call_stack, state.source.pc))
191 {
192 log.warning() << "[symex-complexity] Trying to enter blacklisted loop"
193 << (state.source.pc->source_location().is_not_nil()
194 ? " at: " +
195 state.source.pc->source_location().as_string()
196 : ", location number: " +
197 std::to_string(state.source.pc->location_number) +
198 ".")
199 << messaget::eom;
200
202 }
203
205}
206
208 complexity_violationt complexity_violation,
209 goto_symex_statet &current_state)
210{
211 if(violation_transformations.empty())
212 default_transformation.transform(complexity_violation, current_state);
213 else
214 for(auto transform_lambda : violation_transformations)
215 transform_lambda.transform(complexity_violation, current_state);
216}
217
222static std::size_t
223bounded_expr_size(const exprt &expr, std::size_t count, std::size_t limit)
224{
225 const auto &ops = expr.operands();
226 count += ops.size();
227 for(const auto &op : ops)
228 {
229 if(count >= limit)
230 {
231 return count;
232 }
233 count = bounded_expr_size(op, count, limit);
234 }
235 return count;
236}
237
238std::size_t
239complexity_limitert::bounded_expr_size(const exprt &expr, std::size_t limit)
240{
241 return ::bounded_expr_size(expr, 1, limit);
242}
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:54
operandst & operands()
Definition expr.h:92
instructionst::const_iterator const_targett
guardt guard
Definition goto_state.h:58
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition goto_state.h:62
Central data structure: state.
call_stackt & call_stack()
symex_targett::sourcet source
exprt as_expr() const
Definition guard_expr.h:46
A loop, specified as a set of instructions.
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)
static std::size_t bounded_expr_size(const exprt &expr, std::size_t count, std::size_t limit)
Amount of nodes expr contains, with a bound on how far to search.
Symbolic Execution.
complexity_violationt
What sort of symex-complexity violation has taken place.
Symbolic Execution.
goto_programt::const_targett pc