cprover
language.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract interface to support a programming language
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_LANGAPI_LANGUAGE_H
13 #define CPROVER_LANGAPI_LANGUAGE_H
14 
15 #include <unordered_set>
16 #include <iosfwd>
17 #include <string>
18 #include <memory> // unique_ptr
19 
20 #include <util/symbol.h>
21 #include <util/std_types.h>
22 #include <util/message.h>
23 
25 
26 class symbol_tablet;
27 class symbol_table_baset;
28 class exprt;
29 class namespacet;
30 class typet;
31 class cmdlinet;
32 
33 #define OPT_FUNCTIONS \
34  "(function):"
35 
36 #define HELP_FUNCTIONS \
37  " --function name set main function name\n"
38 
39 class languaget:public messaget
40 {
41 public:
42  // Parse language-specific options
43  virtual void get_language_options(const cmdlinet &) {}
44 
45  // parse file
46 
47  virtual bool preprocess(
48  std::istream &instream,
49  const std::string &path,
50  std::ostream &outstream) { return false; }
51 
52  virtual bool parse(
53  std::istream &instream,
54  const std::string &path)=0;
55 
64  virtual bool generate_support_functions(
65  symbol_tablet &symbol_table)=0;
66 
67  // add external dependencies of a given module to set
68 
69  virtual void dependencies(
70  const std::string &module,
71  std::set<std::string> &modules);
72 
73  // add modules provided by currently parsed file to set
74 
75  virtual void modules_provided(std::set<std::string> &modules)
76  { }
77 
78  // add lazy functions provided to set
79 
80  virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
81  { }
82 
83  // populate a lazy method
84  virtual void
86  const irep_idt &function_id, symbol_table_baset &symbol_table)
87  { }
88 
91  virtual bool final(symbol_table_baset &symbol_table);
92 
93  // type check interfaces of currently parsed file
94 
95  virtual bool interfaces(
96  symbol_tablet &symbol_table);
97 
98  // type check a module in the currently parsed file
99 
100  virtual bool typecheck(
101  symbol_tablet &symbol_table,
102  const std::string &module)=0;
103 
104  // language id / description
105 
106  virtual std::string id() const { return ""; }
107  virtual std::string description() const { return ""; }
108  virtual std::set<std::string> extensions() const
109  { return std::set<std::string>(); }
110 
111  // show parse tree
112 
113  virtual void show_parse(std::ostream &out)=0;
114 
115  // conversion of expressions
116 
122  virtual bool from_expr(
123  const exprt &expr,
124  std::string &code,
125  const namespacet &ns);
126 
132  virtual bool from_type(
133  const typet &type,
134  std::string &code,
135  const namespacet &ns);
136 
142  virtual bool type_to_name(
143  const typet &type,
144  std::string &name,
145  const namespacet &ns);
146 
153  virtual bool to_expr(
154  const std::string &code,
155  const std::string &module,
156  exprt &expr,
157  const namespacet &ns)=0;
158 
159  virtual std::unique_ptr<languaget> new_language()=0;
160 
161  void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
162 
163  // constructor / destructor
164 
165  languaget() { }
166  virtual ~languaget() { }
167 
168 protected:
169  void generate_opaque_method_stubs(symbol_tablet &symbol_table);
171  symbolt &symbol,
172  symbol_tablet &symbol_table);
173 
175  const symbolt &function_symbol,
176  size_t parameter_index,
177  const code_typet::parametert &parameter);
178 
179  static irep_idt get_stub_return_symbol_name(const irep_idt &function_id);
180 
183 
184 private:
185  bool is_symbol_opaque_function(const symbolt &symbol);
187  symbolt &function_symbol,
188  symbol_tablet &symbol_table);
189 
191 };
192 #endif // CPROVER_UTIL_LANGUAGE_H
The type of an expression.
Definition: type.h:22
bool is_symbol_opaque_function(const symbolt &symbol)
To identify if a given symbol is an opaque function and hence needs to be stubbed.
Definition: language.cpp:159
languaget()
Definition: language.h:165
virtual std::set< std::string > extensions() const
Definition: language.h:108
virtual std::string description() const
Definition: language.h:107
Symbol table entry.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:161
virtual ~languaget()
Definition: language.h:166
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
virtual bool type_to_name(const typet &type, std::string &name, const namespacet &ns)
Encodes the given type in a language-specific way.
Definition: language.cpp:55
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Definition: language.h:85
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:47
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
virtual irep_idt generate_opaque_stub_body(symbolt &symbol, symbol_tablet &symbol_table)
To generate the stub function for the opaque function in question.
Definition: language.cpp:114
virtual void modules_provided(std::set< std::string > &modules)
Definition: language.h:75
static irep_idt get_stub_return_symbol_name(const irep_idt &function_id)
To get the name of the symbol to be used for the return value of the function.
Definition: language.cpp:146
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const
Definition: language.h:80
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
virtual bool interfaces(symbol_tablet &symbol_table)
Definition: language.cpp:26
virtual std::string id() const
Definition: language.h:106
virtual bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0
Parses the given string into an expression.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual std::unique_ptr< languaget > new_language()=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool language_options_initialized
Definition: language.h:182
void generate_opaque_parameter_symbols(symbolt &function_symbol, symbol_tablet &symbol_table)
To create stub parameter symbols for each parameter the function has and assign their IDs into the pa...
Definition: language.cpp:177
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
Definition: language.cpp:46
virtual void show_parse(std::ostream &out)=0
API to type classes.
Base class for all expressions.
Definition: expr.h:42
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
Definition: language.cpp:31
The symbol table base class interface.
virtual parameter_symbolt build_stub_parameter_symbol(const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert &parameter)
To build the parameter symbol and choose its name.
Definition: language.cpp:129
bool generate_opaque_stubs
Definition: language.h:181
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition: language.cpp:37
virtual bool parse(std::istream &instream, const std::string &path)=0
system_library_symbolst system_symbols
Definition: language.h:190
void generate_opaque_method_stubs(symbol_tablet &symbol_table)
When there are opaque methods (e.g.
Definition: language.cpp:79
void set_should_generate_opaque_method_stubs(bool should_generate_stubs)
Turn on or off stub generation.
Definition: language.cpp:68