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 
23 {
24  if(language!=nullptr)
25  delete language;
26 }
27 
29 {
31 }
32 
34  const irep_idt &id,
35  symbol_tablet &symbol_table)
36 {
37  language->convert_lazy_method(id, symbol_table);
38 }
39 
40 void language_filest::show_parse(std::ostream &out)
41 {
42  for(file_mapt::iterator it=file_map.begin();
43  it!=file_map.end(); it++)
44  it->second.language->show_parse(out);
45 }
46 
48 {
49  for(file_mapt::iterator it=file_map.begin();
50  it!=file_map.end(); it++)
51  {
52  // open file
53 
54  std::ifstream infile(it->first);
55 
56  if(!infile)
57  {
58  error() << "Failed to open " << it->first << eom;
59  return true;
60  }
61 
62  // parse it
63 
64  languaget &language=*(it->second.language);
65 
66  if(language.parse(infile, it->first))
67  {
68  error() << "Parsing of " << it->first << " failed" << eom;
69  return true;
70  }
71 
72  // what is provided?
73 
74  it->second.get_modules();
75  }
76 
77  return false;
78 }
79 
81 {
82  // typecheck interfaces
83 
84  for(file_mapt::iterator it=file_map.begin();
85  it!=file_map.end(); it++)
86  {
87  if(it->second.language->interfaces(symbol_table))
88  return true;
89  }
90 
91  // build module map
92 
93  unsigned collision_counter=0;
94 
95  for(file_mapt::iterator fm_it=file_map.begin();
96  fm_it!=file_map.end(); fm_it++)
97  {
98  const language_filet::modulest &modules=
99  fm_it->second.modules;
100 
101  for(language_filet::modulest::const_iterator
102  mo_it=modules.begin();
103  mo_it!=modules.end();
104  mo_it++)
105  {
106  // these may collide, and then get renamed
107  std::string module_name=*mo_it;
108 
109  while(module_map.find(module_name)!=module_map.end())
110  {
111  module_name=*mo_it+"#"+std::to_string(collision_counter);
112  collision_counter++;
113  }
114 
115  language_modulet module;
116  module.file=&fm_it->second;
117  module.name=module_name;
118  module_map.insert(
119  std::pair<std::string, language_modulet>(module.name, module));
120  }
121  }
122 
123  // typecheck files
124 
125  for(file_mapt::iterator it=file_map.begin();
126  it!=file_map.end(); it++)
127  {
128  if(it->second.modules.empty())
129  {
130  if(it->second.language->typecheck(symbol_table, ""))
131  return true;
132  // register lazy methods.
133  // TODO: learn about modules and generalise this
134  // to module-providing languages if required.
135  std::set<irep_idt> lazy_method_ids;
136  it->second.language->lazy_methods_provided(lazy_method_ids);
137  for(const auto &id : lazy_method_ids)
138  lazy_method_map[id]=&it->second;
139  }
140  }
141 
142  // typecheck modules
143 
144  for(module_mapt::iterator it=module_map.begin();
145  it!=module_map.end(); it++)
146  {
147  if(typecheck_module(symbol_table, it->second))
148  return true;
149  }
150 
151  return false;
152 }
153 
155  symbol_tablet &symbol_table)
156 {
157  std::set<std::string> languages;
158 
159  for(file_mapt::iterator it=file_map.begin();
160  it!=file_map.end(); it++)
161  {
162  if(languages.insert(it->second.language->id()).second)
163  if(it->second.language->final(symbol_table))
164  return true;
165  }
166 
167  return false;
168 }
169 
171  symbol_tablet &symbol_table)
172 {
173  for(file_mapt::iterator it=file_map.begin();
174  it!=file_map.end(); it++)
175  {
176  if(it->second.language->interfaces(symbol_table))
177  return true;
178  }
179 
180  return false;
181 }
182 
184  symbol_tablet &symbol_table,
185  const std::string &module)
186 {
187  // check module map
188 
189  module_mapt::iterator it=module_map.find(module);
190 
191  if(it==module_map.end())
192  {
193  error() << "found no file that provides module " << module << eom;
194  return true;
195  }
196 
197  return typecheck_module(symbol_table, it->second);
198 }
199 
201  symbol_tablet &symbol_table,
202  language_modulet &module)
203 {
204  // already typechecked?
205 
206  if(module.type_checked)
207  return false;
208 
209  // already in progress?
210 
211  if(module.in_progress)
212  {
213  error() << "circular dependency in " << module.name << eom;
214  return true;
215  }
216 
217  module.in_progress=true;
218 
219  // first get dependencies of current module
220 
221  std::set<std::string> dependency_set;
222 
223  module.file->language->dependencies(module.name, dependency_set);
224 
225  for(std::set<std::string>::const_iterator it=
226  dependency_set.begin();
227  it!=dependency_set.end();
228  it++)
229  {
230  if(typecheck_module(symbol_table, *it))
231  {
232  module.in_progress=false;
233  return true;
234  }
235  }
236 
237  // type check it
238 
239  status() << "Type-checking " << module.name << eom;
240 
241  if(module.file->language->typecheck(symbol_table, module.name))
242  {
243  module.in_progress=false;
244  return true;
245  }
246 
247  module.type_checked=true;
248  module.in_progress=false;
249 
250  return false;
251 }
void show_parse(std::ostream &out)
languaget * language
Definition: language_file.h:41
mstreamt & status()
Definition: message.h:238
bool interfaces(symbol_tablet &symbol_table)
std::set< std::string > modulest
Definition: language_file.h:38
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void modules_provided(std::set< std::string > &modules)
Definition: language.h:52
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
bool typecheck_module(symbol_tablet &symbol_table, language_modulet &module)
The symbol table.
Definition: symbol_table.h:52
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
lazy_method_mapt lazy_method_map
Definition: language_file.h:72
std::string name
Definition: language_file.h:27
bool final(symbol_tablet &symbol_table)
modulest modules
Definition: language_file.h:39
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
Definition: language.cpp:26
file_mapt file_map
Definition: language_file.h:63
mstreamt & error()
Definition: message.h:223
void convert_lazy_method(const irep_idt &id, symbol_tablet &symbol_table)
virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &)
Definition: language.h:61
virtual bool parse(std::istream &instream, const std::string &path)=0
languagest languages
Definition: mode.cpp:29
module_mapt module_map
Definition: language_file.h:67
language_filet * file
Definition: language_file.h:29