CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <util/message.h>
12
13#include "language.h"
14
15#include <fstream>
16
18 modules(rhs.modules),
19 language(rhs.language==nullptr?nullptr:rhs.language->new_language()),
20 filename(rhs.filename)
21{
22}
23
29
30language_filet::language_filet(const std::string &filename)
31 : filename(filename)
32{
33}
34
36{
37 language->modules_provided(modules);
38}
39
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
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
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
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);
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 {
166 symbol_table, module.second, keep_file_local, message_handler))
167 return true;
168 }
169
170 return false;
171}
172
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
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
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
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
240 symbol_table_baset &symbol_table,
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool interfaces(symbol_table_baset &symbol_table, message_handlert &message_handler)
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
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)
lazy_method_mapt lazy_method_map
module_mapt module_map
void show_parse(std::ostream &out, message_handlert &message_handler)
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, message_handlert &message_handler)
std::set< std::string > modulest
std::unique_ptr< languaget > language
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
The symbol table base class interface.
Abstract interface to support a programming language.
double log(double x)
Definition math.c:2449
languagest languages
Definition mode.cpp:33