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 <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 #include <util/std_types.h>
24 #include <util/symbol.h>
25 #include <util/symbol_table_base.h>
26 
27 class symbol_tablet;
28 class exprt;
29 class namespacet;
30 class optionst;
31 class typet;
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:
43  virtual void set_language_options(const optionst &)
44  {
45  }
46 
47  // parse file
48 
49  virtual bool preprocess(
50  std::istream &instream,
51  const std::string &path,
52  std::ostream &outstream)
53  {
54  // unused parameters
55  (void)instream;
56  (void)path;
57  (void)outstream;
58  return false;
59  }
60 
61  virtual bool parse(
62  std::istream &instream,
63  const std::string &path)=0;
64 
74  symbol_tablet &symbol_table)=0;
75 
76  // add external dependencies of a given module to set
77 
78  virtual void dependencies(
79  const std::string &module,
80  std::set<std::string> &modules);
81 
82  // add modules provided by currently parsed file to set
83 
84  virtual void modules_provided(std::set<std::string> &modules)
85  {
86  (void)modules; // unused parameter
87  }
88 
94  virtual void methods_provided(std::unordered_set<irep_idt> &methods) const
95  {
96  (void)methods; // unused parameter
97  }
98 
103  virtual void
105  const irep_idt &function_id, symbol_table_baset &symbol_table)
106  {
107  // unused parameters
108  (void)function_id;
109  (void)symbol_table;
110  }
111 
114  virtual bool final(symbol_table_baset &symbol_table);
115 
116  // type check interfaces of currently parsed file
117 
118  virtual bool interfaces(
119  symbol_tablet &symbol_table);
120 
121  // type check a module in the currently parsed file
122 
123  virtual bool typecheck(
124  symbol_tablet &symbol_table,
125  const std::string &module)=0;
126 
128  virtual bool can_keep_file_local()
129  {
130  return false;
131  }
132 
142  virtual bool typecheck(
143  symbol_tablet &symbol_table,
144  const std::string &module,
145  const bool keep_file_local)
146  {
147  INVARIANT(
148  false,
149  "three-argument typecheck should only be called for files written"
150  " in a language that allows file-local symbols, like C");
151  }
152 
153  // language id / description
154 
155  virtual std::string id() const = 0;
156  virtual std::string description() const = 0;
157  virtual std::set<std::string> extensions() const = 0;
158 
159  // show parse tree
160 
161  virtual void show_parse(std::ostream &out)=0;
162 
163  // conversion of expressions
164 
170  virtual bool from_expr(
171  const exprt &expr,
172  std::string &code,
173  const namespacet &ns);
174 
180  virtual bool from_type(
181  const typet &type,
182  std::string &code,
183  const namespacet &ns);
184 
190  virtual bool type_to_name(
191  const typet &type,
192  std::string &name,
193  const namespacet &ns);
194 
201  virtual bool to_expr(
202  const std::string &code,
203  const std::string &module,
204  exprt &expr,
205  const namespacet &ns)=0;
206 
207  virtual std::unique_ptr<languaget> new_language()=0;
208 
209  // constructor / destructor
210 
211  languaget() { }
212  virtual ~languaget() { }
213 };
214 
215 #endif // CPROVER_UTIL_LANGUAGE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
languaget::id
virtual std::string id() const =0
optionst
Definition: options.h:23
typet
The type of an expression, extends irept.
Definition: type.h:29
languaget::can_keep_file_local
virtual bool can_keep_file_local()
Is it possible to call three-argument typecheck() on this object?
Definition: language.h:128
languaget::description
virtual std::string description() const =0
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
languaget::extensions
virtual std::set< std::string > extensions() const =0
languaget::convert_lazy_method
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:104
languaget::new_language
virtual std::unique_ptr< languaget > new_language()=0
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
languaget::modules_provided
virtual void modules_provided(std::set< std::string > &modules)
Definition: language.h:84
languaget::generate_support_functions
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
languaget::from_type
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
languaget::dependencies
virtual void dependencies(const std::string &module, std::set< std::string > &modules)
Definition: language.cpp:31
languaget::from_expr
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
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
std_types.h
Pre-defined types.
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
symbol.h
Symbol table entry.
languaget::typecheck
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:142
languaget::to_expr
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.
languaget::~languaget
virtual ~languaget()
Definition: language.h:212
languaget::interfaces
virtual bool interfaces(symbol_tablet &symbol_table)
Definition: language.cpp:26
languaget
Definition: language.h:40
languaget::typecheck
virtual bool typecheck(symbol_tablet &symbol_table, const std::string &module)=0
languaget::preprocess
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream)
Definition: language.h:49
symbol_table_base.h
Author: Diffblue Ltd.
message.h
languaget::languaget
languaget()
Definition: language.h:211
languaget::type_to_name
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
languaget::methods_provided
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:94
validation_modet::INVARIANT
@ INVARIANT