cprover
ci_lazy_methods_needed.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Context-insensitive lazy methods container
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
13 #define CPROVER_JAVA_BYTECODE_CI_LAZY_METHODS_H
14 
15 #include <set>
16 #include <unordered_set>
17 #include <util/namespace.h>
18 #include <util/symbol_table.h>
19 #include <vector>
20 
22 class pointer_typet;
23 
25 {
26 public:
28  std::unordered_set<irep_idt> &_callable_methods,
29  std::unordered_set<irep_idt> &_instantiated_classes,
30  const symbol_tablet &_symbol_table,
32  : callable_methods(_callable_methods),
33  instantiated_classes(_instantiated_classes),
34  symbol_table(_symbol_table),
36  {}
37 
38  void add_needed_method(const irep_idt &);
39  // Returns true if new
40  bool add_needed_class(const irep_idt &);
41 
43 
44 private:
45  // callable_methods is a vector because it's used as a work-list
46  // which is periodically cleared. It can't be relied upon to
47  // contain all methods that have previously been elaborated.
48  // It should be changed to a set if we develop the need to use
49  // it that way.
50  std::unordered_set<irep_idt> &callable_methods;
51  // instantiated_classes on the other hand is a true set of every class
52  // found so far, so we can use a membership test to avoid
53  // repeatedly exploring a class hierarchy.
54  std::unordered_set<irep_idt> &instantiated_classes;
56 
58 
59  void add_clinit_call(const irep_idt &class_id);
61 
64  const namespacet &ns);
65 
66  void gather_field_types(const typet &class_type, const namespacet &ns);
67 };
68 
69 #endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ci_lazy_methods_neededt::instantiated_classes
std::unordered_set< irep_idt > & instantiated_classes
Definition: ci_lazy_methods_needed.h:54
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
ci_lazy_methods_neededt::pointer_type_selector
const select_pointer_typet & pointer_type_selector
Definition: ci_lazy_methods_needed.h:57
ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer
void initialize_instantiated_classes_from_pointer(const pointer_typet &pointer_type, const namespacet &ns)
Build up list of methods for types for a specific pointer type.
Definition: ci_lazy_methods_needed.cpp:115
typet
The type of an expression, extends irept.
Definition: type.h:29
ci_lazy_methods_neededt::ci_lazy_methods_neededt
ci_lazy_methods_neededt(std::unordered_set< irep_idt > &_callable_methods, std::unordered_set< irep_idt > &_instantiated_classes, const symbol_tablet &_symbol_table, const select_pointer_typet &pointer_type_selector)
Definition: ci_lazy_methods_needed.h:27
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
namespace.h
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_methods_neededt::symbol_table
const symbol_tablet & symbol_table
Definition: ci_lazy_methods_needed.h:55
select_pointer_typet
Definition: select_pointer_type.h:26
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists
void add_cprover_nondet_initialize_if_it_exists(const irep_idt &class_id)
For a given class id, if cproverNondetInitialize exists on it or any of its ancestors then note that ...
Definition: ci_lazy_methods_needed.cpp:51
ci_lazy_methods_neededt::add_clinit_call
void add_clinit_call(const irep_idt &class_id)
For a given class id, note that its static initializer is needed.
Definition: ci_lazy_methods_needed.cpp:41
ci_lazy_methods_neededt::gather_field_types
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
Definition: ci_lazy_methods_needed.cpp:146
ci_lazy_methods_neededt::add_needed_method
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
Definition: ci_lazy_methods_needed.cpp:27
ci_lazy_methods_neededt
Definition: ci_lazy_methods_needed.h:25
symbol_table.h
Author: Diffblue Ltd.
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
ci_lazy_methods_neededt::callable_methods
std::unordered_set< irep_idt > & callable_methods
Definition: ci_lazy_methods_needed.h:50