cprover
java_bytecode_language.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <string>
12 
13 #include <util/symbol_table.h>
14 #include <util/suffix.h>
15 #include <util/config.h>
16 #include <util/cmdline.h>
17 #include <util/string2int.h>
18 #include <json/json_parser.h>
19 
21 
26 #include "java_entry_point.h"
27 #include "java_bytecode_parser.h"
28 #include "java_class_loader.h"
29 
30 #include "expr2java.h"
31 
36 {
37  assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
38  string_refinement_enabled=cmd.isset("string-refine");
39  if(cmd.isset("java-max-input-array-length"))
41  std::stoi(cmd.get_value("java-max-input-array-length"));
42  if(cmd.isset("java-max-vla-length"))
43  max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length"));
44  if(cmd.isset("lazy-methods-context-sensitive"))
46  else if(cmd.isset("lazy-methods"))
48  else
50 
51  if(cmd.isset("java-cp-include-files"))
52  {
53  java_cp_include_files=cmd.get_value("java-cp-include-files");
54  // load file list from JSON file
55  if(java_cp_include_files[0]=='@')
56  {
57  jsont json_cp_config;
58  if(parse_json(
59  java_cp_include_files.substr(1),
61  json_cp_config))
62  throw "cannot read JSON input configuration for JAR loading";
63 
64  if(!json_cp_config.is_object())
65  throw "the JSON file has a wrong format";
66  jsont include_files=json_cp_config["jar"];
67  if(!include_files.is_array())
68  throw "the JSON file has a wrong format";
69 
70  // add jars from JSON config file to classpath
71  for(const jsont &file_entry : include_files.array)
72  {
73  assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar"));
74  config.java.classpath.push_back(file_entry.value);
75  }
76  }
77  }
78  else
80 }
81 
82 std::set<std::string> java_bytecode_languaget::extensions() const
83 {
84  return { "class", "jar" };
85 }
86 
87 void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
88 {
89  // modules.insert(translation_unit(parse_path));
90 }
91 
94  std::istream &instream,
95  const std::string &path,
96  std::ostream &outstream)
97 {
98  // there is no preprocessing!
99  return true;
100 }
101 
103  std::istream &instream,
104  const std::string &path)
105 {
108 
109  // look at extension
110  if(has_suffix(path, ".class"))
111  {
112  // override main_class
114  }
115  else if(has_suffix(path, ".jar"))
116  {
117  java_class_loader_limitt class_loader_limit(
121  {
122  // Does it have a main class set in the manifest?
123  jar_filet::manifestt manifest=
124  java_class_loader.jar_pool(class_loader_limit, path).get_manifest();
125  std::string manifest_main_class=manifest["Main-Class"];
126 
127  if(manifest_main_class!="")
128  main_class=manifest_main_class;
129  }
130  else
132 
133  // Do we have one now?
134  if(main_class.empty())
135  {
136  status() << "JAR file without entry point: loading class files" << eom;
137  java_class_loader.load_entire_jar(class_loader_limit, path);
138  for(const auto &kv : java_class_loader.jar_map.at(path).entries)
139  main_jar_classes.push_back(kv.first);
140  }
141  else
143  }
144  else
145  assert(false);
146 
147  if(!main_class.empty())
148  {
149  status() << "Java main class: " << main_class << eom;
151  }
152 
153  return false;
154 }
155 
169  const std::set<irep_idt> &needed_classes,
170  const irep_idt &call_basename,
171  const irep_idt &classname,
172  const symbol_tablet &symbol_table)
173 {
174  // Program-wide, is this class ever instantiated?
175  if(!needed_classes.count(classname))
176  return irep_idt();
177  auto methodid=id2string(classname)+"."+id2string(call_basename);
178  if(symbol_table.has_symbol(methodid))
179  return methodid;
180  else
181  return irep_idt();
182 }
183 
196  const code_function_callt &c,
197  const std::set<irep_idt> &needed_classes,
198  std::vector<irep_idt> &needed_methods,
199  symbol_tablet &symbol_table,
200  const class_hierarchyt &class_hierarchy)
201 {
202  const auto &called_function=c.function();
203  assert(called_function.id()==ID_virtual_function);
204 
205  const auto &call_class=called_function.get(ID_C_class);
206  assert(!call_class.empty());
207  const auto &call_basename=called_function.get(ID_component_name);
208  assert(!call_basename.empty());
209 
210  auto old_size=needed_methods.size();
211 
212  auto child_classes=class_hierarchy.get_children_trans(call_class);
213  for(const auto &child_class : child_classes)
214  {
215  auto child_method=
217  needed_classes,
218  call_basename,
219  child_class,
220  symbol_table);
221  if(!child_method.empty())
222  needed_methods.push_back(child_method);
223  }
224 
225  irep_idt parent_class_id=call_class;
226  while(1)
227  {
228  auto parent_method=
230  needed_classes,
231  call_basename,
232  parent_class_id,
233  symbol_table);
234  if(!parent_method.empty())
235  {
236  needed_methods.push_back(parent_method);
237  break;
238  }
239  else
240  {
241  auto findit=class_hierarchy.class_map.find(parent_class_id);
242  if(findit==class_hierarchy.class_map.end())
243  break;
244  else
245  {
246  const auto &entry=findit->second;
247  if(entry.parents.empty())
248  break;
249  else
250  parent_class_id=entry.parents[0];
251  }
252  }
253  }
254 
255  if(needed_methods.size()==old_size)
256  {
257  // Didn't find any candidate callee. Generate a stub.
258  std::string stubname=id2string(call_class)+"."+id2string(call_basename);
259  symbolt symbol;
260  symbol.name=stubname;
261  symbol.base_name=call_basename;
262  symbol.type=c.function().type();
263  symbol.value.make_nil();
264  symbol.mode=ID_java;
265  symbol_table.add(symbol);
266  }
267 }
268 
274  const exprt &e,
275  std::vector<const code_function_callt *> &result)
276 {
277  if(e.id()!=ID_code)
278  return;
279  const codet &c=to_code(e);
280  if(c.get_statement()==ID_function_call &&
281  to_code_function_call(c).function().id()==ID_virtual_function)
282  result.push_back(&to_code_function_call(c));
283  else
284  forall_operands(it, e)
285  gather_virtual_callsites(*it, result);
286 }
287 
294  const exprt &e,
295  const symbol_tablet &symbol_table,
296  symbol_tablet &needed)
297 {
298  if(e.id()==ID_symbol)
299  {
300  // If the symbol isn't in the symbol table at all, then it is defined
301  // on an opaque type (i.e. we don't have the class definition at this point)
302  // and will be created during the typecheck phase.
303  // We don't mark it as 'needed' as it doesn't exist yet to keep.
304  auto findit=symbol_table.symbols.find(to_symbol_expr(e).get_identifier());
305  if(findit!=symbol_table.symbols.end() &&
306  findit->second.is_static_lifetime)
307  {
308  needed.add(findit->second);
309  }
310  }
311  else
312  forall_operands(opit, e)
313  gather_needed_globals(*opit, symbol_table, needed);
314 }
315 
323 static void gather_field_types(
324  const typet &class_type,
325  const namespacet &ns,
327 {
328  const auto &underlying_type=to_struct_type(ns.follow(class_type));
329  for(const auto &field : underlying_type.components())
330  {
331  if(field.type().id()==ID_struct || field.type().id()==ID_symbol)
332  gather_field_types(field.type(), ns, lazy_methods);
333  else if(field.type().id()==ID_pointer)
334  {
335  // Skip array primitive pointers, for example:
336  if(field.type().subtype().id()!=ID_symbol)
337  continue;
338  const auto &field_classid=
339  to_symbol_type(field.type().subtype()).get_identifier();
340  if(lazy_methods.add_needed_class(field_classid))
341  gather_field_types(field.type().subtype(), ns, lazy_methods);
342  }
343  }
344 }
345 
355  const std::vector<irep_idt> &entry_points,
356  const namespacet &ns,
357  const class_hierarchyt &ch,
359 {
360  for(const auto &mname : entry_points)
361  {
362  const auto &symbol=ns.lookup(mname);
363  const auto &mtype=to_code_type(symbol.type);
364  for(const auto &param : mtype.parameters())
365  {
366  if(param.type().id()==ID_pointer)
367  {
368  const auto &param_classid=
369  to_symbol_type(param.type().subtype()).get_identifier();
370  std::vector<irep_idt> class_and_parents=
371  ch.get_parents_trans(param_classid);
372  class_and_parents.push_back(param_classid);
373  for(const auto &classid : class_and_parents)
374  lazy_methods.add_needed_class(classid);
375  gather_field_types(param.type().subtype(), ns, lazy_methods);
376  }
377  }
378  }
379 
380  // Also add classes whose instances are magically
381  // created by the JVM and so won't be spotted by
382  // looking for constructors and calls as usual:
383  lazy_methods.add_needed_class("java::java.lang.String");
384  lazy_methods.add_needed_class("java::java.lang.Class");
385  lazy_methods.add_needed_class("java::java.lang.Object");
386 }
387 
389  symbol_tablet &symbol_table,
390  const std::string &module)
391 {
394 
395  // first convert all
396  for(java_class_loadert::class_mapt::const_iterator
397  c_it=java_class_loader.class_map.begin();
398  c_it!=java_class_loader.class_map.end();
399  c_it++)
400  {
401  if(c_it->second.parsed_class.name.empty())
402  continue;
403 
404  debug() << "Converting class " << c_it->first << eom;
405 
407  c_it->second,
408  symbol_table,
411  lazy_methods,
415  return true;
416  }
417 
418  // Now incrementally elaborate methods
419  // that are reachable from this entry point.
421  {
422  // ci: context-insensitive.
423  if(do_ci_lazy_method_conversion(symbol_table, lazy_methods))
424  return true;
425  }
426 
427  // now typecheck all
430  return true;
431 
432  return false;
433 }
434 
449  symbol_tablet &symbol_table,
451 {
452  class_hierarchyt ch;
453  ch(symbol_table);
454 
455  std::vector<irep_idt> method_worklist1;
456  std::vector<irep_idt> method_worklist2;
457 
458  auto main_function=
459  get_main_symbol(symbol_table, main_class, get_message_handler(), true);
460  if(main_function.stop_convert)
461  {
462  // Failed, mark all functions in the given main class(es) reachable.
463  std::vector<irep_idt> reachable_classes;
464  if(!main_class.empty())
465  reachable_classes.push_back(main_class);
466  else
467  reachable_classes=main_jar_classes;
468  for(const auto &classname : reachable_classes)
469  {
470  const auto &methods=
471  java_class_loader.class_map.at(classname).parsed_class.methods;
472  for(const auto &method : methods)
473  {
474  const irep_idt methodid="java::"+id2string(classname)+"."+
475  id2string(method.name)+":"+
476  id2string(method.signature);
477  method_worklist2.push_back(methodid);
478  }
479  }
480  }
481  else
482  method_worklist2.push_back(main_function.main_function.name);
483 
484  std::set<irep_idt> needed_classes;
485 
486  {
487  std::vector<irep_idt> needed_clinits;
488  ci_lazy_methodst initial_lazy_methods(
489  needed_clinits,
490  needed_classes,
491  symbol_table);
493  method_worklist2,
494  namespacet(symbol_table),
495  ch,
496  initial_lazy_methods);
497  method_worklist2.insert(
498  method_worklist2.end(),
499  needed_clinits.begin(),
500  needed_clinits.end());
501  }
502 
503  std::set<irep_idt> methods_already_populated;
504  std::vector<const code_function_callt *> virtual_callsites;
505 
506  bool any_new_methods;
507  do
508  {
509  any_new_methods=false;
510  while(!method_worklist2.empty())
511  {
512  std::swap(method_worklist1, method_worklist2);
513  for(const auto &mname : method_worklist1)
514  {
515  if(!methods_already_populated.insert(mname).second)
516  continue;
517  auto findit=lazy_methods.find(mname);
518  if(findit==lazy_methods.end())
519  {
520  debug() << "Skip " << mname << eom;
521  continue;
522  }
523  debug() << "CI lazy methods: elaborate " << mname << eom;
524  const auto &parsed_method=findit->second;
525  // Note this wraps *references* to method_worklist2, needed_classes:
527  method_worklist2,
528  needed_classes,
529  symbol_table);
531  *parsed_method.first,
532  *parsed_method.second,
533  symbol_table,
539  symbol_table.lookup(mname).value,
540  virtual_callsites);
541  any_new_methods=true;
542  }
543  method_worklist1.clear();
544  }
545 
546  // Given the object types we now know may be created, populate more
547  // possible virtual function call targets:
548 
549  debug() << "CI lazy methods: add virtual method targets ("
550  << virtual_callsites.size()
551  << " callsites)"
552  << eom;
553 
554  for(const auto &callsite : virtual_callsites)
555  {
556  // This will also create a stub if a virtual callsite has no targets.
558  *callsite,
559  needed_classes,
560  method_worklist2,
561  symbol_table,
562  ch);
563  }
564  }
565  while(any_new_methods);
566 
567  // Remove symbols for methods that were declared but never used:
568  symbol_tablet keep_symbols;
569 
570  for(const auto &sym : symbol_table.symbols)
571  {
572  if(sym.second.is_static_lifetime)
573  continue;
574  if(lazy_methods.count(sym.first) &&
575  !methods_already_populated.count(sym.first))
576  {
577  continue;
578  }
579  if(sym.second.type.id()==ID_code)
580  gather_needed_globals(sym.second.value, symbol_table, keep_symbols);
581  keep_symbols.add(sym.second);
582  }
583 
584  debug() << "CI lazy methods: removed "
585  << symbol_table.symbols.size() - keep_symbols.symbols.size()
586  << " unreachable methods and globals"
587  << eom;
588 
589  symbol_table.swap(keep_symbols);
590 
591  return false;
592 }
593 
600  std::set<irep_idt> &methods) const
601 {
602  for(const auto &kv : lazy_methods)
603  methods.insert(kv.first);
604 }
605 
616  const irep_idt &id,
617  symbol_tablet &symtab)
618 {
619  const auto &lazy_method_entry=lazy_methods.at(id);
621  *lazy_method_entry.first,
622  *lazy_method_entry.second,
623  symtab,
627 }
628 
630 {
631  /*
632  if(c_final(symbol_table, message_handler)) return true;
633  */
634  java_internal_additions(symbol_table);
635 
636 
639  if(res.stop_convert)
640  return res.error_found;
641 
642  symbolt entry=res.main_function;
643 
644  return(
646  symbol_table,
647  main_class,
651 }
652 
653 void java_bytecode_languaget::show_parse(std::ostream &out)
654 {
655  java_class_loader(main_class).output(out);
656 }
657 
659 {
660  return new java_bytecode_languaget;
661 }
662 
664  const exprt &expr,
665  std::string &code,
666  const namespacet &ns)
667 {
668  code=expr2java(expr, ns);
669  return false;
670 }
671 
673  const typet &type,
674  std::string &code,
675  const namespacet &ns)
676 {
677  code=type2java(type, ns);
678  return false;
679 }
680 
682  const std::string &code,
683  const std::string &module,
684  exprt &expr,
685  const namespacet &ns)
686 {
687  #if 0
688  expr.make_nil();
689 
690  // no preprocessing yet...
691 
692  std::istringstream i_preprocessed(code);
693 
694  // parsing
695 
696  java_bytecode_parser.clear();
697  java_bytecode_parser.filename="";
698  java_bytecode_parser.in=&i_preprocessed;
699  java_bytecode_parser.set_message_handler(message_handler);
700  java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
701  java_bytecode_parser.mode=java_bytecode_parsert::GCC;
702  java_bytecode_scanner_init();
703 
704  bool result=java_bytecode_parser.parse();
705 
706  if(java_bytecode_parser.parse_tree.items.empty())
707  result=true;
708  else
709  {
710  expr=java_bytecode_parser.parse_tree.items.front().value();
711 
712  result=java_bytecode_convert(expr, "", message_handler);
713 
714  // typecheck it
715  if(!result)
716  result=java_bytecode_typecheck(expr, message_handler, ns);
717  }
718 
719  // save some memory
720  java_bytecode_parser.clear();
721 
722  return result;
723  #endif
724 
725  return true; // fail for now
726 }
727 
729 {
730 }
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...
const irep_idt & get_statement() const
Definition: std_code.h:37
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:438
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
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.
bool is_object() const
Definition: json.h:47
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
java_class_loadert java_class_loader
irep_idt mode
Language mode.
Definition: symbol.h:55
mstreamt & status()
Definition: message.h:238
void modules_provided(std::set< std::string > &modules) override
Definition: json.h:21
void load_entire_jar(java_class_loader_limitt &, const std::string &f)
exprt value
Initial value of symbol.
Definition: symbol.h:40
std::string get_value(char option) const
Definition: cmdline.cpp:46
static void gather_field_types(const typet &class_type, const namespacet &ns, ci_lazy_methodst &lazy_methods)
See output.
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void show_parse(std::ostream &out) override
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool java_bytecode_convert_class(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, lazy_methodst &lazy_methods, lazy_methods_modet lazy_methods_mode, bool string_refinement_enabled, const character_refine_preprocesst &character_preprocess)
configt config
Definition: config.cpp:21
bool java_entry_point(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length)
find entry point and create initialization code for function symbol_table main class message_handler ...
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Definition: json_parser.cpp:16
virtual void lazy_methods_provided(std::set< irep_idt > &) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
Class Hierarchy.
static irep_idt get_virtual_method_target(const std::set< irep_idt > &needed_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.
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
Definition: irep.h:189
classpatht classpath
Definition: config.h:142
std::set< std::string > extensions() const override
virtual bool isset(char option) const
Definition: cmdline.cpp:30
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
static std::string file_to_class_name(const std::string &)
symbolst symbols
Definition: symbol_table.h:57
character_refine_preprocesst character_preprocess
bool java_bytecode_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
JAVA Bytecode Language Conversion.
virtual void get_language_options(const cmdlinet &) override
Consume options that are java bytecode specific.
void add_jar_file(const std::string &f)
bool typecheck(symbol_tablet &context, const std::string &module) override
static void gather_virtual_callsites(const exprt &e, std::vector< const code_function_callt *> &result)
See output.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
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 set_java_cp_include_files(std::string &)
class_mapt class_map
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
struct configt::javat java
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
std::map< irep_idt, lazy_method_valuet > lazy_methodst
Symbol table.
main_function_resultt get_main_symbol(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool allow_no_body)
languaget * new_java_bytecode_language()
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &) override
Promote a lazy-converted method (one whose type is known but whose body hasn&#39;t been converted) into a...
typet type
Type of symbol.
Definition: symbol.h:37
mstreamt & debug()
Definition: message.h:253
message_handlert & get_message_handler()
Definition: message.h:127
bool is_string() const
Definition: json.h:37
std::map< std::string, std::string > manifestt
Definition: jar_file.h:44
bool is_array() const
Definition: json.h:52
std::string value
Definition: json.h:131
bool final(symbol_tablet &context) override
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
bool parse(std::istream &instream, const std::string &path) override
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
static void initialize_needed_classes(const std::vector< irep_idt > &entry_points, const namespacet &ns, const class_hierarchyt &ch, ci_lazy_methodst &lazy_methods)
See output.
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
lazy_methods_modet lazy_methods_mode
irep_idt main_class
Definition: config.h:143
dstringt irep_idt
Definition: irep.h:32
void swap(symbol_tablet &other)
Definition: symbol_table.h:80
void java_internal_additions(symbol_tablet &dest)
A statement in a programming language.
Definition: std_code.h:19
JAVA Bytecode Language Conversion.
arrayt array
Definition: json.h:126
idst get_children_trans(const irep_idt &id) const
static void gather_needed_globals(const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed)
See output.
message_handlert * message_handler
Definition: message.h:259
bool empty() const
Definition: dstring.h:61
idst get_parents_trans(const irep_idt &id) const
bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &)
Uses a simple context-insensitive (&#39;ci&#39;) analysis to determine which methods may be reachable from th...
std::vector< irep_idt > main_jar_classes
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:431
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
static void get_virtual_method_targets(const code_function_callt &c, const std::set< irep_idt > &needed_classes, std::vector< irep_idt > &needed_methods, symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy)
Find possible callees, excluding types that are not known to be instantiated.