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