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