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  std::stack<irep_idt> queue;
23  // Always require java.lang.Object, as it is the base of
24  // internal classes such as array types.
25  queue.push("java.lang.Object");
26  // java.lang.String
27  queue.push("java.lang.String");
28  // add java.lang.Class
29  queue.push("java.lang.Class");
30  // Require java.lang.Throwable as the catch-type used for
31  // universal exception handlers:
32  queue.push("java.lang.Throwable");
33  queue.push(class_name);
34 
35  // Require user provided classes to be loaded even without explicit reference
36  for(const auto &id : java_load_classes)
37  queue.push(id);
38 
39  java_class_loader_limitt class_loader_limit(
41 
42  while(!queue.empty())
43  {
44  irep_idt c=queue.top();
45  queue.pop();
46 
47  if(class_map.count(c) != 0)
48  continue;
49 
50  debug() << "Reading class " << c << eom;
51 
52  parse_tree_with_overlayst &parse_trees =
53  get_parse_tree(class_loader_limit, c);
54 
55  // Add any dependencies to queue
56  for(const java_bytecode_parse_treet &parse_tree : parse_trees)
57  for(const irep_idt &class_ref : parse_tree.class_refs)
58  queue.push(class_ref);
59 
60  // Add any extra dependencies provided by our caller:
62  {
63  for(const irep_idt &id : get_extra_class_refs(c))
64  queue.push(id);
65  }
66  }
67 
68  return class_map.at(class_name);
69 }
70 
93 {
95  c.annotations, ID_overlay_class)
96  .has_value();
97 }
98 
113  java_class_loader_limitt &class_loader_limit,
114  const irep_idt &class_name)
115 {
116  parse_tree_with_overlayst &parse_trees = class_map[class_name];
117  PRECONDITION(parse_trees.empty());
118 
119  // do we refuse to load?
120  if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
121  {
122  debug() << "not loading " << class_name << " because of limit" << eom;
123  parse_trees.emplace_back(class_name);
124  return parse_trees;
125  }
126 
127  // Rummage through the class path
128  for(const auto &cp_entry : classpath_entries)
129  {
130  auto parse_tree = load_class(class_name, cp_entry);
131  if(parse_tree.has_value())
132  parse_trees.emplace_back(std::move(*parse_tree));
133  }
134 
135  auto parse_tree_it = parse_trees.begin();
136  // If the first class implementation is an overlay emit a warning and
137  // skip over it until we find a non-overlay class
138  while(parse_tree_it != parse_trees.end())
139  {
140  // Skip parse trees that failed to load - though these shouldn't exist yet
141  if(parse_tree_it->loading_successful)
142  {
143  if(!is_overlay_class(parse_tree_it->parsed_class))
144  {
145  // Keep the non-overlay class
146  ++parse_tree_it;
147  break;
148  }
149  warning()
150  << "Skipping class " << class_name
151  << " marked with OverlayClassImplementation but found before"
152  " original definition"
153  << eom;
154  }
155  auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
156  ++parse_tree_it;
157  parse_trees.erase(unloaded_or_overlay_out_of_order_it);
158  }
159  // Collect overlay classes
160  while(parse_tree_it != parse_trees.end())
161  {
162  // Remove non-initial classes that aren't overlays
163  if(!is_overlay_class(parse_tree_it->parsed_class))
164  {
165  warning()
166  << "Skipping duplicate definition of class " << class_name
167  << " not marked with OverlayClassImplementation" << eom;
168  auto duplicate_non_overlay_it = parse_tree_it;
169  ++parse_tree_it;
170  parse_trees.erase(duplicate_non_overlay_it);
171  }
172  else
173  ++parse_tree_it;
174  }
175  if(!parse_trees.empty())
176  return parse_trees;
177 
178  // Not found or failed to load
179  warning() << "failed to load class `" << class_name << '\'' << eom;
180  parse_trees.emplace_back(class_name);
181  return parse_trees;
182 }
183 
187  const std::string &jar_path)
188 {
189  auto classes = read_jar_file(jar_path);
190  if(!classes.has_value())
191  return {};
192 
193  classpath_entries.push_front(
194  classpath_entryt(classpath_entryt::JAR, jar_path));
195 
196  for(const auto &c : *classes)
197  operator()(c);
198 
199  classpath_entries.pop_front();
200 
201  return *classes;
202 }
203 
205 java_class_loadert::read_jar_file(const std::string &jar_path)
206 {
207  std::vector<std::string> filenames;
208  try
209  {
210  filenames = jar_pool(jar_path).filenames();
211  }
212  catch(const std::runtime_error &)
213  {
214  error() << "failed to open JAR file `" << jar_path << "'" << eom;
215  return {};
216  }
217  debug() << "Adding JAR file `" << jar_path << "'" << eom;
218 
219  // Create a new entry in the map and initialize using the list of file names
220  // that are in jar_filet
221  std::vector<irep_idt> classes;
222  for(auto &file_name : filenames)
223  {
224  if(has_suffix(file_name, ".class"))
225  {
226  debug()
227  << "Found class file " << file_name << " in JAR `" << jar_path << "'"
228  << eom;
229  irep_idt class_name=file_to_class_name(file_name);
230  classes.push_back(class_name);
231  }
232  }
233  return classes;
234 }
std::list< classpath_entryt > classpath_entries
List of entries in the classpath.
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &)
attempt to load a class from a classpath_entry
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
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...
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
mstreamt & warning() const
Definition: message.h:391
optionalt< std::vector< irep_idt > > read_jar_file(const std::string &jar_path)
nonstd::optional< T > optionalt
Definition: optional.h:35
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
mstreamt & error() const
Definition: message.h:386
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
jar_poolt jar_pool
a cache for jar_filet, by path name
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Class representing a filter for class file loading.
static eomt eom
Definition: message.h:284
message_handlert & get_message_handler()
Definition: message.h:174
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.
get_extra_class_refs_functiont get_extra_class_refs
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.
parse_tree_with_overlayst & operator()(const irep_idt &class_name)
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.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
mstreamt & debug() const
Definition: message.h:416
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 > load_entire_jar(const std::string &jar_path)
Load all class files from a .jar file.
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.