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