diff --git a/jbmc/src/java_bytecode/jar_file.cpp b/jbmc/src/java_bytecode/jar_file.cpp index 93be4551a43..4df0880309c 100644 --- a/jbmc/src/java_bytecode/jar_file.cpp +++ b/jbmc/src/java_bytecode/jar_file.cpp @@ -77,12 +77,20 @@ optionalt jar_filet::get_entry(const std::string &name) } } +/// Wrapper for `std::isspace` from `cctype` +/// \param ch: the character to check +/// \return true if the parameter is considered to be a space in the current +/// locale, else false static bool is_space(const char ch) { return std::isspace(ch) != 0; } /// Remove leading and trailing whitespace characters from string +/// \param begin: iterator to start search in string +/// \param end: iterator to end search in string +/// \return string truncated from begin to end and all whitespace removed at the +/// begin and end static std::string trim( const std::string::const_iterator begin, const std::string::const_iterator end) diff --git a/jbmc/src/java_bytecode/jar_file.h b/jbmc/src/java_bytecode/jar_file.h index ffb0eb784e8..64fe2301632 100644 --- a/jbmc/src/java_bytecode/jar_file.h +++ b/jbmc/src/java_bytecode/jar_file.h @@ -18,7 +18,8 @@ Author: Diffblue Ltd #include "mz_zip_archive.h" -/// Class representing a .jar archive +/// Class representing a .jar archive. Uses miniz to decompress and index +/// archive. class jar_filet final { public: @@ -44,7 +45,8 @@ class jar_filet final /// \param filename Name of the file in the archive optionalt get_entry(const std::string &filename); - /// Get contents of the Manifest file in the jar archive + /// Get contents of the Manifest file in the jar archive as a key-value map + /// (both as strings) std::unordered_map get_manifest(); /// Get list of filenames in the archive diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index c035a327126..5bdf0c5eaee 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -81,6 +81,11 @@ void java_class_loadert::add_classpath_entry(const std::string &path) } } +/// Load class from jar file. +/// \param class_name: name of class to load in Java source format +/// \param jar_file: path of the jar file +/// \param jar_index: the index of the jar file +/// \return optional value of parse tree, empty if class cannot be loaded optionalt java_class_loadert::get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, @@ -102,6 +107,11 @@ optionalt java_class_loadert::get_class_from_jar( return java_bytecode_parse(istream, get_message_handler()); } +/// Check if class is an overlay class by searching for `ID_overlay_class` in +/// its list of annotations. TODO(nathan) give a short explanation about what +/// overlay classes are. +/// \param c: a `classt` object from a java byte code parse tree +/// \return true if parsed class is an overlay class, else false static bool is_overlay_class(const java_bytecode_parse_treet::classt &c) { return java_bytecode_parse_treet::find_annotation( @@ -228,6 +238,9 @@ java_class_loadert::get_parse_tree( return parse_trees; } +/// Load all class files from a .jar file, and store name of .jar in +/// `classpath_entreies`. +/// \param jar_path: the path for the .jar to load void java_class_loadert::load_entire_jar( const std::string &jar_path) { @@ -280,6 +293,12 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( return std::cref(jar_index); } +/// Convert a file name to the class name. Java interprets folders as packages, +/// therefore a prefix of `./` is removed if necessary, and all `/` are +/// converted to `.`. For example a class file `./com/diffblue/test.class` is +/// converted to the class name `com.diffblue.test`. +/// \param file: the name of the class file +/// \return the file name converted to Java class name std::string java_class_loadert::file_to_class_name(const std::string &file) { std::string result=file; @@ -307,6 +326,10 @@ std::string java_class_loadert::file_to_class_name(const std::string &file) return result; } +/// Convert a class name to a file name, does the inverse of \ref +/// file_to_class_name. +/// \param class_name: the name of the class +/// \return the class name converted to file name std::string java_class_loadert::class_name_to_file(const irep_idt &class_name) { std::string result=id2string(class_name); diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index 8e83c2601ad..406055b62d2 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_parse_tree.h" #include "java_class_loader_limit.h" +/// Class responsible to load .class files. Either directly from a specific +/// file, from a classpath specification or from a Java archive (JAR) file. class java_class_loadert:public messaget { public: @@ -29,7 +31,10 @@ class java_class_loadert:public messaget /// implementing it for all classes inside a single JAR file typedef std::map jar_indext; + /// A list of parse trees supporting overlay classes typedef std::list parse_tree_with_overlayst; + /// A map from class names to list of parse tree where multiple entries can + /// exist in case of overlay classes. typedef std::map parse_tree_with_overridest_mapt; @@ -54,6 +59,8 @@ class java_class_loadert:public messaget java_class_loader_limitt &class_loader_limit, const irep_idt &class_name); + /// Set the argument of the class loader limit \ref java_class_loader_limitt + /// \param java_cp_include_files: argument string for java_class_loader_limit void set_java_cp_include_files(const std::string &java_cp_include_files) { this->java_cp_include_files = java_cp_include_files; diff --git a/jbmc/src/java_bytecode/java_class_loader_limit.cpp b/jbmc/src/java_bytecode/java_class_loader_limit.cpp index 5fc58d4326c..f25e84fe7cf 100644 --- a/jbmc/src/java_bytecode/java_class_loader_limit.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_limit.cpp @@ -13,8 +13,38 @@ Author: Daniel Kroening, kroening@kroening.com #include -/// initializes class with either regex matcher or match set -/// \par parameters: parameter from `java-cp-include-files` +/// Initializes class with either regex matcher or match set. If the string +/// starts with an `@` it is treated as a path to a JSON file. Otherwise, it is +/// treated as a regex. +/// +/// The regex case describes which class files should be loaded in the form of a +/// regular expression used with `regex_match`. +/// +/// The match set is a list of files to load in JSON format, the argument is the +/// name of the JSON file, prefixed with `@`. The file contains one section to +/// list the .jar files to load and one section to list the .class files to load +/// from the .jar. +/// +/// for example a file called `load.json` with the following content: +/// { +/// "jar": +/// [ +/// "A.jar", +/// "B.jar" +/// ], +/// "classFiles": +/// [ +/// "jarfile3$A.class", +/// "jarfile3.class" +/// ] +/// } +/// would be specified via `--java-cp-include-files @load.json` and would +/// instruct the driver to load `A.jar` and `B.jar` and the two .class files +/// `jarfile3$A.class` and `jarfile3.class`. All the rest of the .jar files is +/// ignored. +/// +/// \param java_cp_include_files: parameter from `java-cp-include-files` in the +/// format as described above void java_class_loader_limitt::setup_class_load_limit( const std::string &java_cp_include_files) { @@ -51,7 +81,9 @@ void java_class_loader_limitt::setup_class_load_limit( } } -/// \par parameters: class file name +/// Use the class load limiter to decide whether a class file should be loaded +/// or not. +/// \param file_name: the name of the class file to load /// \return true if file should be loaded, else false bool java_class_loader_limitt::load_class_file(const std::string &file_name) { diff --git a/jbmc/src/java_bytecode/java_class_loader_limit.h b/jbmc/src/java_bytecode/java_class_loader_limit.h index 93c663bcb21..64a7a7b9401 100644 --- a/jbmc/src/java_bytecode/java_class_loader_limit.h +++ b/jbmc/src/java_bytecode/java_class_loader_limit.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +/// Class representing a filter for class file loading. class java_class_loader_limitt:public messaget { /// Whether to use regex_matcher instead of set_matcher