cprover
unwind.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop unwinding
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Daniel Poetzl
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H
14 #define CPROVER_GOTO_INSTRUMENT_UNWIND_H
15 
16 #include <util/json.h>
17 #include <util/json_expr.h>
19 
21 
22 // -1: do not unwind loop
23 typedef std::map<irep_idt, std::map<unsigned, int>> unwind_sett;
24 
25 void parse_unwindset(const std::string &us, unwind_sett &unwind_set);
26 
28 {
29 public:
31 
32  // unwind loop
33 
34  void unwind(
35  goto_programt &goto_program,
36  const goto_programt::const_targett loop_head,
37  const goto_programt::const_targett loop_exit,
38  const unsigned k, // bound for given loop
39  const unwind_strategyt unwind_strategy);
40 
41  void unwind(
42  goto_programt &goto_program,
43  const goto_programt::const_targett loop_head,
44  const goto_programt::const_targett loop_exit,
45  const unsigned k, // bound for given loop
46  const unwind_strategyt unwind_strategy,
47  std::vector<goto_programt::targett> &iteration_points);
48 
49  // unwind function
50 
51  void unwind(
52  goto_programt &goto_program,
53  const unwind_sett &unwind_set,
54  const int k=-1, // -1: no global bound
55  const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
56 
57  // unwind all functions
58 
59  void operator()(
60  goto_functionst &goto_functions,
61  const unsigned k, // global bound
62  const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
63  {
64  const unwind_sett unwind_set;
65  operator()(goto_functions, unwind_set, k, unwind_strategy);
66  }
67 
68  void operator()(
69  goto_functionst &goto_functions,
70  const unwind_sett &unwind_set,
71  const int k=-1, // -1: no global bound
72  const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
73 
74  // unwind log
75 
77  {
78  return unwind_log.output_log_json();
79  }
80 
81  // log
82  // - for each copied instruction the location number of the
83  // original instruction it came from
84  // - for each new instruction the location number of the loop head
85  // or backedge of the loop it is associated with
86  struct unwind_logt
87  {
88  // call after calling goto_functions.update()!
89  jsont output_log_json() const;
90 
91  // remove entries that refer to the given goto program
92  void cleanup(const goto_programt &goto_program)
93  {
94  forall_goto_program_instructions(it, goto_program)
95  location_map.erase(it);
96  }
97 
98  void insert(
99  const goto_programt::const_targett target,
100  const unsigned location_number)
101  {
102  auto r=location_map.insert(std::make_pair(target, location_number));
103  assert(r.second); // did not exist yet
104  }
105 
106  typedef std::map<goto_programt::const_targett, unsigned> location_mapt;
107  location_mapt location_map;
108  };
109 
111 
112 protected:
113  int get_k(
114  const irep_idt func,
115  const unsigned loop_id,
116  const int global_k,
117  const unwind_sett &unwind_set) const;
118 
119  // copy goto program segment and redirect internal edges
120  void copy_segment(
121  const goto_programt::const_targett start,
122  const goto_programt::const_targett end, // exclusive
123  goto_programt &goto_program); // result
124 };
125 
126 #endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H
jsont output_log_json() const
Definition: unwind.h:76
static int8_t r
Definition: irep_hash.h:59
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:98
void parse_unwindset(const std::string &us, unwind_sett &unwind_set)
Definition: unwind.cpp:25
Definition: json.h:21
void operator()(goto_functionst &goto_functions, const unsigned k, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.h:59
unwind_strategyt
Definition: unwind.h:30
instructionst::const_iterator const_targett
Expressions in JSON.
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:59
location_mapt location_map
Definition: unwind.h:107
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void cleanup(const goto_programt &goto_program)
Definition: unwind.h:92
int get_k(const irep_idt func, const unsigned loop_id, const int global_k, const unwind_sett &unwind_set) const
Definition: unwind.cpp:293
jsont output_log_json() const
Definition: unwind.cpp:391
unwind_logt unwind_log
Definition: unwind.h:110
std::map< irep_idt, std::map< unsigned, int > > unwind_sett
Definition: unwind.h:20
std::map< goto_programt::const_targett, unsigned > location_mapt
Definition: unwind.h:106
void unwind(goto_programt &goto_program, const goto_programt::const_targett loop_head, const goto_programt::const_targett loop_exit, const unsigned k, const unwind_strategyt unwind_strategy)
Definition: unwind.cpp:113
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
Concrete Goto Program.