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