CBMC
cpp_language.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Module
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_language.h"
13 
14 #include <util/config.h>
15 #include <util/get_base_name.h>
16 #include <util/symbol_table.h>
17 
19 #include <ansi-c/c_preprocess.h>
20 #include <linking/linking.h>
22 
23 #include "cpp_internal_additions.h"
24 #include "cpp_parser.h"
25 #include "cpp_type2name.h"
26 #include "cpp_typecheck.h"
27 #include "expr2cpp.h"
28 
29 #include <cstring>
30 #include <fstream>
31 
32 std::set<std::string> cpp_languaget::extensions() const
33 {
34  std::set<std::string> s;
35 
36  s.insert("cpp");
37  s.insert("CPP");
38  s.insert("cc");
39  s.insert("cp");
40  s.insert("c++");
41  s.insert("ii");
42  s.insert("cxx");
43 
44  #ifndef _WIN32
45  s.insert("C");
46  #endif
47 
48  return s;
49 }
50 
51 void cpp_languaget::modules_provided(std::set<std::string> &modules)
52 {
53  modules.insert(get_base_name(parse_path, true));
54 }
55 
58  std::istream &instream,
59  const std::string &path,
60  std::ostream &outstream,
61  message_handlert &message_handler)
62 {
63  if(path.empty())
64  return c_preprocess(instream, outstream, message_handler);
65 
66  // check extension
67 
68  const char *ext=strrchr(path.c_str(), '.');
69  if(ext!=nullptr && std::string(ext)==".ipp")
70  {
71  std::ifstream infile(path);
72 
73  char ch;
74 
75  while(infile.read(&ch, 1))
76  outstream << ch;
77 
78  return false;
79  }
80 
81  return c_preprocess(path, outstream, message_handler);
82 }
83 
85  std::istream &instream,
86  const std::string &path,
87  message_handlert &message_handler)
88 {
89  // store the path
90 
91  parse_path=path;
92 
93  // preprocessing
94 
95  std::ostringstream o_preprocessed;
96 
97  cpp_internal_additions(o_preprocessed);
98 
99  if(preprocess(instream, path, o_preprocessed, message_handler))
100  return true;
101 
102  std::istringstream i_preprocessed(o_preprocessed.str());
103 
104  // parsing
105  cpp_parsert cpp_parser{message_handler};
106  cpp_parser.set_file(path);
107  cpp_parser.in=&i_preprocessed;
108  cpp_parser.mode=config.ansi_c.mode;
109 
110  bool result=cpp_parser.parse();
111 
112  // save result
113  cpp_parse_tree.swap(cpp_parser.parse_tree);
114 
115  return result;
116 }
117 
119  symbol_table_baset &symbol_table,
120  const std::string &module,
121  message_handlert &message_handler)
122 {
123  if(module.empty())
124  return false;
125 
126  symbol_tablet new_symbol_table;
127 
128  if(cpp_typecheck(cpp_parse_tree, new_symbol_table, module, message_handler))
129  return true;
130 
131  remove_internal_symbols(new_symbol_table, message_handler, false);
132 
133  return linking(symbol_table, new_symbol_table, message_handler);
134 }
135 
137  symbol_table_baset &symbol_table,
138  message_handlert &message_handler)
139 {
140  return ansi_c_entry_point(
141  symbol_table, message_handler, object_factory_params);
142 }
143 
144 void cpp_languaget::show_parse(std::ostream &out, message_handlert &)
145 {
146  for(const auto &i : cpp_parse_tree.items)
147  show_parse(out, i);
148 }
149 
151  std::ostream &out,
152  const cpp_itemt &item)
153 {
154  if(item.is_linkage_spec())
155  {
156  const cpp_linkage_spect &linkage_spec=
157  item.get_linkage_spec();
158 
159  out << "LINKAGE " << linkage_spec.linkage().get(ID_value) << ":\n";
160 
161  for(const auto &i : linkage_spec.items())
162  show_parse(out, i);
163 
164  out << '\n';
165  }
166  else if(item.is_namespace_spec())
167  {
168  const cpp_namespace_spect &namespace_spec=
169  item.get_namespace_spec();
170 
171  out << "NAMESPACE " << namespace_spec.get_namespace()
172  << ":\n";
173 
174  for(const auto &i : namespace_spec.items())
175  show_parse(out, i);
176 
177  out << '\n';
178  }
179  else if(item.is_using())
180  {
181  const cpp_usingt &cpp_using=item.get_using();
182 
183  out << "USING ";
184  if(cpp_using.get_namespace())
185  out << "NAMESPACE ";
186  out << cpp_using.name().pretty() << '\n';
187  out << '\n';
188  }
189  else if(item.is_declaration())
190  {
191  item.get_declaration().output(out);
192  }
193  else
194  out << "UNKNOWN: " << item.pretty() << '\n';
195 }
196 
197 std::unique_ptr<languaget> new_cpp_language()
198 {
199  return std::make_unique<cpp_languaget>();
200 }
201 
203  const exprt &expr,
204  std::string &code,
205  const namespacet &ns)
206 {
207  code=expr2cpp(expr, ns);
208  return false;
209 }
210 
212  const typet &type,
213  std::string &code,
214  const namespacet &ns)
215 {
216  code=type2cpp(type, ns);
217  return false;
218 }
219 
221  const typet &type,
222  std::string &name,
223  const namespacet &)
224 {
225  name=cpp_type2name(type);
226  return false;
227 }
228 
230  const std::string &code,
231  const std::string &,
232  exprt &expr,
233  const namespacet &ns,
234  message_handlert &message_handler)
235 {
236  expr.make_nil();
237 
238  // no preprocessing yet...
239 
240  std::istringstream i_preprocessed(code);
241 
242  // parsing
243  cpp_parsert cpp_parser{message_handler};
244  cpp_parser.set_file(irep_idt());
245  cpp_parser.in=&i_preprocessed;
246 
247  bool result=cpp_parser.parse();
248 
249  if(cpp_parser.parse_tree.items.empty())
250  result=true;
251  else
252  {
253  // TODO
254  // expr.swap(cpp_parser.parse_tree.declarations.front());
255 
256  // typecheck it
257  result = cpp_typecheck(expr, message_handler, ns);
258  }
259 
260  return result;
261 }
262 
264 {
265 }
bool ansi_c_entry_point(symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
configt config
Definition: config.cpp:25
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
struct configt::ansi_ct ansi_c
void output(std::ostream &out) const
bool is_namespace_spec() const
Definition: cpp_item.h:94
cpp_usingt & get_using()
Definition: cpp_item.h:107
cpp_linkage_spect & get_linkage_spec()
Definition: cpp_item.h:57
bool is_using() const
Definition: cpp_item.h:119
cpp_declarationt & get_declaration()
Definition: cpp_item.h:32
bool is_declaration() const
Definition: cpp_item.h:44
bool is_linkage_spec() const
Definition: cpp_item.h:69
cpp_namespace_spect & get_namespace_spec()
Definition: cpp_item.h:82
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
Formats the given type in a language-specific way.
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
Encodes the given type in a language-specific way.
c_object_factory_parameterst object_factory_params
Definition: cpp_language.h:104
std::string parse_path
Definition: cpp_language.h:102
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler) override
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override
ANSI-C preprocessing.
void show_parse(std::ostream &out, message_handlert &) override
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
std::set< std::string > extensions() const override
~cpp_languaget() override
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
void modules_provided(std::set< std::string > &modules) override
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns, message_handlert &message_handler) override
Parses the given string into an expression.
cpp_parse_treet cpp_parse_tree
Definition: cpp_language.h:101
const itemst & items() const
const itemst & items() const
const irep_idt & get_namespace() const
void swap(cpp_parse_treet &cpp_parse_tree)
cpp_namet & name()
Definition: cpp_using.h:24
bool get_namespace() const
Definition: cpp_using.h:34
Base class for all expressions.
Definition: expr.h:56
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void make_nil()
Definition: irep.h:442
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:29
void cpp_internal_additions(std::ostream &out)
std::unique_ptr< languaget > new_cpp_language()
C++ Language Module.
C++ Parser.
std::string cpp_type2name(const typet &type)
C++ Language Module.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
C++ Language Type Checking.
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:507
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:500
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition: linking.cpp:1616
ANSI-C Linking.
void remove_internal_symbols(symbol_table_baset &symbol_table, message_handlert &mh, const bool keep_file_local)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
Remove symbols that are internal only.
char * strrchr(const char *src, int c)
Definition: string.c:987
flavourt mode
Definition: config.h:252
Author: Diffblue Ltd.
dstringt irep_idt