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/prefix.h>
16 #include <util/suffix.h>
17 
18 #include <fstream>
19 
20 void java_class_loader_baset::add_classpath_entry(const std::string &path)
21 {
22  if(has_suffix(path, ".jar"))
23  {
24  if(std::ifstream(path).good())
25  {
26  classpath_entries.push_back(
27  classpath_entryt(classpath_entryt::JAR, path));
28  }
29  else
30  {
31  warning() << "Warning: failed to access JAR file `" << path << "'" << eom;
32  }
33  }
34  else
35  {
36  if(is_directory(path))
37  {
38  classpath_entries.push_back(
39  classpath_entryt(classpath_entryt::DIRECTORY, path));
40  }
41  else
42  {
43  warning() << "Warning: failed to access directory `" << path << "'"
44  << eom;
45  }
46  }
47 }
48 
55 std::string java_class_loader_baset::file_to_class_name(const std::string &file)
56 {
57  std::string result = file;
58 
59  // Strip .class. Note that the Java class loader would
60  // not do that.
61  if(has_suffix(result, ".class"))
62  result.resize(result.size() - 6);
63 
64  // Strip a "./" prefix. Note that the Java class loader
65  // would not do that.
66 #ifdef _WIN32
67  while(has_prefix(result, ".\\"))
68  result = std::string(result, 2, std::string::npos);
69 #else
70  while(has_prefix(result, "./"))
71  result = std::string(result, 2, std::string::npos);
72 #endif
73 
74  // slash to dot
75  for(std::string::iterator it = result.begin(); it != result.end(); it++)
76  if(*it == '/')
77  *it = '.';
78 
79  return result;
80 }
81 
86 std::string
88 {
89  std::string result = id2string(class_name);
90 
91  // dots (package name separators) to slash
92  for(std::string::iterator it = result.begin(); it != result.end(); it++)
93  if(*it == '.')
94  *it = '/';
95 
96  // add .class suffix
97  result += ".class";
98 
99  return result;
100 }
101 
105 std::string
107 {
108  std::string result = id2string(class_name);
109 
110  // dots (package name separators) to slash, depending on OS
111  for(std::string::iterator it = result.begin(); it != result.end(); it++)
112  if(*it == '.')
113  {
114 #ifdef _WIN32
115  *it = '\\';
116 #else
117  *it = '/';
118 #endif
119  }
120 
121  // add .class suffix
122  result += ".class";
123 
124  return result;
125 }
126 
129  const irep_idt &class_name,
130  const classpath_entryt &cp_entry)
131 {
132  switch(cp_entry.kind)
133  {
134  case classpath_entryt::JAR:
135  return get_class_from_jar(class_name, cp_entry.path);
136 
137  case classpath_entryt::DIRECTORY:
138  return get_class_from_directory(class_name, cp_entry.path);
139  }
140 
141  UNREACHABLE;
142 }
143 
150  const irep_idt &class_name,
151  const std::string &jar_file)
152 {
153  try
154  {
155  auto &jar = jar_pool(jar_file);
156  auto data = jar.get_entry(class_name_to_jar_file(class_name));
157 
158  if(!data.has_value())
159  return {};
160 
161  debug() << "Getting class '" << class_name << "' from JAR " << jar_file
162  << eom;
163 
164  std::istringstream istream(*data);
165  return java_bytecode_parse(istream, class_name, get_message_handler());
166  }
167  catch(const std::runtime_error &)
168  {
169  error() << "failed to open JAR file '" << jar_file << "'" << eom;
170  return {};
171  }
172 }
173 
180  const irep_idt &class_name,
181  const std::string &path)
182 {
183  // Look in the given directory
184  const std::string class_file = class_name_to_os_file(class_name);
185  const std::string full_path = concat_dir_file(path, class_file);
186 
187  if(std::ifstream(full_path))
188  {
189  debug() << "Getting class '" << class_name << "' from file " << full_path
190  << eom;
191  return java_bytecode_parse(full_path, class_name, get_message_handler());
192  }
193  else
194  return {};
195 }
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
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
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_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:55
file_util.h
java_bytecode_parse
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.
Definition: java_bytecode_parser.cpp:1806
data
Definition: kdev_t.h:24
prefix.h
file
Definition: kdev_t.h:19
jar_file.h
messaget::eom
static eomt eom
Definition: message.h:297
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:87
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
java_class_loader_baset::classpath_entryt
An entry in the classpath.
Definition: java_class_loader_base.h:43
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::error
mstreamt & error() const
Definition: message.h:399
java_class_loader_baset::get_class_from_jar
optionalt< java_bytecode_parse_treet > get_class_from_jar(const irep_idt &class_name, const std::string &jar_file)
attempt to load a class from a given jar file
Definition: java_class_loader_base.cpp:149
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
concat_dir_file
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:159
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
java_class_loader_baset::add_classpath_entry
void add_classpath_entry(const std::string &)
Appends an entry to the class path, used for loading classes.
Definition: java_class_loader_base.cpp:20
is_directory
bool is_directory(const std::string &path)
Definition: file_util.cpp:187
java_class_loader_baset::load_class
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &)
attempt to load a class from a classpath_entry
Definition: java_class_loader_base.cpp:128
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_class_loader_baset::classpath_entryt::path
std::string path
Definition: java_class_loader_base.h:46
java_class_loader_baset::class_name_to_os_file
static std::string class_name_to_os_file(const irep_idt &)
Convert a class name to a file name, with OS-dependent syntax.
Definition: java_class_loader_base.cpp:106
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
java_class_loader_baset::classpath_entryt::kind
kindt kind
Definition: java_class_loader_base.h:45
suffix.h
java_class_loader_baset::get_class_from_directory
optionalt< java_bytecode_parse_treet > get_class_from_directory(const irep_idt &class_name, const std::string &path)
attempt to load a class from a given directory
Definition: java_class_loader_base.cpp:179
java_class_loader_base.h
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
messaget::debug
mstreamt & debug() const
Definition: message.h:429
messaget::warning
mstreamt & warning() const
Definition: message.h:404
java_bytecode_parser.h