cprover
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 <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 
28 language_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 
45 void language_filest::show_parse(std::ostream &out)
46 {
47  for(const auto &file : file_map)
48  file.second.language->show_parse(out);
49 }
50 
54  bool stubs_enabled)
55 {
56  for(file_mapt::value_type &language_file_entry : file_map)
57  {
58  auto &language=*language_file_entry.second.language;
59  language.set_should_generate_opaque_method_stubs(stubs_enabled);
60  }
61 }
62 
64 {
65  for(auto &file : file_map)
66  {
67  // open file
68 
69  std::ifstream infile(file.first);
70 
71  if(!infile)
72  {
73  error() << "Failed to open " << file.first << eom;
74  return true;
75  }
76 
77  // parse it
78 
79  languaget &language=*(file.second.language);
80 
81  if(language.parse(infile, file.first))
82  {
83  error() << "Parsing of " << file.first << " failed" << eom;
84  return true;
85  }
86 
87  // what is provided?
88 
89  file.second.get_modules();
90  }
91 
92  return false;
93 }
94 
96 {
97  // typecheck interfaces
98 
99  for(auto &file : file_map)
100  {
101  if(file.second.language->interfaces(symbol_table))
102  return true;
103  }
104 
105  // build module map
106 
107  unsigned collision_counter=0;
108 
109  for(auto &file : file_map)
110  {
111  const language_filet::modulest &modules=
112  file.second.modules;
113 
114  for(language_filet::modulest::const_iterator
115  mo_it=modules.begin();
116  mo_it!=modules.end();
117  mo_it++)
118  {
119  // these may collide, and then get renamed
120  std::string module_name=*mo_it;
121 
122  while(module_map.find(module_name)!=module_map.end())
123  {
124  module_name=*mo_it+"#"+std::to_string(collision_counter);
125  collision_counter++;
126  }
127 
128  language_modulet module;
129  module.file=&file.second;
130  module.name=module_name;
131  module_map.insert(
132  std::pair<std::string, language_modulet>(module.name, module));
133  }
134  }
135 
136  // typecheck files
137 
138  for(auto &file : file_map)
139  {
140  if(file.second.modules.empty())
141  {
142  if(file.second.language->typecheck(symbol_table, ""))
143  return true;
144  // register lazy methods.
145  // TODO: learn about modules and generalise this
146  // to module-providing languages if required.
147  std::unordered_set<irep_idt> lazy_method_ids;
148  file.second.language->methods_provided(lazy_method_ids);
149  for(const auto &id : lazy_method_ids)
150  lazy_method_map[id]=&file.second;
151  }
152  }
153 
154  // typecheck modules
155 
156  for(auto &module : module_map)
157  {
158  if(typecheck_module(symbol_table, module.second))
159  return true;
160  }
161 
162  return false;
163 }
164 
166  symbol_tablet &symbol_table)
167 {
168  std::set<std::string> languages;
169 
170  for(auto &file : file_map)
171  {
172  if(languages.insert(file.second.language->id()).second)
173  if(file.second.language->generate_support_functions(symbol_table))
174  return true;
175  }
176 
177  return false;
178 }
179 
181 {
182  std::set<std::string> languages;
183 
184  for(auto &file : file_map)
185  {
186  if(languages.insert(file.second.language->id()).second)
187  if(file.second.language->final(symbol_table))
188  return true;
189  }
190 
191  return false;
192 }
193 
195  symbol_tablet &symbol_table)
196 {
197  for(auto &file : file_map)
198  {
199  if(file.second.language->interfaces(symbol_table))
200  return true;
201  }
202 
203  return false;
204 }
205 
207  symbol_tablet &symbol_table,
208  const std::string &module)
209 {
210  // check module map
211 
212  module_mapt::iterator it=module_map.find(module);
213 
214  if(it==module_map.end())
215  {
216  error() << "found no file that provides module " << module << eom;
217  return true;
218  }
219 
220  return typecheck_module(symbol_table, it->second);
221 }
222 
224  symbol_tablet &symbol_table,
225  language_modulet &module)
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  if(typecheck_module(symbol_table, *it))
254  {
255  module.in_progress=false;
256  return true;
257  }
258  }
259 
260  // type check it
261 
262  status() << "Type-checking " << module.name << eom;
263 
264  if(module.file->language->typecheck(symbol_table, module.name))
265  {
266  module.in_progress=false;
267  return true;
268  }
269 
270  module.type_checked=true;
271  module.in_progress=false;
272 
273  return false;
274 }
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
bool final(symbol_table_baset &symbol_table)
void show_parse(std::ostream &out)
bool interfaces(symbol_tablet &symbol_table)
std::set< std::string > modulest
Definition: language_file.h:43
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
std::unique_ptr< languaget > language
Definition: language_file.h:46
bool typecheck_module(symbol_tablet &symbol_table, language_modulet &module)
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
lazy_method_mapt lazy_method_map
Definition: language_file.h:73
language_filet(const std::string &filename)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void set_should_generate_opaque_method_stubs(bool stubs_enabled)
Turn on or off stub generation for all the languages.
std::string name
Definition: language_file.h:29
~language_filet()
To avoid compiler errors, the complete definition of a pointed-to type must be visible at the point a...
mstreamt & status() const
Definition: message.h:317
modulest modules
Definition: language_file.h:44
The symbol table base class interface.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
file_mapt file_map
Definition: language_file.h:65
virtual bool parse(std::istream &instream, const std::string &path)=0
bool generate_support_functions(symbol_tablet &symbol_table)
languagest languages
Definition: mode.cpp:32
module_mapt module_map
Definition: language_file.h:68
language_filet * file
Definition: language_file.h:31
Definition: kdev_t.h:19