loop_unroll.h

Go to the documentation of this file.

#ifndef ESBMC_GOTO_ALGORITHMS_H
#define ESBMC_GOTO_ALGORITHMS_H
 
#include <goto-programs/goto_functions_algorithm.h>
#include <util/message/message.h>
#include <unordered_set>

class unsound_loop_unroller : public goto_functions_algorithm
{
public:
  unsound_loop_unroller() : goto_functions_algorithm(true)
  {
  }
 
protected:
  bool runOnLoop(loopst &loop, goto_programt &goto_program) override;

  virtual int get_loop_bounds(loopst &loop) = 0;
};

class bounded_loop_unroller : public unsound_loop_unroller
{
public:
  explicit bounded_loop_unroller(size_t unroll_limit = 1000)
    : unsound_loop_unroller(), unroll_limit(unroll_limit)
  {
  }

  unsigned get_number_of_bounded_loops()
  {
    return number_of_bounded_loops;
  }
 
protected:
  // Sets an upper limit for the quantity of loops
  const size_t unroll_limit;
  int get_loop_bounds(loopst &loop) override;
 
private:
  unsigned number_of_bounded_loops = 0;
};

class apply_intrinsic_unroller : public goto_functions_algorithm
{
public:
  apply_intrinsic_unroller() : goto_functions_algorithm(true)
  {
  }
 
  bool run(goto_functionst &goto_functions) override;
 
protected:
  bool runOnLoop(loopst &loop, goto_programt &goto_program) override;
 
private:
  bool apply_unroll(goto_programt::targett call, loopst &loop);

  std::unordered_set<const goto_programt::instructiont *> matched_calls;
};
 
#endif