CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
java_class_loader.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "java_class_loader.h"
10
11#include <stack>
12
13#include <util/message.h>
14#include <util/suffix.h>
15
17
19operator()(const irep_idt &class_name, message_handlert &message_handler)
20{
21 messaget log(message_handler);
22
23 log.debug() << "Classpath:";
24 for(const auto &entry : classpath_entries)
25 {
26 log.debug() << "\n " << entry.path;
27 }
28 log.debug() << messaget::eom;
29
30 std::stack<irep_idt> queue;
31 // Always require java.lang.Object, as it is the base of
32 // internal classes such as array types.
33 queue.push("java.lang.Object");
34 // java.lang.String
35 queue.push("java.lang.String");
36 // add java.lang.Class
37 queue.push("java.lang.Class");
38 // Require java.lang.Throwable as the catch-type used for
39 // universal exception handlers:
40 queue.push("java.lang.Throwable");
41 queue.push(class_name);
42
43 // Require user provided classes to be loaded even without explicit reference
44 for(const auto &id : java_load_classes)
45 queue.push(id);
46
48 message_handler, java_cp_include_files);
49
50 while(!queue.empty())
51 {
52 irep_idt c=queue.top();
53 queue.pop();
54
55 if(class_map.count(c) != 0)
56 continue;
57
58 log.debug() << "Reading class " << c << messaget::eom;
59
61 get_parse_tree(class_loader_limit, c, message_handler);
62
63 // Add any dependencies to queue
64 for(const java_bytecode_parse_treet &parse_tree : parse_trees)
65 for(const irep_idt &class_ref : parse_tree.class_refs)
66 queue.push(class_ref);
67
68 // Add any extra dependencies provided by our caller:
70 {
71 for(const irep_idt &id : get_extra_class_refs(c))
72 queue.push(id);
73 }
74 }
75
76 return class_map.at(class_name);
77}
78
101{
103 c.annotations, ID_overlay_class)
104 .has_value();
105}
106
108 const irep_idt &class_name,
109 message_handlert &message_handler)
110{
111 for(const auto &cp_entry : classpath_entries)
112 {
113 auto parse_tree = load_class(class_name, cp_entry, message_handler);
114 if(parse_tree.has_value())
115 return true;
116 }
117 return false;
118}
119
136 const irep_idt &class_name,
137 message_handlert &message_handler)
138{
140 PRECONDITION(parse_trees.empty());
141
142 messaget log(message_handler);
143
144 // do we refuse to load?
145 if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
146 {
147 log.debug() << "not loading " << class_name << " because of limit"
148 << messaget::eom;
149 parse_trees.emplace_back(class_name);
150 return parse_trees;
151 }
152
153 // Rummage through the class path
154 for(const auto &cp_entry : classpath_entries)
155 {
156 auto parse_tree = load_class(class_name, cp_entry, message_handler);
157 if(parse_tree.has_value())
158 parse_trees.emplace_back(std::move(*parse_tree));
159 }
160
161 auto parse_tree_it = parse_trees.begin();
162 // If the first class implementation is an overlay emit a warning and
163 // skip over it until we find a non-overlay class
164 while(parse_tree_it != parse_trees.end())
165 {
166 // Skip parse trees that failed to load - though these shouldn't exist yet
167 if(parse_tree_it->loading_successful)
168 {
169 if(!is_overlay_class(parse_tree_it->parsed_class))
170 {
171 // Keep the non-overlay class
173 break;
174 }
175 log.debug() << "Skipping class " << class_name
176 << " marked with OverlayClassImplementation but found before"
177 " original definition"
178 << messaget::eom;
179 }
183 }
184 // Collect overlay classes
185 while(parse_tree_it != parse_trees.end())
186 {
187 // Remove non-initial classes that aren't overlays
188 if(!is_overlay_class(parse_tree_it->parsed_class))
189 {
190 log.debug() << "Skipping duplicate definition of class " << class_name
191 << " not marked with OverlayClassImplementation"
192 << messaget::eom;
196 }
197 else
199 }
200 if(!parse_trees.empty())
201 return parse_trees;
202
203 // Not found or failed to load
204 log.debug() << "failed to load class " << class_name << messaget::eom;
205 parse_trees.emplace_back(class_name);
206 return parse_trees;
207}
208
213 const std::string &jar_path,
214 message_handlert &message_handler)
215{
216 auto classes = read_jar_file(jar_path, message_handler);
217 if(!classes.has_value())
218 return {};
219
220 classpath_entries.push_front(
221 classpath_entryt(classpath_entryt::JAR, jar_path));
222
223 for(const auto &c : *classes)
224 operator()(c, message_handler);
225
226 classpath_entries.pop_front();
227
228 return *classes;
229}
230
231std::optional<std::vector<irep_idt>> java_class_loadert::read_jar_file(
232 const std::string &jar_path,
233 message_handlert &message_handler)
234{
235 messaget log(message_handler);
236
237 std::vector<std::string> filenames;
238 try
239 {
240 filenames = jar_pool(jar_path).filenames();
241 }
242 catch(const std::runtime_error &)
243 {
244 log.error() << "failed to open JAR file '" << jar_path << "'"
245 << messaget::eom;
246 return {};
247 }
248 log.debug() << "Adding JAR file '" << jar_path << "'" << messaget::eom;
249
250 // Create a new entry in the map and initialize using the list of file names
251 // that are in jar_filet
252 std::vector<irep_idt> classes;
253 for(auto &file_name : filenames)
254 {
255 if(has_suffix(file_name, ".class"))
256 {
257 log.debug() << "Found class file " << file_name << " in JAR '" << jar_path
258 << "'" << messaget::eom;
259 irep_idt class_name=file_to_class_name(file_name);
260 classes.push_back(class_name);
261 }
262 }
263 return classes;
264}
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
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_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 representing a filter for class file loading.
std::string java_cp_include_files
Either a regular expression matching files that will be allowed to be loaded or a string of the form ...
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
std::vector< irep_idt > load_entire_jar(const std::string &jar_path, message_handlert &)
Load all class files from a .jar file.
bool can_load_class(const irep_idt &class_name, message_handlert &)
Checks whether class_name is parseable from the classpath, ignoring class loading limits.
parse_tree_with_overlayst & operator()(const irep_idt &class_name, message_handlert &)
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name, message_handlert &)
Check through all the places class parse trees can appear and returns the first implementation it fin...
get_extra_class_refs_functiont get_extra_class_refs
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
A list of parse trees supporting overlay classes.
std::optional< std::vector< irep_idt > > read_jar_file(const std::string &jar_path, message_handlert &)
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
Check if class is an overlay class by searching for ID_overlay_class in its list of annotations.
limit class path loading
double log(double x)
Definition math.c:2449
#define PRECONDITION(CONDITION)
Definition invariant.h:463
static std::optional< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17