cprover
Loading...
Searching...
No Matches
language.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Abstract interface to support a programming language
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_LANGAPI_LANGUAGE_H
13#define CPROVER_LANGAPI_LANGUAGE_H
14
15#include <iosfwd>
16#include <memory> // unique_ptr
17#include <set>
18#include <string>
19#include <unordered_set>
20
21#include <util/invariant.h>
22#include <util/message.h>
23
24class exprt;
25class namespacet;
26class optionst;
28class symbol_tablet;
29class typet;
30
31#define OPT_FUNCTIONS \
32 "(function):"
33
34#define HELP_FUNCTIONS \
35 " --function name set main function name\n"
36
37class languaget:public messaget
38{
39public:
41 virtual void set_language_options(const optionst &)
42 {
43 }
44
45 // parse file
46
47 virtual bool preprocess(
48 std::istream &instream,
49 const std::string &path,
50 std::ostream &outstream)
51 {
52 // unused parameters
53 (void)instream;
54 (void)path;
55 (void)outstream;
56 return false;
57 }
58
59 virtual bool parse(
60 std::istream &instream,
61 const std::string &path)=0;
62
72 symbol_tablet &symbol_table)=0;
73
74 // add external dependencies of a given module to set
75
76 virtual void dependencies(
77 const std::string &module,
78 std::set<std::string> &modules);
79
80 // add modules provided by currently parsed file to set
81
82 virtual void modules_provided(std::set<std::string> &modules)
83 {
84 (void)modules; // unused parameter
85 }
86
92 virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
93 {
94 (void)methods; // unused parameter
95 }
96
101 virtual void
103 const irep_idt &function_id, symbol_table_baset &symbol_table)
104 {
105 // unused parameters
106 (void)function_id;
107 (void)symbol_table;
108 }
109
112 virtual bool final(symbol_table_baset &symbol_table);
113
114 // type check interfaces of currently parsed file
115
116 virtual bool interfaces(
117 symbol_tablet &symbol_table);
118
119 // type check a module in the currently parsed file
120
121 virtual bool typecheck(
122 symbol_tablet &symbol_table,
123 const std::string &module)=0;
124
126 virtual bool can_keep_file_local()
127 {
128 return false;
129 }
130
140 virtual bool typecheck(
141 symbol_tablet &symbol_table,
142 const std::string &module,
143 const bool keep_file_local)
144 {
145 INVARIANT(
146 false,
147 "three-argument typecheck should only be called for files written"
148 " in a language that allows file-local symbols, like C");
149 }
150
151 // language id / description
152
153 virtual std::string id() const = 0;
154 virtual std::string description() const = 0;
155 virtual std::set<std::string> extensions() const = 0;
156
157 // show parse tree
158
159 virtual void show_parse(std::ostream &out)=0;
160
161 // conversion of expressions
162
168 virtual bool from_expr(
169 const exprt &expr,
170 std::string &code,
171 const namespacet &ns);
172
178 virtual bool from_type(
179 const typet &type,
180 std::string &code,
181 const namespacet &ns);
182
188 virtual bool type_to_name(
189 const typet &type,
190 std::string &name,
191 const namespacet &ns);
192
199 virtual bool to_expr(
200 const std::string &code,
201 const std::string &module,
202 exprt &expr,
203 const namespacet &ns)=0;
204
205 virtual std::unique_ptr<languaget> new_language()=0;
206
207 // constructor / destructor
208
210 virtual ~languaget() { }
211};
212
213#endif // CPROVER_UTIL_LANGUAGE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
virtual void modules_provided(std::set< std::string > &modules)
Definition: language.h:82
virtual std::string description() const =0
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:47
languaget()
Definition: language.h:209
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
virtual bool can_keep_file_local()
Is it possible to call three-argument typecheck() on this object?
Definition: language.h:126
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
Definition: language.cpp:26
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:41
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.
virtual bool parse(std::istream &instream, const std::string &path)=0
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:50
virtual std::string id() const =0
virtual std::set< std::string > extensions() const =0
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:32
virtual std::unique_ptr< languaget > new_language()=0
virtual bool interfaces(symbol_tablet &symbol_table)
Definition: language.cpp:21
virtual void convert_lazy_method(const irep_idt &function_id, symbol_table_baset &symbol_table)
Requests this languaget should populate the body of method function_id in symbol_table.
Definition: language.h:102
virtual void show_parse(std::ostream &out)=0
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local)
typecheck without removing specified entries from the symbol table
Definition: language.h:140
virtual void methods_provided(std::unordered_set< irep_idt > &methods) const
Should fill methods with the symbol identifiers of all methods this languaget can provide a body for,...
Definition: language.h:92
virtual ~languaget()
Definition: language.h:210
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:29
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423