cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
language_file.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#include "
language_file.h
"
10
11
#include <
util/message.h
>
12
13
#include "
language.h
"
14
15
#include <fstream>
16
17
language_filet::language_filet
(
const
language_filet
&rhs):
18
modules
(rhs.
modules
),
19
language
(rhs.
language
==nullptr?nullptr:rhs.
language
->new_language()),
20
filename
(rhs.
filename
)
21
{
22
}
23
28
language_filet::~language_filet
()=
default
;
29
30
language_filet::language_filet
(
const
std::string &
filename
)
31
:
filename
(
filename
)
32
{
33
}
34
35
void
language_filet::get_modules
()
36
{
37
language
->modules_provided(
modules
);
38
}
39
40
void
language_filet::convert_lazy_method
(
41
const
irep_idt
&
id
,
42
symbol_table_baset
&symbol_table,
43
message_handlert
&message_handler)
44
{
45
language
->convert_lazy_method(
id
, symbol_table, message_handler);
46
}
47
48
void
language_filest::show_parse
(
49
std::ostream &out,
50
message_handlert
&message_handler)
51
{
52
for
(
const
auto
&
file
:
file_map
)
53
file
.second.language->show_parse(out, message_handler);
54
}
55
56
bool
language_filest::parse
(
message_handlert
&message_handler)
57
{
58
messaget
log(message_handler);
59
60
for
(
auto
&
file
:
file_map
)
61
{
62
// open file
63
64
std::ifstream infile(
file
.first);
65
66
if
(!infile)
67
{
68
log.
error
() <<
"Failed to open "
<<
file
.first <<
messaget::eom
;
69
return
true
;
70
}
71
72
// parse it
73
74
languaget
&language=*(
file
.second.language);
75
76
if
(language.
parse
(infile,
file
.first, message_handler))
77
{
78
log.
error
() <<
"Parsing of "
<<
file
.first <<
" failed"
<<
messaget::eom
;
79
return
true
;
80
}
81
82
// what is provided?
83
84
file
.second.get_modules();
85
}
86
87
return
false
;
88
}
89
90
bool
language_filest::typecheck
(
91
symbol_table_baset
&symbol_table,
92
const
bool
keep_file_local,
93
message_handlert
&message_handler)
94
{
95
// typecheck interfaces
96
97
for
(
auto
&
file
:
file_map
)
98
{
99
if
(
file
.second.language->interfaces(symbol_table, message_handler))
100
return
true
;
101
}
102
103
// build module map
104
105
unsigned
collision_counter=0;
106
107
for
(
auto
&
file
:
file_map
)
108
{
109
const
language_filet::modulest
&modules=
110
file
.second.modules;
111
112
for
(language_filet::modulest::const_iterator
113
mo_it=modules.begin();
114
mo_it!=modules.end();
115
mo_it++)
116
{
117
// these may collide, and then get renamed
118
std::string module_name=*mo_it;
119
120
while
(
module_map
.find(module_name)!=
module_map
.end())
121
{
122
module_name=*mo_it+
"#"
+std::to_string(collision_counter);
123
collision_counter++;
124
}
125
126
language_modulet
module;
127
module
.file=&file.second;
128
module
.name=module_name;
129
module_map
.insert(
130
std::pair<std::string, language_modulet>(module.
name
, module));
131
}
132
}
133
134
// typecheck files
135
136
for
(
auto
&
file
:
file_map
)
137
{
138
if
(
file
.second.modules.empty())
139
{
140
if
(
file
.second.language->can_keep_file_local())
141
{
142
if
(
file
.second.language->typecheck(
143
symbol_table,
""
, message_handler, keep_file_local))
144
return
true
;
145
}
146
else
147
{
148
if
(
file
.second.language->typecheck(symbol_table,
""
, message_handler))
149
return
true
;
150
}
151
// register lazy methods.
152
// TODO: learn about modules and generalise this
153
// to module-providing languages if required.
154
std::unordered_set<irep_idt> lazy_method_ids;
155
file
.second.language->methods_provided(lazy_method_ids);
156
for
(
const
auto
&
id
: lazy_method_ids)
157
lazy_method_map
[id]=&
file
.second;
158
}
159
}
160
161
// typecheck modules
162
163
for
(
auto
&module :
module_map
)
164
{
165
if
(
typecheck_module
(
166
symbol_table, module.second, keep_file_local, message_handler))
167
return
true
;
168
}
169
170
return
false
;
171
}
172
173
bool
language_filest::generate_support_functions
(
174
symbol_table_baset
&symbol_table,
175
message_handlert
&message_handler)
176
{
177
std::set<std::string>
languages
;
178
179
for
(
auto
&
file
:
file_map
)
180
{
181
if
(
languages
.insert(
file
.second.language->id()).second)
182
if
(
file
.second.language->generate_support_functions(
183
symbol_table, message_handler))
184
return
true
;
185
}
186
187
return
false
;
188
}
189
190
bool
language_filest::final
(
symbol_table_baset
&symbol_table)
191
{
192
std::set<std::string>
languages
;
193
194
for
(
auto
&
file
:
file_map
)
195
{
196
if
(
languages
.insert(
file
.second.language->id()).second)
197
if
(
file
.second.language->final(symbol_table))
198
return
true
;
199
}
200
201
return
false
;
202
}
203
204
bool
language_filest::interfaces
(
205
symbol_table_baset
&symbol_table,
206
message_handlert
&message_handler)
207
{
208
for
(
auto
&
file
:
file_map
)
209
{
210
if
(
file
.second.language->interfaces(symbol_table, message_handler))
211
return
true
;
212
}
213
214
return
false
;
215
}
216
217
bool
language_filest::typecheck_module
(
218
symbol_table_baset
&symbol_table,
219
const
std::string &module,
220
const
bool
keep_file_local,
221
message_handlert
&message_handler)
222
{
223
// check module map
224
225
module_mapt::iterator it=
module_map
.find(module);
226
227
if
(it==
module_map
.end())
228
{
229
messaget
log(message_handler);
230
log.
error
() <<
"found no file that provides module "
<<
module
231
<< messaget::eom;
232
return
true
;
233
}
234
235
return
typecheck_module
(
236
symbol_table, it->second, keep_file_local, message_handler);
237
}
238
239
bool
language_filest::typecheck_module
(
240
symbol_table_baset
&symbol_table,
241
language_modulet
&module,
242
const
bool
keep_file_local,
243
message_handlert
&message_handler)
244
{
245
// already typechecked?
246
247
if
(module.
type_checked
)
248
return
false
;
249
250
messaget
log(message_handler);
251
252
// already in progress?
253
254
if
(module.
in_progress
)
255
{
256
log.
error
() <<
"circular dependency in "
<<
module
.name << messaget::eom;
257
return
true
;
258
}
259
260
module
.in_progress=true;
261
262
// first get dependencies of current module
263
264
std::set<std::string> dependency_set;
265
266
module
.file->language->dependencies(module.name, dependency_set);
267
268
for
(std::set<std::string>::const_iterator it=
269
dependency_set.begin();
270
it!=dependency_set.end();
271
it++)
272
{
273
module
.in_progress =
274
!typecheck_module(symbol_table, *it, keep_file_local, message_handler);
275
if
(module.
in_progress
==
false
)
276
return
true
;
277
}
278
279
// type check it
280
281
log.
status
() <<
"Type-checking "
<<
module
.name << messaget::eom;
282
283
if
(module.
file
->
language
->
can_keep_file_local
())
284
{
285
module
.in_progress = !module.file->language->typecheck(
286
symbol_table, module.name, message_handler, keep_file_local);
287
}
288
else
289
{
290
module
.in_progress = !module.file->language->typecheck(
291
symbol_table, module.name, message_handler);
292
}
293
294
if
(!module.
in_progress
)
295
return
true
;
296
297
module
.type_checked=true;
298
module
.in_progress=false;
299
300
return
false
;
301
}
language_filest::interfaces
bool interfaces(symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition
language_file.cpp:204
language_filest::parse
bool parse(message_handlert &message_handler)
Definition
language_file.cpp:56
language_filest::typecheck_module
bool typecheck_module(symbol_table_baset &symbol_table, language_modulet &module, const bool keep_file_local, message_handlert &message_handler)
Definition
language_file.cpp:239
language_filest::typecheck
bool typecheck(symbol_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
Definition
language_file.cpp:90
language_filest::file_map
file_mapt file_map
Definition
language_file.h:66
language_filest::generate_support_functions
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition
language_file.cpp:173
language_filest::lazy_method_map
lazy_method_mapt lazy_method_map
Definition
language_file.h:74
language_filest::module_map
module_mapt module_map
Definition
language_file.h:69
language_filest::show_parse
void show_parse(std::ostream &out, message_handlert &message_handler)
Definition
language_file.cpp:48
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition
language_file.cpp:190
language_filet::language_filet
language_filet(const std::string &filename)
Definition
language_file.cpp:30
language_filet::filename
std::string filename
Definition
language_file.h:47
language_filet::modules
modulest modules
Definition
language_file.h:44
language_filet::~language_filet
~language_filet()
To avoid compiler errors, the complete definition of a pointed-to type must be visible at the point a...
language_filet::get_modules
void get_modules()
Definition
language_file.cpp:35
language_filet::convert_lazy_method
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table, message_handlert &message_handler)
Definition
language_file.cpp:40
language_filet::modulest
std::set< std::string > modulest
Definition
language_file.h:43
language_filet::language
std::unique_ptr< languaget > language
Definition
language_file.h:46
language_modulet
Definition
language_file.h:27
language_modulet::name
std::string name
Definition
language_file.h:29
language_modulet::in_progress
bool in_progress
Definition
language_file.h:30
language_modulet::file
language_filet * file
Definition
language_file.h:31
language_modulet::type_checked
bool type_checked
Definition
language_file.h:30
languaget
Definition
language.h:37
languaget::can_keep_file_local
virtual bool can_keep_file_local()
Is it possible to call three-argument typecheck() on this object?
Definition
language.h:132
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
message_handlert
Definition
message.h:27
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition
message.h:154
messaget::error
mstreamt & error() const
Definition
message.h:391
messaget::eom
static eomt eom
Definition
message.h:289
messaget::status
mstreamt & status() const
Definition
message.h:406
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
language.h
Abstract interface to support a programming language.
language_file.h
languages
languagest languages
Definition
mode.cpp:33
message.h
file
Definition
kdev_t.h:19
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
langapi
language_file.cpp
Generated by
1.17.0