CBMC
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>
18 
19 class unwindsett;
20 
22 {
23 public:
24  enum class unwind_strategyt
25  {
26  CONTINUE,
27  PARTIAL,
30  ASSUME
31  };
32 
33  // unwind loop
34 
35  void unwind(
36  const irep_idt &function_id,
37  goto_programt &goto_program,
38  const goto_programt::const_targett loop_head,
39  const goto_programt::const_targett loop_exit,
40  const unsigned k, // bound for given loop
41  const unwind_strategyt unwind_strategy);
42 
43  void unwind(
44  const irep_idt &function_id,
45  goto_programt &goto_program,
46  const goto_programt::const_targett loop_head,
47  const goto_programt::const_targett loop_exit,
48  const unsigned k, // bound for given loop
49  const unwind_strategyt unwind_strategy,
50  std::vector<goto_programt::targett> &iteration_points);
51 
52  // unwind function
53 
54  void unwind(
55  const irep_idt &function_id,
56  goto_programt &goto_program,
57  const unwindsett &unwindset,
58  const unwind_strategyt unwind_strategy = unwind_strategyt::PARTIAL);
59 
60  // unwind all functions
61  void operator()(
63  const unwindsett &unwindset,
64  const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL);
65 
66  void operator()(
67  goto_modelt &goto_model,
68  const unwindsett &unwindset,
69  const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
70  {
71  operator()(
72  goto_model.goto_functions, unwindset, unwind_strategy);
73  }
74 
75  // unwind log
76 
78  {
79  return unwind_log.output_log_json();
80  }
81 
82  // log
83  // - for each copied instruction the location number of the
84  // original instruction it came from
85  // - for each new instruction the location number of the loop head
86  // or backedge of the loop it is associated with
87  struct unwind_logt
88  {
89  // call after calling goto_functions.update()!
90  jsont output_log_json() const;
91 
92  // remove entries that refer to the given goto program
93  void cleanup(const goto_programt &goto_program)
94  {
95  forall_goto_program_instructions(it, goto_program)
96  location_map.erase(it);
97  }
98 
99  void insert(
100  const goto_programt::const_targett target,
101  const unsigned location_number)
102  {
103  auto r=location_map.insert(std::make_pair(target, location_number));
104  INVARIANT(r.second, "target already exists");
105  }
106 
107  typedef std::map<
109  unsigned,
113  };
114 
116 
117 protected:
118  int get_k(
119  const irep_idt func,
120  const unsigned loop_id,
121  const unwindsett &unwindset) const;
122 
123  // copy goto program segment and redirect internal edges
124  void copy_segment(
125  const goto_programt::const_targett start,
126  const goto_programt::const_targett end, // exclusive
127  goto_programt &goto_program); // result
128 };
129 
130 #endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:615
void operator()(goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.h:66
unwind_strategyt
Definition: unwind.h:25
int get_k(const irep_idt func, const unsigned loop_id, const unwindsett &unwindset) const
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:327
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:26
void unwind(const irep_idt &function_id, 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:84
jsont output_log_json() const
Definition: unwind.h:77
unwind_logt unwind_log
Definition: unwind.h:115
Definition: json.h:27
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
static int8_t r
Definition: irep_hash.h:60
A total order over targett and const_targett.
Definition: goto_program.h:392
jsont output_log_json() const
Definition: unwind.cpp:350
std::map< goto_programt::const_targett, unsigned, goto_programt::target_less_than > location_mapt
Definition: unwind.h:111
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:99
void cleanup(const goto_programt &goto_program)
Definition: unwind.h:93
location_mapt location_map
Definition: unwind.h:112