cprover
Loading...
Searching...
No Matches
unwind.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop unwinding
4
5Author: 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
19class unwindsett;
20
22{
23public:
25
26 // unwind loop
27
28 void unwind(
29 const irep_idt &function_id,
30 goto_programt &goto_program,
33 const unsigned k, // bound for given loop
35
36 void unwind(
37 const irep_idt &function_id,
38 goto_programt &goto_program,
41 const unsigned k, // bound for given loop
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,
52
53 // unwind all functions
54 void operator()(
56 const unwindsett &unwindset,
58
60 goto_modelt &goto_model,
61 const unwindsett &unwindset,
63 {
65 goto_model.goto_functions, unwindset, unwind_strategy);
66 }
67
68 // unwind log
69
71 {
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
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(
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
106protected:
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(
115 const goto_programt::const_targett end, // exclusive
116 goto_programt &goto_program); // result
117};
118
119#endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
instructionst::const_iterator const_targett
void operator()(goto_modelt &goto_model, const unwindsett &unwindset, const unwind_strategyt unwind_strategy=unwind_strategyt::PARTIAL)
Definition unwind.h:59
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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