Merge pull request #5384 from martin-cs/refactor/split-up-histories

Move call_stack_history to own file

Author: martin-cs

src/analyses/Makefile

@@ -3,6 +3,7 @@ SRC = ai.cpp \
       ai_history.cpp \
       call_graph.cpp \
       call_graph_helpers.cpp \
+      call_stack_history.cpp \
       constant_propagator.cpp \
       custom_bitvector_analysis.cpp \
       dependence_graph.cpp \

src/analyses/ai_history.cpp

@@ -27,205 +27,3 @@ xmlt ai_history_baset::output_xml(void) const
   xml.data = out.str();
   return xml;
 }
-
-ai_history_baset::step_returnt
-call_stack_historyt::step(locationt to, const trace_sett &others) const
-{
-  DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");
-
-  cse_ptrt next_stack = nullptr;
-
-  // First construct what the new history would be.
-  // This requires special handling if this edge is a function call or return
-  if(current_stack->current_location->is_function_call())
-  {
-    locationt l_return = std::next(current_stack->current_location);
-
-    if(l_return->location_number == to->location_number)
-    {
-      // Is skipping the function call, only update the location
-      next_stack = cse_ptrt(
-        std::make_shared<call_stack_entryt>(l_return, current_stack->caller));
-    }
-    else
-    {
-      // An interprocedural (call) edge; add to the current stack
-
-      // If the recursion limit has been reached
-      // shorten the stack / merge with the most recent invocation
-      // before we extend
-      cse_ptrt shorten = current_stack;
-
-      if(has_recursion_limit())
-      {
-        unsigned int number_of_recursive_calls = 0;
-        cse_ptrt first_found = nullptr; // The most recent recursive call
-
-        // Iterate back through the call stack
-        for(cse_ptrt i = current_stack->caller; i != nullptr; i = i->caller)
-        {
-          if(
-            i->current_location->location_number ==
-            current_stack->current_location->location_number)
-          {
-            // Found a recursive instance
-            if(first_found == nullptr)
-            {
-              first_found = i;
-            }
-            ++number_of_recursive_calls;
-            if(number_of_recursive_calls == recursion_limit)
-            {
-              shorten = first_found;
-              break;
-            }
-          }
-        }
-      }
-
-      next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(to, shorten));
-    }
-  }
-  else if(current_stack->current_location->is_end_function())
-  {
-    if(current_stack->caller == nullptr)
-    {
-      // Trying to return but there was no caller?
-      // Refuse to do the transition outright
-      return std::make_pair(ai_history_baset::step_statust::BLOCKED, nullptr);
-    }
-    else
-    {
-      // The expected call return site...
-      locationt l_caller_return =
-        std::next(current_stack->caller->current_location);
-
-      if(l_caller_return->location_number == to->location_number)
-      {
-        // ... which is where we are going
-        next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(
-          to, current_stack->caller->caller));
-      }
-      else
-      {
-        // Not possible to return to somewhere other than the call site
-        return std::make_pair(ai_history_baset::step_statust::BLOCKED, nullptr);
-      }
-    }
-  }
-  else
-  {
-    // Just update the location
-    next_stack =
-      cse_ptrt(std::make_shared<call_stack_entryt>(to, current_stack->caller));
-  }
-  INVARIANT(next_stack != nullptr, "All branches should initialise next_stack");
-
-  // Create the potential next history
-  trace_ptrt next(new call_stack_historyt(next_stack, recursion_limit));
-  // It would be nice to use make_shared here but ... that doesn't work with
-  // protected constructors
-
-  // If there is already an equivalent history, merge with that instead
-  auto it = others.find(next);
-
-  if(it == others.end())
-  {
-    return std::make_pair(ai_history_baset::step_statust::NEW, next);
-  }
-  else
-  {
-    return std::make_pair(ai_history_baset::step_statust::MERGED, *it);
-  }
-}
-
-bool call_stack_historyt::operator<(const ai_history_baset &op) const
-{
-  auto other = dynamic_cast<const call_stack_historyt *>(&op);
-  PRECONDITION(other != nullptr);
-
-  return *(this->current_stack) < *(other->current_stack);
-}
-
-bool call_stack_historyt::operator==(const ai_history_baset &op) const
-{
-  auto other = dynamic_cast<const call_stack_historyt *>(&op);
-  PRECONDITION(other != nullptr);
-
-  return *(this->current_stack) == *(other->current_stack);
-}
-
-void call_stack_historyt::output(std::ostream &out) const
-{
-  out << "call_stack_history : stack "
-      << current_stack->current_location->location_number;
-  cse_ptrt working = current_stack->caller;
-  while(working != nullptr)
-  {
-    out << " from " << working->current_location->location_number;
-    working = working->caller;
-  }
-  return;
-}
-
-bool call_stack_historyt::call_stack_entryt::
-operator<(const call_stack_entryt &op) const
-{
-  if(
-    this->current_location->location_number <
-    op.current_location->location_number)
-  {
-    return true;
-  }
-  else if(
-    this->current_location->location_number >
-    op.current_location->location_number)
-  {
-    return false;
-  }
-  else
-  {
-    INVARIANT(
-      this->current_location->location_number ==
-        op.current_location->location_number,
-      "Implied by if-then-else");
-
-    if(this->caller == op.caller)
-    {
-      return false; // Because they are equal
-    }
-    else if(this->caller == nullptr)
-    {
-      return true; // Shorter stacks are 'lower'
-    }
-    else if(op.caller == nullptr)
-    {
-      return false;
-    }
-    else
-    {
-      // Sort by the rest of the stack
-      return *(this->caller) < *(op.caller);
-    }
-  }
-  UNREACHABLE;
-}
-
-bool call_stack_historyt::call_stack_entryt::
-operator==(const call_stack_entryt &op) const
-{
-  if(
-    this->current_location->location_number ==
-    op.current_location->location_number)
-  {
-    if(this->caller == op.caller)
-    {
-      return true;
-    }
-    else if(this->caller != nullptr && op.caller != nullptr)
-    {
-      return *(this->caller) == *(op.caller);
-    }
-  }
-  return false;
-}

src/analyses/ai_history.h

@@ -219,93 +219,6 @@ class ahistoricalt : public ai_history_baset
   }
 };
 
-/// Records the call stack
-/// Care must be taken when using this on recursive code; it will need the
-/// domain to be capable of limiting the recursion.
-class call_stack_historyt : public ai_history_baset
-{
-protected:
-  class call_stack_entryt;
-  typedef std::shared_ptr<const call_stack_entryt> cse_ptrt;
-  class call_stack_entryt
-  {
-  public:
-    locationt current_location;
-    cse_ptrt caller;
-
-    call_stack_entryt(locationt l, cse_ptrt p) : current_location(l), caller(p)
-    {
-    }
-
-    bool operator<(const call_stack_entryt &op) const;
-    bool operator==(const call_stack_entryt &op) const;
-  };
-
-  cse_ptrt current_stack;
-  // DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");
-  // DATA_INVARIANT(current_stack->current.is_dereferenceable(),
-  //                "Must not be _::end()")
-
-  // At what point to merge with a previous call stack when handling recursion
-  // Setting to 0 disables completely
-  unsigned int recursion_limit;
-
-  bool has_recursion_limit(void) const
-  {
-    return recursion_limit != 0;
-  }
-
-  call_stack_historyt(cse_ptrt cur_stack, unsigned int rec_lim)
-    : ai_history_baset(cur_stack->current_location),
-      current_stack(cur_stack),
-      recursion_limit(rec_lim)
-  {
-    PRECONDITION(
-      cur_stack != nullptr); // A little late by now but worth documenting
-  }
-
-public:
-  explicit call_stack_historyt(locationt l)
-    : ai_history_baset(l),
-      current_stack(std::make_shared<call_stack_entryt>(l, nullptr)),
-      recursion_limit(0)
-  {
-  }
-
-  call_stack_historyt(locationt l, unsigned int rec_lim)
-    : ai_history_baset(l),
-      current_stack(std::make_shared<call_stack_entryt>(l, nullptr)),
-      recursion_limit(rec_lim)
-  {
-  }
-
-  call_stack_historyt(const call_stack_historyt &old)
-    : ai_history_baset(old),
-      current_stack(old.current_stack),
-      recursion_limit(old.recursion_limit)
-  {
-  }
-
-  step_returnt step(locationt to, const trace_sett &others) const override;
-
-  bool operator<(const ai_history_baset &op) const override;
-  bool operator==(const ai_history_baset &op) const override;
-
-  const locationt &current_location(void) const override
-  {
-    return current_stack->current_location;
-  }
-
-  // Use default widening
-  // Typically this would be used for loops, which are not tracked
-  // it would be possible to use this to improve the handling of recursion
-  bool should_widen(const ai_history_baset &other) const override
-  {
-    return ai_history_baset::should_widen(other);
-  }
-
-  void output(std::ostream &out) const override;
-};
 
 /// As more detailed histories can get complex (for example, nested loops
 /// or deep, mutually recursive call stacks) they often need some user
@@ -335,28 +248,4 @@ class ai_history_factory_default_constructort : public ai_history_factory_baset
   }
 };
 
-// Allows passing a recursion limit
-class call_stack_history_factoryt : public ai_history_factory_baset
-{
-protected:
-  unsigned int recursion_limit;
-
-public:
-  explicit call_stack_history_factoryt(unsigned int rec_lim)
-    : recursion_limit(rec_lim)
-  {
-  }
-
-  ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
-  {
-    ai_history_baset::trace_ptrt p(
-      std::make_shared<call_stack_historyt>(l, recursion_limit));
-    return p;
-  }
-
-  virtual ~call_stack_history_factoryt()
-  {
-  }
-};
-
 #endif // CPROVER_ANALYSES_AI_HISTORY_H