cprover
java_class_loader.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_class_loader.h"
10 
11 #include <stack>
12 #include <map>
13 #include <fstream>
14 
15 #include <util/suffix.h>
16 #include <util/prefix.h>
17 #include <util/config.h>
18 
19 #include "java_bytecode_parser.h"
20 #include "jar_file.h"
21 
23  const irep_idt &class_name)
24 {
25  std::stack<irep_idt> queue;
26 
27  // Always require java.lang.Object, as it is the base of
28  // internal classes such as array types.
29  queue.push("java.lang.Object");
30  // java.lang.String
31  queue.push("java.lang.String");
32  // add java.lang.Class
33  queue.push("java.lang.Class");
34  queue.push(class_name);
35 
36  java_class_loader_limitt class_loader_limit(
38 
39  while(!queue.empty())
40  {
41  irep_idt c=queue.top();
42  queue.pop();
43 
44  // do we have the class already?
45  if(class_map.find(c)!=class_map.end())
46  continue; // got it already
47 
48  debug() << "Reading class " << c << eom;
49 
50  java_bytecode_parse_treet &parse_tree=
51  get_parse_tree(class_loader_limit, c);
52 
53  // add any dependencies to queue
54  for(java_bytecode_parse_treet::class_refst::const_iterator
55  it=parse_tree.class_refs.begin();
56  it!=parse_tree.class_refs.end();
57  it++)
58  queue.push(*it);
59  }
60 
61  return class_map[class_name];
62 }
63 
65  std::string &_java_cp_include_files)
66 {
67  java_cp_include_files=_java_cp_include_files;
69 }
70 
72  java_class_loader_limitt &class_loader_limit,
73  const irep_idt &class_name)
74 {
75  java_bytecode_parse_treet &parse_tree=class_map[class_name];
76 
77  // First check given JAR files
78  for(const auto &jf : jar_files)
79  {
80  read_jar_file(class_loader_limit, jf);
81 
82  const auto &jm=jar_map[jf];
83 
84  auto jm_it=jm.entries.find(class_name);
85 
86  if(jm_it!=jm.entries.end())
87  {
88  debug() << "Getting class `" << class_name << "' from JAR "
89  << jf << eom;
90 
91  std::string data=jar_pool(class_loader_limit, jf)
92  .get_entry(jm_it->second.class_file_name);
93 
94  std::istringstream istream(data);
95 
97  istream,
98  parse_tree,
100 
101  return parse_tree;
102  }
103  }
104 
105  // See if we can find it in the class path
106  for(const auto &cp : config.java.classpath)
107  {
108  // in a JAR?
109  if(has_suffix(cp, ".jar"))
110  {
111  read_jar_file(class_loader_limit, cp);
112 
113  const auto &jm=jar_map[cp];
114 
115  auto jm_it=jm.entries.find(class_name);
116 
117  if(jm_it!=jm.entries.end())
118  {
119  debug() << "Getting class `" << class_name << "' from JAR "
120  << cp << eom;
121 
122  std::string data=jar_pool(class_loader_limit, cp)
123  .get_entry(jm_it->second.class_file_name);
124 
125  std::istringstream istream(data);
126 
128  istream,
129  parse_tree,
131 
132  return parse_tree;
133  }
134  }
135  else
136  {
137  // in a given directory?
138  std::string full_path=
139  #ifdef _WIN32
140  cp+'\\'+class_name_to_file(class_name);
141  #else
142  cp+'/'+class_name_to_file(class_name);
143  #endif
144 
145  // full class path starts with './'
146  if(class_loader_limit.load_class_file(full_path.substr(2)) &&
147  std::ifstream(full_path))
148  {
150  full_path,
151  parse_tree,
153  return parse_tree;
154  }
155  }
156  }
157 
158  // not found
159  warning() << "failed to load class `" << class_name << '\'' << eom;
160  parse_tree.parsed_class.name=class_name;
161  return parse_tree;
162 }
163 
165  java_class_loader_limitt &class_loader_limit,
166  const std::string &file)
167 {
168  read_jar_file(class_loader_limit, file);
169 
170  const auto &jm=jar_map[file];
171 
172  jar_files.push_front(file);
173 
174  for(const auto &e : jm.entries)
175  operator()(e.first);
176 
177  jar_files.pop_front();
178 }
179 
181  java_class_loader_limitt &class_loader_limit,
182  const irep_idt &file)
183 {
184  // done already?
185  if(jar_map.find(file)!=jar_map.end())
186  return;
187 
188  jar_filet &jar_file=jar_pool(class_loader_limit, id2string(file));
189 
190  if(!jar_file)
191  {
192  error() << "failed to open JAR file `" << file << "'" << eom;
193  return;
194  }
195 
196  debug() << "adding JAR file `" << file << "'" << eom;
197 
198  auto &jm=jar_map[file];
199 
200  for(auto &jar_entry : jar_file.filtered_jar)
201  {
202  std::string file_name=id2string(jar_entry.first);
203 
204  // does it end on .class?
205  if(has_suffix(file_name, ".class"))
206  {
207  irep_idt class_name=file_to_class_name(file_name);
208 
209  // record
210  jm.entries[class_name].class_file_name=file_name;
211  }
212  }
213 }
214 
215 std::string java_class_loadert::file_to_class_name(const std::string &file)
216 {
217  std::string result=file;
218 
219  // Strip .class. Note that the Java class loader would
220  // not do that.
221  if(has_suffix(result, ".class"))
222  result.resize(result.size()-6);
223 
224  // Strip a "./" prefix. Note that the Java class loader
225  // would not do that.
226  #ifdef _WIN32
227  while(has_prefix(result, ".\\"))
228  result=std::string(result, 2, std::string::npos);
229  #else
230  while(has_prefix(result, "./"))
231  result=std::string(result, 2, std::string::npos);
232  #endif
233 
234  // slash to dot
235  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
236  if(*it=='/')
237  *it='.';
238 
239  return result;
240 }
241 
242 std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
243 {
244  std::string result=id2string(class_name);
245 
246  // dots (package name separators) to slash, depending on OS
247  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
248  if(*it=='.')
249  {
250  #ifdef _WIN32
251  *it='\\';
252  #else
253  *it='/';
254  #endif
255  }
256 
257  // add .class suffix
258  result+=".class";
259 
260  return result;
261 }
mstreamt & warning()
Definition: message.h:228
mstreamt & result()
Definition: message.h:233
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::list< std::string > jar_files
bool java_bytecode_parse(std::istream &istream, java_bytecode_parse_treet &parse_tree, message_handlert &message_handler)
void load_entire_jar(java_class_loader_limitt &, const std::string &f)
java_bytecode_parse_treet & get_parse_tree(java_class_loader_limitt &, const irep_idt &)
filtered_jart filtered_jar
Definition: jar_file.h:40
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
classpatht classpath
Definition: config.h:142
static std::string file_to_class_name(const std::string &)
void set_java_cp_include_files(std::string &)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
struct configt::javat java
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
JAR File Reading.
mstreamt & debug()
Definition: message.h:253
message_handlert & get_message_handler()
Definition: message.h:127
java_bytecode_parse_treet & operator()(const irep_idt &)
bool load_class_file(const irep_idt &class_file_name)
mstreamt & error()
Definition: message.h:223
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
void read_jar_file(java_class_loader_limitt &, const irep_idt &)
std::string java_cp_include_files
Definition: kdev_t.h:24
static std::string class_name_to_file(const irep_idt &)
Definition: kdev_t.h:19