unwindset.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Loop unwinding setup
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
 
#include <util/irep.h>
 
#include <list>
#include <map>
#include <optional>
#include <string>
 
class abstract_goto_modelt;
class message_handlert;
 
class unwindsett
{
public:
  // We have
  // 1) a global limit
  // 2) a limit per loop, all threads
  // 3) a limit for a particular thread.
  // We use the most specific of the above.
  unwindsett() = default;
 
  // global limit for all loops
  void parse_unwind(const std::string &unwind);
 
  // limit for instances of a loop
  void parse_unwindset(
    const std::list<std::string> &unwindset,
    abstract_goto_modelt &goto_model,
    message_handlert &message_handler);
 
  // queries
  std::optional<unsigned>
  get_limit(const irep_idt &loop, unsigned thread_id) const;
 
  // read unwindset directives from a file
  void parse_unwindset_file(
    const std::string &file_name,
    abstract_goto_modelt &goto_model,
    message_handlert &message_handler);
 
protected:
  std::optional<unsigned> global_limit;
 
  // Limit for all instances of a loop.
  // This may have 'no value'.
  typedef std::map<irep_idt, std::optional<unsigned>> loop_mapt;
  loop_mapt loop_map;
 
  // separate limits per thread
  using thread_loop_mapt =
    std::map<std::pair<irep_idt, unsigned>, std::optional<unsigned>>;
  thread_loop_mapt thread_loop_map;
 
  void parse_unwindset_one_loop(
    std::string loop_limit,
    abstract_goto_modelt &goto_model,
    message_handlert &message_handler);
};
 
#define OPT_UNWINDSET                                                          \
  "(show-loops)"                                                               \
  "(unwind):"                                                                  \
  "(unwindset):"
 
#define HELP_UNWINDSET                                                         \
  " {y--show-loops} \t show the loops in the program\n"                        \
  " {y--unwind} {unr} \t unwind loops {unr} times\n"                           \
  " {y--unwindset} [{uT}{y:}]{uL}{y:}{uB},... \t "                             \
  "unwind loop {uL} with a bound of {uB} (optionally restricted to thread "    \
  "{uT}) (use {y--show-loops} to get the loop IDs)\n"
 
#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H