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 
15 #include "ci_lazy_methods_needed.h"
17 #include "java_class_loader.h"
18 #include "select_pointer_type.h"
19 #include "synthetic_methods_map.h"
20 
21 #include <map>
22 #include <functional>
23 
24 #include <util/irep.h>
25 #include <util/symbol_table.h>
26 #include <util/message.h>
27 
29 
31 
32 // Map from method id to class_method_and_bytecodet
34 {
35 public:
38  {
42  };
43 
46 
47 private:
48  typedef std::map<irep_idt, class_method_and_bytecodet> mapt;
50 
51 public:
52  bool contains_method(const irep_idt &method_id) const
53  {
54  return map.count(method_id) != 0;
55  }
56 
57  void add(const class_method_and_bytecodet &method_class_and_bytecode)
58  {
59  map.emplace(
60  std::make_pair(
61  method_class_and_bytecode.method_id, method_class_and_bytecode));
62  }
63 
64  void add(
65  const irep_idt &class_id,
66  const irep_idt &method_id,
68  {
69  add(class_method_and_bytecodet{class_id, method_id, method});
70  }
71 
72  mapt::const_iterator begin() const
73  {
74  return map.begin();
75  }
76  mapt::const_iterator end() const
77  {
78  return map.end();
79  }
80 
81  opt_reft get(const irep_idt &method_id)
82  {
83  const auto it = map.find(method_id);
84  if(it == map.end())
85  return opt_reft();
86  return std::cref(it->second);
87  }
88 };
89 
90 typedef std::function<
91  bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
93 
94 typedef std::function<std::vector<irep_idt>(const symbol_tablet &)>
96 
98 {
99 public:
101  const symbol_tablet &symbol_table,
102  const irep_idt &main_class,
103  const std::vector<irep_idt> &main_jar_classes,
104  const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
106  const std::vector<irep_idt> &extra_instantiated_classes,
110 
111  // not const since messaget
112  bool operator()(
113  symbol_tablet &symbol_table,
114  method_bytecodet &method_bytecode,
115  const method_convertert &method_converter);
116 
117 private:
119  const std::unordered_set<irep_idt> &entry_points,
120  const namespacet &ns,
121  ci_lazy_methods_neededt &needed_lazy_methods);
122 
124  const exprt &e,
125  std::unordered_set<class_method_descriptor_exprt, irep_hash> &result);
126 
128  const class_method_descriptor_exprt &called_function,
129  const std::unordered_set<irep_idt> &instantiated_classes,
130  std::unordered_set<irep_idt> &callable_methods,
131  symbol_tablet &symbol_table);
132 
134  const exprt &e,
135  const symbol_tablet &symbol_table,
136  symbol_tablet &needed);
137 
139  const std::unordered_set<irep_idt> &instantiated_classes,
140  const irep_idt &call_basename,
141  const irep_idt &classname,
142  const symbol_tablet &symbol_table);
143 
145  const irep_idt &class_name,
146  const irep_idt &component_method_name);
147 
150  std::vector<irep_idt> main_jar_classes;
151  const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points;
153  const std::vector<irep_idt> &extra_instantiated_classes;
156 
157  std::unordered_set<irep_idt>
158  entry_point_methods(const symbol_tablet &symbol_table);
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 
178  std::unordered_set<irep_idt> &methods_to_convert_later,
179  std::unordered_set<irep_idt> &instantiated_classes,
180  const std::unordered_set<class_method_descriptor_exprt, irep_hash>
181  &virtual_functions,
182  symbol_tablet &symbol_table);
183 };
184 
185 #endif // CPROVER_JAVA_BYTECODE_GATHER_METHODS_LAZILY_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
method_bytecodet
Definition: ci_lazy_methods.h:34
method_bytecodet::class_method_and_bytecodet::method_id
irep_idt method_id
Definition: ci_lazy_methods.h:40
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
method_bytecodet::class_method_and_bytecodet
Pair of class id and methodt.
Definition: ci_lazy_methods.h:38
method_bytecodet::class_method_and_bytecodet::method
const java_bytecode_parse_treet::methodt & method
Definition: ci_lazy_methods.h:41
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
ci_lazy_methodst::convert_method_resultt
Definition: ci_lazy_methods.h:161
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
method_bytecodet::class_method_and_bytecodet::class_id
irep_idt class_id
Definition: ci_lazy_methods.h:39
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
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
method_bytecodet::add
void add(const irep_idt &class_id, const irep_idt &method_id, const java_bytecode_parse_treet::methodt &method)
Definition: ci_lazy_methods.h:64
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:86
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
method_bytecodet::map
mapt map
Definition: ci_lazy_methods.h:49
method_bytecodet::opt_reft
optionalt< std::reference_wrapper< const class_method_and_bytecodet > > opt_reft
Definition: ci_lazy_methods.h:45
method_bytecodet::get
opt_reft get(const irep_idt &method_id)
Definition: ci_lazy_methods.h:81
exprt
Base class for all expressions.
Definition: expr.h:53
ci_lazy_methodst::build_virtual_method_name
static irep_idt build_virtual_method_name(const irep_idt &class_name, const irep_idt &component_method_name)
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
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
method_bytecodet::add
void add(const class_method_and_bytecodet &method_class_and_bytecode)
Definition: ci_lazy_methods.h:57
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
ci_lazy_methodst::class_hierarchy
class_hierarchyt class_hierarchy
Definition: ci_lazy_methods.h:148
ci_lazy_methodst::convert_method_resultt::class_initializer_seen
bool class_initializer_seen
Definition: ci_lazy_methods.h:162
messaget::result
mstreamt & result() const
Definition: message.h:409
method_bytecodet::end
mapt::const_iterator end() const
Definition: ci_lazy_methods.h:76
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
java_bytecode_parse_tree.h
ci_lazy_methods_needed.h
Context-insensitive lazy methods container.
java_class_loader.h
load_extra_methodst
std::function< std::vector< irep_idt >const symbol_tablet &)> load_extra_methodst
Definition: ci_lazy_methods.h:95
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
message_handlert
Definition: message.h:28
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
method_bytecodet::mapt
std::map< irep_idt, class_method_and_bytecodet > mapt
Definition: ci_lazy_methods.h:48
ci_lazy_methodst::java_class_loader
java_class_loadert & java_class_loader
Definition: ci_lazy_methods.h:152
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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
java_class_loadert
Class responsible to load .class files.
Definition: java_class_loader.h:27
class_hierarchy.h
Class Hierarchy.
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
method_bytecodet::contains_method
bool contains_method(const irep_idt &method_id) const
Definition: ci_lazy_methods.h:52
ci_lazy_methodst
Definition: ci_lazy_methods.h:98
ci_lazy_methodst::synthetic_methods
const synthetic_methods_mapt & synthetic_methods
Definition: ci_lazy_methods.h:155
java_string_library_preprocesst
Definition: java_string_library_preprocess.h:36
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
ci_lazy_methods_neededt
Definition: ci_lazy_methods_needed.h:25
method_bytecodet::begin
mapt::const_iterator begin() const
Definition: ci_lazy_methods.h:72
symbol_table.h
Author: Diffblue Ltd.
message.h
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
ci_lazy_methodst::convert_method_resultt::new_method_seen
bool new_method_seen
Definition: ci_lazy_methods.h:163
synthetic_methods_map.h
Synthetic methods are particular methods internally generated by the Java frontend,...
irep.h
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