cprover
Loading...
Searching...
No Matches
ci_lazy_methods.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java Bytecode
4
5Author: 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
17
18#include <functional>
19#include <map>
20#include <unordered_set>
21
22#include <util/irep.h>
23
25
31
32// Map from method id to class_method_and_bytecodet
34{
35public:
43
46
47private:
48 typedef std::map<irep_idt, class_method_and_bytecodet> mapt;
50
51public:
52 bool contains_method(const irep_idt &method_id) const
53 {
54 return map.count(method_id) != 0;
55 }
56
58 {
59 map.emplace(
60 std::make_pair(
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
90typedef std::function<
91 bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
93
94typedef std::function<std::vector<irep_idt>(const symbol_table_baset &)>
96
98{
99public:
101 const symbol_table_baset &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,
109
110 // not const since messaget
111 bool operator()(
112 symbol_table_baset &symbol_table,
113 method_bytecodet &method_bytecode,
115 message_handlert &message_handler);
116
117private:
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_table_baset &symbol_table);
132
134 const exprt &e,
135 const symbol_table_baset &symbol_table,
137
139 const std::unordered_set<irep_idt> &instantiated_classes,
140 const irep_idt &call_basename,
141 const irep_idt &classname,
142 const symbol_table_baset &symbol_table);
143
145 const irep_idt &class_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> entry_point_methods(
158 const symbol_table_baset &symbol_table,
159 message_handlert &message_handler);
160
162 {
164 bool new_method_seen = false;
165 };
166
169 std::unordered_set<irep_idt> &methods_already_populated,
171 const irep_idt &method_name,
172 symbol_table_baset &symbol_table,
173 std::unordered_set<irep_idt> &methods_to_convert_later,
174 std::unordered_set<irep_idt> &instantiated_classes,
175 std::unordered_set<class_method_descriptor_exprt, irep_hash>
177 message_handlert &message_handler);
178
180 std::unordered_set<irep_idt> &methods_to_convert_later,
181 std::unordered_set<irep_idt> &instantiated_classes,
182 const std::unordered_set<class_method_descriptor_exprt, irep_hash>
184 symbol_table_baset &symbol_table);
185};
186
187#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_table_baset &)> load_extra_methodst
Class Hierarchy.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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_table_baset &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...
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)
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_table_baset &symbol_table)
Find a virtual callee, if one is defined and the callee type is known to exist.
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_table_baset &symbol_table)
Find possible callees, excluding types that are not known to be instantiated.
std::vector< irep_idt > main_jar_classes
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
bool operator()(symbol_table_baset &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...
const synthetic_methods_mapt & synthetic_methods
void gather_needed_globals(const exprt &e, const symbol_table_baset &symbol_table, symbol_table_baset &needed)
See output.
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_table_baset &symbol_table)
Look for virtual callsites with no candidate targets.
std::unordered_set< irep_idt > entry_point_methods(const symbol_table_baset &symbol_table, message_handlert &message_handler)
Entry point methods are either:
Non-graph-based representation of the class hierarchy.
An expression describing a method on a class.
Definition std_expr.h:3448
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
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 base class interface.
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.