cprover
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 #include <regex>
15 #include <set>
16 
18 
19 #include "jar_file.h"
21 #include "java_class_loader_base.h"
23 
27 {
28 public:
30  typedef std::list<java_bytecode_parse_treet> parse_tree_with_overlayst;
33  typedef std::map<irep_idt, parse_tree_with_overlayst>
35 
37  typedef std::function<std::vector<irep_idt>(const irep_idt &)>
39 
41  {
42  }
43 
45  operator()(const irep_idt &class_name, message_handlert &);
46 
49  bool can_load_class(const irep_idt &class_name, message_handlert &);
50 
52  java_class_loader_limitt &class_loader_limit,
53  const irep_idt &class_name,
55 
58  void set_java_cp_include_files(const std::string &cp_include_files)
59  {
60  java_cp_include_files = cp_include_files;
61  }
67  {
68  get_extra_class_refs = func;
69  }
73  void add_load_classes(const std::vector<irep_idt> &classes)
74  {
75  for(const auto &id : classes)
76  java_load_classes.push_back(id);
77  }
78 
79  std::vector<irep_idt>
80  load_entire_jar(const std::string &jar_path, message_handlert &);
81 
85  {
87  }
89  const irep_idt &class_name)
90  {
91  return class_map.at(class_name).front();
92  }
93 
94 private:
101 
103  std::vector<irep_idt> java_load_classes;
105 
108 
110  read_jar_file(const std::string &jar_path, message_handlert &);
111 };
112 
113 #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:37
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.
optionalt< std::vector< irep_idt > > read_jar_file(const std::string &jar_path, message_handlert &)
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...
A wrapper for maps that gives read-write access to elements but without allowing addition or removal ...
limit class path loading
nonstd::optional< T > optionalt
Definition: optional.h:35