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::unordered_set<irep_idt, irep_id_hash> id_sett;
24  typedef std::map<goto_programt::const_targett, goto_programt::const_targett>
26  typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> dead_mapt;
27  typedef std::list<std::pair<goto_programt::const_targett, bool> >
29 
30  struct caset
31  {
32  const exprt value; // condition upon which this case is taken
35  goto_programt::const_targett case_last; // last instruction of case
36 
38  const exprt &v,
41  value(v), case_selector(sel), case_start(st),
42  case_last(goto_program.instructions.end())
43  {
44  }
45  };
46  typedef std::list<caset> cases_listt;
47 
48 public:
50  const irep_idt &identifier,
51  const goto_programt &_goto_program,
52  symbol_tablet &_symbol_table,
53  code_blockt &_dest,
54  id_listt &_local_static,
55  id_listt &_type_names,
56  const id_sett &_typedef_names,
57  std::set<std::string> &_system_headers):
58  func_name(identifier),
59  goto_program(_goto_program),
60  symbol_table(_symbol_table),
61  ns(_symbol_table),
62  toplevel_block(_dest),
63  local_static(_local_static),
64  type_names(_type_names),
65  typedef_names(_typedef_names),
66  system_headers(_system_headers)
67  {
68  assert(local_static.empty());
69 
70  for(id_listt::const_iterator
71  it=type_names.begin();
72  it!=type_names.end();
73  ++it)
74  type_names_set.insert(*it);
75  }
76 
77  void operator()();
78 
79 protected:
83  const namespacet ns;
85  id_listt &local_static;
86  id_listt &type_names;
87  const id_sett &typedef_names;
88  std::set<std::string> &system_headers;
89  std::unordered_set<exprt, irep_hash> va_list_expr;
90 
93  id_sett labels_in_use;
94  dead_mapt dead_map;
97  id_sett type_names_set;
98  id_sett const_removed;
99 
100  void build_loop_map();
101  void build_dead_map();
102  void scan_for_varargs();
103 
104  void cleanup_code(codet &code, const irep_idt parent_stmt);
105 
107  const exprt &function,
109 
110  void cleanup_code_block(
111  codet &code,
112  const irep_idt parent_stmt);
113 
115  codet &code,
116  const irep_idt parent_stmt);
117 
118  void cleanup_expr(exprt &expr, bool no_typecast);
119 
120  void add_local_types(const typet &type);
121 
122  void remove_const(typet &type);
123 
126  goto_programt::const_targett upper_bound,
127  codet &dest);
128 
129  void convert_labels(
131  codet &dest);
132 
135  goto_programt::const_targett upper_bound,
136  codet &dest);
137 
140  goto_programt::const_targett upper_bound,
141  codet &dest);
142 
143  void convert_assign_rec(
144  const code_assignt &assign,
145  codet &dest);
146 
149  goto_programt::const_targett upper_bound,
150  codet &dest);
151 
154  goto_programt::const_targett upper_bound,
155  codet &dest);
156 
160  codet &dest);
161 
164  goto_programt::const_targett upper_bound,
165  codet &dest);
166 
170  codet &dest);
171 
174  goto_programt::const_targett upper_bound,
175  codet &dest);
176 
179  goto_programt::const_targett upper_bound,
180  const exprt &switch_var,
181  cases_listt &cases,
182  goto_programt::const_targett &first_target,
183  goto_programt::const_targett &default_target);
184 
186  goto_programt::const_targett upper_bound,
187  const cfg_dominatorst &dominators,
188  cases_listt &cases,
189  std::set<unsigned> &processed_locations);
190 
191  bool remove_default(
192  const cfg_dominatorst &dominators,
193  const cases_listt &cases,
194  goto_programt::const_targett default_target);
195 
198  goto_programt::const_targett upper_bound,
199  codet &dest);
200 
203  goto_programt::const_targett upper_bound,
204  codet &dest);
205 
208  codet &dest);
209 
212  goto_programt::const_targett upper_bound,
213  codet &dest);
214 
217  codet &dest);
218 
221  goto_programt::const_targett upper_bound,
222  codet &dest);
223 };
224 
225 #endif // CPROVER_GOTO_INSTRUMENT_GOTO_PROGRAM2CODE_H
const goto_programt & goto_program
The type of an expression.
Definition: type.h:20
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)
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)
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:687
goto_programt::const_targett convert_catch(goto_programt::const_targett target, goto_programt::const_targett upper_bound, codet &dest)
const id_sett & 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
instructionst::const_iterator const_targett
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:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::unordered_set< irep_idt, irep_id_hash > id_sett
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)
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 id_sett &_typedef_names, std::set< std::string > &_system_headers)
void cleanup_function_call(const exprt &function, code_function_callt::argumentst &arguments)
code_blockt & toplevel_block
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
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:46
goto_programt::const_targett case_selector
goto_programt::const_targett case_start
Sequential composition.
Definition: std_code.h:63
std::unordered_map< irep_idt, unsigned, irep_id_hash > dead_mapt
natural_loopst loops
Compute natural loops in a goto_function.
A statement in a programming language.
Definition: std_code.h:19
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)
Assignment.
Definition: std_code.h:144
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)