cprover
dump_c_class.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_DUMP_C_CLASS_H
13 #define CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
14 
15 #include <set>
16 #include <string>
17 
19 
22 {
25 
28 
30  bool include_global_decls = true;
31 
33  bool include_typedefs = true;
34 
36  bool include_global_vars = true;
37 
39  bool include_compounds = true;
40 
42  bool follow_compounds = true;
43 
45  bool include_headers = false;
46 
48  {
49  }
50 
53 
56 
58  {
59  this->include_function_decls = false;
60  return *this;
61  }
62 
64  {
65  this->include_function_bodies = false;
66  return *this;
67  }
68 
70  {
71  this->include_global_decls = false;
72  return *this;
73  }
74 
76  {
77  this->include_typedefs = false;
78  return *this;
79  }
80 
82  {
83  this->include_global_vars = false;
84  return *this;
85  }
86 
88  {
89  this->include_compounds = false;
90  return *this;
91  }
92 
94  {
95  this->follow_compounds = false;
96  return *this;
97  }
98 
100  {
101  this->include_headers = true;
102  return *this;
103  }
104 };
105 
106 class dump_ct
107 {
108 public:
110  const goto_functionst &_goto_functions,
111  const bool use_system_headers,
112  const bool use_all_headers,
113  const bool include_harness,
114  const namespacet &_ns,
115  const irep_idt &mode,
117  : goto_functions(_goto_functions),
118  copied_symbol_table(_ns.get_symbol_table()),
121  mode(mode),
122  harness(include_harness),
123  system_symbols(use_system_headers)
124  {
125  system_symbols.set_use_all_headers(use_all_headers);
126  }
127 
129  const goto_functionst &_goto_functions,
130  const bool use_system_headers,
131  const bool use_all_headers,
132  const bool include_harness,
133  const namespacet &_ns,
134  const irep_idt &mode)
135  : dump_ct(
136  _goto_functions,
137  use_system_headers,
138  use_all_headers,
139  include_harness,
140  _ns,
141  mode,
142  dump_c_configurationt::default_configuration)
143  {
144  }
145 
146  virtual ~dump_ct()=default;
147 
148  void operator()(std::ostream &out);
149 
150 protected:
153  const namespacet ns;
155  const irep_idt mode;
156  const bool harness;
157 
158  typedef std::unordered_set<irep_idt> convertedt;
160 
161  std::set<std::string> system_headers;
162 
164 
165  typedef std::unordered_map<irep_idt, irep_idt> declared_enum_constants_mapt;
167 
169  {
171  std::string type_decl_str;
172  bool early;
173  std::unordered_set<irep_idt> dependencies;
174 
175  explicit typedef_infot(const irep_idt &name):
176  typedef_name(name),
177  early(false)
178  {
179  }
180  };
181  typedef std::map<irep_idt, typedef_infot> typedef_mapt;
183  typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
185 
186  std::string type_to_string(const typet &type);
187  std::string expr_to_string(const exprt &expr);
188 
189  static std::string indent(const unsigned n)
190  {
191  return std::string(2*n, ' ');
192  }
193 
194  std::string make_decl(
195  const irep_idt &identifier,
196  const typet &type)
197  {
198  symbol_exprt sym(identifier, type);
199  code_declt d(sym);
200 
201  std::string d_str=expr_to_string(d);
202  assert(!d_str.empty());
203  assert(*d_str.rbegin()==';');
204 
205  return d_str.substr(0, d_str.size()-1);
206  }
207 
208  void collect_typedefs(const typet &type, bool early);
210  const typet &type,
211  bool early,
212  std::unordered_set<irep_idt> &dependencies);
213  void gather_global_typedefs();
214  void dump_typedefs(std::ostream &os) const;
215 
217  const symbolt &symbol,
218  std::ostream &os_body);
219  void convert_compound(
220  const typet &type,
221  const typet &unresolved,
222  bool recursive,
223  std::ostream &os);
224  void convert_compound(
225  const struct_union_typet &type,
226  const typet &unresolved,
227  bool recursive,
228  std::ostream &os);
230  const typet &type,
231  std::ostream &os);
232 
233  typedef std::unordered_map<irep_idt, code_declt> local_static_declst;
234 
236  const symbolt &symbol,
237  std::ostream &os,
238  local_static_declst &local_static_decls);
239 
241  const symbolt &symbol,
242  const bool skip_main,
243  std::ostream &os_decl,
244  std::ostream &os_body,
245  local_static_declst &local_static_decls);
246 
248  code_blockt &b,
249  const std::list<irep_idt> &local_static,
250  local_static_declst &local_static_decls,
251  std::list<irep_idt> &type_decls);
252 
254  code_blockt &b,
255  const std::list<irep_idt> &type_decls);
256 
257  void cleanup_expr(exprt &expr);
258  void cleanup_type(typet &type);
259  void cleanup_decl(
260  code_declt &decl,
261  std::list<irep_idt> &local_static,
262  std::list<irep_idt> &local_type_decls);
263  void cleanup_harness(code_blockt &b);
264 };
265 
266 #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_CLASS_H
A codet representing sequential composition of program statements.
Definition: std_code.h:170
A codet representing the declaration of a local variable.
Definition: std_code.h:402
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
std::unordered_set< irep_idt > convertedt
Definition: dump_c_class.h:158
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:341
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:373
const namespacet ns
Definition: dump_c_class.h:153
virtual ~dump_ct()=default
void insert_local_type_decls(code_blockt &b, const std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1231
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1272
void insert_local_static_decls(code_blockt &b, const std::list< irep_idt > &local_static, local_static_declst &local_static_decls, std::list< irep_idt > &type_decls)
Definition: dump_c.cpp:1197
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1562
void operator()(std::ostream &out)
Definition: dump_c.cpp:47
const goto_functionst & goto_functions
Definition: dump_c_class.h:151
convertedt converted_compound
Definition: dump_c_class.h:159
void collect_typedefs(const typet &type, bool early)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
Definition: dump_c.cpp:692
dump_ct(const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &_ns, const irep_idt &mode)
Definition: dump_c_class.h:128
void gather_global_typedefs()
Find all global typdefs in the symbol table and store them in typedef_types.
Definition: dump_c.cpp:782
typedef_typest typedef_types
Definition: dump_c_class.h:184
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:152
typedef_mapt typedef_map
Definition: dump_c_class.h:182
void cleanup_decl(code_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)
Definition: dump_c.cpp:648
void collect_typedefs_rec(const typet &type, bool early, std::unordered_set< irep_idt > &dependencies)
Find any typedef names contained in the input type and store their declaration strings in typedef_map...
Definition: dump_c.cpp:705
std::unordered_map< irep_idt, code_declt > local_static_declst
Definition: dump_c_class.h:233
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:166
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:194
convertedt converted_enum
Definition: dump_c_class.h:159
const irep_idt mode
Definition: dump_c_class.h:155
void convert_global_variable(const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)
Definition: dump_c.cpp:898
std::set< std::string > system_headers
Definition: dump_c_class.h:161
void dump_typedefs(std::ostream &os) const
Print all typedefs that are not covered via typedef struct xyz { ...
Definition: dump_c.cpp:813
const bool harness
Definition: dump_c_class.h:156
system_library_symbolst system_symbols
Definition: dump_c_class.h:163
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:605
std::unordered_map< irep_idt, irep_idt > declared_enum_constants_mapt
Definition: dump_c_class.h:165
std::map< irep_idt, typedef_infot > typedef_mapt
Definition: dump_c_class.h:181
const dump_c_configurationt dump_c_config
Definition: dump_c_class.h:154
void cleanup_harness(code_blockt &b)
Replace CPROVER internal symbols in b by printable values and generate necessary declarations.
Definition: dump_c.cpp:968
void cleanup_type(typet &type)
Definition: dump_c.cpp:1505
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1548
std::unordered_map< typet, irep_idt, irep_hash > typedef_typest
Definition: dump_c_class.h:183
static std::string indent(const unsigned n)
Definition: dump_c_class.h:189
void convert_function_declaration(const symbolt &symbol, const bool skip_main, std::ostream &os_decl, std::ostream &os_body, local_static_declst &local_static_decls)
Definition: dump_c.cpp:1023
dump_ct(const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &_ns, const irep_idt &mode, const dump_c_configurationt config)
Definition: dump_c_class.h:109
convertedt converted_global
Definition: dump_c_class.h:159
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Base type for structs and unions.
Definition: std_types.h:57
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:28
configt config
Definition: config.cpp:24
Used for configuring the behaviour of dump_c.
Definition: dump_c_class.h:22
dump_c_configurationt disable_include_function_decls()
Definition: dump_c_class.h:57
dump_c_configurationt disable_include_typedefs()
Definition: dump_c_class.h:75
dump_c_configurationt disable_follow_compounds()
Definition: dump_c_class.h:93
bool include_global_decls
Include the global declarations in the dump.
Definition: dump_c_class.h:30
bool include_typedefs
Include the typedefs in the dump.
Definition: dump_c_class.h:33
bool include_global_vars
Include global variable definitions in the dump.
Definition: dump_c_class.h:36
static dump_c_configurationt default_configuration
The default used for dump-c and dump-cpp.
Definition: dump_c_class.h:52
bool include_function_decls
Include the function declarations in the dump.
Definition: dump_c_class.h:24
bool include_headers
Include headers type declarations are borrowed from.
Definition: dump_c_class.h:45
bool include_compounds
Include struct definitions in the dump.
Definition: dump_c_class.h:39
dump_c_configurationt disable_include_global_vars()
Definition: dump_c_class.h:81
dump_c_configurationt disable_include_compunds()
Definition: dump_c_class.h:87
static dump_c_configurationt type_header_configuration
The config used for dump-c-type-header.
Definition: dump_c_class.h:55
dump_c_configurationt disable_include_function_bodies()
Definition: dump_c_class.h:63
dump_c_configurationt disable_include_global_decls()
Definition: dump_c_class.h:69
dump_c_configurationt enable_include_headers()
Definition: dump_c_class.h:99
bool include_function_bodies
Include the functions in the dump.
Definition: dump_c_class.h:27
bool follow_compounds
Define whether to follow compunds recursively.
Definition: dump_c_class.h:42
typedef_infot(const irep_idt &name)
Definition: dump_c_class.h:175
std::unordered_set< irep_idt > dependencies
Definition: dump_c_class.h:173
std::string type_decl_str
Definition: dump_c_class.h:171