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 
99  void build_loop_map();
100  void build_dead_map();
101  void scan_for_varargs();
102 
103  void cleanup_code(codet &code, const irep_idt parent_stmt);
104 
106  const exprt &function,
108 
109  void cleanup_code_block(
110  codet &code,
111  const irep_idt parent_stmt);
112 
114  codet &code,
115  const irep_idt parent_stmt);
116 
117  void cleanup_expr(exprt &expr, bool no_typecast);
118 
119  void add_local_types(const typet &type);
120 
121  void remove_const(typet &type);
122 
125  goto_programt::const_targett upper_bound,
126  codet &dest);
127 
128  void convert_labels(
130  codet &dest);
131 
134  goto_programt::const_targett upper_bound,
135  codet &dest);
136 
139  goto_programt::const_targett upper_bound,
140  codet &dest);
141 
142  void convert_assign_rec(
143  const code_assignt &assign,
144  codet &dest);
145 
148  goto_programt::const_targett upper_bound,
149  codet &dest);
150 
153  goto_programt::const_targett upper_bound,
154  codet &dest);
155 
159  codet &dest);
160 
163  goto_programt::const_targett upper_bound,
164  codet &dest);
165 
169  codet &dest);
170 
173  goto_programt::const_targett upper_bound,
174  codet &dest);
175 
178  goto_programt::const_targett upper_bound,
179  const exprt &switch_var,
180  cases_listt &cases,
181  goto_programt::const_targett &first_target,
182  goto_programt::const_targett &default_target);
183 
185  goto_programt::const_targett upper_bound,
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 
197  goto_programt::const_targett upper_bound,
198  codet &dest);
199 
202  goto_programt::const_targett upper_bound,
203  codet &dest);
204 
207  codet &dest);
208 
211  goto_programt::const_targett upper_bound,
212  codet &dest);
213 
216  codet &dest);
217 
220  goto_programt::const_targett upper_bound,
221  codet &dest);
222 };
223 
224 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H
const goto_programt & goto_program
The type of an expression.
Definition: type.h:22
goto_programt::const_targett convert_do_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, codet &dest)
goto_programt::const_targett convert_instruction(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_switch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
bool remove_default(const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)
void cleanup_code_ifthenelse(codet &code, const irep_idt parent_stmt)
void convert_assign_rec(const code_assignt &assign, codet &dest)
std::unordered_set< irep_idt > labels_in_use
caset(const goto_programt &goto_program, const exprt &v, goto_programt::const_targett sel, goto_programt::const_targett st)
std::map< goto_programt::const_targett, goto_programt::const_targett > loopt
void convert_labels(goto_programt::const_targett target, codet &dest)
goto_programt::const_targett convert_assign(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_start_thread(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
std::unordered_set< irep_idt > type_names_set
goto_programt::const_targett convert_goto_if(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
goto_programt::const_targett convert_goto_goto(goto_programt::const_targett target, codet &dest)
exprt::operandst argumentst
Definition: std_code.h:858
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
std::unordered_set< irep_idt > const_removed
std::unordered_set< irep_idt > local_static_set
const std::unordered_set< irep_idt > & typedef_names
goto_programt::const_targett convert_goto_break_continue(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const namespacet ns
loop_last_stackt loop_last_stack
goto_programt::const_targett convert_decl(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void cleanup_code(codet &code, const irep_idt parent_stmt)
void add_local_types(const typet &type)
goto_programt::const_targett convert_goto_while(goto_programt::const_targett target, goto_programt::const_targett loop_end, codet &dest)
goto_programt::const_targett convert_assign_varargs(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void cleanup_expr(exprt &expr, bool no_typecast)
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::set< std::string > & system_headers
std::list< irep_idt > id_listt
bool set_block_end_points(goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
code_blockt & toplevel_block
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
goto_programt::const_targett convert_return(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const irep_idt & func_name
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)
goto_programt::const_targett convert_throw(goto_programt::const_targett target, codet &dest)
std::list< std::pair< goto_programt::const_targett, bool > > loop_last_stackt
Base class for all expressions.
Definition: expr.h:42
std::unordered_map< irep_idt, unsigned > dead_mapt
goto_programt::const_targett case_selector
goto_programt::const_targett case_start
Sequential composition.
Definition: std_code.h:88
natural_loopst loops
Compute natural loops in a goto_function.
A statement in a programming language.
Definition: std_code.h:21
std::list< caset > cases_listt
goto_programt::const_targett convert_goto(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
void remove_const(typet &type)
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)
Assignment.
Definition: std_code.h:195
std::unordered_set< exprt, irep_hash > va_list_expr
symbol_tablet & symbol_table
goto_programt::const_targett case_last
void cleanup_code_block(codet &code, const irep_idt parent_stmt)