cprover
language_file.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_LANGAPI_LANGUAGE_FILE_H
11 #define CPROVER_LANGAPI_LANGUAGE_FILE_H
12 
13 #include <iosfwd>
14 #include <map>
15 #include <memory> // unique_ptr
16 #include <set>
17 #include <string>
18 #include <unordered_set>
19 
20 #include <util/message.h>
21 #include <util/symbol_table_base.h>
22 
23 class language_filet;
24 class languaget;
25 class symbol_tablet;
26 
27 class language_modulet final
28 {
29 public:
30  std::string name;
33 
35  type_checked(false),
36  in_progress(false),
37  file(nullptr)
38  {}
39 };
40 
41 class language_filet final
42 {
43 public:
44  typedef std::set<std::string> modulest;
46 
47  std::unique_ptr<languaget> language;
48  std::string filename;
49 
50  void get_modules();
51 
53  const irep_idt &id,
54  symbol_table_baset &symbol_table);
55 
56  explicit language_filet(const std::string &filename);
57  language_filet(const language_filet &rhs);
58 
60 };
61 
63 {
64 private:
65  typedef std::map<std::string, language_filet> file_mapt;
67 
68  typedef std::map<std::string, language_modulet> module_mapt;
70 
71  // Contains pointers into file_map!
72  // This is safe-ish as long as this is std::map.
73  typedef std::map<irep_idt, language_filet *> lazy_method_mapt;
75 
76 public:
77  language_filet &add_file(const std::string &filename)
78  {
79  language_filet language_file(filename);
80  return file_map.emplace(filename, std::move(language_file)).first->second;
81  }
82 
83  void remove_file(const std::string &filename)
84  {
85  // Clear relevant entries from lazy_method_map
86  language_filet *language_file = &file_map.at(filename);
87  std::unordered_set<irep_idt> files_methods;
88  for(auto const &method : lazy_method_map)
89  {
90  if(method.second == language_file)
91  files_methods.insert(method.first);
92  }
93  for(const irep_idt &method_name : files_methods)
94  lazy_method_map.erase(method_name);
95 
96  file_map.erase(filename);
97  }
98 
99  void clear_files()
100  {
101  lazy_method_map.clear();
102  file_map.clear();
103  }
104 
105  bool parse();
106 
107  void show_parse(std::ostream &out);
108 
109  bool generate_support_functions(symbol_tablet &symbol_table);
110 
111  bool
112  typecheck(symbol_tablet &symbol_table, const bool keep_file_local = false);
113 
114  bool final(symbol_table_baset &symbol_table);
115 
116  bool interfaces(symbol_tablet &symbol_table);
117 
118  // The method must have been added to the symbol table and registered
119  // in lazy_method_map (currently always in language_filest::typecheck)
120  // for this to be legal.
122  const irep_idt &id,
123  symbol_table_baset &symbol_table)
124  {
125  PRECONDITION(symbol_table.has_symbol(id));
126  lazy_method_mapt::iterator it=lazy_method_map.find(id);
127  if(it!=lazy_method_map.end())
128  it->second->convert_lazy_method(id, symbol_table);
129  }
130 
131  bool can_convert_lazy_method(const irep_idt &id) const
132  {
133  return lazy_method_map.count(id) != 0;
134  }
135 
136  void clear()
137  {
138  file_map.clear();
139  module_map.clear();
140  lazy_method_map.clear();
141  }
142 
143 protected:
144  bool typecheck_module(
145  symbol_tablet &symbol_table,
146  language_modulet &module,
147  const bool keep_file_local);
148 
149  bool typecheck_module(
150  symbol_tablet &symbol_table,
151  const std::string &module,
152  const bool keep_file_local);
153 };
154 
155 #endif // CPROVER_UTIL_LANGUAGE_FILE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
language_filet & add_file(const std::string &filename)
Definition: language_file.h:77
bool typecheck_module(symbol_tablet &symbol_table, language_modulet &module, const bool keep_file_local)
std::map< std::string, language_modulet > module_mapt
Definition: language_file.h:68
file_mapt file_map
Definition: language_file.h:66
void show_parse(std::ostream &out)
std::map< std::string, language_filet > file_mapt
Definition: language_file.h:65
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
bool interfaces(symbol_tablet &symbol_table)
lazy_method_mapt lazy_method_map
Definition: language_file.h:74
bool can_convert_lazy_method(const irep_idt &id) const
std::map< irep_idt, language_filet * > lazy_method_mapt
Definition: language_file.h:73
void convert_lazy_method(const irep_idt &id, symbol_table_baset &symbol_table)
void remove_file(const std::string &filename)
Definition: language_file.h:83
module_mapt module_map
Definition: language_file.h:69
bool generate_support_functions(symbol_tablet &symbol_table)
language_filet(const std::string &filename)
std::string filename
Definition: language_file.h:48
modulest modules
Definition: language_file.h:45
~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)
std::set< std::string > modulest
Definition: language_file.h:44
std::unique_ptr< languaget > language
Definition: language_file.h:47
std::string name
Definition: language_file.h:30
language_filet * file
Definition: language_file.h:32
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
The symbol table base class interface.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Definition: symbol_table.h:14
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Definition: kdev_t.h:19
Author: Diffblue Ltd.