cprover
language.cpp
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 #include "language.h"
13 
14 #include <util/expr.h>
15 #include <util/symbol.h>
16 #include <util/symbol_table.h>
17 #include <util/prefix.h>
18 #include <util/cprover_prefix.h>
19 #include <util/std_types.h>
20 
22 {
23  return false;
24 }
25 
27 {
28  return false;
29 }
30 
32  const std::string &,
33  std::set<std::string> &)
34 {
35 }
36 
38  const exprt &expr,
39  std::string &code,
40  const namespacet &)
41 {
42  code=expr.pretty();
43  return false;
44 }
45 
47  const typet &type,
48  std::string &code,
49  const namespacet &)
50 {
51  code=type.pretty();
52  return false;
53 }
54 
56  const typet &type,
57  std::string &name,
58  const namespacet &)
59 {
60  // probably ansi-c/type2name could be used as better fallback if moved to
61  // util/
62  name=type.pretty();
63  return false;
64 }
65 
69  bool should_generate_stubs)
70 {
71  generate_opaque_stubs=should_generate_stubs;
72 }
73 
80 {
82  {
84 
85  for(auto &symbol_entry : symbol_table.symbols)
86  {
87  if(is_symbol_opaque_function(symbol_entry.second))
88  {
89  symbolt &symbol=
90  *symbol_table.get_writeable(symbol_entry.second.name);
91 
92  generate_opaque_parameter_symbols(symbol, symbol_table);
93 
94  irep_idt return_symbol_id=generate_opaque_stub_body(
95  symbol,
96  symbol_table);
97 
98  if(return_symbol_id!=ID_nil)
99  {
100  symbol.type.set("opaque_method_capture_symbol", return_symbol_id);
101  }
102  }
103  }
104  }
105 }
106 
115  symbolt &symbol,
116  symbol_tablet &symbol_table)
117 {
118  return ID_nil;
119 }
120 
130  const symbolt &function_symbol,
131  size_t parameter_index,
132  const code_typet::parametert &parameter)
133 {
134  error() << "language " << id()
135  << " doesn't implement build_stub_parameter_symbol. "
136  << "This means cannot use opaque functions." << eom;
137 
138  return parameter_symbolt();
139 }
140 
147 {
148  std::ostringstream return_symbol_name_builder;
149  return_symbol_name_builder << "to_return_" << function_id;
150  return return_symbol_name_builder.str();
151 }
152 
153 
160 {
161  std::set<std::string> headers;
162  // Don't create stubs for symbols like:
163  // __CPROVER_blah (which aren't real external functions)
164  // and strstr (which we will model for ourselves later)
165  bool is_internal=system_symbols.is_symbol_internal_symbol(symbol, headers);
166 
167  return !symbol.is_type &&
168  symbol.value.id()==ID_nil &&
169  symbol.type.id()==ID_code &&
170  !is_internal;
171 }
172 
178  symbolt &function_symbol,
179  symbol_tablet &symbol_table)
180 {
181  code_typet &function_type = to_code_type(function_symbol.type);
182  code_typet::parameterst &parameters=function_type.parameters();
183  for(std::size_t i=0; i<parameters.size(); ++i)
184  {
185  code_typet::parametert &param=parameters[i];
186  const parameter_symbolt &param_symbol=
187  build_stub_parameter_symbol(function_symbol, i, param);
188 
189  param.set_base_name(param_symbol.base_name);
190  param.set_identifier(param_symbol.name);
191 
192  symbol_table.add(param_symbol);
193  }
194 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
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
Base type of functions.
Definition: std_types.h:764
Symbol table entry.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
Definition: symbol.h:161
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
bool is_symbol_internal_symbol(const symbolt &symbol, std::set< std::string > &out_system_headers) const
To find out if a symbol is an internal symbol.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
std::vector< parametert > parameterst
Definition: std_types.h:767
exprt value
Initial value of symbol.
Definition: symbol.h:37
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
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void set_base_name(const irep_idt &name)
Definition: std_types.h:835
virtual symbolt * get_writeable(const irep_idt &name) override
Find a symbol in the symbol table for read-write access.
Definition: symbol_table.h:87
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
const irep_idt & id() const
Definition: irep.h:259
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 bool final(symbol_table_baset &symbol_table)
Final adjustments, e.g.
Definition: language.cpp:21
virtual bool interfaces(symbol_tablet &symbol_table)
Definition: language.cpp:26
virtual std::string id() const
Definition: language.h:106
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Abstract interface to support a programming language.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
const symbolst & symbols
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
typet type
Type of symbol.
Definition: symbol.h:34
void set_identifier(const irep_idt &identifier)
Definition: std_types.h:830
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
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
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
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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
bool is_type
Definition: symbol.h:63
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(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void set_should_generate_opaque_method_stubs(bool should_generate_stubs)
Turn on or off stub generation.
Definition: language.cpp:68