1/*******************************************************************\
3Module: Symbolic Execution
7\*******************************************************************/
20 :
log(message_handler)
25 // This gives a curve that allows low limits to be rightly restrictive,
26 // while larger numbers are very large.
30 "symex-complexity-failed-child-loops-limit");
33 // If we have complexity enabled, try to work out a failed_children_limit.
34 // In order of priority:
36 // * inferred limit from unwind
37 // * best limit we can apply with very little information.
54 // As we're walking bottom-up, the first frame we find with active loops
55 // is our closest active one.
93 // This will walk all currently active loops, from inner-most to outer-most,
94 // and sum the times their branches have failed.
96 // If we find that this sum is higher than our max_loops_complexity we take
97 // note of the loop that happens in and then cause every parent still
98 // executing that loop to blacklist it.
100 // This acts as a context-sensitive loop cancel, so if we've got unwind 20
101 // and find out at the 3rd iteration a particular nested loop is too
102 // complicated, we make sure we don't execute it the other 17 times. But as
103 // soon as we're running the loop again via a different context it gets a
104 // chance to redeem itself.
110 for(
auto it =
frame_iter->active_loops.rbegin();
116 // Because we're walking in reverse this will only be non-empty for
117 // parents of the loop that's been blacklisted. We then add that to their
118 // internal lists of blacklisted children.
150 // Check if this branch is too complicated to continue.
154 // If we're too complex, add a counter to the current loop we're in and
155 // check if we've violated child-loop complexity limits.
160 // If we're considered too complex, cancel branch.
164 <<
"[symex-complexity] Loop operations considered too complex"
165 << (state.
source.
pc->source_location().is_not_nil()
166 ?
" at: " + state.
source.
pc->source_location().as_string()
167 :
", location number: " +
168 std::to_string(state.
source.
pc->location_number) +
".")
175 log.
warning() <<
"[symex-complexity] Branch considered too complex"
176 << (state.
source.
pc->source_location().is_not_nil()
178 state.
source.
pc->source_location().as_string()
179 :
", location number: " +
180 std::to_string(state.
source.
pc->location_number) +
184 // Then kill this branch.
188 // If we're not in any loop, return with no violation.
192 // Check if we've entered a loop that has been previously black-listed, and
193 // if so then cancel before we go any further.
196 log.
warning() <<
"[symex-complexity] Trying to enter blacklisted loop"
197 << (state.
source.
pc->source_location().is_not_nil()
199 state.
source.
pc->source_location().as_string()
200 :
", location number: " +
201 std::to_string(state.
source.
pc->location_number) +
231 for(
const auto &op :
ops)
245 return ::bounded_expr_size(expr, 1,
limit);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
complexity_limitert(message_handlert &logger, const optionst &options)
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 ¤t_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 ¤t_call_stack)
Returns inner-most currently active loop.
symex_complexity_limit_exceeded_actiont default_transformation
Default heuristic transformation. Sets state as unreachable.
void run_transformations(complexity_violationt complexity_violation, goto_symex_statet ¤t_state)
Runs a suite of transformations on the state and symex executable, performing whatever transformation...
bool are_loop_children_too_complicated(call_stackt ¤t_call_stack)
Checks whether the current loop execution stack has violated max_loops_complexity.
Base class for all expressions.
instructionst::const_iterator const_targett
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Central data structure: state.
call_stackt & call_stack()
symex_targett::sourcet source
mstreamt & warning() const
signed int get_signed_int_option(const std::string &option) const
virtual void transform(const complexity_violationt heuristic_result, goto_symex_statet ¤t_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.
complexity_violationt
What sort of symex-complexity violation has taken place.
goto_programt::const_targett pc