CBMC
Loading...
Searching...
No Matches
java_class_loader_base.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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"
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 "
40 }
41 }
42 else
43 {
44 if(std::filesystem::is_directory(path))
45 {
46 classpath_entries.push_back(
47 classpath_entryt(classpath_entryt::DIRECTORY, path));
48 }
49 else
50 {
51 log.warning() << "Warning: failed to access directory "
54 }
55 }
56}
57
64std::string java_class_loader_baset::file_to_class_name(const std::string &file)
65{
66 std::string result = file;
67
68 // Strip .class. Note that the Java class loader would
69 // not do that.
70 if(has_suffix(result, ".class"))
71 result.resize(result.size() - 6);
72
73 // Strip a "./" prefix. Note that the Java class loader
74 // would not do that.
75#ifdef _WIN32
76 while(has_prefix(result, ".\\"))
77 result = std::string(result, 2, std::string::npos);
78#else
79 while(has_prefix(result, "./"))
80 result = std::string(result, 2, std::string::npos);
81#endif
82
83 // slash to dot
84 for(std::string::iterator it = result.begin(); it != result.end(); it++)
85 if(*it == '/')
86 *it = '.';
87
88 return result;
89}
90
95std::string
97{
98 std::string result = id2string(class_name);
99
100 // dots (package name separators) to slash
101 for(std::string::iterator it = result.begin(); it != result.end(); it++)
102 if(*it == '.')
103 *it = '/';
104
105 // add .class suffix
106 result += ".class";
107
108 return result;
109}
110
114std::string
116{
117 std::string result = id2string(class_name);
118
119 // dots (package name separators) to slash, depending on OS
120 for(std::string::iterator it = result.begin(); it != result.end(); it++)
121 if(*it == '.')
122 {
123#ifdef _WIN32
124 *it = '\\';
125#else
126 *it = '/';
127#endif
128 }
129
130 // add .class suffix
131 result += ".class";
132
133 return result;
134}
135
137std::optional<java_bytecode_parse_treet> java_class_loader_baset::load_class(
138 const irep_idt &class_name,
140 message_handlert &message_handler)
141{
142 switch(cp_entry.kind)
143 {
144 case classpath_entryt::JAR:
145 return get_class_from_jar(class_name, cp_entry.path, message_handler);
146
147 case classpath_entryt::DIRECTORY:
148 return get_class_from_directory(class_name, cp_entry.path, message_handler);
149 }
150
152}
153
159std::optional<java_bytecode_parse_treet>
161 const irep_idt &class_name,
162 const std::string &jar_file,
163 message_handlert &message_handler)
164{
165 messaget log(message_handler);
166
167 try
168 {
169 auto &jar = jar_pool(jar_file);
170 auto data = jar.get_entry(class_name_to_jar_file(class_name));
171
172 if(!data.has_value())
173 return {};
174
175 log.debug() << "Getting class '" << class_name << "' from JAR " << jar_file
176 << messaget::eom;
177
178 std::istringstream istream(*data);
179 return java_bytecode_parse(istream, class_name, message_handler);
180 }
181 catch(const std::runtime_error &)
182 {
183 log.error() << "failed to open JAR file '" << jar_file << "'"
184 << messaget::eom;
185 return {};
186 }
187}
188
194std::optional<java_bytecode_parse_treet>
196 const irep_idt &class_name,
197 const std::string &path,
198 message_handlert &message_handler)
199{
200 // Look in the given directory
201 const std::string class_file = class_name_to_os_file(class_name);
202 const std::string full_path =
203 std::filesystem::path(path).append(class_file).string();
204
205 if(std::ifstream(full_path))
206 {
207 messaget log(message_handler);
208 log.debug() << "Getting class '" << class_name << "' from file "
209 << full_path << messaget::eom;
210 return java_bytecode_parse(full_path, class_name, message_handler);
211 }
212 else
213 return {};
214}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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 const commandt quote_begin
Start quoted text.
Definition message.h:389
static const commandt quote_end
End quoted text.
Definition message.h:393
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:2416
#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