cprover
ci_lazy_methods.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Bytecode
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
13 #define CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
14 
16 #include "synthetic_methods_map.h"
17 
18 #include <functional>
19 #include <map>
20 #include <unordered_set>
21 
22 #include <util/irep.h>
23 
25 
27 class java_class_loadert;
28 class message_handlert;
30 
31 // Map from method id to class_method_and_bytecodet
33 {
34 public:
37  {
41  };
42 
45 
46 private:
47  typedef std::map<irep_idt, class_method_and_bytecodet> mapt;
49 
50 public:
51  bool contains_method(const irep_idt &method_id) const
52  {
53  return map.count(method_id) != 0;
54  }
55 
56  void add(const class_method_and_bytecodet &method_class_and_bytecode)
57  {
58  map.emplace(
59  std::make_pair(
60  method_class_and_bytecode.method_id, method_class_and_bytecode));
61  }
62 
63  void add(
64  const irep_idt &class_id,
65  const irep_idt &method_id,
67  {
68  add(class_method_and_bytecodet{class_id, method_id, method});
69  }
70 
71  mapt::const_iterator begin() const
72  {
73  return map.begin();
74  }
75  mapt::const_iterator end() const
76  {
77  return map.end();
78  }
79 
80  opt_reft get(const irep_idt &method_id)
81  {
82  const auto it = map.find(method_id);
83  if(it == map.end())
84  return opt_reft();
85  return std::cref(it->second);
86  }
87 };
88 
89 typedef std::function<
90  bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
92 
93 typedef std::function<std::vector<irep_idt>(const symbol_tablet &)>
95 
97 {
98 public:
100  const symbol_tablet &symbol_table,
101  const irep_idt &main_class,
102  const std::vector<irep_idt> &main_jar_classes,
103  const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
105  const std::vector<irep_idt> &extra_instantiated_classes,
108 
109  // not const since messaget
110  bool operator()(
111  symbol_tablet &symbol_table,
112  method_bytecodet &method_bytecode,
113  const method_convertert &method_converter,
114  message_handlert &message_handler);
115 
116 private:
118  const std::unordered_set<irep_idt> &entry_points,
119  const namespacet &ns,
120  ci_lazy_methods_neededt &needed_lazy_methods);
121 
123  const exprt &e,
124  std::unordered_set<class_method_descriptor_exprt, irep_hash> &result);
125 
127  const class_method_descriptor_exprt &called_function,
128  const std::unordered_set<irep_idt> &instantiated_classes,
129  std::unordered_set<irep_idt> &callable_methods,
130  symbol_tablet &symbol_table);
131 
133  const exprt &e,
134  const symbol_tablet &symbol_table,
135  symbol_tablet &needed);
136 
138  const std::unordered_set<irep_idt> &instantiated_classes,
139  const irep_idt &call_basename,
140  const irep_idt &classname,
141  const symbol_tablet &symbol_table);
142 
144  const irep_idt &class_name,
145  const irep_idt &component_method_name);
146 
149  std::vector<irep_idt> main_jar_classes;
150  const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points;
152  const std::vector<irep_idt> &extra_instantiated_classes;
155 
156  std::unordered_set<irep_idt> entry_point_methods(
157  const symbol_tablet &symbol_table,
158  message_handlert &message_handler);
159 
161  {
163  bool new_method_seen = false;
164  };
165 
167  const method_convertert &method_converter,
168  std::unordered_set<irep_idt> &methods_already_populated,
169  const bool class_initializer_already_seen,
170  const irep_idt &method_name,
171  symbol_tablet &symbol_table,
172  std::unordered_set<irep_idt> &methods_to_convert_later,
173  std::unordered_set<irep_idt> &instantiated_classes,
174  std::unordered_set<class_method_descriptor_exprt, irep_hash>
175  &called_virtual_functions,
176  message_handlert &message_handler);
177 
179  std::unordered_set<irep_idt> &methods_to_convert_later,
180  std::unordered_set<irep_idt> &instantiated_classes,
181  const std::unordered_set<class_method_descriptor_exprt, irep_hash>
182  &virtual_functions,
183  symbol_tablet &symbol_table);
184 };
185 
186 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
std::function< std::vector< irep_idt >const symbol_tablet &)> load_extra_methodst
Class Hierarchy.
const std::vector< irep_idt > & extra_instantiated_classes
static irep_idt build_virtual_method_name(const irep_idt &class_name, const irep_idt &component_method_name)
void gather_needed_globals(const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed)
See output.
std::vector< irep_idt > main_jar_classes
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, const synthetic_methods_mapt &synthetic_methods)
Constructor for lazy-method loading.
const select_pointer_typet & pointer_type_selector
const std::vector< load_extra_methodst > & lazy_methods_extra_entry_points
class_hierarchyt class_hierarchy
void gather_virtual_callsites(const exprt &e, std::unordered_set< class_method_descriptor_exprt, irep_hash > &result)
Get places where virtual functions are called.
java_class_loadert & java_class_loader
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.
const synthetic_methods_mapt & synthetic_methods
std::unordered_set< irep_idt > entry_point_methods(const symbol_tablet &symbol_table, message_handlert &message_handler)
Entry point methods are either:
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, message_handlert &message_handler)
Convert a method, add it to the populated set, add needed methods to methods_to_convert_later and add...
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.
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.
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.
bool operator()(symbol_tablet &symbol_table, method_bytecodet &method_bytecode, const method_convertert &method_converter, message_handlert &message_handler)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
Non-graph-based representation of the class hierarchy.
An expression describing a method on a class.
Definition: std_expr.h:3272
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Class responsible to load .class files.
mapt::const_iterator begin() const
opt_reft get(const irep_idt &method_id)
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
std::map< irep_idt, class_method_and_bytecodet > mapt
void add(const class_method_and_bytecodet &method_class_and_bytecode)
bool contains_method(const irep_idt &method_id) const
void add(const irep_idt &class_id, const irep_idt &method_id, const java_bytecode_parse_treet::methodt &method)
mapt::const_iterator end() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The symbol table.
Definition: symbol_table.h:14
nonstd::optional< T > optionalt
Definition: optional.h:35
const java_bytecode_parse_treet::methodt & method
Synthetic methods are particular methods internally generated by the Java frontend,...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.