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/suffix.h>
16 
17 #include <fstream>
18 
19 void java_class_loader_baset::add_classpath_entry(const std::string &path)
20 {
21  if(has_suffix(path, ".jar"))
22  {
23  classpath_entries.push_back(classpath_entryt(classpath_entryt::JAR, path));
24  }
25  else
26  {
27  classpath_entries.push_back(
28  classpath_entryt(classpath_entryt::DIRECTORY, path));
29  }
30 }
31 
38 std::string java_class_loader_baset::file_to_class_name(const std::string &file)
39 {
40  std::string result = file;
41 
42  // Strip .class. Note that the Java class loader would
43  // not do that.
44  if(has_suffix(result, ".class"))
45  result.resize(result.size() - 6);
46 
47  // Strip a "./" prefix. Note that the Java class loader
48  // would not do that.
49 #ifdef _WIN32
50  while(has_prefix(result, ".\\"))
51  result = std::string(result, 2, std::string::npos);
52 #else
53  while(has_prefix(result, "./"))
54  result = std::string(result, 2, std::string::npos);
55 #endif
56 
57  // slash to dot
58  for(std::string::iterator it = result.begin(); it != result.end(); it++)
59  if(*it == '/')
60  *it = '.';
61 
62  return result;
63 }
64 
69 std::string
71 {
72  std::string result = id2string(class_name);
73 
74  // dots (package name separators) to slash
75  for(std::string::iterator it = result.begin(); it != result.end(); it++)
76  if(*it == '.')
77  *it = '/';
78 
79  // add .class suffix
80  result += ".class";
81 
82  return result;
83 }
84 
88 std::string
90 {
91  std::string result = id2string(class_name);
92 
93  // dots (package name separators) to slash, depending on OS
94  for(std::string::iterator it = result.begin(); it != result.end(); it++)
95  if(*it == '.')
96  {
97 #ifdef _WIN32
98  *it = '\\';
99 #else
100  *it = '/';
101 #endif
102  }
103 
104  // add .class suffix
105  result += ".class";
106 
107  return result;
108 }
109 
112  const irep_idt &class_name,
113  const classpath_entryt &cp_entry)
114 {
115  switch(cp_entry.kind)
116  {
117  case classpath_entryt::JAR:
118  return get_class_from_jar(class_name, cp_entry.path);
119 
120  case classpath_entryt::DIRECTORY:
121  return get_class_from_directory(class_name, cp_entry.path);
122  }
123 
124  UNREACHABLE;
125 }
126 
133  const irep_idt &class_name,
134  const std::string &jar_file)
135 {
136  try
137  {
138  auto &jar = jar_pool(jar_file);
139  auto data = jar.get_entry(class_name_to_jar_file(class_name));
140 
141  if(!data.has_value())
142  return {};
143 
144  debug() << "Getting class `" << class_name << "' from JAR " << jar_file
145  << eom;
146 
147  std::istringstream istream(*data);
148  return java_bytecode_parse(istream, get_message_handler());
149  }
150  catch(const std::runtime_error &)
151  {
152  error() << "failed to open JAR file `" << jar_file << "'" << eom;
153  return {};
154  }
155 }
156 
163  const irep_idt &class_name,
164  const std::string &path)
165 {
166  // Look in the given directory
167  const std::string class_file = class_name_to_os_file(class_name);
168  const std::string full_path = concat_dir_file(path, class_file);
169 
170  if(std::ifstream(full_path))
171  {
172  debug() << "Getting class `" << class_name << "' from file " << full_path
173  << eom;
174  return java_bytecode_parse(full_path, get_message_handler());
175  }
176  else
177  return {};
178 }
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:141
std::list< classpath_entryt > classpath_entries
List of entries in the classpath.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void add_classpath_entry(const std::string &)
Appends an entry to the class path, used for loading classes.
optionalt< java_bytecode_parse_treet > load_class(const irep_idt &class_name, const classpath_entryt &)
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.
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
nonstd::optional< T > optionalt
Definition: optional.h:35
static std::string file_to_class_name(const std::string &)
Convert a file name to the class name.
mstreamt & error() const
Definition: message.h:386
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
jar_poolt jar_pool
a cache for jar_filet, by path name
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
static eomt eom
Definition: message.h:284
optionalt< java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, message_handlert &message_handler, bool skip_instructions)
Attempt to parse a Java class from the given stream.
message_handlert & get_message_handler()
Definition: message.h:174
mstreamt & result() const
Definition: message.h:396
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
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.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
mstreamt & debug() const
Definition: message.h:416
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: kdev_t.h:24
Definition: kdev_t.h:19