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 operator()(const irep_idt &class_name, message_handlert &message_handler)
21 {
22  messaget log(message_handler);
23 
24  log.debug() << "Classpath:";
25  for(const auto &entry : classpath_entries)
26  {
27  log.debug() << "\n " << entry.path;
28  }
29  log.debug() << messaget::eom;
30 
31  std::stack<irep_idt> queue;
32  // Always require java.lang.Object, as it is the base of
33  // internal classes such as array types.
34  queue.push("java.lang.Object");
35  // java.lang.String
36  queue.push("java.lang.String");
37  // add java.lang.Class
38  queue.push("java.lang.Class");
39  // Require java.lang.Throwable as the catch-type used for
40  // universal exception handlers:
41  queue.push("java.lang.Throwable");
42  queue.push(class_name);
43 
44  // Require user provided classes to be loaded even without explicit reference
45  for(const auto &id : java_load_classes)
46  queue.push(id);
47 
48  java_class_loader_limitt class_loader_limit(
49  message_handler, java_cp_include_files);
50 
51  while(!queue.empty())
52  {
53  irep_idt c=queue.top();
54  queue.pop();
55 
56  if(class_map.count(c) != 0)
57  continue;
58 
59  log.debug() << "Reading class " << c << messaget::eom;
60 
61  parse_tree_with_overlayst &parse_trees =
62  get_parse_tree(class_loader_limit, c, message_handler);
63 
64  // Add any dependencies to queue
65  for(const java_bytecode_parse_treet &parse_tree : parse_trees)
66  for(const irep_idt &class_ref : parse_tree.class_refs)
67  queue.push(class_ref);
68 
69  // Add any extra dependencies provided by our caller:
71  {
72  for(const irep_idt &id : get_extra_class_refs(c))
73  queue.push(id);
74  }
75  }
76 
77  return class_map.at(class_name);
78 }
79 
102 {
104  c.annotations, ID_overlay_class)
105  .has_value();
106 }
107 
109  const irep_idt &class_name,
110  message_handlert &message_handler)
111 {
112  for(const auto &cp_entry : classpath_entries)
113  {
114  auto parse_tree = load_class(class_name, cp_entry, message_handler);
115  if(parse_tree.has_value())
116  return true;
117  }
118  return false;
119 }
120 
136  java_class_loader_limitt &class_loader_limit,
137  const irep_idt &class_name,
138  message_handlert &message_handler)
139 {
140  parse_tree_with_overlayst &parse_trees = class_map[class_name];
141  PRECONDITION(parse_trees.empty());
142 
143  messaget log(message_handler);
144 
145  // do we refuse to load?
146  if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
147  {
148  log.debug() << "not loading " << class_name << " because of limit"
149  << messaget::eom;
150  parse_trees.emplace_back(class_name);
151  return parse_trees;
152  }
153 
154  // Rummage through the class path
155  for(const auto &cp_entry : classpath_entries)
156  {
157  auto parse_tree = load_class(class_name, cp_entry, message_handler);
158  if(parse_tree.has_value())
159  parse_trees.emplace_back(std::move(*parse_tree));
160  }
161 
162  auto parse_tree_it = parse_trees.begin();
163  // If the first class implementation is an overlay emit a warning and
164  // skip over it until we find a non-overlay class
165  while(parse_tree_it != parse_trees.end())
166  {
167  // Skip parse trees that failed to load - though these shouldn't exist yet
168  if(parse_tree_it->loading_successful)
169  {
170  if(!is_overlay_class(parse_tree_it->parsed_class))
171  {
172  // Keep the non-overlay class
173  ++parse_tree_it;
174  break;
175  }
176  log.debug() << "Skipping class " << class_name
177  << " marked with OverlayClassImplementation but found before"
178  " original definition"
179  << messaget::eom;
180  }
181  auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
182  ++parse_tree_it;
183  parse_trees.erase(unloaded_or_overlay_out_of_order_it);
184  }
185  // Collect overlay classes
186  while(parse_tree_it != parse_trees.end())
187  {
188  // Remove non-initial classes that aren't overlays
189  if(!is_overlay_class(parse_tree_it->parsed_class))
190  {
191  log.debug() << "Skipping duplicate definition of class " << class_name
192  << " not marked with OverlayClassImplementation"
193  << messaget::eom;
194  auto duplicate_non_overlay_it = parse_tree_it;
195  ++parse_tree_it;
196  parse_trees.erase(duplicate_non_overlay_it);
197  }
198  else
199  ++parse_tree_it;
200  }
201  if(!parse_trees.empty())
202  return parse_trees;
203 
204  // Not found or failed to load
205  log.debug() << "failed to load class " << class_name << messaget::eom;
206  parse_trees.emplace_back(class_name);
207  return parse_trees;
208 }
209 
213  const std::string &jar_path,
214  message_handlert &message_handler)
215 {
216  auto classes = read_jar_file(jar_path, message_handler);
217  if(!classes.has_value())
218  return {};
219 
220  classpath_entries.push_front(
221  classpath_entryt(classpath_entryt::JAR, jar_path));
222 
223  for(const auto &c : *classes)
224  operator()(c, message_handler);
225 
226  classpath_entries.pop_front();
227 
228  return *classes;
229 }
230 
232  const std::string &jar_path,
233  message_handlert &message_handler)
234 {
235  messaget log(message_handler);
236 
237  std::vector<std::string> filenames;
238  try
239  {
240  filenames = jar_pool(jar_path).filenames();
241  }
242  catch(const std::runtime_error &)
243  {
244  log.error() << "failed to open JAR file '" << jar_path << "'"
245  << messaget::eom;
246  return {};
247  }
248  log.debug() << "Adding JAR file '" << jar_path << "'" << messaget::eom;
249 
250  // Create a new entry in the map and initialize using the list of file names
251  // that are in jar_filet
252  std::vector<irep_idt> classes;
253  for(auto &file_name : filenames)
254  {
255  if(has_suffix(file_name, ".class"))
256  {
257  log.debug() << "Found class file " << file_name << " in JAR '" << jar_path
258  << "'" << messaget::eom;
259  irep_idt class_name=file_to_class_name(file_name);
260  classes.push_back(class_name);
261  }
262  }
263  return classes;
264 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
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:100
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:61
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::read_jar_file
optionalt< std::vector< irep_idt > > read_jar_file(const std::string &jar_path, message_handlert &)
Definition: java_class_loader.cpp:231
java_class_loadert::get_extra_class_refs
get_extra_class_refs_functiont get_extra_class_refs
Definition: java_class_loader.h:104
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::get_parse_tree
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...
Definition: java_class_loader.cpp:135
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:93
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:103
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
java_class_loader_baset::load_class
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &, message_handlert &)
attempt to load a class from a classpath_entry
Definition: java_class_loader_base.cpp:134
java_class_loadert::can_load_class
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
Definition: java_class_loader.cpp:108
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:101
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::operator()
parse_tree_with_overlayst & operator()(const irep_idt &class_name, message_handlert &)
Definition: java_class_loader.cpp:20
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
message_handlert
Definition: message.h:28
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_class_loadert::load_entire_jar
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
Definition: java_class_loader.cpp:212
java_class_loader_limitt
Class representing a filter for class file loading.
Definition: java_class_loader_limit.h:22
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:107
suffix.h
java_bytecode_parse_treet::classt
Definition: java_bytecode_parse_tree.h:198
messaget::debug
mstreamt & debug() const
Definition: message.h:429
java_bytecode_parser.h