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