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/message.h>
21 #include <util/std_types.h>
22 #include <util/symbol.h>
23 #include <util/symbol_table_base.h>
24 
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 
73  virtual bool generate_support_functions(
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 
127  // language id / description
128 
129  virtual std::string id() const { return ""; }
130  virtual std::string description() const { return ""; }
131  virtual std::set<std::string> extensions() const
132  { return std::set<std::string>(); }
133 
134  // show parse tree
135 
136  virtual void show_parse(std::ostream &out)=0;
137 
138  // conversion of expressions
139 
145  virtual bool from_expr(
146  const exprt &expr,
147  std::string &code,
148  const namespacet &ns);
149 
155  virtual bool from_type(
156  const typet &type,
157  std::string &code,
158  const namespacet &ns);
159 
165  virtual bool type_to_name(
166  const typet &type,
167  std::string &name,
168  const namespacet &ns);
169 
176  virtual bool to_expr(
177  const std::string &code,
178  const std::string &module,
179  exprt &expr,
180  const namespacet &ns)=0;
181 
182  virtual std::unique_ptr<languaget> new_language()=0;
183 
184  // constructor / destructor
185 
186  languaget() { }
187  virtual ~languaget() { }
188 
189 protected:
192 };
193 
194 #endif // CPROVER_UTIL_LANGUAGE_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
languaget::show_parse
virtual void show_parse(std::ostream &out)=0
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
system_library_symbolst
Definition: system_library_symbols.h:25
optionst
Definition: options.h:22
typet
The type of an expression, extends irept.
Definition: type.h:27
languaget::language_options_initialized
bool language_options_initialized
Definition: language.h:190
exprt
Base class for all expressions.
Definition: expr.h:54
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:93
languaget::modules_provided
virtual void modules_provided(std::set< std::string > &modules)
Definition: language.h:84
languaget::description
virtual std::string description() const
Definition: language.h:130
system_library_symbols.h
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::extensions
virtual std::set< std::string > extensions() const
Definition: language.h:131
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:21
std_types.h
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
symbol.h
Symbol table entry.
languaget::system_symbols
system_library_symbolst system_symbols
Definition: language.h:191
languaget::id
virtual std::string id() const
Definition: language.h:129
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:187
languaget::interfaces
virtual bool interfaces(symbol_tablet &symbol_table)
Definition: language.cpp:26
languaget
Definition: language.h:39
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:186
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