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
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:24
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:82
jsont
Definition: json.h:27
goto_unwindt::unwind_logt::cleanup
void cleanup(const goto_programt &goto_program)
Definition: unwind.h:86
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:92
unwindsett
Definition: unwindset.h:23
goto_unwindt::unwind_logt::output_log_json
jsont output_log_json() const
Definition: unwind.cpp:337
goto_unwindt::unwind_logt
Definition: unwind.h:81
goto_unwindt
Definition: unwind.h:22
goto_unwindt::operator()
void operator()(goto_functionst &, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.cpp:314
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:101
goto_unwindt::operator()
void operator()(goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition: unwind.h:59
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:26
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_unwindt::unwind_logt::location_mapt
std::map< goto_programt::const_targett, unsigned > location_mapt
Definition: unwind.h:100
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:71
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
r
static int8_t r
Definition: irep_hash.h:60
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1255
goto_unwindt::output_log_json
jsont output_log_json() const
Definition: unwind.h:70
goto_unwindt::unwind_log
unwind_logt unwind_log
Definition: unwind.h:104