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>
23 
25 #include <ansi-c/c_preprocess.h>
26 
27 #include "cpp_internal_additions.h"
28 #include "expr2cpp.h"
29 #include "cpp_parser.h"
30 #include "cpp_typecheck.h"
31 #include "cpp_type2name.h"
32 
33 std::set<std::string> cpp_languaget::extensions() const
34 {
35  std::set<std::string> s;
36 
37  s.insert("cpp");
38  s.insert("CPP");
39  s.insert("cc");
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 {
62  if(path=="")
63  return c_preprocess(instream, outstream, get_message_handler());
64 
65  // check extension
66 
67  const char *ext=strrchr(path.c_str(), '.');
68  if(ext!=nullptr && std::string(ext)==".ipp")
69  {
70  std::ifstream infile(path);
71 
72  char ch;
73 
74  while(infile.read(&ch, 1))
75  outstream << ch;
76 
77  return false;
78  }
79 
80  return c_preprocess(path, outstream, get_message_handler());
81 }
82 
84  std::istream &instream,
85  const std::string &path)
86 {
87  // store the path
88 
89  parse_path=path;
90 
91  // preprocessing
92 
93  std::ostringstream o_preprocessed;
94 
95  cpp_internal_additions(o_preprocessed);
96 
97  if(preprocess(instream, path, o_preprocessed))
98  return true;
99 
100  std::istringstream i_preprocessed(o_preprocessed.str());
101 
102  // parsing
103 
104  cpp_parser.clear();
105  cpp_parser.set_file(path);
106  cpp_parser.in=&i_preprocessed;
109 
110  bool result=cpp_parser.parse();
111 
112  // save result
114 
115  // save some memory
116  cpp_parser.clear();
117 
118  return result;
119 }
120 
122  symbol_tablet &symbol_table,
123  const std::string &module)
124 {
125  if(module=="")
126  return false;
127 
128  symbol_tablet new_symbol_table;
129 
130  if(cpp_typecheck(
131  cpp_parse_tree, new_symbol_table, module, get_message_handler()))
132  return true;
133 
134  return linking(symbol_table, new_symbol_table, get_message_handler());
135 }
136 
138 {
139  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
140  return true;
141 
142  return false;
143 }
144 
145 void cpp_languaget::show_parse(std::ostream &out)
146 {
147  for(cpp_parse_treet::itemst::const_iterator it=
148  cpp_parse_tree.items.begin();
149  it!=cpp_parse_tree.items.end();
150  it++)
151  show_parse(out, *it);
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("value")
164  << ":\n";
165 
166  for(cpp_linkage_spect::itemst::const_iterator
167  it=linkage_spec.items().begin();
168  it!=linkage_spec.items().end();
169  it++)
170  show_parse(out, *it);
171 
172  out << '\n';
173  }
174  else if(item.is_namespace_spec())
175  {
176  const cpp_namespace_spect &namespace_spec=
177  item.get_namespace_spec();
178 
179  out << "NAMESPACE " << namespace_spec.get_namespace()
180  << ":\n";
181 
182  for(cpp_namespace_spect::itemst::const_iterator
183  it=namespace_spec.items().begin();
184  it!=namespace_spec.items().end();
185  it++)
186  show_parse(out, *it);
187 
188  out << '\n';
189  }
190  else if(item.is_using())
191  {
192  const cpp_usingt &cpp_using=item.get_using();
193 
194  out << "USING ";
195  if(cpp_using.get_namespace())
196  out << "NAMESPACE ";
197  out << cpp_using.name().pretty() << '\n';
198  out << '\n';
199  }
200  else if(item.is_declaration())
201  {
202  item.get_declaration().output(out);
203  }
204  else
205  out << "UNKNOWN: " << item.pretty() << '\n';
206 }
207 
209 {
210  return new cpp_languaget;
211 }
212 
214  const exprt &expr,
215  std::string &code,
216  const namespacet &ns)
217 {
218  code=expr2cpp(expr, ns);
219  return false;
220 }
221 
223  const typet &type,
224  std::string &code,
225  const namespacet &ns)
226 {
227  code=type2cpp(type, ns);
228  return false;
229 }
230 
232  const typet &type,
233  std::string &name,
234  const namespacet &ns)
235 {
236  name=cpp_type2name(type);
237  return false;
238 }
239 
241  const std::string &code,
242  const std::string &module,
243  exprt &expr,
244  const namespacet &ns)
245 {
246  expr.make_nil();
247 
248  // no preprocessing yet...
249 
250  std::istringstream i_preprocessed(code);
251 
252  // parsing
253 
254  cpp_parser.clear();
256  cpp_parser.in=&i_preprocessed;
258 
259  bool result=cpp_parser.parse();
260 
261  if(cpp_parser.parse_tree.items.empty())
262  result=true;
263  else
264  {
265  // TODO
266  // expr.swap(cpp_parser.parse_tree.declarations.front());
267 
268  // typecheck it
270  }
271 
272  // save some memory
273  cpp_parser.clear();
274 
275  return result;
276 }
277 
279 {
280 }
bool final(symbol_tablet &symbol_table) override
The type of an expression.
Definition: type.h:20
bool is_using() const
Definition: cpp_item.h:121
mstreamt & result()
Definition: message.h:233
struct configt::ansi_ct ansi_c
virtual void clear() override
Definition: cpp_parser.h:33
cpp_usingt & get_using()
Definition: cpp_item.h:109
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
ANSI-C Linking.
std::istream * in
Definition: parser.h:26
void swap(cpp_parse_treet &cpp_parse_tree)
~cpp_languaget() override
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1336
bool cpp_typecheck(cpp_parse_treet &cpp_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
bool c_preprocess(std::istream &instream, std::ostream &outstream, message_handlert &message_handler)
ANSI-C preprocessing.
configt config
Definition: config.cpp:21
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
void modules_provided(std::set< std::string > &modules) override
bool is_declaration() const
Definition: cpp_item.h:46
bool is_namespace_spec() const
Definition: cpp_item.h:96
cpp_namespace_spect & get_namespace_spec()
Definition: cpp_item.h:84
cpp_parse_treet cpp_parse_tree
Definition: cpp_language.h:84
void cpp_internal_additions(std::ostream &out)
void show_parse(std::ostream &out) override
flavourt mode
Definition: config.h:105
virtual bool parse() override
Definition: cpp_parser.cpp:20
void set_file(const irep_idt &file)
Definition: parser.h:85
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition: expr2cpp.cpp:505
C++ Language Module.
bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
C++ Language Module.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
cpp_parse_treet parse_tree
Definition: cpp_parser.h:29
std::string cpp_type2name(const typet &type)
languaget * new_cpp_language()
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
ansi_c_parsert::modet mode
Definition: cpp_parser.h:50
C++ Language Type Checking.
bool get_namespace() const
Definition: cpp_using.h:34
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
const itemst & items() const
bool parse(std::istream &instream, const std::string &path) override
message_handlert & get_message_handler()
Definition: message.h:127
bool ansi_c_entry_point(symbol_tablet &symbol_table, const std::string &standard_main, message_handlert &message_handler)
std::set< std::string > extensions() const override
const irep_idt & get_namespace() const
std::string type2cpp(const typet &type, const namespacet &ns)
Definition: expr2cpp.cpp:512
Base class for all expressions.
Definition: expr.h:46
bool type_to_name(const typet &type, std::string &name, const namespacet &ns) override
cpp_declarationt & get_declaration()
Definition: cpp_item.h:34
cpp_namet & name()
Definition: cpp_using.h:24
cpp_linkage_spect & get_linkage_spec()
Definition: cpp_item.h:59
void make_nil()
Definition: irep.h:243
dstringt irep_idt
Definition: irep.h:32
C++ Parser.
const itemst & items() const
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
std::string parse_path
Definition: cpp_language.h:85
void output(std::ostream &out) const
cpp_parsert cpp_parser
Definition: cpp_parser.cpp:16
bool is_linkage_spec() const
Definition: cpp_item.h:71