Initial commit of symex complexity work

This work allows for a more intelligent way of pathing  around / slicing
away problematic code dynamically as symex runs. Every path will have a
'complexity' rating that shows currently how difficult the code it's
running is for symex to analyze (alternatively also for the SAT solver
to solve) and when that rating breaches a certain range, that path will
be shut down.

This means we won't be able to generate traces that would use the
discarded path, but when that path is not important it's a net benefit,
and when it was important CBMC wouldn't have completed anyway so we
trade an inaccurate trace for nothing at all.

Note: There is special consideration for loops: when any of a loops
children fails (inc. loops / recursion) it increments a counter, and
when that counter reaches a certain limit the whole loop itself gets
cancelled. This is done because when a branch deep within a loop gets
cancelled along all paths the loop will simply try again even though
it's been proven that the code will become too complicated to analyze.

Author: JohnDumbell

src/goto-symex/Makefile

@@ -35,6 +35,7 @@ SRC = auto_objects.cpp \
       symex_target.cpp \
       symex_target_equation.cpp \
       symex_throw.cpp \
+      complexity_limiter.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/goto-symex/complexity_limiter.cpp

@@ -0,0 +1,214 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: John Dumbell
+
+\*******************************************************************/
+
+#include "complexity_limiter.h"
+#include "goto_symex_state.h"
+#include <cmath>
+
+complexity_limitert::complexity_limitert(
+  message_handlert &message_handler,
+  const optionst &options)
+  : log(message_handler)
+{
+  std::size_t limit = options.get_signed_int_option("symex-complexity-limit");
+  if((complexity_active = limit > 0))
+  {
+    // This gives a curve that allows low limits to be rightly restrictive,
+    // while larger numbers are very large.
+    max_complexity = static_cast<std::size_t>((limit * limit) * 25);
+
+    const std::size_t failed_child_loops_limit = options.get_signed_int_option(
+      "symex-complexity-failed-child-loops-limit");
+    const std::size_t unwind = options.get_signed_int_option("unwind");
+
+    // If we have complexity enabled, try to work out a failed_children_limit.
+    // In order of priority:
+    //  * explicit limit
+    //  * inferred limit from unwind
+    //  * best limit we can apply with very little information.
+    if(failed_child_loops_limit > 0)
+      max_loops_complexity = failed_child_loops_limit;
+    else if(unwind > 0)
+      max_loops_complexity = std::max(static_cast<int>(floor(unwind / 3)), 1);
+    else
+      max_loops_complexity = limit;
+  }
+}
+
+framet::active_loop_infot *
+complexity_limitert::get_current_active_loop(call_stackt &current_call_stack)
+{
+  for(auto frame_iter = current_call_stack.rbegin();
+      frame_iter != current_call_stack.rend();
+      ++frame_iter)
+  {
+    // As we're walking bottom-up, the first frame we find with active loops
+    // is our closest active one.
+    if(!frame_iter->active_loops.empty())
+    {
+      return &frame_iter->active_loops.back();
+    }
+  }
+
+  return {};
+}
+
+bool complexity_limitert::in_blacklisted_loop(
+  const call_stackt &current_call_stack,
+  const goto_programt::const_targett &instr)
+{
+  for(auto frame_iter = current_call_stack.rbegin();
+      frame_iter != current_call_stack.rend();
+      ++frame_iter)
+  {
+    for(auto &loop_iter : frame_iter->active_loops)
+    {
+      for(auto &blacklisted_loop : loop_iter.blacklisted_loops)
+      {
+        if(blacklisted_loop.get().contains(instr))
+        {
+          return true;
+        }
+      }
+    }
+  }
+
+  return false;
+}
+
+bool complexity_limitert::are_loop_children_too_complicated(
+  call_stackt &current_call_stack)
+{
+  std::size_t sum_complexity = 0;
+
+  // This will walk all currently active loops, from inner-most to outer-most,
+  // and sum the times their branches have failed.
+  //
+  // If we find that this sum is higher than our max_loops_complexity we take
+  // note of the loop that happens in and then cause every parent still
+  // executing that loop to blacklist it.
+  //
+  // This acts as a context-sensitive loop cancel, so if we've got unwind 20
+  // and find out at the 3rd iteration a particular nested loop is too
+  // complicated, we make sure we don't execute it the other 17 times. But as
+  // soon as we're running the loop again via a different context it gets a
+  // chance to redeem itself.
+  optionalt<std::reference_wrapper<lexical_loopst::loopt>> loop_to_blacklist;
+  for(auto frame_iter = current_call_stack.rbegin();
+      frame_iter != current_call_stack.rend();
+      ++frame_iter)
+  {
+    for(auto it = frame_iter->active_loops.rbegin();
+        it != frame_iter->active_loops.rend();
+        it++)
+    {
+      auto &loop_info = *it;
+
+      // Because we're walking in reverse this will only be non-empty for
+      // parents of the loop that's been blacklisted. We then add that to their
+      // internal lists of blacklisted children.
+      if(loop_to_blacklist)
+      {
+        loop_info.blacklisted_loops.emplace_back(*loop_to_blacklist);
+      }
+      else
+      {
+        sum_complexity += loop_info.children_too_complex;
+        if(sum_complexity > max_loops_complexity)
+        {
+          loop_to_blacklist =
+            std::reference_wrapper<lexical_loopst::loopt>(loop_info.loop);
+        }
+      }
+    }
+  }
+
+  return !loop_to_blacklist;
+}
+
+complexity_violationt
+complexity_limitert::check_complexity(goto_symex_statet &state)
+{
+  if(!complexity_limits_active() || !state.reachable)
+    return complexity_violationt::NONE;
+
+  std::size_t complexity = state.complexity();
+  if(complexity == 0)
+    return complexity_violationt::NONE;
+
+  auto &current_call_stack = state.call_stack();
+
+  // Check if this branch is too complicated to continue.
+  auto active_loop = get_current_active_loop(current_call_stack);
+  if(complexity >= max_complexity)
+  {
+    // If we're too complex, add a counter to the current loop we're in and
+    // check if we've violated child-loop complexity limits.
+    if(active_loop != nullptr)
+    {
+      active_loop->children_too_complex++;
+
+      // If we're considered too complex, cancel branch.
+      if(are_loop_children_too_complicated(current_call_stack))
+      {
+        log.warning()
+          << "[symex-complexity] Loop operations considered too complex"
+          << (state.source.pc->source_location.is_not_nil()
+                ? " at: " + state.source.pc->source_location.as_string()
+                : ", location number: " +
+                    std::to_string(state.source.pc->location_number) + ".")
+          << messaget::eom;
+
+        return complexity_violationt::LOOP;
+      }
+    }
+
+    log.warning() << "[symex-complexity] Branch considered too complex"
+                  << (state.source.pc->source_location.is_not_nil()
+                        ? " at: " + state.source.pc->source_location.as_string()
+                        : ", location number: " +
+                            std::to_string(state.source.pc->location_number) +
+                            ".")
+                  << messaget::eom;
+
+    // Then kill this branch.
+    return complexity_violationt::BRANCH;
+  }
+
+  // If we're not in any loop, return with no violation.
+  if(!active_loop)
+    return complexity_violationt::NONE;
+
+  // Check if we've entered a loop that has been previously black-listed, and
+  // if so then cancel before we go any further.
+  if(in_blacklisted_loop(current_call_stack, state.source.pc))
+  {
+    log.warning() << "[symex-complexity] Trying to enter blacklisted loop"
+                  << (state.source.pc->source_location.is_not_nil()
+                        ? " at: " + state.source.pc->source_location.as_string()
+                        : ", location number: " +
+                            std::to_string(state.source.pc->location_number) +
+                            ".")
+                  << messaget::eom;
+
+    return complexity_violationt::LOOP;
+  }
+
+  return complexity_violationt::NONE;
+}
+
+void complexity_limitert::run_transformations(
+  complexity_violationt complexity_violation,
+  goto_symex_statet &current_state)
+{
+  if(violation_transformations.empty())
+    default_transformation.transform(complexity_violation, current_state);
+  else
+    for(auto transform_lambda : violation_transformations)
+      transform_lambda.transform(complexity_violation, current_state);
+}

src/goto-symex/complexity_limiter.h

@@ -0,0 +1,113 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: John Dumbell
+
+\*******************************************************************/
+
+/// \file
+/// Symbolic Execution
+
+#ifndef CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
+#define CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H
+
+#include "complexity_violation.h"
+#include "goto_symex_state.h"
+#include "symex_complexity_limit_exceeded_action.h"
+
+/// Symex complexity module.
+///
+/// Dynamically sets branches as unreachable symex considers them too complex.
+/// A branch is too complex when runtime may be beyond reasonable
+/// bounds due to internal structures becoming too large or solving conditions
+/// becoming too big for the SAT solver to deal with.
+///
+/// On top of the branch cancelling there is special consideration for loops.
+/// As branches get cancelled it keeps track of what loops are currently active
+/// up through the stack. If a loop has too many of its child branches killed
+/// (including additional loops or recursion) it won't do any more unwinds of
+/// that particular loop and will blacklist it.
+///
+/// This blacklist is only held for as long as any loop is still active. As soon
+/// as the loop iteration ends and the context in which the code is being
+/// executed changes it'll be able to be run again.
+///
+/// Example of loop blacklisting:
+///
+///     loop A: (complexity: 5070)
+///         loop B: (complexity: 5000)
+///         loop C: (complexity: 70)
+///
+/// In the above loop B will be blacklisted if we have a complexity limitation
+/// < 5000, but loop A and C will still be run, because when loop B is removed
+/// the complexity of the loop as a whole is acceptable.
+class complexity_limitert
+{
+public:
+  complexity_limitert() = default;
+
+  complexity_limitert(message_handlert &logger, const optionst &options);
+
+  /// Is the complexity module active?
+  /// \return Whether complexity limits are active or not.
+  inline bool complexity_limits_active()
+  {
+    return this->complexity_active;
+  }
+
+  /// Checks the passed-in state to see if its become too complex for us to deal
+  /// with, and if so set its guard to false.
+  /// \param state goto_symex_statet you want to check the complexity of.
+  /// \return True/false depending on whether this branch should be abandoned.
+  complexity_violationt check_complexity(goto_symex_statet &state);
+
+  /// Runs a suite of transformations on the state and symex executable,
+  /// performing whatever transformations are required depending on
+  /// the modules that have been loaded.
+  void run_transformations(
+    complexity_violationt complexity_violation,
+    goto_symex_statet &current_state);
+
+protected:
+  mutable messaget log;
+
+  /// Is the complexity module active, usually coincides with a max_complexity
+  /// value above 0.
+  bool complexity_active = false;
+
+  /// Functions called when the heuristic has been violated. Can perform
+  /// any form of branch, state or full-program transformation.
+  std::vector<symex_complexity_limit_exceeded_actiont>
+    violation_transformations;
+
+  /// Default heuristic transformation. Sets state as unreachable.
+  symex_complexity_limit_exceeded_actiont default_transformation;
+
+  /// The max complexity rating that a branch can be before it's abandoned. The
+  /// internal representation for computing complexity, has no relation to the
+  /// argument passed in via options.
+  std::size_t max_complexity = 0;
+
+  /// The amount of branches that can fail within the scope of a loops execution
+  /// before the entire loop is abandoned.
+  std::size_t max_loops_complexity = 0;
+
+  /// Checks whether the current loop execution stack has violated
+  /// max_loops_complexity.
+  bool are_loop_children_too_complicated(call_stackt &current_call_stack);
+
+  /// Checks whether we're in a loop that is currently considered blacklisted,
+  /// and shouldn't be executed.
+  static bool in_blacklisted_loop(
+    const call_stackt &current_call_stack,
+    const goto_programt::const_targett &instr);
+
+  /// Returns inner-most currently active loop. This is frame-agnostic, so if
+  /// we're in a loop further up the stack that will still be returned as
+  /// the 'active' one.
+  static framet::active_loop_infot *
+  get_current_active_loop(call_stackt &current_call_stack);
+};
+
+#endif // CPROVER_GOTO_SYMEX_COMPLEXITY_LIMITER_H

src/goto-symex/complexity_violation.h

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: John Dumbell
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_SYMEX_COMPLEXITY_VIOLATION_H
+#define CPROVER_GOTO_SYMEX_COMPLEXITY_VIOLATION_H
+
+/// What sort of symex-complexity violation has taken place.
+///
+/// Loop: If we've violated a loop complexity boundary, or are part of
+/// a blacklisted loop.
+/// Branch: If this particular branch has been deemed too complex.
+enum class complexity_violationt
+{
+  NONE,
+  LOOP,
+  BRANCH,
+};
+
+#endif // CPROVER_GOTO_SYMEX_COMPLEXITY_VIOLATION_H

src/goto-symex/frame.h

@@ -14,6 +14,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include "goto_state.h"
 #include "symex_target.h"
+#include <analyses/lexical_loops.h>
 
 /// Stack frames -- these are used for function calls and for exceptions
 struct framet
@@ -46,6 +47,27 @@ struct framet
     bool is_recursion = false;
   };
 
+  class active_loop_infot
+  {
+  public:
+    explicit active_loop_infot(lexical_loopst::loopt &_loop) : loop(_loop)
+    {
+    }
+
+    /// Incremental counter on how many branches this loop has had killed.
+    std::size_t children_too_complex = 0;
+
+    /// Set of loop ID's that have been blacklisted.
+    std::vector<std::reference_wrapper<lexical_loopst::loopt>>
+      blacklisted_loops;
+
+    // Loop information.
+    lexical_loopst::loopt &loop;
+  };
+
+  std::shared_ptr<lexical_loopst> loops_info;
+  std::vector<active_loop_infot> active_loops;
+
   std::unordered_map<irep_idt, loop_infot> loop_iterations;
 
   framet(symex_targett::sourcet _calling_location, const guardt &state_guard)