cprover
java_class_loader.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_class_loader.h"
10 
11 #include <stack>
12 #include <fstream>
13 
14 #include <util/suffix.h>
15 #include <util/prefix.h>
16 
17 #include "java_bytecode_parser.h"
18 
20  const irep_idt &class_name)
21 {
22  debug() << "Classpath:";
23  for(const auto &entry : classpath_entries)
24  {
25  debug() << "\n " << entry.path;
26  }
27  debug() << messaget::eom;
28 
29  std::stack<irep_idt> queue;
30  // Always require java.lang.Object, as it is the base of
31  // internal classes such as array types.
32  queue.push("java.lang.Object");
33  // java.lang.String
34  queue.push("java.lang.String");
35  // add java.lang.Class
36  queue.push("java.lang.Class");
37  // Require java.lang.Throwable as the catch-type used for
38  // universal exception handlers:
39  queue.push("java.lang.Throwable");
40  queue.push(class_name);
41 
42  // Require user provided classes to be loaded even without explicit reference
43  for(const auto &id : java_load_classes)
44  queue.push(id);
45 
46  java_class_loader_limitt class_loader_limit(
48 
49  while(!queue.empty())
50  {
51  irep_idt c=queue.top();
52  queue.pop();
53 
54  if(class_map.count(c) != 0)
55  continue;
56 
57  debug() << "Reading class " << c << eom;
58 
59  parse_tree_with_overlayst &parse_trees =
60  get_parse_tree(class_loader_limit, c);
61 
62  // Add any dependencies to queue
63  for(const java_bytecode_parse_treet &parse_tree : parse_trees)
64  for(const irep_idt &class_ref : parse_tree.class_refs)
65  queue.push(class_ref);
66 
67  // Add any extra dependencies provided by our caller:
69  {
70  for(const irep_idt &id : get_extra_class_refs(c))
71  queue.push(id);
72  }
73  }
74 
75  return class_map.at(class_name);
76 }
77 
100 {
102  c.annotations, ID_overlay_class)
103  .has_value();
104 }
105 
107 {
108  for(const auto &cp_entry : classpath_entries)
109  {
110  auto parse_tree = load_class(class_name, cp_entry);
111  if(parse_tree.has_value())
112  return true;
113  }
114  return false;
115 }
116 
131  java_class_loader_limitt &class_loader_limit,
132  const irep_idt &class_name)
133 {
134  parse_tree_with_overlayst &parse_trees = class_map[class_name];
135  PRECONDITION(parse_trees.empty());
136 
137  // do we refuse to load?
138  if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
139  {
140  debug() << "not loading " << class_name << " because of limit" << eom;
141  parse_trees.emplace_back(class_name);
142  return parse_trees;
143  }
144 
145  // Rummage through the class path
146  for(const auto &cp_entry : classpath_entries)
147  {
148  auto parse_tree = load_class(class_name, cp_entry);
149  if(parse_tree.has_value())
150  parse_trees.emplace_back(std::move(*parse_tree));
151  }
152 
153  auto parse_tree_it = parse_trees.begin();
154  // If the first class implementation is an overlay emit a warning and
155  // skip over it until we find a non-overlay class
156  while(parse_tree_it != parse_trees.end())
157  {
158  // Skip parse trees that failed to load - though these shouldn't exist yet
159  if(parse_tree_it->loading_successful)
160  {
161  if(!is_overlay_class(parse_tree_it->parsed_class))
162  {
163  // Keep the non-overlay class
164  ++parse_tree_it;
165  break;
166  }
167  debug() << "Skipping class " << class_name
168  << " marked with OverlayClassImplementation but found before"
169  " original definition"
170  << eom;
171  }
172  auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
173  ++parse_tree_it;
174  parse_trees.erase(unloaded_or_overlay_out_of_order_it);
175  }
176  // Collect overlay classes
177  while(parse_tree_it != parse_trees.end())
178  {
179  // Remove non-initial classes that aren't overlays
180  if(!is_overlay_class(parse_tree_it->parsed_class))
181  {
182  debug() << "Skipping duplicate definition of class " << class_name
183  << " not marked with OverlayClassImplementation" << eom;
184  auto duplicate_non_overlay_it = parse_tree_it;
185  ++parse_tree_it;
186  parse_trees.erase(duplicate_non_overlay_it);
187  }
188  else
189  ++parse_tree_it;
190  }
191  if(!parse_trees.empty())
192  return parse_trees;
193 
194  // Not found or failed to load
195  debug() << "failed to load class " << class_name << eom;
196  parse_trees.emplace_back(class_name);
197  return parse_trees;
198 }
199 
203  const std::string &jar_path)
204 {
205  auto classes = read_jar_file(jar_path);
206  if(!classes.has_value())
207  return {};
208 
209  classpath_entries.push_front(
210  classpath_entryt(classpath_entryt::JAR, jar_path));
211 
212  for(const auto &c : *classes)
213  operator()(c);
214 
215  classpath_entries.pop_front();
216 
217  return *classes;
218 }
219 
221 java_class_loadert::read_jar_file(const std::string &jar_path)
222 {
223  std::vector<std::string> filenames;
224  try
225  {
226  filenames = jar_pool(jar_path).filenames();
227  }
228  catch(const std::runtime_error &)
229  {
230  error() << "failed to open JAR file '" << jar_path << "'" << eom;
231  return {};
232  }
233  debug() << "Adding JAR file '" << jar_path << "'" << eom;
234 
235  // Create a new entry in the map and initialize using the list of file names
236  // that are in jar_filet
237  std::vector<irep_idt> classes;
238  for(auto &file_name : filenames)
239  {
240  if(has_suffix(file_name, ".class"))
241  {
242  debug() << "Found class file " << file_name << " in JAR '" << jar_path
243  << "'" << eom;
244  irep_idt class_name=file_to_class_name(file_name);
245  classes.push_back(class_name);
246  }
247  }
248  return classes;
249 }
java_class_loader_baset::jar_pool
jar_poolt jar_pool
a cache for jar_filet, by path name
Definition: java_class_loader_base.h:38
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_class_loadert::java_cp_include_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 ...
Definition: java_class_loader.h:97
java_class_loader_baset::file_to_class_name
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
Definition: java_class_loader_base.cpp:55
java_class_loader_limitt::load_class_file
bool load_class_file(const std::string &class_file_name)
Use the class load limiter to decide whether a class file should be loaded or not.
Definition: java_class_loader_limit.cpp:89
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:24
java_class_loadert::get_extra_class_refs
get_extra_class_refs_functiont get_extra_class_refs
Definition: java_class_loader.h:101
java_class_loadert::load_entire_jar
std::vector< irep_idt > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
Definition: java_class_loader.cpp:202
prefix.h
java_bytecode_parse_treet::find_annotation
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
Definition: java_bytecode_parse_tree.cpp:97
messaget::eom
static eomt eom
Definition: message.h:297
java_class_loadert::read_jar_file
optionalt< std::vector< irep_idt > > read_jar_file(const std::string &jar_path)
Definition: java_class_loader.cpp:221
java_class_loader_baset::class_name_to_jar_file
static std::string class_name_to_jar_file(const irep_idt &)
Convert a class name to a file name, does the inverse of file_to_class_name.
Definition: java_class_loader_base.cpp:87
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
java_class_loadert::java_load_classes
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
Definition: java_class_loader.h:100
java_class_loader_baset::classpath_entryt
An entry in the classpath.
Definition: java_class_loader_base.h:43
java_bytecode_parse_treet::classt::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:282
is_overlay_class
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
Check if class is an overlay class by searching for ID_overlay_class in its list of annotations.
Definition: java_class_loader.cpp:99
messaget::error
mstreamt & error() const
Definition: message.h:399
java_class_loadert::parse_tree_with_overlayst
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
Definition: java_class_loader.h:30
java_class_loadert::get_parse_tree
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name)
Check through all the places class parse trees can appear and returns the first implementation it fin...
Definition: java_class_loader.cpp:130
java_class_loader_baset::classpath_entries
std::list< classpath_entryt > classpath_entries
List of entries in the classpath.
Definition: java_class_loader_base.h:55
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
java_class_loader.h
java_class_loader_baset::load_class
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &)
attempt to load a class from a classpath_entry
Definition: java_class_loader_base.cpp:128
java_class_loadert::can_load_class
bool can_load_class(const irep_idt &class_name)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
Definition: java_class_loader.cpp:106
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_class_loader_limitt
Class representing a filter for class file loading.
Definition: java_class_loader_limit.h:23
java_class_loadert::class_map
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
Definition: java_class_loader.h:104
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
suffix.h
java_bytecode_parse_treet::classt
Definition: java_bytecode_parse_tree.h:198
java_class_loadert::operator()
parse_tree_with_overlayst & operator()(const irep_idt &class_name)
Definition: java_class_loader.cpp:19
messaget::debug
mstreamt & debug() const
Definition: message.h:429
java_bytecode_parser.h