CBMC
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 
18  modules(rhs.modules),
19  language(rhs.language==nullptr?nullptr:rhs.language->new_language()),
20  filename(rhs.filename)
21 {
22 }
23 
29 
30 language_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);
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 
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,
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 }
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
Definition: language_file.h:66
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)
lazy_method_mapt lazy_method_map
Definition: language_file.h:74
module_mapt module_map
Definition: language_file.h:69
void show_parse(std::ostream &out, message_handlert &message_handler)
bool final(symbol_table_baset &symbol_table)
language_filet(const std::string &filename)
modulest modules
Definition: language_file.h:44
~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
Definition: language_file.h:43
std::unique_ptr< languaget > language
Definition: language_file.h:46
std::string name
Definition: language_file.h:29
language_filet * file
Definition: language_file.h:31
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:2776
languagest languages
Definition: mode.cpp:33
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.