cprover
Loading...
Searching...
No Matches
cpp_language.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Module
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include "cpp_language.h"
13
14#include <cstring>
15#include <fstream>
16
17#include <util/config.h>
18#include <util/get_base_name.h>
19
20#include <linking/linking.h>
22
24#include <ansi-c/c_preprocess.h>
25
27#include "expr2cpp.h"
28#include "cpp_parser.h"
29#include "cpp_typecheck.h"
30#include "cpp_type2name.h"
31
32std::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
51void 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.empty())
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
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
117
118 return result;
119}
120
122 symbol_tablet &symbol_table,
123 const std::string &module)
124{
125 if(module.empty())
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 remove_internal_symbols(new_symbol_table, get_message_handler(), false);
135
136 return linking(symbol_table, new_symbol_table, get_message_handler());
137}
138
140 symbol_tablet &symbol_table)
141{
142 return ansi_c_entry_point(
144}
145
146void cpp_languaget::show_parse(std::ostream &out)
147{
148 for(const auto &i : cpp_parse_tree.items)
149 show_parse(out, i);
150}
151
153 std::ostream &out,
154 const cpp_itemt &item)
155{
156 if(item.is_linkage_spec())
157 {
158 const cpp_linkage_spect &linkage_spec=
159 item.get_linkage_spec();
160
161 out << "LINKAGE " << linkage_spec.linkage().get(ID_value) << ":\n";
162
163 for(const auto &i : linkage_spec.items())
164 show_parse(out, i);
165
166 out << '\n';
167 }
168 else if(item.is_namespace_spec())
169 {
170 const cpp_namespace_spect &namespace_spec=
171 item.get_namespace_spec();
172
173 out << "NAMESPACE " << namespace_spec.get_namespace()
174 << ":\n";
175
176 for(const auto &i : namespace_spec.items())
177 show_parse(out, i);
178
179 out << '\n';
180 }
181 else if(item.is_using())
182 {
183 const cpp_usingt &cpp_using=item.get_using();
184
185 out << "USING ";
186 if(cpp_using.get_namespace())
187 out << "NAMESPACE ";
188 out << cpp_using.name().pretty() << '\n';
189 out << '\n';
190 }
191 else if(item.is_declaration())
192 {
193 item.get_declaration().output(out);
194 }
195 else
196 out << "UNKNOWN: " << item.pretty() << '\n';
197}
198
199std::unique_ptr<languaget> new_cpp_language()
200{
201 return util_make_unique<cpp_languaget>();
202}
203
205 const exprt &expr,
206 std::string &code,
207 const namespacet &ns)
208{
209 code=expr2cpp(expr, ns);
210 return false;
211}
212
214 const typet &type,
215 std::string &code,
216 const namespacet &ns)
217{
218 code=type2cpp(type, ns);
219 return false;
220}
221
223 const typet &type,
224 std::string &name,
225 const namespacet &)
226{
227 name=cpp_type2name(type);
228 return false;
229}
230
232 const std::string &code,
233 const std::string &,
234 exprt &expr,
235 const namespacet &ns)
236{
237 expr.make_nil();
238
239 // no preprocessing yet...
240
241 std::istringstream i_preprocessed(code);
242
243 // parsing
244
247 cpp_parser.in=&i_preprocessed;
249
250 bool result=cpp_parser.parse();
251
252 if(cpp_parser.parse_tree.items.empty())
253 result=true;
254 else
255 {
256 // TODO
257 // expr.swap(cpp_parser.parse_tree.declarations.front());
258
259 // typecheck it
261 }
262
263 // save some memory
265
266 return result;
267}
268
270{
271}
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_namespace_spect & get_namespace_spec()
Definition cpp_item.h:82
cpp_usingt & get_using()
Definition cpp_item.h:107
cpp_declarationt & get_declaration()
Definition cpp_item.h:32
cpp_linkage_spect & get_linkage_spec()
Definition cpp_item.h:57
bool is_using() const
Definition cpp_item.h:119
bool is_declaration() const
Definition cpp_item.h:44
bool is_linkage_spec() const
Definition cpp_item.h:69
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
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
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
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:29
cpp_parse_treet parse_tree
Definition cpp_parser.h:25
virtual bool parse() override
ansi_c_parsert::modet mode
Definition cpp_parser.h:46
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:495
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void make_nil()
Definition irep.h:454
message_handlert & get_message_handler()
Definition message.h:184
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
mstreamt & result() const
Definition message.h:409
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
std::istream * in
Definition parser.h:26
void set_file(const irep_idt &file)
Definition parser.h:85
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
configt config
Definition config.cpp:25
void cpp_internal_additions(std::ostream &out)
std::unique_ptr< languaget > new_cpp_language()
C++ Language Module.
cpp_parsert cpp_parser
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:498
std::string expr2cpp(const exprt &expr, const namespacet &ns)
Definition expr2cpp.cpp:491
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, const symbol_tablet &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:1470
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:222