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 "unwindset.h"
17 
18 #include <util/json.h>
19 #include <util/json_expr.h>
21 
22 class goto_modelt;
23 
25 {
26 public:
28 
29  // unwind loop
30 
31  void unwind(
32  goto_programt &goto_program,
33  const goto_programt::const_targett loop_head,
34  const goto_programt::const_targett loop_exit,
35  const unsigned k, // bound for given loop
36  const unwind_strategyt unwind_strategy);
37 
38  void unwind(
39  goto_programt &goto_program,
40  const goto_programt::const_targett loop_head,
41  const goto_programt::const_targett loop_exit,
42  const unsigned k, // bound for given loop
43  const unwind_strategyt unwind_strategy,
44  std::vector<goto_programt::targett> &iteration_points);
45 
46  // unwind function
47 
48  void unwind(
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
jsont output_log_json() const
Definition: unwind.h:70
static int8_t r
Definition: irep_hash.h:59
void insert(const goto_programt::const_targett target, const unsigned location_number)
Definition: unwind.h:92
Definition: json.h:23
unwind_strategyt
Definition: unwind.h:27
Symbol Table + CFG.
Expressions in JSON.
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A collection of goto functions.
void copy_segment(const goto_programt::const_targett start, const goto_programt::const_targett end, goto_programt &goto_program)
Definition: unwind.cpp:27
location_mapt location_map
Definition: unwind.h:101
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Loop unwinding.
void operator()(goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.h:59
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void cleanup(const goto_programt &goto_program)
Definition: unwind.h:86
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:308
jsont output_log_json() const
Definition: unwind.cpp:331
int get_k(const irep_idt func, const unsigned loop_id, const unwindsett &unwindset) const
unwind_logt unwind_log
Definition: unwind.h:104
std::map< goto_programt::const_targett, unsigned > location_mapt
Definition: unwind.h:100
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:82
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32