cprover
java_class_loader_base.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include "jar_file.h"
12 #include "java_bytecode_parser.h"
13 
14 #include <util/file_util.h>
15 #include <util/message.h>
16 #include <util/prefix.h>
17 #include <util/suffix.h>
18 
19 #include <fstream>
20 
22  const std::string &path,
23  message_handlert &message_handler)
24 {
25  messaget log(message_handler);
26 
27  if(has_suffix(path, ".jar"))
28  {
29  if(std::ifstream(path).good())
30  {
31  classpath_entries.push_back(
32  classpath_entryt(classpath_entryt::JAR, path));
33  }
34  else
35  {
36  log.warning() << "Warning: failed to access JAR file `" << path << "'"
37  << messaget::eom;
38  }
39  }
40  else
41  {
42  if(is_directory(path))
43  {
44  classpath_entries.push_back(
45  classpath_entryt(classpath_entryt::DIRECTORY, path));
46  }
47  else
48  {
49  log.warning() << "Warning: failed to access directory `" << path << "'"
50  << messaget::eom;
51  }
52  }
53 }
54 
61 std::string java_class_loader_baset::file_to_class_name(const std::string &file)
62 {
63  std::string result = file;
64 
65  // Strip .class. Note that the Java class loader would
66  // not do that.
67  if(has_suffix(result, ".class"))
68  result.resize(result.size() - 6);
69 
70  // Strip a "./" prefix. Note that the Java class loader
71  // would not do that.
72 #ifdef _WIN32
73  while(has_prefix(result, ".\\"))
74  result = std::string(result, 2, std::string::npos);
75 #else
76  while(has_prefix(result, "./"))
77  result = std::string(result, 2, std::string::npos);
78 #endif
79 
80  // slash to dot
81  for(std::string::iterator it = result.begin(); it != result.end(); it++)
82  if(*it == '/')
83  *it = '.';
84 
85  return result;
86 }
87 
92 std::string
94 {
95  std::string result = id2string(class_name);
96 
97  // dots (package name separators) to slash
98  for(std::string::iterator it = result.begin(); it != result.end(); it++)
99  if(*it == '.')
100  *it = '/';
101 
102  // add .class suffix
103  result += ".class";
104 
105  return result;
106 }
107 
111 std::string
113 {
114  std::string result = id2string(class_name);
115 
116  // dots (package name separators) to slash, depending on OS
117  for(std::string::iterator it = result.begin(); it != result.end(); it++)
118  if(*it == '.')
119  {
120 #ifdef _WIN32
121  *it = '\\';
122 #else
123  *it = '/';
124 #endif
125  }
126 
127  // add .class suffix
128  result += ".class";
129 
130  return result;
131 }
132 
135  const irep_idt &class_name,
136  const classpath_entryt &cp_entry,
137  message_handlert &message_handler)
138 {
139  switch(cp_entry.kind)
140  {
141  case classpath_entryt::JAR:
142  return get_class_from_jar(class_name, cp_entry.path, message_handler);
143 
144  case classpath_entryt::DIRECTORY:
145  return get_class_from_directory(class_name, cp_entry.path, message_handler);
146  }
147 
148  UNREACHABLE;
149 }
150 
158  const irep_idt &class_name,
159  const std::string &jar_file,
160  message_handlert &message_handler)
161 {
162  messaget log(message_handler);
163 
164  try
165  {
166  auto &jar = jar_pool(jar_file);
167  auto data = jar.get_entry(class_name_to_jar_file(class_name));
168 
169  if(!data.has_value())
170  return {};
171 
172  log.debug() << "Getting class '" << class_name << "' from JAR " << jar_file
173  << messaget::eom;
174 
175  std::istringstream istream(*data);
176  return java_bytecode_parse(istream, class_name, message_handler);
177  }
178  catch(const std::runtime_error &)
179  {
180  log.error() << "failed to open JAR file '" << jar_file << "'"
181  << messaget::eom;
182  return {};
183  }
184 }
185 
193  const irep_idt &class_name,
194  const std::string &path,
195  message_handlert &message_handler)
196 {
197  // Look in the given directory
198  const std::string class_file = class_name_to_os_file(class_name);
199  const std::string full_path = concat_dir_file(path, class_file);
200 
201  if(std::ifstream(full_path))
202  {
203  messaget log(message_handler);
204  log.debug() << "Getting class '" << class_name << "' from file "
205  << full_path << messaget::eom;
206  return java_bytecode_parse(full_path, class_name, message_handler);
207  }
208  else
209  return {};
210 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
void add_classpath_entry(const std::string &, message_handlert &)
Appends an entry to the class path, used for loading classes.
optionalt< java_bytecode_parse_treet > get_class_from_jar(const irep_idt &class_name, const std::string &jar_file, message_handlert &)
attempt to load a class from a given jar file
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
jar_poolt jar_pool
a cache for jar_filet, by path name
static std::string class_name_to_os_file(const irep_idt &)
Convert a class name to a file name, with OS-dependent syntax.
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.
std::list< classpath_entryt > classpath_entries
List of entries in the classpath.
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
optionalt< java_bytecode_parse_treet > get_class_from_directory(const irep_idt &class_name, const std::string &path, message_handlert &)
attempt to load a class from a given directory
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
bool is_directory(const std::string &path)
Definition: file_util.cpp:187
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:159
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
optionalt< java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, const irep_idt &class_name, message_handlert &message_handler, bool skip_instructions)
Attempt to parse a Java class from the given stream.
nonstd::optional< T > optionalt
Definition: optional.h:35
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
Definition: kdev_t.h:24
Definition: kdev_t.h:19
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17