Merge pull request #2772 from mgudemann/doc/doc-21/java_load_jar

[DOC-21] Documentation for java loading from jar / class files

jbmc/src/java_bytecode/jar_file.cpp

@@ -77,12 +77,20 @@ optionalt<std::string> 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)

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 @@ public:
   /// \param filename Name of the file in the archive
   optionalt<std::string> 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<std::string, std::string> get_manifest();
 
   /// Get list of filenames in the archive

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_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
   const irep_idt &class_name,
   const std::string &jar_file,
@@ -102,6 +107,11 @@ optionalt<java_bytecode_parse_treet> 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);

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 @@ public:
   /// implementing it for all classes inside a single JAR file
   typedef std::map<irep_idt, std::string> jar_indext;
 
+  /// A list of parse trees supporting overlay classes
   typedef std::list<java_bytecode_parse_treet> 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<irep_idt, parse_tree_with_overlayst>
     parse_tree_with_overridest_mapt;
 
@@ -54,6 +59,8 @@ public:
     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;

jbmc/src/java_bytecode/java_class_loader_limit.cpp

@@ -13,8 +13,38 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <json/json_parser.h>
 
-/// 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)
 {

jbmc/src/java_bytecode/java_class_loader_limit.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/irep.h>
 #include <util/message.h>
 
+/// Class representing a filter for class file loading.
 class java_class_loader_limitt:public messaget
 {
   /// Whether to use regex_matcher instead of set_matcher