cprover
goto_program2code.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dump Goto-Program as C/C++ Source
4 
5 Author: 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 
18 #include <analyses/natural_loops.h>
19 
21 {
22  typedef std::list<irep_idt> id_listt;
23  typedef std::map<goto_programt::const_targett, goto_programt::const_targett>
25  typedef std::unordered_map<irep_idt, unsigned> dead_mapt;
26  typedef std::list<std::pair<goto_programt::const_targett, bool> >
28 
29  struct caset
30  {
31  const exprt value; // condition upon which this case is taken
34  goto_programt::const_targett case_last; // last instruction of case
35 
37  const exprt &v,
40  value(v), case_selector(sel), case_start(st),
41  case_last(goto_program.instructions.end())
42  {
43  }
44  };
45  typedef std::list<caset> cases_listt;
46 
47 public:
49  const irep_idt &identifier,
50  const goto_programt &_goto_program,
51  symbol_tablet &_symbol_table,
52  code_blockt &_dest,
53  id_listt &_local_static,
54  id_listt &_type_names,
55  const std::unordered_set<irep_idt> &_typedef_names,
56  std::set<std::string> &_system_headers)
57  : func_name(identifier),
58  goto_program(_goto_program),
59  symbol_table(_symbol_table),
60  ns(_symbol_table),
61  toplevel_block(_dest),
62  local_static(_local_static),
63  type_names(_type_names),
64  typedef_names(_typedef_names),
65  system_headers(_system_headers)
66  {
67  assert(local_static.empty());
68 
69  for(id_listt::const_iterator
70  it=type_names.begin();
71  it!=type_names.end();
72  ++it)
73  type_names_set.insert(*it);
74  }
75 
76  void operator()();
77 
78 protected:
82  const namespacet ns;
86  const std::unordered_set<irep_idt> &typedef_names;
87  std::set<std::string> &system_headers;
88  std::unordered_set<exprt, irep_hash> va_list_expr;
89 
92  std::unordered_set<irep_idt> labels_in_use;
95  std::unordered_set<irep_idt> local_static_set;
96  std::unordered_set<irep_idt> type_names_set;
97  std::unordered_set<irep_idt> const_removed;
98 
100 
101  void build_loop_map();
102  void build_dead_map();
103  void scan_for_varargs();
104 
105  void cleanup_code(codet &code, const irep_idt parent_stmt);
106 
108  const exprt &function,
110 
111  void cleanup_code_block(
112  codet &code,
113  const irep_idt parent_stmt);
114 
116  codet &code,
117  const irep_idt parent_stmt);
118 
119  void cleanup_expr(exprt &expr, bool no_typecast);
120 
121  void add_local_types(const typet &type);
122 
123  void remove_const(typet &type);
124 
127  goto_programt::const_targett upper_bound,
128  code_blockt &dest);
129 
131 
134  goto_programt::const_targett upper_bound,
135  code_blockt &dest);
136 
139  goto_programt::const_targett upper_bound,
140  code_blockt &dest);
141 
142  void convert_assign_rec(const code_assignt &assign, code_blockt &dest);
143 
146  goto_programt::const_targett upper_bound,
147  code_blockt &dest);
148 
151  goto_programt::const_targett upper_bound,
152  code_blockt &dest);
153 
157  code_blockt &dest);
158 
161  goto_programt::const_targett upper_bound,
162  code_blockt &dest);
163 
167  code_blockt &dest);
168 
171  goto_programt::const_targett upper_bound,
172  code_blockt &dest);
173 
176  goto_programt::const_targett upper_bound,
177  const exprt &switch_var,
178  cases_listt &cases,
179  goto_programt::const_targett &first_target,
180  goto_programt::const_targett &default_target);
181 
183  goto_programt::const_targett upper_bound,
184  const cfg_dominatorst &dominators,
185  cases_listt &cases,
186  std::set<unsigned> &processed_locations);
187 
188  bool remove_default(
189  const cfg_dominatorst &dominators,
190  const cases_listt &cases,
191  goto_programt::const_targett default_target);
192 
195  goto_programt::const_targett upper_bound,
196  code_blockt &dest);
197 
200  goto_programt::const_targett upper_bound,
201  code_blockt &dest);
202 
205 
208  goto_programt::const_targett upper_bound,
209  code_blockt &dest);
210 
213 
216  goto_programt::const_targett upper_bound,
217  code_blockt &dest);
218 };
219 
220 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H
goto_program2codet::caset::caset
caset(const goto_programt &goto_program, const exprt &v, goto_programt::const_targett sel, goto_programt::const_targett st)
Definition: goto_program2code.h:36
goto_program2codet::caset::value
const exprt value
Definition: goto_program2code.h:31
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
goto_program2codet::va_list_expr
std::unordered_set< exprt, irep_hash > va_list_expr
Definition: goto_program2code.h:88
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_program2codet::cleanup_code_ifthenelse
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
Definition: goto_program2code.cpp:1636
goto_program2codet::remove_default
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
Definition: goto_program2code.cpp:793
goto_program2codet::convert_goto_break_continue
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:1097
goto_program2codet::loopt
std::map< goto_programt::const_targett, goto_programt::const_targett > loopt
Definition: goto_program2code.h:24
goto_program2codet::cleanup_function_call
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
Definition: goto_program2code.cpp:1480
goto_program2codet::convert_goto
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:527
typet
The type of an expression, extends irept.
Definition: type.h:29
goto_program2codet::convert_assign_rec
void convert_assign_rec(const code_assignt &assign, code_blockt &dest)
Definition: goto_program2code.cpp:386
goto_program2codet::const_removed
std::unordered_set< irep_idt > const_removed
Definition: goto_program2code.h:97
goto_program2codet::caset
Definition: goto_program2code.h:30
goto_program2codet::copy_source_location
void copy_source_location(goto_programt::const_targett, codet &dst)
Definition: goto_program2code.cpp:1941
goto_program2codet::loops
natural_loopst loops
Definition: goto_program2code.h:90
goto_program2codet::cleanup_expr
void cleanup_expr(exprt &expr, bool no_typecast)
Definition: goto_program2code.cpp:1726
goto_program2codet::labels_in_use
std::unordered_set< irep_idt > labels_in_use
Definition: goto_program2code.h:92
goto_program2codet::convert_instruction
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:127
exprt
Base class for all expressions.
Definition: expr.h:53
goto_program2codet::local_static_set
std::unordered_set< irep_idt > local_static_set
Definition: goto_program2code.h:95
goto_program2codet::type_names_set
std::unordered_set< irep_idt > type_names_set
Definition: goto_program2code.h:96
goto_program2codet::goto_program2codet
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)
Definition: goto_program2code.h:48
goto_program2codet::convert_catch
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:1344
goto_program2codet::add_local_types
void add_local_types(const typet &type)
Definition: goto_program2code.cpp:1354
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_program2codet::toplevel_block
code_blockt & toplevel_block
Definition: goto_program2code.h:83
goto_program2codet::convert_start_thread
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:1223
goto_program2codet::build_dead_map
void build_dead_map()
Definition: goto_program2code.cpp:87
goto_program2codet::convert_goto_if
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:1020
goto_program2codet::func_name
const irep_idt & func_name
Definition: goto_program2code.h:79
goto_program2codet::convert_goto_goto
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, code_blockt &dest)
Definition: goto_program2code.cpp:1168
goto_program2codet::ns
const namespacet ns
Definition: goto_program2code.h:82
goto_program2codet::type_names
id_listt & type_names
Definition: goto_program2code.h:85
goto_program2codet::cleanup_code
void cleanup_code(codet &code, const irep_idt parent_stmt)
Definition: goto_program2code.cpp:1392
goto_program2codet::loop_last_stack
loop_last_stackt loop_last_stack
Definition: goto_program2code.h:94
natural_loopst
A concretized version of natural_loops_templatet<const goto_programt, goto_programt::const_targett>
Definition: natural_loops.h:86
goto_program2codet::convert_decl
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:440
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1192
goto_program2codet::scan_for_varargs
void scan_for_varargs()
Definition: goto_program2code.cpp:97
goto_program2codet::dead_mapt
std::unordered_map< irep_idt, unsigned > dead_mapt
Definition: goto_program2code.h:25
goto_program2codet::get_cases
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)
Definition: goto_program2code.cpp:640
goto_program2codet::dead_map
dead_mapt dead_map
Definition: goto_program2code.h:93
goto_program2codet::loop_last_stackt
std::list< std::pair< goto_programt::const_targett, bool > > loop_last_stackt
Definition: goto_program2code.h:27
goto_program2codet::goto_program
const goto_programt & goto_program
Definition: goto_program2code.h:80
goto_program2codet::caset::case_start
goto_programt::const_targett case_start
Definition: goto_program2code.h:33
goto_program2codet::convert_labels
void convert_labels(goto_programt::const_targett target, code_blockt &dest)
Definition: goto_program2code.cpp:232
goto_program2codet::convert_assign_varargs
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:292
goto_program2codet::symbol_table
symbol_tablet & symbol_table
Definition: goto_program2code.h:81
goto_program2codet::convert_throw
goto_programt::const_targett convert_throw(goto_programt::const_targett target, code_blockt &dest)
Definition: goto_program2code.cpp:1335
natural_loops.h
Compute natural loops in a goto_function.
goto_program2codet::convert_return
goto_programt::const_targett convert_return(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:408
goto_program2codet::convert_goto_switch
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:850
goto_program2codet
Definition: goto_program2code.h:21
goto_program2codet::id_listt
std::list< irep_idt > id_listt
Definition: goto_program2code.h:22
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_program2codet::operator()
void operator()()
Definition: goto_program2code.cpp:24
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_program2codet::caset::case_last
goto_programt::const_targett case_last
Definition: goto_program2code.h:34
goto_program2codet::local_static
id_listt & local_static
Definition: goto_program2code.h:84
goto_program2codet::set_block_end_points
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
Definition: goto_program2code.cpp:742
goto_program2codet::system_headers
std::set< std::string > & system_headers
Definition: goto_program2code.h:87
goto_program2codet::loop_map
loopt loop_map
Definition: goto_program2code.h:91
goto_program2codet::remove_const
void remove_const(typet &type)
Definition: goto_program2code.cpp:1562
goto_program2codet::convert_goto_while
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
Definition: goto_program2code.cpp:550
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_program2codet::caset::case_selector
goto_programt::const_targett case_selector
Definition: goto_program2code.h:32
goto_program2codet::convert_do_while
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)
Definition: goto_program2code.cpp:502
goto_program2codet::cleanup_code_block
void cleanup_code_block(codet &code, const irep_idt parent_stmt)
Definition: goto_program2code.cpp:1510
goto_program2codet::cases_listt
std::list< caset > cases_listt
Definition: goto_program2code.h:45
goto_program2codet::typedef_names
const std::unordered_set< irep_idt > & typedef_names
Definition: goto_program2code.h:86
goto_program2codet::convert_assign
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)
Definition: goto_program2code.cpp:277
goto_program2codet::build_loop_map
void build_loop_map()
Definition: goto_program2code.cpp:51
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false >
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35