cprover
ci_lazy_methods.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Bytecode
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #include "ci_lazy_methods.h"
10 #include "java_entry_point.h"
11 #include "java_class_loader.h"
12 #include "java_utils.h"
14 #include "remove_exceptions.h"
15 
16 #include <util/expr_iterator.h>
17 #include <util/suffix.h>
18 
20 
38  const symbol_tablet &symbol_table,
39  const irep_idt &main_class,
40  const std::vector<irep_idt> &main_jar_classes,
41  const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
42  java_class_loadert &java_class_loader,
43  const std::vector<irep_idt> &extra_instantiated_classes,
44  const select_pointer_typet &pointer_type_selector,
45  message_handlert &message_handler,
46  const synthetic_methods_mapt &synthetic_methods)
47  : messaget(message_handler),
48  main_class(main_class),
49  main_jar_classes(main_jar_classes),
50  lazy_methods_extra_entry_points(lazy_methods_extra_entry_points),
51  java_class_loader(java_class_loader),
52  extra_instantiated_classes(extra_instantiated_classes),
53  pointer_type_selector(pointer_type_selector),
54  synthetic_methods(synthetic_methods)
55 {
56  // build the class hierarchy
57  class_hierarchy(symbol_table);
58 }
59 
66 static bool references_class_model(const exprt &expr)
67 {
68  static const struct_tag_typet class_type("java::java.lang.Class");
69 
70  for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)
71  {
73  it->type() == class_type &&
74  has_suffix(
77  {
78  return true;
79  }
80  }
81 
82  return false;
83 }
84 
101  symbol_tablet &symbol_table,
102  method_bytecodet &method_bytecode,
103  const method_convertert &method_converter)
104 {
105  std::unordered_set<irep_idt> methods_to_convert_later =
106  entry_point_methods(symbol_table);
107 
108  // Add any extra entry points specified; we should elaborate these in the
109  // same way as the main function.
110  for(const auto &extra_function_generator : lazy_methods_extra_entry_points)
111  {
112  std::vector<irep_idt> extra_methods =
113  extra_function_generator(symbol_table);
114  methods_to_convert_later.insert(extra_methods.begin(), extra_methods.end());
115  }
116 
117  std::unordered_set<irep_idt> instantiated_classes;
118 
119  {
120  std::unordered_set<irep_idt> initial_callable_methods;
121  ci_lazy_methods_neededt initial_lazy_methods(
122  initial_callable_methods,
123  instantiated_classes,
124  symbol_table,
127  methods_to_convert_later, namespacet(symbol_table), initial_lazy_methods);
128  methods_to_convert_later.insert(
129  initial_callable_methods.begin(), initial_callable_methods.end());
130  }
131 
132  std::unordered_set<irep_idt> methods_already_populated;
133  std::unordered_set<class_method_descriptor_exprt, irep_hash>
134  called_virtual_functions;
135  bool class_initializer_seen = false;
136 
137  bool any_new_classes = true;
138  while(any_new_classes)
139  {
140  bool any_new_methods = true;
141  while(any_new_methods)
142  {
143  any_new_methods = false;
144  while(!methods_to_convert_later.empty())
145  {
146  std::unordered_set<irep_idt> methods_to_convert;
147  std::swap(methods_to_convert, methods_to_convert_later);
148  for(const auto &mname : methods_to_convert)
149  {
150  const auto conversion_result = convert_and_analyze_method(
151  method_converter,
152  methods_already_populated,
153  class_initializer_seen,
154  mname,
155  symbol_table,
156  methods_to_convert_later,
157  instantiated_classes,
158  called_virtual_functions);
159  any_new_methods |= conversion_result.new_method_seen;
160  class_initializer_seen |= conversion_result.class_initializer_seen;
161  }
162  }
163 
164  // Given the object types we now know may be created, populate more
165  // possible virtual function call targets:
166 
167  debug() << "CI lazy methods: add virtual method targets ("
168  << called_virtual_functions.size() << " callsites)" << eom;
169 
170  for(const class_method_descriptor_exprt &called_virtual_function :
171  called_virtual_functions)
172  {
174  called_virtual_function,
175  instantiated_classes,
176  methods_to_convert_later,
177  symbol_table);
178  }
179  }
180 
181  any_new_classes = handle_virtual_methods_with_no_callees(
182  methods_to_convert_later,
183  instantiated_classes,
184  called_virtual_functions,
185  symbol_table);
186  }
187 
188  // Remove symbols for methods that were declared but never used:
189  symbol_tablet keep_symbols;
190  // Manually keep @inflight_exception, as it is unused at this stage
191  // but will become used when the `remove_exceptions` pass is run:
192  keep_symbols.add(symbol_table.lookup_ref(INFLIGHT_EXCEPTION_VARIABLE_NAME));
193 
194  for(const auto &sym : symbol_table.symbols)
195  {
196  // Don't keep global variables (unless they're gathered below from a
197  // function that references them)
198  if(sym.second.is_static_lifetime)
199  continue;
200  if(sym.second.type.id()==ID_code)
201  {
202  // Don't keep functions that belong to this language that we haven't
203  // converted above
204  if(
205  (method_bytecode.contains_method(sym.first) ||
206  synthetic_methods.count(sym.first)) &&
207  !methods_already_populated.count(sym.first))
208  {
209  continue;
210  }
211  // If this is a function then add all the things used in it
212  gather_needed_globals(sym.second.value, symbol_table, keep_symbols);
213  }
214  keep_symbols.add(sym.second);
215  }
216 
217  debug() << "CI lazy methods: removed "
218  << symbol_table.symbols.size() - keep_symbols.symbols.size()
219  << " unreachable methods and globals" << eom;
220 
221  symbol_table.swap(keep_symbols);
222 
223  return false;
224 }
225 
234  std::unordered_set<irep_idt> &methods_to_convert_later,
235  std::unordered_set<irep_idt> &instantiated_classes,
236  const std::unordered_set<class_method_descriptor_exprt, irep_hash>
237  &virtual_functions,
238  symbol_tablet &symbol_table)
239 {
240  ci_lazy_methods_neededt lazy_methods_loader(
241  methods_to_convert_later,
242  instantiated_classes,
243  symbol_table,
245 
246  bool any_new_classes = false;
247  for(const class_method_descriptor_exprt &virtual_function : virtual_functions)
248  {
249  std::unordered_set<irep_idt> candidate_target_methods;
251  virtual_function,
252  instantiated_classes,
253  candidate_target_methods,
254  symbol_table);
255 
256  if(!candidate_target_methods.empty())
257  continue;
258 
259  const java_method_typet &java_method_type =
260  to_java_method_type(virtual_function.type());
261 
262  // Add the call class to instantiated_classes and assert that it
263  // didn't already exist. It can't be instantiated already, otherwise it
264  // would give a concrete definition of the called method, and
265  // candidate_target_methods would be non-empty.
266  const irep_idt &call_class = virtual_function.class_id();
267  bool was_missing = instantiated_classes.count(call_class) == 0;
268  CHECK_RETURN(was_missing);
269  any_new_classes = true;
270 
271  const typet &this_type = java_method_type.get_this()->type();
272  if(
273  const pointer_typet *this_pointer_type =
274  type_try_dynamic_cast<pointer_typet>(this_type))
275  {
276  lazy_methods_loader.add_all_needed_classes(*this_pointer_type);
277  }
278 
279  // That should in particular have added call_class to the possibly
280  // instantiated types.
281  bool still_missing = instantiated_classes.count(call_class) == 0;
282  CHECK_RETURN(!still_missing);
283 
284  // Make sure we add our return type as required, as we may not have
285  // seen any concrete instances of it being created.
286  const typet &return_type = java_method_type.return_type();
287  if(
288  const pointer_typet *return_pointer_type =
289  type_try_dynamic_cast<pointer_typet>(return_type))
290  {
291  lazy_methods_loader.add_all_needed_classes(*return_pointer_type);
292  }
293 
294  // Check that `get_virtual_method_target` returns a method now
295  const irep_idt &method_name = virtual_function.mangled_method_name();
296  const irep_idt method_id = get_virtual_method_target(
297  instantiated_classes, method_name, call_class, symbol_table);
298  CHECK_RETURN(!method_id.empty());
299 
300  // Add what it returns to methods_to_convert_later
301  methods_to_convert_later.insert(method_id);
302  }
303  return any_new_classes;
304 }
305 
317  const method_convertert &method_converter,
318  std::unordered_set<irep_idt> &methods_already_populated,
319  const bool class_initializer_already_seen,
320  const irep_idt &method_name,
321  symbol_tablet &symbol_table,
322  std::unordered_set<irep_idt> &methods_to_convert_later,
323  std::unordered_set<irep_idt> &instantiated_classes,
324  std::unordered_set<class_method_descriptor_exprt, irep_hash>
325  &called_virtual_functions)
326 {
328  if(!methods_already_populated.insert(method_name).second)
329  return result;
330 
331  debug() << "CI lazy methods: elaborate " << method_name << eom;
332 
333  // Note this wraps *references* to methods_to_convert_later &
334  // instantiated_classes
335  ci_lazy_methods_neededt needed_methods(
336  methods_to_convert_later,
337  instantiated_classes,
338  symbol_table,
340 
341  if(method_converter(method_name, needed_methods))
342  return result;
343 
344  const exprt &method_body = symbol_table.lookup_ref(method_name).value;
345  gather_virtual_callsites(method_body, called_virtual_functions);
346 
347  if(!class_initializer_already_seen && references_class_model(method_body))
348  {
349  result.class_initializer_seen = true;
350  const irep_idt initializer_signature =
352  if(symbol_table.has_symbol(initializer_signature))
353  methods_to_convert_later.insert(initializer_signature);
354  }
355  result.new_method_seen = true;
356  return result;
357 }
358 
364 std::unordered_set<irep_idt>
366 {
367  std::unordered_set<irep_idt> methods_to_convert_later;
368 
369  const main_function_resultt main_function = get_main_symbol(
370  symbol_table, this->main_class, this->get_message_handler());
371  if(!main_function.is_success())
372  {
373  // Failed, mark all functions in the given main class(es)
374  // reachable.
375  std::vector<irep_idt> reachable_classes;
376  if(!this->main_class.empty())
377  reachable_classes.push_back(this->main_class);
378  else
379  reachable_classes = this->main_jar_classes;
380  for(const irep_idt &class_name : reachable_classes)
381  {
382  const auto &methods =
383  this->java_class_loader.get_original_class(class_name)
385  for(const auto &method : methods)
386  {
387  const irep_idt methodid = "java::" + id2string(class_name) + "." +
388  id2string(method.name) + ":" +
389  id2string(method.descriptor);
390  methods_to_convert_later.insert(methodid);
391  }
392  }
393  }
394  else
395  methods_to_convert_later.insert(main_function.main_function.name);
396  return methods_to_convert_later;
397 }
398 
408  const std::unordered_set<irep_idt> &entry_points,
409  const namespacet &ns,
410  ci_lazy_methods_neededt &needed_lazy_methods)
411 {
412  for(const auto &mname : entry_points)
413  {
414  const auto &symbol=ns.lookup(mname);
415  const auto &mtype = to_java_method_type(symbol.type);
416  for(const auto &param : mtype.parameters())
417  {
418  if(param.type().id()==ID_pointer)
419  {
420  const pointer_typet &original_pointer = to_pointer_type(param.type());
421  needed_lazy_methods.add_all_needed_classes(original_pointer);
422  }
423  }
424  }
425 
426  // Also add classes whose instances are magically
427  // created by the JVM and so won't be spotted by
428  // looking for constructors and calls as usual:
429  needed_lazy_methods.add_needed_class("java::java.lang.String");
430  needed_lazy_methods.add_needed_class("java::java.lang.Class");
431  needed_lazy_methods.add_needed_class("java::java.lang.Object");
432 
433  // As in class_loader, ensure these classes stay available
434  for(const auto &id : extra_instantiated_classes)
435  needed_lazy_methods.add_needed_class("java::" + id2string(id));
436 }
437 
443  const exprt &e,
444  std::unordered_set<class_method_descriptor_exprt, irep_hash> &result)
445 {
446  if(e.id()!=ID_code)
447  return;
448  const codet &c=to_code(e);
449  if(
450  c.get_statement() == ID_function_call &&
452  to_code_function_call(c).function()))
453  {
454  result.insert(
456  }
457  else
458  {
459  for(const exprt &op : e.operands())
461  }
462 }
463 
475  const class_method_descriptor_exprt &called_function,
476  const std::unordered_set<irep_idt> &instantiated_classes,
477  std::unordered_set<irep_idt> &callable_methods,
478  symbol_tablet &symbol_table)
479 {
480  const auto &call_class = called_function.class_id();
481  const auto &method_name = called_function.mangled_method_name();
482 
483  class_hierarchyt::idst self_and_child_classes =
485  self_and_child_classes.push_back(call_class);
486 
487  for(const irep_idt &class_name : self_and_child_classes)
488  {
489  const irep_idt method_id = get_virtual_method_target(
490  instantiated_classes, method_name, class_name, symbol_table);
491  if(!method_id.empty())
492  callable_methods.insert(method_id);
493  }
494 }
495 
502  const exprt &e,
503  const symbol_tablet &symbol_table,
504  symbol_tablet &needed)
505 {
506  if(e.id()==ID_symbol)
507  {
508  // If the symbol isn't in the symbol table at all, then it is defined
509  // on an opaque type (i.e. we don't have the class definition at this point)
510  // and will be created during the typecheck phase.
511  // We don't mark it as 'needed' as it doesn't exist yet to keep.
512  const auto findit=
513  symbol_table.symbols.find(to_symbol_expr(e).get_identifier());
514  if(findit!=symbol_table.symbols.end() &&
515  findit->second.is_static_lifetime)
516  {
517  needed.add(findit->second);
518  // Gather any globals referenced in the initialiser:
519  gather_needed_globals(findit->second.value, symbol_table, needed);
520  }
521  }
522  else
523  forall_operands(opit, e)
524  gather_needed_globals(*opit, symbol_table, needed);
525 }
526 
540  const std::unordered_set<irep_idt> &instantiated_classes,
541  const irep_idt &call_basename,
542  const irep_idt &classname,
543  const symbol_tablet &symbol_table)
544 {
545  // Program-wide, is this class ever instantiated?
546  if(!instantiated_classes.count(classname))
547  return irep_idt();
548 
549  auto resolved_call =
550  get_inherited_method_implementation(call_basename, classname, symbol_table);
551 
552  if(resolved_call)
553  return resolved_call->get_full_component_identifier();
554  else
555  return irep_idt();
556 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
method_bytecodet
Definition: ci_lazy_methods.h:34
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:161
JAVA_CLASS_MODEL_SUFFIX
#define JAVA_CLASS_MODEL_SUFFIX
Definition: java_bytecode_language.h:272
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
java_class_loadert::get_original_class
const java_bytecode_parse_treet & get_original_class(const irep_idt &class_name)
Definition: java_class_loader.h:85
ci_lazy_methodst::convert_method_resultt
Definition: ci_lazy_methods.h:161
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:4545
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:94
get_inherited_method_implementation
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
Definition: resolve_inherited_component.cpp:124
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
ci_lazy_methodst::ci_lazy_methodst
ci_lazy_methodst(const symbol_tablet &symbol_table, const irep_idt &main_class, const std::vector< irep_idt > &main_jar_classes, const std::vector< load_extra_methodst > &lazy_methods_extra_entry_points, java_class_loadert &java_class_loader, const std::vector< irep_idt > &extra_instantiated_classes, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler, const synthetic_methods_mapt &synthetic_methods)
Constructor for lazy-method loading.
Definition: ci_lazy_methods.cpp:37
typet
The type of an expression, extends irept.
Definition: type.h:29
ci_lazy_methodst::operator()
bool operator()(symbol_tablet &symbol_table, method_bytecodet &method_bytecode, const method_convertert &method_converter)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
Definition: ci_lazy_methods.cpp:100
ci_lazy_methodst::lazy_methods_extra_entry_points
const std::vector< load_extra_methodst > & lazy_methods_extra_entry_points
Definition: ci_lazy_methods.h:151
get_main_symbol
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
Definition: java_entry_point.cpp:514
exprt
Base class for all expressions.
Definition: expr.h:53
java_string_library_preprocess.h
Produce code for simple implementation of String Java libraries.
ci_lazy_methods_neededt::add_needed_class
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
Definition: ci_lazy_methods_needed.cpp:71
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
irep_idt
dstringt irep_idt
Definition: irep.h:32
ci_lazy_methodst::entry_point_methods
std::unordered_set< irep_idt > entry_point_methods(const symbol_tablet &symbol_table)
Entry point methods are either:
Definition: ci_lazy_methods.cpp:365
messaget::eom
static eomt eom
Definition: message.h:297
ci_lazy_methodst::main_jar_classes
std::vector< irep_idt > main_jar_classes
Definition: ci_lazy_methods.h:150
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:53
method_convertert
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
Definition: ci_lazy_methods.h:92
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
code_typet::get_this
const parametert * get_this() const
Definition: std_types.h:823
resolve_inherited_component.h
Given a class and a component (either field or method), find the closest parent that defines that com...
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:109
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
ci_lazy_methodst::class_hierarchy
class_hierarchyt class_hierarchy
Definition: ci_lazy_methods.h:148
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
messaget::result
mstreamt & result() const
Definition: message.h:409
get_java_class_literal_initializer_signature
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
Definition: java_entry_point.cpp:75
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
ci_lazy_methodst::convert_and_analyze_method
convert_method_resultt convert_and_analyze_method(const method_convertert &method_converter, std::unordered_set< irep_idt > &methods_already_populated, const bool class_initializer_already_seen, const irep_idt &method_name, symbol_tablet &symbol_table, std::unordered_set< irep_idt > &methods_to_convert_later, std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< class_method_descriptor_exprt, irep_hash > &called_virtual_functions)
Convert a method, add it to the populated set, add needed methods to methods_to_convert_later and add...
Definition: ci_lazy_methods.cpp:316
ci_lazy_methodst::pointer_type_selector
const select_pointer_typet & pointer_type_selector
Definition: ci_lazy_methods.h:154
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
java_class_loader.h
INFLIGHT_EXCEPTION_VARIABLE_NAME
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Definition: remove_exceptions.h:23
java_entry_point.h
select_pointer_typet
Definition: select_pointer_type.h:26
ci_lazy_methodst::handle_virtual_methods_with_no_callees
bool handle_virtual_methods_with_no_callees(std::unordered_set< irep_idt > &methods_to_convert_later, std::unordered_set< irep_idt > &instantiated_classes, const std::unordered_set< class_method_descriptor_exprt, irep_hash > &virtual_functions, symbol_tablet &symbol_table)
Look for virtual callsites with no candidate targets.
Definition: ci_lazy_methods.cpp:233
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
class_hierarchyt::idst
std::vector< irep_idt > idst
Definition: class_hierarchy.h:45
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
dstringt::empty
bool empty() const
Definition: dstring.h:88
ci_lazy_methodst::get_virtual_method_targets
void get_virtual_method_targets(const class_method_descriptor_exprt &called_function, const std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< irep_idt > &callable_methods, symbol_tablet &symbol_table)
Find possible callees, excluding types that are not known to be instantiated.
Definition: ci_lazy_methods.cpp:474
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:281
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
ci_lazy_methodst::java_class_loader
java_class_loadert & java_class_loader
Definition: ci_lazy_methods.h:152
main_function_resultt
Definition: java_entry_point.h:87
ci_lazy_methods.h
Collect methods needed to be loaded using the lazy method.
ci_lazy_methodst::gather_needed_globals
void gather_needed_globals(const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed)
See output.
Definition: ci_lazy_methods.cpp:501
remove_exceptions.h
Remove function exceptional returns.
references_class_model
static bool references_class_model(const exprt &expr)
Checks if an expression refers to any class literals (e.g.
Definition: ci_lazy_methods.cpp:66
java_class_loadert
Class responsible to load .class files.
Definition: java_class_loader.h:27
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:311
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
method_bytecodet::contains_method
bool contains_method(const irep_idt &method_id) const
Definition: ci_lazy_methods.h:52
suffix.h
can_cast_expr< class_method_descriptor_exprt >
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:4608
to_class_method_descriptor_expr
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition: std_expr.h:4598
symbol_tablet::swap
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
Definition: symbol_table.h:80
ci_lazy_methodst::synthetic_methods
const synthetic_methods_mapt & synthetic_methods
Definition: ci_lazy_methods.h:155
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
ci_lazy_methodst::main_class
irep_idt main_class
Definition: ci_lazy_methods.h:149
ci_lazy_methodst::gather_virtual_callsites
void gather_virtual_callsites(const exprt &e, std::unordered_set< class_method_descriptor_exprt, irep_hash > &result)
Get places where virtual functions are called.
Definition: ci_lazy_methods.cpp:442
class_method_descriptor_exprt::class_id
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition: std_expr.h:4553
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
ci_lazy_methods_neededt
Definition: ci_lazy_methods_needed.h:25
exprt::operands
operandst & operands()
Definition: expr.h:95
messaget::debug
mstreamt & debug() const
Definition: message.h:429
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
ci_lazy_methods_neededt::add_all_needed_classes
void add_all_needed_classes(const pointer_typet &pointer_type)
Add to the needed classes all classes specified, the replacement type if it will be replaced,...
Definition: ci_lazy_methods_needed.cpp:93
java_utils.h
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
ci_lazy_methodst::extra_instantiated_classes
const std::vector< irep_idt > & extra_instantiated_classes
Definition: ci_lazy_methods.h:153
ci_lazy_methodst::initialize_instantiated_classes
void initialize_instantiated_classes(const std::unordered_set< irep_idt > &entry_points, const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods)
Build up a list of methods whose type may be passed around reachable from the entry point.
Definition: ci_lazy_methods.cpp:407
java_method_typet
Definition: java_types.h:103
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
class_hierarchyt::get_children_trans
idst get_children_trans(const irep_idt &id) const
Definition: class_hierarchy.h:68
ci_lazy_methodst::get_virtual_method_target
irep_idt get_virtual_method_target(const std::unordered_set< irep_idt > &instantiated_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
Find a virtual callee, if one is defined and the callee type is known to exist.
Definition: ci_lazy_methods.cpp:539
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35