cprover
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
34{
35 language->modules_provided(modules);
36}
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 for(auto &file : file_map)
54 {
55 // open file
56
57 std::ifstream infile(file.first);
58
59 if(!infile)
60 {
61 error() << "Failed to open " << file.first << eom;
62 return true;
63 }
64
65 // parse it
66
67 languaget &language=*(file.second.language);
68
69 if(language.parse(infile, file.first))
70 {
71 error() << "Parsing of " << file.first << " failed" << eom;
72 return true;
73 }
74
75 // what is provided?
76
77 file.second.get_modules();
78 }
79
80 return false;
81}
82
84 symbol_tablet &symbol_table,
85 const bool keep_file_local)
86{
87 // typecheck interfaces
88
89 for(auto &file : file_map)
90 {
91 if(file.second.language->interfaces(symbol_table))
92 return true;
93 }
94
95 // build module map
96
97 unsigned collision_counter=0;
98
99 for(auto &file : file_map)
100 {
101 const language_filet::modulest &modules=
102 file.second.modules;
103
104 for(language_filet::modulest::const_iterator
105 mo_it=modules.begin();
106 mo_it!=modules.end();
107 mo_it++)
108 {
109 // these may collide, and then get renamed
110 std::string module_name=*mo_it;
111
112 while(module_map.find(module_name)!=module_map.end())
113 {
114 module_name=*mo_it+"#"+std::to_string(collision_counter);
115 collision_counter++;
116 }
117
118 language_modulet module;
119 module.file=&file.second;
120 module.name=module_name;
121 module_map.insert(
122 std::pair<std::string, language_modulet>(module.name, module));
123 }
124 }
125
126 // typecheck files
127
128 for(auto &file : file_map)
129 {
130 if(file.second.modules.empty())
131 {
132 if(file.second.language->can_keep_file_local())
133 {
134 if(file.second.language->typecheck(symbol_table, "", keep_file_local))
135 return true;
136 }
137 else
138 {
139 if(file.second.language->typecheck(symbol_table, ""))
140 return true;
141 }
142 // register lazy methods.
143 // TODO: learn about modules and generalise this
144 // to module-providing languages if required.
145 std::unordered_set<irep_idt> lazy_method_ids;
146 file.second.language->methods_provided(lazy_method_ids);
147 for(const auto &id : lazy_method_ids)
148 lazy_method_map[id]=&file.second;
149 }
150 }
151
152 // typecheck modules
153
154 for(auto &module : module_map)
155 {
156 if(typecheck_module(symbol_table, module.second, keep_file_local))
157 return true;
158 }
159
160 return false;
161}
162
164 symbol_tablet &symbol_table)
165{
166 std::set<std::string> languages;
167
168 for(auto &file : file_map)
169 {
170 if(languages.insert(file.second.language->id()).second)
171 if(file.second.language->generate_support_functions(symbol_table))
172 return true;
173 }
174
175 return false;
176}
177
179{
180 std::set<std::string> languages;
181
182 for(auto &file : file_map)
183 {
184 if(languages.insert(file.second.language->id()).second)
185 if(file.second.language->final(symbol_table))
186 return true;
187 }
188
189 return false;
190}
191
193 symbol_tablet &symbol_table)
194{
195 for(auto &file : file_map)
196 {
197 if(file.second.language->interfaces(symbol_table))
198 return true;
199 }
200
201 return false;
202}
203
205 symbol_tablet &symbol_table,
206 const std::string &module,
207 const bool keep_file_local)
208{
209 // check module map
210
211 module_mapt::iterator it=module_map.find(module);
212
213 if(it==module_map.end())
214 {
215 error() << "found no file that provides module " << module << eom;
216 return true;
217 }
218
219 return typecheck_module(symbol_table, it->second, keep_file_local);
220}
221
223 symbol_tablet &symbol_table,
224 language_modulet &module,
225 const bool keep_file_local)
226{
227 // already typechecked?
228
229 if(module.type_checked)
230 return false;
231
232 // already in progress?
233
234 if(module.in_progress)
235 {
236 error() << "circular dependency in " << module.name << eom;
237 return true;
238 }
239
240 module.in_progress=true;
241
242 // first get dependencies of current module
243
244 std::set<std::string> dependency_set;
245
246 module.file->language->dependencies(module.name, dependency_set);
247
248 for(std::set<std::string>::const_iterator it=
249 dependency_set.begin();
250 it!=dependency_set.end();
251 it++)
252 {
253 module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local);
254 if(module.in_progress == false)
255 return true;
256 }
257
258 // type check it
259
260 status() << "Type-checking " << module.name << eom;
261
262 if(module.file->language->can_keep_file_local())
263 {
264 module.in_progress = !module.file->language->typecheck(
265 symbol_table, module.name, keep_file_local);
266 }
267 else
268 {
269 module.in_progress =
270 !module.file->language->typecheck(symbol_table, module.name);
271 }
272
273 if(!module.in_progress)
274 return true;
275
276 module.type_checked=true;
277 module.in_progress=false;
278
279 return false;
280}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool typecheck_module(symbol_tablet &symbol_table, language_modulet &module, const bool keep_file_local)
file_mapt file_map
Definition: language_file.h:66
void show_parse(std::ostream &out)
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
bool interfaces(symbol_tablet &symbol_table)
lazy_method_mapt lazy_method_map
Definition: language_file.h:74
module_mapt module_map
Definition: language_file.h:69
bool generate_support_functions(symbol_tablet &symbol_table)
bool final(symbol_table_baset &symbol_table)
language_filet(const std::string &filename)
modulest modules
Definition: language_file.h:45
~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
Definition: language_file.h:44
std::unique_ptr< languaget > language
Definition: language_file.h:47
std::string name
Definition: language_file.h:30
language_filet * file
Definition: language_file.h:32
virtual bool parse(std::istream &instream, const std::string &path)=0
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.
The symbol table.
Definition: symbol_table.h:14
Abstract interface to support a programming language.
languagest languages
Definition: mode.cpp:33
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: kdev_t.h:19