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 {
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->typecheck(symbol_table, ""))
133  return true;
134  // register lazy methods.
135  // TODO: learn about modules and generalise this
136  // to module-providing languages if required.
137  std::unordered_set<irep_idt> lazy_method_ids;
138  file.second.language->methods_provided(lazy_method_ids);
139  for(const auto &id : lazy_method_ids)
140  lazy_method_map[id]=&file.second;
141  }
142  }
143 
144  // typecheck modules
145 
146  for(auto &module : module_map)
147  {
148  if(typecheck_module(symbol_table, module.second))
149  return true;
150  }
151 
152  return false;
153 }
154 
156  symbol_tablet &symbol_table)
157 {
158  std::set<std::string> languages;
159 
160  for(auto &file : file_map)
161  {
162  if(languages.insert(file.second.language->id()).second)
163  if(file.second.language->generate_support_functions(symbol_table))
164  return true;
165  }
166 
167  return false;
168 }
169 
171 {
172  std::set<std::string> languages;
173 
174  for(auto &file : file_map)
175  {
176  if(languages.insert(file.second.language->id()).second)
177  if(file.second.language->final(symbol_table))
178  return true;
179  }
180 
181  return false;
182 }
183 
185  symbol_tablet &symbol_table)
186 {
187  for(auto &file : file_map)
188  {
189  if(file.second.language->interfaces(symbol_table))
190  return true;
191  }
192 
193  return false;
194 }
195 
197  symbol_tablet &symbol_table,
198  const std::string &module)
199 {
200  // check module map
201 
202  module_mapt::iterator it=module_map.find(module);
203 
204  if(it==module_map.end())
205  {
206  error() << "found no file that provides module " << module << eom;
207  return true;
208  }
209 
210  return typecheck_module(symbol_table, it->second);
211 }
212 
214  symbol_tablet &symbol_table,
215  language_modulet &module)
216 {
217  // already typechecked?
218 
219  if(module.type_checked)
220  return false;
221 
222  // already in progress?
223 
224  if(module.in_progress)
225  {
226  error() << "circular dependency in " << module.name << eom;
227  return true;
228  }
229 
230  module.in_progress=true;
231 
232  // first get dependencies of current module
233 
234  std::set<std::string> dependency_set;
235 
236  module.file->language->dependencies(module.name, dependency_set);
237 
238  for(std::set<std::string>::const_iterator it=
239  dependency_set.begin();
240  it!=dependency_set.end();
241  it++)
242  {
243  if(typecheck_module(symbol_table, *it))
244  {
245  module.in_progress=false;
246  return true;
247  }
248  }
249 
250  // type check it
251 
252  status() << "Type-checking " << module.name << eom;
253 
254  if(module.file->language->typecheck(symbol_table, module.name))
255  {
256  module.in_progress=false;
257  return true;
258  }
259 
260  module.type_checked=true;
261  module.in_progress=false;
262 
263  return false;
264 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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
bool typecheck(symbol_tablet &symbol_table)
Definition: language_file.cpp:85
messaget::status
mstreamt & status() const
Definition: message.h:401
language_filest::typecheck_module
bool typecheck_module(symbol_tablet &symbol_table, language_modulet &module)
Definition: language_file.cpp:213
language_filet
Definition: language_file.h:40
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:53
messaget::eom
static eomt eom
Definition: message.h:284
language_modulet
Definition: language_file.h:26
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:155
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:386
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:21
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
language.h
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:170
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:184
language_filest::parse
bool parse()
Definition: language_file.cpp:53
languaget
Definition: language.h:39
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