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 typet;
29
30#define OPT_FUNCTIONS \
31 "(function):"
32
33#define HELP_FUNCTIONS " {y--function} {uname} \t set main function name\n"
34
35class languaget:public messaget
36{
37public:
39 virtual void set_language_options(const optionst &)
40 {
41 }
42
43 // parse file
44
45 virtual bool preprocess(
46 std::istream &instream,
47 const std::string &path,
48 std::ostream &outstream)
49 {
50 // unused parameters
51 (void)instream;
52 (void)path;
53 (void)outstream;
54 return false;
55 }
56
57 virtual bool parse(
58 std::istream &instream,
59 const std::string &path)=0;
60
69 virtual bool generate_support_functions(symbol_table_baset &symbol_table) = 0;
70
71 // add external dependencies of a given module to set
72
73 virtual void dependencies(
74 const std::string &module,
75 std::set<std::string> &modules);
76
77 // add modules provided by currently parsed file to set
78
79 virtual void modules_provided(std::set<std::string> &modules)
80 {
81 (void)modules; // unused parameter
82 }
83
89 virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
90 {
91 (void)methods; // unused parameter
92 }
93
98 virtual void
100 const irep_idt &function_id, symbol_table_baset &symbol_table)
101 {
102 // unused parameters
103 (void)function_id;
104 (void)symbol_table;
105 }
106
109 virtual bool final(symbol_table_baset &symbol_table);
110
111 // type check interfaces of currently parsed file
112
113 virtual bool interfaces(symbol_table_baset &symbol_table);
114
115 // type check a module in the currently parsed file
116
117 virtual bool
118 typecheck(symbol_table_baset &symbol_table, const std::string &module) = 0;
119
121 virtual bool can_keep_file_local()
122 {
123 return false;
124 }
125
135 virtual bool typecheck(
136 symbol_table_baset &symbol_table,
137 const std::string &module,
138 const bool keep_file_local)
139 {
140 INVARIANT(
141 false,
142 "three-argument typecheck should only be called for files written"
143 " in a language that allows file-local symbols, like C");
144 }
145
146 // language id / description
147
148 virtual std::string id() const = 0;
149 virtual std::string description() const = 0;
150 virtual std::set<std::string> extensions() const = 0;
151
152 // show parse tree
153
154 virtual void show_parse(std::ostream &out)=0;
155
156 // conversion of expressions
157
163 virtual bool from_expr(
164 const exprt &expr,
165 std::string &code,
166 const namespacet &ns);
167
173 virtual bool from_type(
174 const typet &type,
175 std::string &code,
176 const namespacet &ns);
177
183 virtual bool type_to_name(
184 const typet &type,
185 std::string &name,
186 const namespacet &ns);
187
194 virtual bool to_expr(
195 const std::string &code,
196 const std::string &module,
197 exprt &expr,
198 const namespacet &ns)=0;
199
200 virtual std::unique_ptr<languaget> new_language()=0;
201
202 // constructor / destructor
203
205 virtual ~languaget() { }
206};
207
208#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:39
Base class for all expressions.
Definition expr.h:56
virtual bool interfaces(symbol_table_baset &symbol_table)
Definition language.cpp:21
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition language.h:39
virtual void modules_provided(std::set< std::string > &modules)
Definition language.h:79
virtual std::string description() const =0
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition language.h:45
virtual bool can_keep_file_local()
Is it possible to call three-argument typecheck() on this object?
Definition language.h:121
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 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:99
virtual void show_parse(std::ostream &out)=0
virtual bool typecheck(symbol_table_baset &symbol_table, const std::string &module)=0
virtual bool generate_support_functions(symbol_table_baset &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
virtual bool typecheck(symbol_table_baset &symbol_table, const std::string &module, const bool keep_file_local)
typecheck without removing specified entries from the symbol table
Definition language.h:135
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:89
virtual ~languaget()
Definition language.h:205
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 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