cprover
Loading...
Searching...
No Matches
goto_program2code.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dump Goto-Program as C/C++ Source
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H
13#define CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H
14
15#include <list>
16#include <unordered_set>
17
19
20#include <util/std_code.h>
21
23{
24 typedef std::list<irep_idt> id_listt;
25 typedef std::map<goto_programt::const_targett, goto_programt::const_targett>
27 typedef std::unordered_map<irep_idt, unsigned> dead_mapt;
28 typedef std::list<std::pair<goto_programt::const_targett, bool> >
30
31 struct caset
32 {
33 const exprt value; // condition upon which this case is taken
36 goto_programt::const_targett case_last; // last instruction of case
37
39 const exprt &v,
42 value(v), case_selector(sel), case_start(st),
43 case_last(goto_program.instructions.end())
44 {
45 }
46 };
47 typedef std::list<caset> cases_listt;
48
49public:
51 const irep_idt &identifier,
52 const goto_programt &_goto_program,
53 symbol_tablet &_symbol_table,
54 code_blockt &_dest,
55 id_listt &_local_static,
56 id_listt &_type_names,
57 const std::unordered_set<irep_idt> &_typedef_names,
58 std::set<std::string> &_system_headers)
59 : func_name(identifier),
60 goto_program(_goto_program),
61 symbol_table(_symbol_table),
62 ns(_symbol_table),
63 toplevel_block(_dest),
64 local_static(_local_static),
65 type_names(_type_names),
66 typedef_names(_typedef_names),
67 system_headers(_system_headers)
68 {
69 assert(local_static.empty());
70
71 for(id_listt::const_iterator
72 it=type_names.begin();
73 it!=type_names.end();
74 ++it)
75 type_names_set.insert(*it);
76 }
77
78 void operator()();
79
80protected:
88 const std::unordered_set<irep_idt> &typedef_names;
89 std::set<std::string> &system_headers;
90 std::unordered_set<exprt, irep_hash> va_list_expr;
91
94 std::unordered_set<irep_idt> labels_in_use;
97 std::unordered_set<irep_idt> local_static_set;
98 std::unordered_set<irep_idt> type_names_set;
99 std::unordered_set<irep_idt> const_removed;
100
102
103 void build_loop_map();
104 void build_dead_map();
105 void scan_for_varargs();
106
107 void cleanup_code(codet &code, const irep_idt parent_stmt);
108
110 const exprt &function,
112
114 codet &code,
115 const irep_idt parent_stmt);
116
118 codet &code,
119 const irep_idt parent_stmt);
120
121 void cleanup_expr(exprt &expr, bool no_typecast);
122
123 void add_local_types(const typet &type);
124
125 void remove_const(typet &type);
126
130 code_blockt &dest);
131
133
137 code_blockt &dest);
138
142 code_blockt &dest);
143
144 void convert_assign_rec(const code_assignt &assign, code_blockt &dest);
145
149 code_blockt &dest);
150
154 code_blockt &dest);
155
159 code_blockt &dest);
160
164 code_blockt &dest);
165
169 code_blockt &dest);
170
174 code_blockt &dest);
175
179 const exprt &switch_var,
180 cases_listt &cases,
181 goto_programt::const_targett &first_target,
182 goto_programt::const_targett &default_target);
183
186 const cfg_dominatorst &dominators,
187 cases_listt &cases,
188 std::set<unsigned> &processed_locations);
189
190 bool remove_default(
191 const cfg_dominatorst &dominators,
192 const cases_listt &cases,
193 goto_programt::const_targett default_target);
194
198 code_blockt &dest);
199
203 code_blockt &dest);
204
207
211 code_blockt &dest);
212
215
219 code_blockt &dest);
220};
221
222#endif // CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition std_code.h:130
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::map< goto_programt::const_targett, goto_programt::const_targett > loopt
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::list< irep_idt > id_listt
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::unordered_set< irep_idt > local_static_set
std::unordered_set< irep_idt > type_names_set
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
loop_last_stackt loop_last_stack
void convert_labels(goto_programt::const_targett target, code_blockt &dest)
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
symbol_tablet & symbol_table
goto_program2codet(const irep_idt &identifier, const goto_programt &_goto_program, symbol_tablet &_symbol_table, code_blockt &_dest, id_listt &_local_static, id_listt &_type_names, const std::unordered_set< irep_idt > &_typedef_names, std::set< std::string > &_system_headers)
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, code_blockt &dest)
const goto_programt & goto_program
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett get_cases(goto_programt::const_targett target, goto_programt::const_targett upper_bound, const exprt &switch_var, cases_listt &cases, goto_programt::const_targett &first_target, goto_programt::const_targett &default_target)
void cleanup_code_block(codet &code, const irep_idt parent_stmt)
std::list< caset > cases_listt
void copy_source_location(goto_programt::const_targett, codet &dst)
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
goto_programt::const_targett convert_throw(goto_programt::const_targett target, code_blockt &dest)
std::unordered_set< irep_idt > const_removed
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void remove_const(typet &type)
std::list< std::pair< goto_programt::const_targett, bool > > loop_last_stackt
std::unordered_set< exprt, irep_hash > va_list_expr
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void add_local_types(const typet &type)
void cleanup_expr(exprt &expr, bool no_typecast)
void cleanup_code(codet &code, const irep_idt parent_stmt)
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
void convert_assign_rec(const code_assignt &assign, code_blockt &dest)
std::unordered_set< irep_idt > labels_in_use
std::unordered_map< irep_idt, unsigned > dead_mapt
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
std::set< std::string > & system_headers
const namespacet ns
code_blockt & toplevel_block
const std::unordered_set< irep_idt > & typedef_names
const irep_idt & func_name
goto_programt::const_targett convert_set_return_value(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
Compute natural loops in a goto_function.
goto_programt::const_targett case_start
caset(const goto_programt &goto_program, const exprt &v, goto_programt::const_targett sel, goto_programt::const_targett st)
goto_programt::const_targett case_selector
goto_programt::const_targett case_last