cprover
java_bytecode_vtable.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_bytecode_vtable.h"
10 
11 #include <algorithm>
12 #include <iterator>
13 
14 #include <util/symbol.h>
15 #include <util/symbol_table.h>
16 #include <util/namespace.h>
17 #include <util/std_expr.h>
18 #include <util/std_types.h>
19 #include <util/vtable.h>
20 
21 const char ID_virtual_name[]="virtual_name";
22 
24 {
26 public:
28  virtual_name(method.get(ID_virtual_name))
29  {
30  }
31 
32  bool operator()(const class_typet::methodt &method) const
33  {
34  return virtual_name==method.get(ID_virtual_name);
35  }
36 };
37 
39 {
40  const irep_idt &name;
41 
42 public:
43  explicit is_name_equalt(const irep_idt &name):
44  name(name)
45  {
46  }
47 
48  bool operator()(const class_typet::componentt &component) const
49  {
50  return name==component.get_name();
51  }
52 };
53 
55 {
57  const std::string &module;
58  const namespacet ns;
59 
60 public:
61  bool has_error;
62 
65  const std::string &module):
67  module(module),
69  has_error(false)
70  {
71  }
72 
74  {
75  const std::string &class_name(id2string(class_type.get(ID_name)));
76  return symbol_table.lookup(vtnamest::get_type(class_name));
77  }
78 
79  void create_vtable_symbol(symbolt &result, const class_typet &class_type)
80  {
81  const std::string &class_name=id2string(class_type.get(ID_name));
82  const std::string &base_class_name=id2string(class_type.get(ID_base_name));
83  const symbolt &type_symbol(get_vt_type_symbol(class_type));
84  result.name=vtnamest::get_table(class_name);
85  result.base_name=vtnamest::get_table_base(base_class_name);
86  result.pretty_name=result.base_name;
87  result.mode=type_symbol.mode;
88  result.module=module;
89  result.location=type_symbol.location;
90  result.type=symbol_typet(type_symbol.name);
91  result.is_lvalue=true;
92  result.is_state_var=true;
93  result.is_static_lifetime=true;
94  }
95 
96  bool has_component(const class_typet &vtable_type, const irep_idt &ifc_name)
97  {
98  const class_typet::componentst &comps(vtable_type.components());
99  const is_name_equalt pred(ifc_name);
100  return std::find_if(comps.begin(), comps.end(), pred)!=comps.end();
101  }
102 
103  void add_vtable_entry(struct_exprt &vtable_value,
104  const class_typet &interface, const class_typet &implementor,
105  const class_typet::methodt &implementation)
106  {
107  const class_typet::methodst &methods(interface.methods());
108  const is_virtual_name_equalt pred(implementation);
109  const class_typet::methodst::const_iterator ifc_method(
110  std::find_if(methods.begin(), methods.end(), pred));
111  assert(methods.end()!=ifc_method);
112  symbolt &vtable_type_symbol(get_vt_type_symbol(implementor));
113  class_typet &vtable_type(to_class_type(vtable_type_symbol.type));
114  const irep_idt &ifc_name(ifc_method->get_name());
115  if(has_component(vtable_type, ifc_name))
116  return;
117 
118  struct_typet::componentt entry_component;
119  entry_component.set_name(ifc_name);
120  entry_component.set_base_name(ifc_method->get_base_name());
121  entry_component.type()=pointer_type(implementation.type());
122  vtable_type.components().push_back(entry_component);
123 
124  const irep_idt &impl_name(implementation.get_name());
125  const symbol_exprt impl_symbol(impl_name, implementation.type());
126  const address_of_exprt impl_ref(impl_symbol);
127  vtable_value.copy_to_operands(impl_ref);
128  }
129 
130  const class_typet &get_class_type(const irept &base)
131  {
132  const typet &type(static_cast<const typet &>(base.find(ID_type)));
133  const symbol_typet &symbol_type(to_symbol_type(type));
134  const irep_idt &base_class_name(symbol_type.get_identifier());
135  assert(symbol_table.has_symbol(base_class_name));
136  const symbolt &base_class_symbol(ns.lookup(base_class_name));
137  return to_class_type(base_class_symbol.type);
138  }
139 
140  bool has_method(const irept &base, const class_typet::methodt &method)
141  {
142  const typet &type(static_cast<const typet &>(base.find(ID_type)));
143  const symbol_typet &symbol_type(to_symbol_type(type));
144  const irep_idt &base_class_name(symbol_type.get_identifier());
145  if(!symbol_table.has_symbol(base_class_name))
146  return false;
147  const symbolt &base_class_symbol(ns.lookup(base_class_name));
148  const class_typet &base_class_type(to_class_type(base_class_symbol.type));
149  const class_typet::methodst &methods(base_class_type.methods());
150  const is_virtual_name_equalt pred(method);
151  return std::find_if(methods.begin(), methods.end(), pred)!=methods.end();
152  }
153 
155  std::vector<class_typet> &result,
156  const irept::subt &types,
157  const class_typet::methodt &method)
158  {
159  for(irept::subt::const_iterator it=types.begin();
160  it!=types.end(); ++it)
161  {
162  if(!has_method(*it, method))
163  continue;
164  result.push_back(get_class_type(*it));
165  }
166  }
167 
168  bool is_virtual(const class_typet::methodt &method)
169  {
170  return method.get_bool(ID_is_virtual)
171  && !method.get_bool(ID_constructor);
172  }
173 
175  struct_exprt &vtable_value,
176  const class_typet &class_type,
177  const class_typet::methodt &method)
178  {
179  if(!is_virtual(method))
180  return;
181  std::vector<class_typet> bases;
182  extract_types(bases, class_type.bases(), method);
183  // extract_types(bases, class_type.find(ID_interfaces).get_sub(), method);
184  for(const std::vector<class_typet>::value_type &b : bases)
185  add_vtable_entry(vtable_value, b, class_type, method);
186  }
187 
188  void create_vtable_entry(struct_exprt &vtable_value,
189  const class_typet &class_type, const class_typet::methodt &method)
190  {
191  if(!is_virtual(method))
192  return;
193  add_vtable_entry(vtable_value, class_type, class_type, method);
194  }
195 
196  void set_vtable_value(symbolt &vtable_symbol, const class_typet &class_type,
197  struct_exprt &vtable_value)
198  {
199  const std::string &class_name(id2string(class_type.get(ID_name)));
200  const irep_idt vttype(vtnamest::get_type(class_name));
201  vtable_value.type()=symbol_typet(vttype);
202  vtable_symbol.value=vtable_value;
203  }
204 
205  bool is_class_with_vt(const symbolt &symbol)
206  {
207  if(!symbol.is_type || ID_struct!=symbol.type.id())
208  return false;
209  const class_typet &class_type(to_class_type(symbol.type));
210  const std::string &class_name(id2string(class_type.get(ID_name)));
211  return symbol_table.has_symbol(vtnamest::get_type(class_name));
212  }
213 
214  void operator()(const irep_idt &symbol_name)
215  {
216  const symbolt &symbol=symbol_table.lookup(symbol_name);
217  if(!is_class_with_vt(symbol))
218  return;
219  const class_typet &class_type(to_class_type(symbol.type));
220  const std::string &class_name(id2string(symbol_name));
221  if(symbol_table.has_symbol(vtnamest::get_table(class_name)))
222  return;
223  symbolt vtable_symbol;
224  create_vtable_symbol(vtable_symbol, class_type);
225  const class_typet::methodst &methods(class_type.methods());
226  struct_exprt vtable_value;
227  for(const class_typet::methodst::value_type &m : methods)
228  create_base_vtable_entries(vtable_value, class_type, m);
229  for(const class_typet::methodst::value_type &m : methods)
230  create_vtable_entry(vtable_value, class_type, m);
231  set_vtable_value(vtable_symbol, class_type, vtable_value);
232  assert(!symbol_table.add(vtable_symbol));
233  }
234 };
235 
236 
237 /*******************************************************************
238 
239  Function: java_bytecode_vtable
240 
241  Inputs:
242 
243  Outputs:
244 
245  Purpose:
246 
247 \*******************************************************************/
248 
250  symbol_tablet &symbol_table,
251  const std::string &module)
252 {
253  const symbol_tablet::symbolst &symbols(symbol_table.symbols);
254  std::vector<irep_idt> names;
255  names.reserve(symbols.size());
256  std::transform(symbols.begin(), symbols.end(), std::back_inserter(names),
257  [](const std::pair<irep_idt, symbolt> &entry)
258  { return entry.first;});
259  java_bytecode_vtable_factoryt factory(symbol_table, module);
260  std::for_each(names.begin(), names.end(), factory);
261  return factory.has_error;
262 }
263 
264 static void create_vtable_type(
265  const irep_idt &vt_name,
266  symbol_tablet &symbol_table,
267  const symbolt &class_symbol)
268 {
269  symbolt vt_symb_type;
270  vt_symb_type.name=vt_name;
271  vt_symb_type.base_name=vtnamest::get_type_base(
272  id2string(class_symbol.base_name));
273  vt_symb_type.pretty_name=vt_symb_type.base_name;
274  vt_symb_type.mode=class_symbol.mode;
275  vt_symb_type.module=class_symbol.module;
276  vt_symb_type.location=class_symbol.location;
277  vt_symb_type.type=struct_typet();
278  vt_symb_type.type.set(ID_name, vt_symb_type.name);
279  vt_symb_type.is_type=true;
280  assert(!symbol_table.add(vt_symb_type));
281 }
282 
283 #define ID_vtable_pointer "@vtable_pointer"
284 
286  const irep_idt &vt_name,
287  symbolt &class_symbol)
288 {
290 
291  comp.type()=pointer_type(symbol_typet(vt_name));
295  comp.set("is_vtptr", true);
296 
297  struct_typet &class_type=to_struct_type(class_symbol.type);
298  class_type.components().push_back(comp);
299 }
300 
301 /*******************************************************************
302 
303  Function: create_vtable_symbol
304 
305  Inputs:
306 
307  Outputs:
308 
309  Purpose:
310 
311 \*******************************************************************/
312 
314  symbol_tablet &symbol_table,
315  const symbolt &class_symbol)
316 {
317  const irep_idt vttype=
318  vtnamest::get_type(id2string(class_symbol.name));
319 
320  if(!symbol_table.has_symbol(vttype))
321  create_vtable_type(vttype, symbol_table, class_symbol);
322 }
323 
324 /*******************************************************************
325 
326  Function: has_vtable_info
327 
328  Inputs:
329 
330  Outputs:
331 
332  Purpose:
333 
334 \*******************************************************************/
335 
337  const symbol_tablet &symbol_table,
338  const symbolt &class_symbol)
339 {
340  return
341  symbol_table.has_symbol(vtnamest::get_type(id2string(class_symbol.name))) &&
343 }
344 
345 /*******************************************************************
346 
347  Function: create_vtable_pointer
348 
349  Inputs:
350 
351  Outputs:
352 
353  Purpose:
354 
355 \*******************************************************************/
356 
357 void create_vtable_pointer(symbolt &class_symbol)
358 {
359  const irep_idt vttype=
360  vtnamest::get_type(id2string(class_symbol.name));
361 
362  add_vtable_pointer_member(vttype, class_symbol);
363 }
364 
365 /*******************************************************************
366 
367  Function: get_virtual_name
368 
369  Inputs:
370 
371  Outputs:
372 
373  Purpose:
374 
375 \*******************************************************************/
376 
378 {
379  const std::string &name(id2string(method.get(ID_name)));
380  const std::string::size_type vname_start(name.find_last_of('.') + 1);
381  std::string virtual_name(name.substr(vname_start));
382  method.set(ID_virtual_name, virtual_name);
383 }
384 
385 static exprt get_ref(
386  const exprt &this_obj,
387  const symbol_typet &target_type)
388 {
389  const typet &type(this_obj.type());
390  const irep_idt &type_id(type.id());
391  if(ID_symbol==type_id)
392  return get_ref(address_of_exprt(this_obj), target_type);
393  assert(ID_pointer==type_id);
394  const typecast_exprt cast(this_obj, pointer_type(target_type));
395  return dereference_exprt(cast, target_type);
396 }
397 
398 static std::string get_full_class_name(const std::string &name)
399 {
400  const bool has_prefix(name.find("java::")!=std::string::npos);
401  const std::string::size_type offset=
402  has_prefix ? std::string("java::").size() : 0;
403  const std::string::size_type end(name.find_first_of(':', offset));
404  const std::string::size_type last_sep(name.rfind('.', end));
405  return name.substr(0, last_sep);
406 }
407 
408 /*******************************************************************
409 
410  Function: make_vtable_function
411 
412  Inputs:
413 
414  Outputs:
415 
416  Purpose:
417 
418 \*******************************************************************/
419 
421  const exprt &func,
422  const exprt &this_obj)
423 {
424  const irep_idt &func_name(func.get(ID_identifier));
425  const std::string class_id(get_full_class_name(id2string(func_name)));
426 
427  // TODO: Handle unavailable models!
428  if(class_id.find("java.")!=std::string::npos)
429  {
430  // When translating a single java_bytecode_parse_treet, we don't know
431  // which classes will eventually be available yet. If we could provide
432  // access to the class loader here, we know which classes have been
433  // loaded successfully. For classes which have not been loaded, returning
434  // "func" is equivalent to an unimplemented function.
435  return func;
436  }
437 
438  const symbol_typet vtable_type(vtnamest::get_type(class_id));
439  const pointer_typet vt_ptr_type=pointer_type(vtable_type);
440  const symbol_typet target_type(class_id);
441  const exprt this_ref(get_ref(this_obj, target_type));
442  const typet ref_type(this_ref.type());
443  const member_exprt vtable_member(this_ref, ID_vtable_pointer, vt_ptr_type);
444  const dereference_exprt vtable(vtable_member, vtable_type); // TODO: cast?
445  const pointer_typet func_ptr_type=pointer_type(func.type());
446  const member_exprt func_ptr(vtable, func_name, func_ptr_type);
447  const dereference_exprt virtual_func(func_ptr, func.type());
448  return virtual_func;
449 }
const irep_idt & get_name() const
Definition: std_types.h:179
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
static exprt get_ref(const exprt &this_obj, const symbol_typet &target_type)
semantic type conversion
Definition: std_expr.h:1725
void set_virtual_name(class_typet::methodt &method)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
const char ID_virtual_name[]
Symbol table entry.
const class_typet & get_class_type(const irept &base)
bool is_virtual(const class_typet::methodt &method)
std::vector< irept > subt
Definition: irep.h:91
irep_idt mode
Language mode.
Definition: symbol.h:55
void set_base_name(const irep_idt &base_name)
Definition: std_types.h:194
void set_name(const irep_idt &name)
Definition: std_types.h:184
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void create_vtable_entry(struct_exprt &vtable_value, const class_typet &class_type, const class_typet::methodt &method)
std::vector< componentt > componentst
Definition: std_types.h:240
exprt value
Initial value of symbol.
Definition: symbol.h:40
const componentst & components() const
Definition: std_types.h:242
bool operator()(const class_typet::methodt &method) const
static void add_vtable_pointer_member(const irep_idt &vt_name, symbolt &class_symbol)
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:58
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const irep_idt & name
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
symbolt & get_vt_type_symbol(const class_typet &class_type)
bool is_static_lifetime
Definition: symbol.h:70
java_bytecode_vtable_factoryt(symbol_tablet &symbol_table, const std::string &module)
bool has_method(const irept &base, const class_typet::methodt &method)
typet get_type(const format_tokent &token)
Extract member of struct or union.
Definition: std_expr.h:3214
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const irep_idt & id() const
Definition: irep.h:189
bool has_vtable_info(const symbol_tablet &symbol_table, const symbolt &class_symbol)
const methodst & methods() const
Definition: std_types.h:345
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
symbolst symbols
Definition: symbol_table.h:57
A reference into the symbol table.
Definition: std_types.h:109
exprt make_vtable_function(const exprt &func, const exprt &this_obj)
void create_vtable_pointer(symbolt &class_symbol)
The pointer type.
Definition: std_types.h:1343
void set_vtable_value(symbolt &vtable_symbol, const class_typet &class_type, struct_exprt &vtable_value)
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void create_base_vtable_entries(struct_exprt &vtable_value, const class_typet &class_type, const class_typet::methodt &method)
std::unordered_map< irep_idt, symbolt, irep_id_hash > symbolst
Definition: symbol_table.h:55
Base class for tree-like data structures with sharing.
Definition: irep.h:87
bool operator()(const class_typet::componentt &component) const
is_name_equalt(const irep_idt &name)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
Operator to return the address of an object.
Definition: std_expr.h:2593
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:252
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
static void create_vtable_type(const irep_idt &vt_name, symbol_tablet &symbol_table, const symbolt &class_symbol)
componentt methodt
Definition: std_types.h:342
#define ID_vtable_pointer
void create_vtable_symbol(symbol_tablet &symbol_table, const symbolt &class_symbol)
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
API to type classes.
void create_vtable_symbol(symbolt &result, const class_typet &class_type)
bool is_class_with_vt(const symbolt &symbol)
void operator()(const irep_idt &symbol_name)
Base class for all expressions.
Definition: expr.h:46
bool is_state_var
Definition: symbol.h:66
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
void set_pretty_name(const irep_idt &name)
Definition: std_types.h:214
is_virtual_name_equalt(const class_typet::methodt &method)
bool has_component(const class_typet &vtable_type, const irep_idt &ifc_name)
void add_vtable_entry(struct_exprt &vtable_value, const class_typet &interface, const class_typet &implementor, const class_typet::methodt &implementation)
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const irept::subt & bases() const
Definition: std_types.h:365
bool is_type
Definition: symbol.h:66
C++ class type.
Definition: std_types.h:334
struct constructor from list of elements
Definition: std_expr.h:1464
bool java_bytecode_vtable(symbol_tablet &symbol_table, const std::string &module)
void extract_types(std::vector< class_typet > &result, const irept::subt &types, const class_typet::methodt &method)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const irep_idt & get_identifier() const
Definition: std_types.h:126
static std::string get_full_class_name(const std::string &name)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
componentst methodst
Definition: std_types.h:343
bool is_lvalue
Definition: symbol.h:71
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:407