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 
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 
49 public:
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 
80 protected:
84  const namespacet ns;
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 
113  void cleanup_code_block(
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 
129  goto_programt::const_targett upper_bound,
130  code_blockt &dest);
131 
133 
136  goto_programt::const_targett upper_bound,
137  code_blockt &dest);
138 
141  goto_programt::const_targett upper_bound,
142  code_blockt &dest);
143 
144  void convert_assign_rec(const code_assignt &assign, code_blockt &dest);
145 
148  goto_programt::const_targett upper_bound,
149  code_blockt &dest);
150 
153  goto_programt::const_targett upper_bound,
154  code_blockt &dest);
155 
159  code_blockt &dest);
160 
163  goto_programt::const_targett upper_bound,
164  code_blockt &dest);
165 
169  code_blockt &dest);
170 
173  goto_programt::const_targett upper_bound,
174  code_blockt &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  code_blockt &dest);
199 
202  goto_programt::const_targett upper_bound,
203  code_blockt &dest);
204 
207 
210  goto_programt::const_targett upper_bound,
211  code_blockt &dest);
212 
215 
218  goto_programt::const_targett upper_bound,
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
exprt::operandst argumentst
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
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
natural_loopst loops
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.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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>
Definition: natural_loops.h:86
The symbol table.
Definition: symbol_table.h:14
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