lexical_loops.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Compute lexical loops in a goto_function
 
Author: Diffblue Ltd
 
\*******************************************************************/

 
#ifndef CPROVER_ANALYSES_LEXICAL_LOOPS_H
#define CPROVER_ANALYSES_LEXICAL_LOOPS_H
 
#include <iosfwd>
#include <set>
#include <stack>
 
#include <goto-programs/goto_model.h>
 
#include "loop_analysis.h"

template <class P, class T, typename C>
class lexical_loops_templatet : public loop_analysist<T, C>
{
  typedef loop_analysist<T, C> parentt;
 
public:
  typedef typename parentt::loopt lexical_loopt;
 
  void operator()(P &program)
  {
    compute(program);
  }
 
  lexical_loops_templatet() = default;
 
  explicit lexical_loops_templatet(P &program)
  {
    compute(program);
  }
 
  bool all_cycles_in_lexical_loop_form() const
  {
    return all_in_lexical_loop_form;
  }
 
  void output(std::ostream &out) const
  {
    parentt::output(out);
    if(!all_in_lexical_loop_form)
      out << "Note not all loops were in lexical loop form\n";
  }
 
  virtual ~lexical_loops_templatet() = default;
 
protected:
  void compute(P &program);
  bool compute_lexical_loop(T, T);
 
  bool all_in_lexical_loop_form = false;
};
 
typedef lexical_loops_templatet<
  const goto_programt,
  goto_programt::const_targett,
  goto_programt::target_less_than>
  lexical_loopst;
 
#ifdef DEBUG
#  include <iostream>
#endif

template <class P, class T, typename C>
void lexical_loops_templatet<P, T, C>::compute(P &program)
{
  all_in_lexical_loop_form = true;
 
  // find back-edges m->n
  for(auto it = program.instructions.begin(); it != program.instructions.end();
      ++it)
  {
    if(it->is_backwards_goto())
    {
      const auto &target = it->get_target();
 
      if(target->location_number <= it->location_number)
      {
#ifdef DEBUG
        std::cout << "Computing loop for " << it->location_number << " -> "
                  << target->location_number << "\n";
#endif
 
        if(!compute_lexical_loop(it, target))
          all_in_lexical_loop_form = false;
      }
    }
  }
}

template <class P, class T, typename C>
bool lexical_loops_templatet<P, T, C>::compute_lexical_loop(
  T loop_tail,
  T loop_head)
{
  INVARIANT(
    loop_head->location_number <= loop_tail->location_number,
    "loop header should come lexically before the tail");
 
  std::stack<T> stack;
  std::set<T, C> loop_instructions;
 
  loop_instructions.insert(loop_head);
  loop_instructions.insert(loop_tail);
 
  if(loop_head != loop_tail)
    stack.push(loop_tail);
 
  while(!stack.empty())
  {
    T loop_instruction = stack.top();
    stack.pop();
 
    for(auto predecessor : loop_instruction->incoming_edges)
    {
      if(
        predecessor->location_number > loop_tail->location_number ||
        predecessor->location_number < loop_head->location_number)
      {
        // Not a lexical loop: has an incoming edge from outside.
        return false;
      }
      if(loop_instructions.insert(predecessor).second)
        stack.push(predecessor);
    }
  }
 
  auto insert_result = parentt::loop_map.emplace(
    loop_head, lexical_loopt{std::move(loop_instructions)});
 
  // If this isn't a new loop head (i.e. return_result.second is false) then we
  // have multiple backedges targeting one loop header: this is not in simple
  // lexical loop form.
  return insert_result.second;
}
 
inline void show_lexical_loops(const goto_modelt &goto_model, std::ostream &out)
{
  show_loops<lexical_loopst>(goto_model, out);
}
 
#endif // CPROVER_ANALYSES_LEXICAL_LOOPS_H