allow regex to limit class files loaded from JAR

Author: Matthias Güdemann

src/cbmc/cbmc_parse_options.cpp

@@ -1155,6 +1155,7 @@ void cbmc_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --java-max-vla-length        limit the length of user-code-created arrays\n"
     // NOLINTNEXTLINE(whitespace/line_length)
+    " --java-cp-include-files      regexp of class files to load\n"
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n"
     "\n"
     "Semantic transformations:\n"

src/cbmc/cbmc_parse_options.h

@@ -55,6 +55,7 @@ class optionst;
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
+  "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)

src/java_bytecode/jar_file.cpp

@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
 #include <cstring>
 #include <cassert>
 #include <sstream>
-
 #include "jar_file.h"
+#include <util/suffix.h>
 
 /*******************************************************************\
 
@@ -24,7 +24,7 @@ Function: jar_filet::open
 
 \*******************************************************************/
 
-void jar_filet::open(const std::string &filename)
+void jar_filet::open(std::string &java_cp_include_files, const std::string &filename)
 {
   if(!mz_ok)
   {
@@ -38,8 +38,7 @@ void jar_filet::open(const std::string &filename)
     std::size_t number_of_files=
       mz_zip_reader_get_num_files(&zip);
 
-    index.reserve(number_of_files);
-
+    size_t filtered_index=0;
     for(std::size_t i=0; i<number_of_files; i++)
     {
       mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
@@ -48,8 +47,17 @@ void jar_filet::open(const std::string &filename)
         mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
       assert(filename_length==filename_len);
       std::string file_name(filename_char);
+      std::smatch string_matcher;
+      std::regex matcher(java_cp_include_files);
+      // load .class files only if they match regex
+      if(std::regex_match(file_name, string_matcher, matcher) ||
+         !has_suffix(file_name, ".class"))
+      {
+        index.push_back(file_name);
+        filtered_jar[filtered_index]=i;
+        filtered_index++;
+      }
       delete[] filename_char;
-      index.push_back(file_name);
     }
   }
 }
@@ -96,16 +104,17 @@ std::string jar_filet::get_entry(std::size_t i)
 
   std::string dest;
 
+  size_t real_index=filtered_jar[i];
   mz_zip_archive_file_stat file_stat;
   memset(&file_stat, 0, sizeof(file_stat));
-  mz_bool stat_ok=mz_zip_reader_file_stat(&zip, i, &file_stat);
+  mz_bool stat_ok=mz_zip_reader_file_stat(&zip, real_index, &file_stat);
   if(stat_ok!=MZ_TRUE)
     return std::string();
   std::vector<char> buffer;
   size_t bufsize=file_stat.m_uncomp_size;
   buffer.resize(bufsize);
   mz_bool read_ok=
-    mz_zip_reader_extract_to_mem(&zip, i, buffer.data(), bufsize, 0);
+    mz_zip_reader_extract_to_mem(&zip, real_index, buffer.data(), bufsize, 0);
   if(read_ok!=MZ_TRUE)
     return std::string();
 

src/java_bytecode/jar_file.h

@@ -15,27 +15,26 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 #include <vector>
 #include <map>
+#include <regex>
 
 class jar_filet
 {
 public:
   jar_filet():mz_ok(false) { }
-
-  inline explicit jar_filet(const std::string &file_name)
-  {
-    open(file_name);
-  }
+  inline explicit jar_filet(const std::string &file_name) { }
 
   ~jar_filet();
 
-  void open(const std::string &);
+  void open(std::string &java_cp_include_files, const std::string &);
 
   // Test for error; 'true' means we are good.
-  inline explicit operator bool() const { return true;  // TODO
-  }
+  inline explicit operator bool() const { return mz_ok; }
 
   typedef std::vector<std::string> indext;
   indext index;
+  // map internal index to real index in jar central directory
+  typedef std::map<int, int> filtered_jart;
+  filtered_jart filtered_jar;
 
   std::string get_entry(std::size_t i);
 
@@ -45,18 +44,25 @@ class jar_filet
 protected:
   mz_zip_archive zip;
   bool mz_ok;
+  std::string matcher;
+  std::map<int, int> index_map;
 };
 
 class jar_poolt
 {
 public:
+  void set_java_cp_include_files(std::string &_java_cp_include_files)
+  {
+    java_cp_include_files=_java_cp_include_files;
+  }
   jar_filet &operator()(const std::string &file_name)
   {
+    assert(!java_cp_include_files.empty() && "class regexp cannot be empty");
     file_mapt::iterator it=file_map.find(file_name);
     if(it==file_map.end())
     {
       jar_filet &jar_file=file_map[file_name];
-      jar_file.open(file_name);
+      jar_file.open(java_cp_include_files, file_name);
       return jar_file;
     }
     else
@@ -66,6 +72,7 @@ class jar_poolt
 protected:
   typedef std::map<std::string, jar_filet> file_mapt;
   file_mapt file_map;
+  std::string java_cp_include_files;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAR_FILE_H

src/java_bytecode/java_bytecode_language.cpp

@@ -55,6 +55,10 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
+  if(cmd.isset("java-cp-include-files"))
+    java_cp_include_files=cmd.get_value("java-cp-include-files");
+  else
+    java_cp_include_files=".*";
 }
 
 /*******************************************************************\
@@ -129,6 +133,7 @@ bool java_bytecode_languaget::parse(
   const std::string &path)
 {
   java_class_loader.set_message_handler(get_message_handler());
+  java_class_loader.set_java_cp_include_files(java_cp_include_files);
 
   // look at extension
   if(has_suffix(path, ".class"))

src/java_bytecode/java_bytecode_language.h

@@ -105,6 +105,7 @@ class java_bytecode_languaget:public languaget
   lazy_methodst lazy_methods;
   lazy_methods_modet lazy_methods_mode;
   bool string_refinement_enabled;
+  std::string java_cp_include_files;
 };
 
 languaget *new_java_bytecode_language();

src/java_bytecode/java_class_loader.h

@@ -20,6 +20,10 @@ class java_class_loadert:public messaget
 {
 public:
   java_bytecode_parse_treet &operator()(const irep_idt &);
+  void set_java_cp_include_files(std::string &java_cp_include_files)
+  {
+    jar_pool.set_java_cp_include_files(java_cp_include_files);
+  }
 
   // maps class names to the parse trees
   typedef std::map<irep_idt, java_bytecode_parse_treet> class_mapt;