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