CBMC
java_class_loader.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H
12 
13 #include <map>
14 
16 
18 #include "java_class_loader_base.h"
19 
21 class message_handlert;
22 
26 {
27 public:
29  typedef std::list<java_bytecode_parse_treet> parse_tree_with_overlayst;
32  typedef std::map<irep_idt, parse_tree_with_overlayst>
34 
36  typedef std::function<std::vector<irep_idt>(const irep_idt &)>
38 
40  {
41  }
42 
44  operator()(const irep_idt &class_name, message_handlert &);
45 
48  bool can_load_class(const irep_idt &class_name, message_handlert &);
49 
51  java_class_loader_limitt &class_loader_limit,
52  const irep_idt &class_name,
54 
57  void set_java_cp_include_files(const std::string &cp_include_files)
58  {
59  java_cp_include_files = cp_include_files;
60  }
66  {
67  get_extra_class_refs = func;
68  }
72  void add_load_classes(const std::vector<irep_idt> &classes)
73  {
74  for(const auto &id : classes)
75  java_load_classes.push_back(id);
76  }
77 
78  std::vector<irep_idt>
79  load_entire_jar(const std::string &jar_path, message_handlert &);
80 
84  {
86  }
88  const irep_idt &class_name)
89  {
90  return class_map.at(class_name).front();
91  }
92 
93 private:
99  std::string java_cp_include_files;
100 
102  std::vector<irep_idt> java_load_classes;
104 
107 
108  std::optional<std::vector<irep_idt>>
109  read_jar_file(const std::string &jar_path, message_handlert &);
110 };
111 
112 #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for maintaining classpath.
Class representing a filter for class file loading.
Class responsible to load .class files.
std::string java_cp_include_files
Either a regular expression matching files that will be allowed to be loaded or a string of the form ...
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
std::map< irep_idt, parse_tree_with_overlayst > parse_tree_with_overridest_mapt
A map from class names to list of parse tree where multiple entries can exist in case of overlay clas...
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
void set_extra_class_refs_function(get_extra_class_refs_functiont func)
Sets a function that provides extra dependencies for a particular class.
parse_tree_with_overlayst & operator()(const irep_idt &class_name, message_handlert &)
void set_java_cp_include_files(const std::string &cp_include_files)
Set the argument of the class loader limit java_class_loader_limitt.
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name, message_handlert &)
Check through all the places class parse trees can appear and returns the first implementation it fin...
fixed_keys_map_wrappert< parse_tree_with_overridest_mapt > get_class_with_overlays_map()
Map from class names to the bytecode parse trees.
const java_bytecode_parse_treet & get_original_class(const irep_idt &class_name)
get_extra_class_refs_functiont get_extra_class_refs
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
std::function< std::vector< irep_idt >const irep_idt &)> get_extra_class_refs_functiont
A function that yields a list of extra dependencies based on a class name.
void add_load_classes(const std::vector< irep_idt > &classes)
Adds the list of classes to the load queue, forcing them to be loaded even without explicit reference...
std::optional< std::vector< irep_idt > > read_jar_file(const std::string &jar_path, message_handlert &)
A wrapper for maps that gives read-write access to elements but without allowing addition or removal ...