From c4569dde236ad88f7894752089dcaf5d34c7430c Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Wed, 4 Jul 2018 14:19:37 +0100
Subject: [PATCH] remove java_class_loader_limitt from jar_filet

---
 jbmc/src/java_bytecode/jar_file.cpp          | 19 +++++++++----------
 jbmc/src/java_bytecode/jar_file.h            | 10 +++-------
 jbmc/src/java_bytecode/java_class_loader.cpp | 14 ++++++++++++--
 3 files changed, 24 insertions(+), 19 deletions(-)

diff --git a/jbmc/src/java_bytecode/jar_file.cpp b/jbmc/src/java_bytecode/jar_file.cpp
index b1ae84ea9fa..93be4551a43 100644
--- a/jbmc/src/java_bytecode/jar_file.cpp
+++ b/jbmc/src/java_bytecode/jar_file.cpp
@@ -16,44 +16,43 @@ Author: Diffblue Ltd
 
 #include "java_class_loader_limit.h"
 
-void jar_filet::initialize_file_index(java_class_loader_limitt &limit)
+void jar_filet::initialize_file_index()
 {
   const size_t file_count=m_zip_archive.get_num_files();
   for(size_t index=0; index<file_count; index++)
   {
     const auto filename=m_zip_archive.get_filename(index);
-    if(!has_suffix(filename, ".class") || limit.load_class_file(filename))
-      m_name_to_index.emplace(filename, index);
+    m_name_to_index.emplace(filename, index);
   }
 }
 
 /// This constructor creates a jar_file object whose contents
 /// are extracted from a file with given name.
 jar_filet::jar_filet(
-  java_class_loader_limitt &limit,
   const std::string &filename):
   m_zip_archive(filename)
 {
-  initialize_file_index(limit);
+  initialize_file_index();
 }
 
 /// This constructor creates a jar_file object whose contents
 /// are extracted from a memory buffer (byte array) as opposed
 /// to a jar file.
 jar_filet::jar_filet(
-  java_class_loader_limitt &limit,
   const void *data,
   size_t size):
   m_zip_archive(data, size)
 {
-  initialize_file_index(limit);
+  initialize_file_index();
 }
 
 // VS: No default move constructors or assigns
 
-jar_filet::jar_filet(jar_filet &&other):
-  m_zip_archive(std::move(other.m_zip_archive)),
-  m_name_to_index((other.m_name_to_index)) {}
+jar_filet::jar_filet(jar_filet &&other)
+  : m_zip_archive(std::move(other.m_zip_archive)),
+    m_name_to_index(std::move(other.m_name_to_index))
+{
+}
 
 jar_filet &jar_filet::operator=(jar_filet &&other)
 {
diff --git a/jbmc/src/java_bytecode/jar_file.h b/jbmc/src/java_bytecode/jar_file.h
index 4cf81d6f4bb..ffb0eb784e8 100644
--- a/jbmc/src/java_bytecode/jar_file.h
+++ b/jbmc/src/java_bytecode/jar_file.h
@@ -18,24 +18,20 @@ Author: Diffblue Ltd
 
 #include "mz_zip_archive.h"
 
-class java_class_loader_limitt;
-
 /// Class representing a .jar archive
 class jar_filet final
 {
 public:
   /// Open java file for reading.
-  /// \param limit Object limiting number of loaded .class files
   /// \param filename Name of the file
   /// \throw Throws std::runtime_error if file cannot be opened
-  jar_filet(java_class_loader_limitt &limit, const std::string &filename);
+  explicit jar_filet(const std::string &filename);
 
   /// Open a JAR file of size \p size loaded in memory at address \p data.
-  /// \param limit Object limiting number of loaded .class files
   /// \param data memory buffer with the contents of the jar file
   /// \param size size  of the memory buffer
   /// \throw Throws std::runtime_error if file cannot be opened
-  jar_filet(java_class_loader_limitt &limit, const void *data, size_t size);
+  jar_filet(const void *data, size_t size);
 
   jar_filet(const jar_filet &)=delete;
   jar_filet &operator=(const jar_filet &)=delete;
@@ -57,7 +53,7 @@ class jar_filet final
 private:
   /// Loads the fileindex (m_name_to_index) with a map of loaded files to
   /// indices.
-  void initialize_file_index(java_class_loader_limitt &limit);
+  void initialize_file_index();
 
   mz_zip_archivet m_zip_archive;
 
diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp
index 048d41cc5fb..b6a98f2160e 100644
--- a/jbmc/src/java_bytecode/java_class_loader.cpp
+++ b/jbmc/src/java_bytecode/java_class_loader.cpp
@@ -116,6 +116,16 @@ java_class_loadert::get_parse_tree(
   parse_tree_with_overlayst &parse_trees = class_map[class_name];
   PRECONDITION(parse_trees.empty());
 
+  // do we refuse to load?
+  if(!class_loader_limit.load_class_file(class_name_to_file(class_name)))
+  {
+    debug() << "not loading " << class_name << " because of limit" << eom;
+    java_bytecode_parse_treet parse_tree;
+    parse_tree.parsed_class.name = class_name;
+    parse_trees.push_back(std::move(parse_tree));
+    return parse_trees;
+  }
+
   // First add all given JAR files
   for(const auto &jar_file : jar_files)
   {
@@ -328,7 +338,7 @@ jar_filet &java_class_loadert::jar_pool(
   if(it==m_archives.end())
   {
     // VS: Can't construct in place
-    auto file=jar_filet(class_loader_limit, file_name);
+    auto file = jar_filet(file_name);
     return m_archives.emplace(file_name, std::move(file)).first->second;
   }
   else
@@ -345,7 +355,7 @@ jar_filet &java_class_loadert::jar_pool(
   if(it==m_archives.end())
   {
     // VS: Can't construct in place
-    auto file=jar_filet(class_loader_limit, pmem, size);
+    auto file = jar_filet(pmem, size);
     return m_archives.emplace(buffer_name, std::move(file)).first->second;
   }
   else