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 
24 class dump_ct
25 {
26 public:
28  const goto_functionst &_goto_functions,
29  const bool use_system_headers,
30  const bool use_all_headers,
31  const bool include_harness,
32  const namespacet &_ns,
33  language_factoryt factory):
34  goto_functions(_goto_functions),
35  copied_symbol_table(_ns.get_symbol_table()),
37  language(factory()),
38  harness(include_harness),
39  system_symbols(use_system_headers)
40  {
41  system_symbols.set_use_all_headers(use_all_headers);
42  }
43 
44  virtual ~dump_ct()=default;
45 
46  void operator()(std::ostream &out);
47 
48 protected:
51  const namespacet ns;
52  std::unique_ptr<languaget> language;
53  const bool harness;
54 
55  typedef std::unordered_set<irep_idt> convertedt;
57 
58  std::set<std::string> system_headers;
59 
61 
62  typedef std::unordered_map<irep_idt, irep_idt> declared_enum_constants_mapt;
64 
66  {
68  std::string type_decl_str;
69  bool early;
70  std::unordered_set<irep_idt> dependencies;
71 
72  explicit typedef_infot(const irep_idt &name):
73  typedef_name(name),
74  type_decl_str(""),
75  early(false)
76  {
77  }
78  };
79  typedef std::map<irep_idt, typedef_infot> typedef_mapt;
81  typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
83 
84  std::string type_to_string(const typet &type);
85  std::string expr_to_string(const exprt &expr);
86 
87  static std::string indent(const unsigned n)
88  {
89  return std::string(2*n, ' ');
90  }
91 
92  std::string make_decl(
93  const irep_idt &identifier,
94  const typet &type)
95  {
96  symbol_exprt sym(identifier, type);
97  code_declt d(sym);
98 
99  std::string d_str=expr_to_string(d);
100  assert(!d_str.empty());
101  assert(*d_str.rbegin()==';');
102 
103  return d_str.substr(0, d_str.size()-1);
104  }
105 
106  void collect_typedefs(const typet &type, bool early);
108  const typet &type,
109  bool early,
110  std::unordered_set<irep_idt> &dependencies);
111  void gather_global_typedefs();
112  void dump_typedefs(std::ostream &os) const;
113 
115  const symbolt &symbol,
116  std::ostream &os_body);
117  void convert_compound(
118  const typet &type,
119  const typet &unresolved,
120  bool recursive,
121  std::ostream &os);
122  void convert_compound(
123  const struct_union_typet &type,
124  const typet &unresolved,
125  bool recursive,
126  std::ostream &os);
128  const typet &type,
129  std::ostream &os);
130 
131  typedef std::unordered_map<irep_idt, code_declt> local_static_declst;
132 
134  const symbolt &symbol,
135  std::ostream &os,
136  local_static_declst &local_static_decls);
137 
139  const symbolt &symbol,
140  const bool skip_main,
141  std::ostream &os_decl,
142  std::ostream &os_body,
143  local_static_declst &local_static_decls);
144 
146  code_blockt &b,
147  const std::list<irep_idt> &local_static,
148  local_static_declst &local_static_decls,
149  std::list<irep_idt> &type_decls);
150 
152  code_blockt &b,
153  const std::list<irep_idt> &type_decls);
154 
155  void cleanup_expr(exprt &expr);
156  void cleanup_type(typet &type);
157  void cleanup_decl(
158  code_declt &decl,
159  std::list<irep_idt> &local_static,
160  std::list<irep_idt> &local_type_decls);
161  void cleanup_harness(code_blockt &b);
162 };
163 
164 #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:62
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:150
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:646
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
dump_ct::indent
static std::string indent(const unsigned n)
Definition: dump_c_class.h:87
dump_ct::goto_functions
const goto_functionst & goto_functions
Definition: dump_c_class.h:49
system_library_symbolst
Definition: system_library_symbols.h:25
dump_ct::ns
const namespacet ns
Definition: dump_c_class.h:51
typet
The type of an expression, extends irept.
Definition: type.h:27
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:114
language_factoryt
std::unique_ptr< languaget >(* language_factoryt)()
Definition: mode.h:29
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
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:970
dump_ct::system_symbols
system_library_symbolst system_symbols
Definition: dump_c_class.h:60
exprt
Base class for all expressions.
Definition: expr.h:54
mode.h
dump_ct::language
std::unique_ptr< languaget > language
Definition: dump_c_class.h:52
dump_ct::convert_compound
void convert_compound(const typet &type, const typet &unresolved, bool recursive, std::ostream &os)
Definition: dump_c.cpp:310
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:27
dump_ct::typedef_map
typedef_mapt typedef_map
Definition: dump_c_class.h:80
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
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:1178
dump_ct::expr_to_string
std::string expr_to_string(const exprt &expr)
Definition: dump_c.cpp:1394
dump_ct::converted_compound
convertedt converted_compound
Definition: dump_c_class.h:56
dump_ct::harness
const bool harness
Definition: dump_c_class.h:53
dump_ct::system_headers
std::set< std::string > system_headers
Definition: dump_c_class.h:58
dump_ct::make_decl
std::string make_decl(const irep_idt &identifier, const typet &type)
Definition: dump_c_class.h:92
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:760
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
dump_ct::declared_enum_constants
declared_enum_constants_mapt declared_enum_constants
Definition: dump_c_class.h:63
dump_ct::converted_global
convertedt converted_global
Definition: dump_c_class.h:56
dump_ct::cleanup_type
void cleanup_type(typet &type)
Definition: dump_c.cpp:1359
dump_ct::typedef_mapt
std::map< irep_idt, typedef_infot > typedef_mapt
Definition: dump_c_class.h:79
system_library_symbols.h
dump_ct::convert_compound_enum
void convert_compound_enum(const typet &type, std::ostream &os)
Definition: dump_c.cpp:540
dump_ct::cleanup_expr
void cleanup_expr(exprt &expr)
Definition: dump_c.cpp:1215
dump_ct::local_static_declst
std::unordered_map< irep_idt, code_declt > local_static_declst
Definition: dump_c_class.h:131
dump_ct::typedef_infot::early
bool early
Definition: dump_c_class.h:69
dump_ct::convertedt
std::unordered_set< irep_idt > convertedt
Definition: dump_c_class.h:55
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:583
language.h
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:1144
dump_ct::operator()
void operator()(std::ostream &out)
Definition: dump_c.cpp:34
dump_ct::~dump_ct
virtual ~dump_ct()=default
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
system_library_symbolst::set_use_all_headers
void set_use_all_headers(bool use)
Definition: system_library_symbols.h:43
dump_ct::typedef_typest
std::unordered_map< typet, irep_idt, irep_hash > typedef_typest
Definition: dump_c_class.h:81
dump_ct::typedef_infot::dependencies
std::unordered_set< irep_idt > dependencies
Definition: dump_c_class.h:70
dump_ct::typedef_infot::typedef_name
irep_idt typedef_name
Definition: dump_c_class.h:67
symbolt
Symbol table entry.
Definition: symbol.h:27
dump_ct::copied_symbol_table
symbol_tablet copied_symbol_table
Definition: dump_c_class.h:50
dump_ct::typedef_infot::typedef_infot
typedef_infot(const irep_idt &name)
Definition: dump_c_class.h:72
dump_ct::typedef_infot
Definition: dump_c_class.h:65
dump_ct::typedef_types
typedef_typest typedef_types
Definition: dump_c_class.h:82
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:915
dump_ct::typedef_infot::type_decl_str
std::string type_decl_str
Definition: dump_c_class.h:68
dump_ct::convert_compound_declaration
void convert_compound_declaration(const symbolt &symbol, std::ostream &os_body)
declare compound types
Definition: dump_c.cpp:296
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:845
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:633
dump_ct
Definition: dump_c_class.h:24
dump_ct::type_to_string
std::string type_to_string(const typet &type)
Definition: dump_c.cpp:1385
dump_ct::converted_enum
convertedt converted_enum
Definition: dump_c_class.h:56
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:729