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