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 #include <util/config.h>
17 
18 #include "java_bytecode_parser.h"
19 
21  const irep_idt &class_name)
22 {
23  std::stack<irep_idt> queue;
24  // Always require java.lang.Object, as it is the base of
25  // internal classes such as array types.
26  queue.push("java.lang.Object");
27  // java.lang.String
28  queue.push("java.lang.String");
29  // add java.lang.Class
30  queue.push("java.lang.Class");
31  // Require java.lang.Throwable as the catch-type used for
32  // universal exception handlers:
33  queue.push("java.lang.Throwable");
34  queue.push(class_name);
35 
36  // Require user provided classes to be loaded even without explicit reference
37  for(const auto &id : java_load_classes)
38  queue.push(id);
39 
40  java_class_loader_limitt class_loader_limit(
42 
43  while(!queue.empty())
44  {
45  irep_idt c=queue.top();
46  queue.pop();
47 
48  if(class_map.count(c) != 0)
49  continue;
50 
51  debug() << "Reading class " << c << eom;
52 
53  parse_tree_with_overlayst &parse_trees =
54  get_parse_tree(class_loader_limit, c);
55 
56  // Add any dependencies to queue
57  for(const java_bytecode_parse_treet &parse_tree : parse_trees)
58  for(const irep_idt &class_ref : parse_tree.class_refs)
59  queue.push(class_ref);
60 
61  // Add any extra dependencies provided by our caller:
63  {
64  for(const irep_idt &id : get_extra_class_refs(c))
65  queue.push(id);
66  }
67  }
68 
69  return class_map.at(class_name);
70 }
71 
73  const irep_idt &class_name,
74  const std::string &jar_file,
75  const jar_indext &jar_index,
76  java_class_loader_limitt &class_loader_limit)
77 {
78  auto jar_index_it = jar_index.find(class_name);
79  if(jar_index_it == jar_index.end())
80  return {};
81 
82  debug()
83  << "Getting class `" << class_name << "' from JAR " << jar_file << eom;
84 
85  auto data =
86  jar_pool(class_loader_limit, jar_file).get_entry(jar_index_it->second);
87 
88  if(!data.has_value())
89  return {};
90 
91  std::istringstream istream(*data);
92  return java_bytecode_parse(istream, get_message_handler());
93 }
94 
96 {
98  c.annotations, ID_overlay_class)
99  .has_value();
100 }
101 
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  // First add all given JAR files
120  for(const auto &jar_file : jar_files)
121  {
122  jar_index_optcreft index = read_jar_file(class_loader_limit, jar_file);
123  if(!index)
124  continue;
126  get_class_from_jar(class_name, jar_file, *index, class_loader_limit);
127  if(parse_tree)
128  parse_trees.emplace_back(std::move(*parse_tree));
129  }
130 
131  // Then add everything on the class path
132  for(const auto &cp_entry : config.java.classpath)
133  {
134  if(has_suffix(cp_entry, ".jar"))
135  {
136  jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry);
137  if(!index)
138  continue;
140  get_class_from_jar(class_name, cp_entry, *index, class_loader_limit);
141  if(parse_tree)
142  parse_trees.emplace_back(std::move(*parse_tree));
143  }
144  else
145  {
146  // Look in the given directory
147  const std::string class_file = class_name_to_file(class_name);
148  const std::string full_path =
149  #ifdef _WIN32
150  cp_entry + '\\' + class_file;
151  #else
152  cp_entry + '/' + class_file;
153  #endif
154 
155  if(!class_loader_limit.load_class_file(class_file))
156  continue;
157 
158  if(std::ifstream(full_path))
159  {
160  debug()
161  << "Getting class `" << class_name << "' from file " << full_path
162  << eom;
165  if(parse_tree)
166  parse_trees.emplace_back(std::move(*parse_tree));
167  }
168  }
169  }
170 
171  if(!parse_trees.empty())
172  {
173  auto parse_tree_it = parse_trees.begin();
174  // If the first class implementation is an overlay emit a warning and
175  // skip over it until we find a non-overlay class
176  while(parse_tree_it != parse_trees.end())
177  {
178  // Skip parse trees that failed to load - though these shouldn't exist yet
179  if(parse_tree_it->loading_successful)
180  {
181  if(!is_overlay_class(parse_tree_it->parsed_class))
182  {
183  // Keep the non-overlay class
184  ++parse_tree_it;
185  break;
186  }
187  warning()
188  << "Skipping class " << class_name
189  << " marked with OverlayClassImplementation but found before"
190  " original definition"
191  << eom;
192  }
193  auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
194  ++parse_tree_it;
195  parse_trees.erase(unloaded_or_overlay_out_of_order_it);
196  }
197  // Collect overlay classes
198  while(parse_tree_it != parse_trees.end())
199  {
200  // Remove non-initial classes that aren't overlays
201  if(!is_overlay_class(parse_tree_it->parsed_class))
202  {
203  warning()
204  << "Skipping duplicate definition of class " << class_name
205  << " not marked with OverlayClassImplementation" << eom;
206  auto duplicate_non_overlay_it = parse_tree_it;
207  ++parse_tree_it;
208  parse_trees.erase(duplicate_non_overlay_it);
209  }
210  else
211  ++parse_tree_it;
212  }
213  return parse_trees;
214  }
215 
216  // Not found or failed to load
217  warning() << "failed to load class `" << class_name << '\'' << eom;
218  java_bytecode_parse_treet parse_tree;
219  parse_tree.parsed_class.name=class_name;
220  parse_trees.push_back(std::move(parse_tree));
221  return parse_trees;
222 }
223 
225  java_class_loader_limitt &class_loader_limit,
226  const std::string &jar_path)
227 {
228  jar_index_optcreft jar_index = read_jar_file(class_loader_limit, jar_path);
229  if(!jar_index)
230  return;
231 
232  jar_files.push_front(jar_path);
233 
234  for(const auto &e : jar_index->get())
235  operator()(e.first);
236 
237  jar_files.pop_front();
238 }
239 
241  java_class_loader_limitt &class_loader_limit,
242  const std::string &jar_path)
243 {
244  auto existing_it = jars_by_path.find(jar_path);
245  if(existing_it != jars_by_path.end())
246  return std::cref(existing_it->second);
247 
248  std::vector<std::string> filenames;
249  try
250  {
251  filenames = this->jar_pool(class_loader_limit, jar_path).filenames();
252  }
253  catch(const std::runtime_error &)
254  {
255  error() << "failed to open JAR file `" << jar_path << "'" << eom;
256  return jar_index_optcreft();
257  }
258  debug() << "Adding JAR file `" << jar_path << "'" << eom;
259 
260  // Create a new entry in the map and initialize using the list of file names
261  // that were retained in the jar_filet by the class_loader_limit filter
262  jar_indext &jar_index = jars_by_path[jar_path];
263  for(auto &file_name : filenames)
264  {
265  if(has_suffix(file_name, ".class"))
266  {
267  debug()
268  << "Found class file " << file_name << " in JAR `" << jar_path << "'"
269  << eom;
270  irep_idt class_name=file_to_class_name(file_name);
271  jar_index[class_name] = file_name;
272  }
273  }
274  return std::cref(jar_index);
275 }
276 
277 std::string java_class_loadert::file_to_class_name(const std::string &file)
278 {
279  std::string result=file;
280 
281  // Strip .class. Note that the Java class loader would
282  // not do that.
283  if(has_suffix(result, ".class"))
284  result.resize(result.size()-6);
285 
286  // Strip a "./" prefix. Note that the Java class loader
287  // would not do that.
288  #ifdef _WIN32
289  while(has_prefix(result, ".\\"))
290  result=std::string(result, 2, std::string::npos);
291  #else
292  while(has_prefix(result, "./"))
293  result=std::string(result, 2, std::string::npos);
294  #endif
295 
296  // slash to dot
297  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
298  if(*it=='/')
299  *it='.';
300 
301  return result;
302 }
303 
304 std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
305 {
306  std::string result=id2string(class_name);
307 
308  // dots (package name separators) to slash, depending on OS
309  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
310  if(*it=='.')
311  {
312  #ifdef _WIN32
313  *it='\\';
314  #else
315  *it='/';
316  #endif
317  }
318 
319  // add .class suffix
320  result+=".class";
321 
322  return result;
323 }
324 
326  java_class_loader_limitt &class_loader_limit,
327  const std::string &file_name)
328 {
329  const auto it=m_archives.find(file_name);
330  if(it==m_archives.end())
331  {
332  // VS: Can't construct in place
333  auto file=jar_filet(class_loader_limit, file_name);
334  return m_archives.emplace(file_name, std::move(file)).first->second;
335  }
336  else
337  return it->second;
338 }
339 
341  java_class_loader_limitt &class_loader_limit,
342  const std::string &buffer_name,
343  const void *pmem,
344  size_t size)
345 {
346  const auto it=m_archives.find(buffer_name);
347  if(it==m_archives.end())
348  {
349  // VS: Can't construct in place
350  auto file=jar_filet(class_loader_limit, pmem, size);
351  return m_archives.emplace(buffer_name, std::move(file)).first->second;
352  }
353  else
354  return it->second;
355 }
std::map< std::string, jar_indext > jars_by_path
The jar_indext for each jar file we&#39;ve read.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
jar_index_optcreft read_jar_file(java_class_loader_limitt &class_loader_limit, const std::string &jar_path)
std::list< std::string > jar_files
List of filesystem paths to .jar files that will be used, in the given order, to find and load a clas...
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
std::vector< std::string > filenames() const
Get list of filenames in the archive.
Definition: jar_file.cpp:123
optionalt< std::string > get_entry(const std::string &filename)
Get contents of a file in the jar archive.
Definition: jar_file.cpp:65
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name)
Given a class_name (e.g.
jar_filet & jar_pool(java_class_loader_limitt &limit, const std::string &filename)
Load jar archive or retrieve from cache if already loaded.
std::map< irep_idt, std::string > jar_indext
A map associating logical class names with the name of the .class file implementing it for all classe...
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
void load_entire_jar(java_class_loader_limitt &, const std::string &jar_path)
mstreamt & warning() const
Definition: message.h:307
classpatht classpath
Definition: config.h:147
static std::string file_to_class_name(const std::string &)
nonstd::optional< T > optionalt
Definition: optional.h:35
mstreamt & error() const
Definition: message.h:302
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
struct configt::javat java
optionalt< class java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
Class representing a .jar archive.
Definition: jar_file.h:24
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & result() const
Definition: message.h:312
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
optionalt< std::reference_wrapper< const jar_indext > > jar_index_optcreft
std::map< std::string, jar_filet > m_archives
Jar files that have been loaded.
get_extra_class_refs_functiont get_extra_class_refs
bool load_class_file(const std::string &class_file_name)
parse_tree_with_overlayst & operator()(const irep_idt &class_name)
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
mstreamt & debug() const
Definition: message.h:332
optionalt< java_bytecode_parse_treet > get_class_from_jar(const irep_idt &class_name, const std::string &jar_file, const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit)
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: kdev_t.h:24
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
static std::string class_name_to_file(const irep_idt &)
Definition: kdev_t.h:19