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);
128 parse_trees.emplace_back(std::move(*parse_tree));
142 parse_trees.emplace_back(std::move(*parse_tree));
148 const std::string full_path =
150 cp_entry +
'\\' + class_file;
152 cp_entry +
'/' + class_file;
158 if(std::ifstream(full_path))
161 <<
"Getting class `" << class_name <<
"' from file " << full_path
166 parse_trees.emplace_back(std::move(*parse_tree));
171 if(!parse_trees.empty())
173 auto parse_tree_it = parse_trees.begin();
176 while(parse_tree_it != parse_trees.end())
179 if(parse_tree_it->loading_successful)
188 <<
"Skipping class " << class_name
189 <<
" marked with OverlayClassImplementation but found before" 190 " original definition" 193 auto unloaded_or_overlay_out_of_order_it = parse_tree_it;
195 parse_trees.erase(unloaded_or_overlay_out_of_order_it);
198 while(parse_tree_it != parse_trees.end())
204 <<
"Skipping duplicate definition of class " << class_name
205 <<
" not marked with OverlayClassImplementation" <<
eom;
206 auto duplicate_non_overlay_it = parse_tree_it;
208 parse_trees.erase(duplicate_non_overlay_it);
217 warning() <<
"failed to load class `" << class_name <<
'\'' <<
eom;
220 parse_trees.push_back(std::move(parse_tree));
226 const std::string &jar_path)
234 for(
const auto &e : jar_index->get())
242 const std::string &jar_path)
246 return std::cref(existing_it->second);
248 std::vector<std::string> filenames;
253 catch(
const std::runtime_error &)
255 error() <<
"failed to open JAR file `" << jar_path <<
"'" <<
eom;
258 debug() <<
"Adding JAR file `" << jar_path <<
"'" <<
eom;
263 for(
auto &file_name : filenames)
268 <<
"Found class file " << file_name <<
" in JAR `" << jar_path <<
"'" 271 jar_index[class_name] = file_name;
274 return std::cref(jar_index);
297 for(std::string::iterator it=
result.begin(); it!=
result.end(); it++)
309 for(std::string::iterator it=
result.begin(); it!=
result.end(); it++)
327 const std::string &file_name)
334 return m_archives.emplace(file_name, std::move(
file)).first->second;
342 const std::string &buffer_name,
351 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.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
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)
mstreamt & warning() const
static std::string file_to_class_name(const std::string &)
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
bool has_prefix(const std::string &s, const std::string &prefix)
struct configt::javat java
optionalt< class java_bytecode_parse_treet > java_bytecode_parse(std::istream &istream, message_handlert &message_handler)
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 &)