cprover
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 <cstring>
15 #include <sstream>
16 #include <fstream>
17 
18 #include <util/config.h>
19 #include <util/replace_symbol.h>
20 #include <util/get_base_name.h>
21 
22 #include <linking/linking.h>
24 
26 #include <ansi-c/c_preprocess.h>
27 
28 #include "cpp_internal_additions.h"
29 #include "expr2cpp.h"
30 #include "cpp_parser.h"
31 #include "cpp_typecheck.h"
32 #include "cpp_type2name.h"
33 
34 std::set<std::string> cpp_languaget::extensions() const
35 {
36  std::set<std::string> s;
37 
38  s.insert("cpp");
39  s.insert("CPP");
40  s.insert("cc");
41  s.insert("cp");
42  s.insert("c++");
43  s.insert("ii");
44  s.insert("cxx");
45 
46  #ifndef _WIN32
47  s.insert("C");
48  #endif
49 
50  return s;
51 }
52 
53 void cpp_languaget::modules_provided(std::set<std::string> &modules)
54 {
55  modules.insert(get_base_name(parse_path, true));
56 }
57 
60  std::istream &instream,
61  const std::string &path,
62  std::ostream &outstream)
63 {
64  if(path.empty())
65  return c_preprocess(instream, outstream, get_message_handler());
66 
67  // check extension
68 
69  const char *ext=strrchr(path.c_str(), '.');
70  if(ext!=nullptr && std::string(ext)==".ipp")
71  {
72  std::ifstream infile(path);
73 
74  char ch;
75 
76  while(infile.read(&ch, 1))
77  outstream << ch;
78 
79  return false;
80  }
81 
82  return c_preprocess(path, outstream, get_message_handler());
83 }
84 
86  std::istream &instream,
87  const std::string &path)
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))
100  return true;
101 
102  std::istringstream i_preprocessed(o_preprocessed.str());
103 
104  // parsing
105 
106  cpp_parser.clear();
107  cpp_parser.set_file(path);
108  cpp_parser.in=&i_preprocessed;
111 
112  bool result=cpp_parser.parse();
113 
114  // save result
116 
117  // save some memory
118  cpp_parser.clear();
119 
120  return result;
121 }
122 
124  symbol_tablet &symbol_table,
125  const std::string &module)
126 {
127  if(module.empty())
128  return false;
129 
130  symbol_tablet new_symbol_table;
131 
132  if(cpp_typecheck(
133  cpp_parse_tree, new_symbol_table, module, get_message_handler()))
134  return true;
135 
136  remove_internal_symbols(new_symbol_table, get_message_handler(), false);
137 
138  return linking(symbol_table, new_symbol_table, get_message_handler());
139 }
140 
142  symbol_tablet &symbol_table)
143 {
144  return ansi_c_entry_point(
145  symbol_table, get_message_handler(), object_factory_params);
146 }
147 
148 void cpp_languaget::show_parse(std::ostream &out)
149 {
150  for(const auto &i : cpp_parse_tree.items)
151  show_parse(out, i);
152 }
153 
155  std::ostream &out,
156  const cpp_itemt &item)
157 {
158  if(item.is_linkage_spec())
159  {
160  const cpp_linkage_spect &linkage_spec=
161  item.get_linkage_spec();
162 
163  out << "LINKAGE " << linkage_spec.linkage().get(ID_value) << ":\n";
164 
165  for(const auto &i : linkage_spec.items())
166  show_parse(out, i);
167 
168  out << '\n';
169  }
170  else if(item.is_namespace_spec())
171  {
172  const cpp_namespace_spect &namespace_spec=
173  item.get_namespace_spec();
174 
175  out << "NAMESPACE " << namespace_spec.get_namespace()
176  << ":\n";
177 
178  for(const auto &i : namespace_spec.items())
179  show_parse(out, i);
180 
181  out << '\n';
182  }
183  else if(item.is_using())
184  {
185  const cpp_usingt &cpp_using=item.get_using();
186 
187  out << "USING ";
188  if(cpp_using.get_namespace())
189  out << "NAMESPACE ";
190  out << cpp_using.name().pretty() << '\n';
191  out << '\n';
192  }
193  else if(item.is_declaration())
194  {
195  item.get_declaration().output(out);
196  }
197  else
198  out << "UNKNOWN: " << item.pretty() << '\n';
199 }
200 
201 std::unique_ptr<languaget> new_cpp_language()
202 {
203  return util_make_unique<cpp_languaget>();
204 }
205 
207  const exprt &expr,
208  std::string &code,
209  const namespacet &ns)
210 {
211  code=expr2cpp(expr, ns);
212  return false;
213 }
214 
216  const typet &type,
217  std::string &code,
218  const namespacet &ns)
219 {
220  code=type2cpp(type, ns);
221  return false;
222 }
223 
225  const typet &type,
226  std::string &name,
227  const namespacet &)
228 {
229  name=cpp_type2name(type);
230  return false;
231 }
232 
234  const std::string &code,
235  const std::string &,
236  exprt &expr,
237  const namespacet &ns)
238 {
239  expr.make_nil();
240 
241  // no preprocessing yet...
242 
243  std::istringstream i_preprocessed(code);
244 
245  // parsing
246 
247  cpp_parser.clear();
249  cpp_parser.in=&i_preprocessed;
251 
252  bool result=cpp_parser.parse();
253 
254  if(cpp_parser.parse_tree.items.empty())
255  result=true;
256  else
257  {
258  // TODO
259  // expr.swap(cpp_parser.parse_tree.declarations.front());
260 
261  // typecheck it
263  }
264 
265  // save some memory
266  cpp_parser.clear();
267 
268  return result;
269 }
270 
272 {
273 }
bool ansi_c_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
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 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:97
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
Parses the given string into an expression.
std::string parse_path
Definition: cpp_language.h:95
std::set< std::string > extensions() const override
~cpp_languaget() override
bool generate_support_functions(symbol_tablet &symbol_table) override
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Formats the given expression in a language-specific way.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
bool parse(std::istream &instream, const std::string &path) override
void modules_provided(std::set< std::string > &modules) override
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
cpp_parse_treet cpp_parse_tree
Definition: cpp_language.h:94
void show_parse(std::ostream &out) override
const itemst & items() const
const itemst & items() const
const irep_idt & get_namespace() const
void swap(cpp_parse_treet &cpp_parse_tree)
virtual void clear() override
Definition: cpp_parser.h:31
cpp_parse_treet parse_tree
Definition: cpp_parser.h:27
virtual bool parse() override
Definition: cpp_parser.cpp:20
ansi_c_parsert::modet mode
Definition: cpp_parser.h:48
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:54
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:492
void make_nil()
Definition: irep.h:464
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
mstreamt & result() const
Definition: message.h:409
message_handlert & get_message_handler()
Definition: message.h:184
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
std::istream * in
Definition: parser.h:26
void set_file(const irep_idt &file)
Definition: parser.h:85
The symbol table.
Definition: symbol_table.h:20
The type of an expression, extends irept.
Definition: type.h:28
configt config
Definition: config.cpp:24
void cpp_internal_additions(std::ostream &out)
std::unique_ptr< languaget > new_cpp_language()
C++ Language Module.
cpp_parsert cpp_parser
Definition: cpp_parser.cpp:16
C++ Parser.
std::string cpp_type2name(const typet &type)
C++ Language Module.
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_tablet &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:497
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:490
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
dstringt irep_idt
Definition: irep.h:37
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1437
ANSI-C Linking.
void remove_internal_symbols(symbol_tablet &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.
flavourt mode
Definition: config.h:196