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