23 std::stack<irep_idt> queue;
26 queue.push(
"java.lang.Object");
28 queue.push(
"java.lang.String");
30 queue.push(
"java.lang.Class");
33 queue.push(
"java.lang.Throwable");
34 queue.push(class_name);
51 debug() <<
"Reading class " << c <<
eom;
58 for(
const irep_idt &class_ref : parse_tree.class_refs)
59 queue.push(class_ref);
74 const std::string &jar_file,
78 auto jar_index_it = jar_index.find(class_name);
79 if(jar_index_it == jar_index.end())
83 <<
"Getting class `" << class_name <<
"' from JAR " << jar_file <<
eom;
91 std::istringstream istream(*
data);
122 debug() <<
"not loading " << class_name <<
" because of limit" <<
eom;
125 parse_trees.push_back(std::move(parse_tree));
138 parse_trees.emplace_back(std::move(*parse_tree));
152 parse_trees.emplace_back(std::move(*parse_tree));
158 const std::string full_path =
160 cp_entry +
'\\' + class_file;
162 cp_entry +
'/' + class_file;
168 if(std::ifstream(full_path))
171 <<
"Getting class `" << class_name <<
"' from file " << full_path
176 parse_trees.emplace_back(std::move(*parse_tree));
181 auto parse_tree_it = parse_trees.begin();
184 while(parse_tree_it != parse_trees.end())
187 if(parse_tree_it->loading_successful)
196 <<
"Skipping class " << class_name
197 <<
" marked with OverlayClassImplementation but found before" 198 " original definition" 201 auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
203 parse_trees.erase(unloaded_or_overlay_out_of_order_it);
206 while(parse_tree_it != parse_trees.end())
212 <<
"Skipping duplicate definition of class " << class_name
213 <<
" not marked with OverlayClassImplementation" <<
eom;
214 auto duplicate_non_overlay_it = parse_tree_it;
216 parse_trees.erase(duplicate_non_overlay_it);
221 if(!parse_trees.empty())
225 warning() <<
"failed to load class `" << class_name <<
'\'' <<
eom;
228 parse_trees.push_back(std::move(parse_tree));
234 const std::string &jar_path)
242 for(
const auto &e : jar_index->get())
250 const std::string &jar_path)
254 return std::cref(existing_it->second);
256 std::vector<std::string> filenames;
261 catch(
const std::runtime_error &)
263 error() <<
"failed to open JAR file `" << jar_path <<
"'" <<
eom;
266 debug() <<
"Adding JAR file `" << jar_path <<
"'" <<
eom;
271 for(
auto &file_name : filenames)
276 <<
"Found class file " << file_name <<
" in JAR `" << jar_path <<
"'" 279 jar_index[class_name] = file_name;
282 return std::cref(jar_index);
305 for(std::string::iterator it=
result.begin(); it!=
result.end(); it++)
317 for(std::string::iterator it=
result.begin(); it!=
result.end(); it++)
335 const std::string &file_name)
342 return m_archives.emplace(file_name, std::move(
file)).first->second;
350 const std::string &buffer_name,
359 return m_archives.emplace(buffer_name, std::move(
file)).first->second;
std::map< std::string, jar_indext > jars_by_path
The jar_indext for each jar file we've read.
const std::string & id2string(const irep_idt &d)
jar_index_optcreft read_jar_file(java_class_loader_limitt &class_loader_limit, const std::string &jar_path)
std::list< std::string > jar_files
List of filesystem paths to .jar files that will be used, in the given order, to find and load a clas...
std::vector< irep_idt > java_load_classes
Classes to be explicitly loaded.
std::vector< std::string > filenames() const
Get list of filenames in the archive.
optionalt< std::string > get_entry(const std::string &filename)
Get contents of a file in the jar archive.
parse_tree_with_overlayst & get_parse_tree(java_class_loader_limitt &class_loader_limit, const irep_idt &class_name)
Given a class_name (e.g.
jar_filet & jar_pool(java_class_loader_limitt &limit, const std::string &filename)
Load jar archive or retrieve from cache if already loaded.
std::map< irep_idt, std::string > jar_indext
A map associating logical class names with the name of the .class file implementing it for all classe...
static mstreamt & eom(mstreamt &m)
std::list< java_bytecode_parse_treet > parse_tree_with_overlayst
void load_entire_jar(java_class_loader_limitt &, const std::string &jar_path)
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
mstreamt & warning() const
static std::string file_to_class_name(const std::string &)
optionalt< java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
bool has_prefix(const std::string &s, const std::string &prefix)
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Class representing a .jar archive.
message_handlert & get_message_handler()
mstreamt & result() const
static bool is_overlay_class(const java_bytecode_parse_treet::classt &c)
optionalt< std::reference_wrapper< const jar_indext > > jar_index_optcreft
std::map< std::string, jar_filet > m_archives
Jar files that have been loaded.
get_extra_class_refs_functiont get_extra_class_refs
bool load_class_file(const std::string &class_file_name)
parse_tree_with_overlayst & operator()(const irep_idt &class_name)
bool has_suffix(const std::string &s, const std::string &suffix)
optionalt< java_bytecode_parse_treet > get_class_from_jar(const irep_idt &class_name, const std::string &jar_file, const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit)
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 ...
parse_tree_with_overridest_mapt class_map
Map from class names to the bytecode parse trees.
static std::string class_name_to_file(const irep_idt &)