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  // do we refuse to load?
120  if(!class_loader_limit.load_class_file(class_name_to_file(class_name)))
121  {
122  debug() << "not loading " << class_name << " because of limit" << eom;
123  java_bytecode_parse_treet parse_tree;
124  parse_tree.parsed_class.name = class_name;
125  parse_trees.push_back(std::move(parse_tree));
126  return parse_trees;
127  }
128 
129  // First add all given JAR files
130  for(const auto &jar_file : jar_files)
131  {
132  jar_index_optcreft index = read_jar_file(class_loader_limit, jar_file);
133  if(!index)
134  continue;
136  get_class_from_jar(class_name, jar_file, *index, class_loader_limit);
137  if(parse_tree)
138  parse_trees.emplace_back(std::move(*parse_tree));
139  }
140 
141  // Then add everything on the class path
142  for(const auto &cp_entry : config.java.classpath)
143  {
144  if(has_suffix(cp_entry, ".jar"))
145  {
146  jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry);
147  if(!index)
148  continue;
150  get_class_from_jar(class_name, cp_entry, *index, class_loader_limit);
151  if(parse_tree)
152  parse_trees.emplace_back(std::move(*parse_tree));
153  }
154  else
155  {
156  // Look in the given directory
157  const std::string class_file = class_name_to_file(class_name);
158  const std::string full_path =
159  #ifdef _WIN32
160  cp_entry + '\\' + class_file;
161  #else
162  cp_entry + '/' + class_file;
163  #endif
164 
165  if(!class_loader_limit.load_class_file(class_file))
166  continue;
167 
168  if(std::ifstream(full_path))
169  {
170  debug()
171  << "Getting class `" << class_name << "' from file " << full_path
172  << eom;
175  if(parse_tree)
176  parse_trees.emplace_back(std::move(*parse_tree));
177  }
178  }
179  }
180 
181  auto parse_tree_it = parse_trees.begin();
182  // If the first class implementation is an overlay emit a warning and
183  // skip over it until we find a non-overlay class
184  while(parse_tree_it != parse_trees.end())
185  {
186  // Skip parse trees that failed to load - though these shouldn't exist yet
187  if(parse_tree_it->loading_successful)
188  {
189  if(!is_overlay_class(parse_tree_it->parsed_class))
190  {
191  // Keep the non-overlay class
192  ++parse_tree_it;
193  break;
194  }
195  warning()
196  << "Skipping class " << class_name
197  << " marked with OverlayClassImplementation but found before"
198  " original definition"
199  << eom;
200  }
201  auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
202  ++parse_tree_it;
203  parse_trees.erase(unloaded_or_overlay_out_of_order_it);
204  }
205  // Collect overlay classes
206  while(parse_tree_it != parse_trees.end())
207  {
208  // Remove non-initial classes that aren't overlays
209  if(!is_overlay_class(parse_tree_it->parsed_class))
210  {
211  warning()
212  << "Skipping duplicate definition of class " << class_name
213  << " not marked with OverlayClassImplementation" << eom;
214  auto duplicate_non_overlay_it = parse_tree_it;
215  ++parse_tree_it;
216  parse_trees.erase(duplicate_non_overlay_it);
217  }
218  else
219  ++parse_tree_it;
220  }
221  if(!parse_trees.empty())
222  return parse_trees;
223 
224  // Not found or failed to load
225  warning() << "failed to load class `" << class_name << '\'' << eom;
226  java_bytecode_parse_treet parse_tree;
227  parse_tree.parsed_class.name=class_name;
228  parse_trees.push_back(std::move(parse_tree));
229  return parse_trees;
230 }
231 
233  java_class_loader_limitt &class_loader_limit,
234  const std::string &jar_path)
235 {
236  jar_index_optcreft jar_index = read_jar_file(class_loader_limit, jar_path);
237  if(!jar_index)
238  return;
239 
240  jar_files.push_front(jar_path);
241 
242  for(const auto &e : jar_index->get())
243  operator()(e.first);
244 
245  jar_files.pop_front();
246 }
247 
249  java_class_loader_limitt &class_loader_limit,
250  const std::string &jar_path)
251 {
252  auto existing_it = jars_by_path.find(jar_path);
253  if(existing_it != jars_by_path.end())
254  return std::cref(existing_it->second);
255 
256  std::vector<std::string> filenames;
257  try
258  {
259  filenames = this->jar_pool(class_loader_limit, jar_path).filenames();
260  }
261  catch(const std::runtime_error &)
262  {
263  error() << "failed to open JAR file `" << jar_path << "'" << eom;
264  return jar_index_optcreft();
265  }
266  debug() << "Adding JAR file `" << jar_path << "'" << eom;
267 
268  // Create a new entry in the map and initialize using the list of file names
269  // that were retained in the jar_filet by the class_loader_limit filter
270  jar_indext &jar_index = jars_by_path[jar_path];
271  for(auto &file_name : filenames)
272  {
273  if(has_suffix(file_name, ".class"))
274  {
275  debug()
276  << "Found class file " << file_name << " in JAR `" << jar_path << "'"
277  << eom;
278  irep_idt class_name=file_to_class_name(file_name);
279  jar_index[class_name] = file_name;
280  }
281  }
282  return std::cref(jar_index);
283 }
284 
285 std::string java_class_loadert::file_to_class_name(const std::string &file)
286 {
287  std::string result=file;
288 
289  // Strip .class. Note that the Java class loader would
290  // not do that.
291  if(has_suffix(result, ".class"))
292  result.resize(result.size()-6);
293 
294  // Strip a "./" prefix. Note that the Java class loader
295  // would not do that.
296  #ifdef _WIN32
297  while(has_prefix(result, ".\\"))
298  result=std::string(result, 2, std::string::npos);
299  #else
300  while(has_prefix(result, "./"))
301  result=std::string(result, 2, std::string::npos);
302  #endif
303 
304  // slash to dot
305  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
306  if(*it=='/')
307  *it='.';
308 
309  return result;
310 }
311 
312 std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
313 {
314  std::string result=id2string(class_name);
315 
316  // dots (package name separators) to slash, depending on OS
317  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
318  if(*it=='.')
319  {
320  #ifdef _WIN32
321  *it='\\';
322  #else
323  *it='/';
324  #endif
325  }
326 
327  // add .class suffix
328  result+=".class";
329 
330  return result;
331 }
332 
334  java_class_loader_limitt &class_loader_limit,
335  const std::string &file_name)
336 {
337  const auto it=m_archives.find(file_name);
338  if(it==m_archives.end())
339  {
340  // VS: Can't construct in place
341  auto file = jar_filet(file_name);
342  return m_archives.emplace(file_name, std::move(file)).first->second;
343  }
344  else
345  return it->second;
346 }
347 
349  java_class_loader_limitt &class_loader_limit,
350  const std::string &buffer_name,
351  const void *pmem,
352  size_t size)
353 {
354  const auto it=m_archives.find(buffer_name);
355  if(it==m_archives.end())
356  {
357  // VS: Can't construct in place
358  auto file = jar_filet(pmem, size);
359  return m_archives.emplace(buffer_name, std::move(file)).first->second;
360  }
361  else
362  return it->second;
363 }
std::map< std::string, jar_indext > jars_by_path
The jar_indext for each jar file we&#39;ve read.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:122
optionalt< std::string > get_entry(const std::string &filename)
Get contents of a file in the jar archive.
Definition: jar_file.cpp:64
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)
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:307
classpatht classpath
Definition: config.h:155
static std::string file_to_class_name(const std::string &)
optionalt< java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
nonstd::optional< T > optionalt
Definition: optional.h:35
mstreamt & error() const
Definition: message.h:302
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Class representing a .jar archive.
Definition: jar_file.h:22
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