CBMC
unwindset.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop unwinding setup
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
13 #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
14 
15 #include <util/irep.h>
16 
17 #include <list>
18 #include <map>
19 #include <optional>
20 #include <string>
21 
23 class message_handlert;
24 
26 {
27 public:
28  // We have
29  // 1) a global limit
30  // 2) a limit per loop, all threads
31  // 3) a limit for a particular thread.
32  // We use the most specific of the above.
34  {
35  }
36 
37  // global limit for all loops
38  void parse_unwind(const std::string &unwind);
39 
40  // limit for instances of a loop
41  void parse_unwindset(
42  const std::list<std::string> &unwindset,
43  message_handlert &message_handler);
44 
45  // queries
46  std::optional<unsigned>
47  get_limit(const irep_idt &loop, unsigned thread_id) const;
48 
49  // read unwindset directives from a file
51  const std::string &file_name,
52  message_handlert &message_handler);
53 
54 protected:
56 
57  std::optional<unsigned> global_limit;
58 
59  // Limit for all instances of a loop.
60  // This may have 'no value'.
61  typedef std::map<irep_idt, std::optional<unsigned>> loop_mapt;
63 
64  // separate limits per thread
66  std::map<std::pair<irep_idt, unsigned>, std::optional<unsigned>>;
68 
70  std::string loop_limit,
71  message_handlert &message_handler);
72 };
73 
74 #define OPT_UNWINDSET \
75  "(show-loops)" \
76  "(unwind):" \
77  "(unwindset):"
78 
79 #define HELP_UNWINDSET \
80  " {y--show-loops} \t show the loops in the program\n" \
81  " {y--unwind} {unr} \t unwind loops {unr} times\n" \
82  " {y--unwindset} [{uT}{y:}]{uL}{y:}{uB},... \t " \
83  "unwind loop {uL} with a bound of {uB} (optionally restricted to thread " \
84  "{uT}) (use {y--show-loops} to get the loop IDs)\n"
85 
86 #endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H
Abstract interface to eager or lazy GOTO models.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
loop_mapt loop_map
Definition: unwindset.h:62
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:191
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
Definition: unwindset.cpp:29
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:23
std::map< std::pair< irep_idt, unsigned >, std::optional< unsigned > > thread_loop_mapt
Definition: unwindset.h:66
std::optional< unsigned > global_limit
Definition: unwindset.h:57
thread_loop_mapt thread_loop_map
Definition: unwindset.h:67
unwindsett(abstract_goto_modelt &goto_model)
Definition: unwindset.h:33
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
Definition: unwindset.cpp:212
abstract_goto_modelt & goto_model
Definition: unwindset.h:55
std::map< irep_idt, std::optional< unsigned > > loop_mapt
Definition: unwindset.h:61
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
Definition: unwindset.cpp:182
const std::string thread_id