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 
14 
15 #include "language.h"
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 {
44  language->convert_lazy_method(id, symbol_table);
45 }
46 
47 void language_filest::show_parse(std::ostream &out)
48 {
49  for(const auto &file : file_map)
50  file.second.language->show_parse(out);
51 }
52 
54 {
55  for(auto &file : file_map)
56  {
57  // open file
58 
59  std::ifstream infile(file.first);
60 
61  if(!infile)
62  {
63  error() << "Failed to open " << file.first << 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  error() << "Parsing of " << file.first << " failed" << 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_tablet &symbol_table,
87  const bool keep_file_local)
88 {
89  // typecheck interfaces
90 
91  for(auto &file : file_map)
92  {
93  if(file.second.language->interfaces(symbol_table))
94  return true;
95  }
96 
97  // build module map
98 
99  unsigned collision_counter=0;
100 
101  for(auto &file : file_map)
102  {
103  const language_filet::modulest &modules=
104  file.second.modules;
105 
106  for(language_filet::modulest::const_iterator
107  mo_it=modules.begin();
108  mo_it!=modules.end();
109  mo_it++)
110  {
111  // these may collide, and then get renamed
112  std::string module_name=*mo_it;
113 
114  while(module_map.find(module_name)!=module_map.end())
115  {
116  module_name=*mo_it+"#"+std::to_string(collision_counter);
117  collision_counter++;
118  }
119 
120  language_modulet module;
121  module.file=&file.second;
122  module.name=module_name;
123  module_map.insert(
124  std::pair<std::string, language_modulet>(module.name, module));
125  }
126  }
127 
128  // typecheck files
129 
130  for(auto &file : file_map)
131  {
132  if(file.second.modules.empty())
133  {
134  if(file.second.language->can_keep_file_local())
135  {
136  if(file.second.language->typecheck(symbol_table, "", keep_file_local))
137  return true;
138  }
139  else
140  {
141  if(file.second.language->typecheck(symbol_table, ""))
142  return true;
143  }
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, keep_file_local))
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  const bool keep_file_local)
210 {
211  // check module map
212 
213  module_mapt::iterator it=module_map.find(module);
214 
215  if(it==module_map.end())
216  {
217  error() << "found no file that provides module " << module << eom;
218  return true;
219  }
220 
221  return typecheck_module(symbol_table, it->second, keep_file_local);
222 }
223 
225  symbol_tablet &symbol_table,
226  language_modulet &module,
227  const bool keep_file_local)
228 {
229  // already typechecked?
230 
231  if(module.type_checked)
232  return false;
233 
234  // already in progress?
235 
236  if(module.in_progress)
237  {
238  error() << "circular dependency in " << module.name << eom;
239  return true;
240  }
241 
242  module.in_progress=true;
243 
244  // first get dependencies of current module
245 
246  std::set<std::string> dependency_set;
247 
248  module.file->language->dependencies(module.name, dependency_set);
249 
250  for(std::set<std::string>::const_iterator it=
251  dependency_set.begin();
252  it!=dependency_set.end();
253  it++)
254  {
255  module.in_progress = !typecheck_module(symbol_table, *it, keep_file_local);
256  if(module.in_progress == false)
257  return true;
258  }
259 
260  // type check it
261 
262  status() << "Type-checking " << module.name << eom;
263 
264  if(module.file->language->can_keep_file_local())
265  {
266  module.in_progress = !module.file->language->typecheck(
267  symbol_table, module.name, keep_file_local);
268  }
269  else
270  {
271  module.in_progress =
272  !module.file->language->typecheck(symbol_table, module.name);
273  }
274 
275  if(!module.in_progress)
276  return true;
277 
278  module.type_checked=true;
279  module.in_progress=false;
280 
281  return false;
282 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
language_filet::~language_filet
~language_filet()
To avoid compiler errors, the complete definition of a pointed-to type must be visible at the point a...
language_filest::lazy_method_map
lazy_method_mapt lazy_method_map
Definition: language_file.h:73
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:35
language_filest::typecheck_module
bool typecheck_module(symbol_tablet &symbol_table, language_modulet &module, const bool keep_file_local)
Definition: language_file.cpp:224
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:85
messaget::status
mstreamt & status() const
Definition: message.h:414
language_filet
Definition: language_file.h:41
file
Definition: kdev_t.h:19
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
language_modulet
Definition: language_file.h:27
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:165
language_filest::module_map
module_mapt module_map
Definition: language_file.h:68
language_filest::file_map
file_mapt file_map
Definition: language_file.h:65
messaget::error
mstreamt & error() const
Definition: message.h:399
language_modulet::file
language_filet * file
Definition: language_file.h:31
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
language.h
Abstract interface to support a programming language.
language_filest::show_parse
void show_parse(std::ostream &out)
Definition: language_file.cpp:47
object_factory_parameters.h
language_modulet::name
std::string name
Definition: language_file.h:29
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
language_filet::modules
modulest modules
Definition: language_file.h:44
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:180
language_filet::modulest
std::set< std::string > modulest
Definition: language_file.h:43
language_filest::interfaces
bool interfaces(symbol_tablet &symbol_table)
Definition: language_file.cpp:194
language_filest::parse
bool parse()
Definition: language_file.cpp:53
languaget
Definition: language.h:40
language_modulet::in_progress
bool in_progress
Definition: language_file.h:30
language_filet::language_filet
language_filet(const std::string &filename)
Definition: language_file.cpp:30
languages
languagest languages
Definition: mode.cpp:32
language_modulet::type_checked
bool type_checked
Definition: language_file.h:30
language_filet::convert_lazy_method
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
Definition: language_file.cpp:40
language_file.h