CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 `" << path << "'"
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 << "'"
52 }
53 }
54}
55
62std::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
93std::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
112std::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
135std::optional<java_bytecode_parse_treet> java_class_loader_baset::load_class(
136 const irep_idt &class_name,
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
150}
151
157std::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
192std::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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:2449
#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