Merge pull request #2013 from LAJW/lajw/java-no-load-class

Add --java-no-load-class option

Author: forejtv

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -37,12 +37,14 @@ class java_bytecode_convert_classt:public messaget
     message_handlert &_message_handler,
     size_t _max_array_length,
     method_bytecodet &method_bytecode,
-    java_string_library_preprocesst &_string_preprocess)
+    java_string_library_preprocesst &_string_preprocess,
+    const std::unordered_set<std::string> &no_load_classes)
     : messaget(_message_handler),
       symbol_table(_symbol_table),
       max_array_length(_max_array_length),
       method_bytecode(method_bytecode),
-      string_preprocess(_string_preprocess)
+      string_preprocess(_string_preprocess),
+      no_load_classes(no_load_classes)
   {
   }
 
@@ -51,7 +53,9 @@ class java_bytecode_convert_classt:public messaget
     // add array types to the symbol table
     add_array_types(symbol_table);
 
-    bool loading_success=parse_tree.loading_successful;
+    const bool loading_success =
+      parse_tree.loading_successful &&
+      !no_load_classes.count(id2string(parse_tree.parsed_class.name));
     if(loading_success)
       convert(parse_tree.parsed_class);
 
@@ -81,6 +85,7 @@ class java_bytecode_convert_classt:public messaget
 
   // see definition below for more info
   static void add_array_types(symbol_tablet &symbol_table);
+  std::unordered_set<std::string> no_load_classes;
 };
 
 /// Auxiliary function to extract the generic superclass reference from the
@@ -667,14 +672,16 @@ bool java_bytecode_convert_class(
   message_handlert &message_handler,
   size_t max_array_length,
   method_bytecodet &method_bytecode,
-  java_string_library_preprocesst &string_preprocess)
+  java_string_library_preprocesst &string_preprocess,
+  const std::unordered_set<std::string> &no_load_classes)
 {
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
     max_array_length,
     method_bytecode,
-    string_preprocess);
+    string_preprocess,
+    no_load_classes);
 
   try
   {

src/java_bytecode/java_bytecode_convert_class.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H
 
+#include <unordered_set>
 #include <util/symbol_table.h>
 #include <util/message.h>
 
@@ -25,7 +26,8 @@ bool java_bytecode_convert_class(
   message_handlert &message_handler,
   size_t max_array_length,
   method_bytecodet &,
-  java_string_library_preprocesst &string_preprocess);
+  java_string_library_preprocesst &string_preprocess,
+  const std::unordered_set<std::string> &no_load_classes);
 
 void mark_java_implicitly_generic_class_type(
   const irep_idt &class_name,

src/java_bytecode/java_bytecode_language.cpp

@@ -79,6 +79,11 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     java_load_classes.insert(
         java_load_classes.end(), values.begin(), values.end());
   }
+  if(cmd.isset("java-no-load-class"))
+  {
+    const auto &values = cmd.get_values("java-no-load-class");
+    no_load_classes = {values.begin(), values.end()};
+  }
 
   const std::list<std::string> &extra_entry_points=
     cmd.get_values("lazy-methods-extra-entry-point");
@@ -576,13 +581,15 @@ bool java_bytecode_languaget::typecheck(
     java_class_loader.class_map.find("java.lang.Object");
   if(it!=java_class_loader.class_map.end())
   {
-    if(java_bytecode_convert_class(
-     it->second,
-     symbol_table,
-     get_message_handler(),
-     max_user_array_length,
-     method_bytecode,
-     string_preprocess))
+    if(
+      java_bytecode_convert_class(
+        it->second,
+        symbol_table,
+        get_message_handler(),
+        max_user_array_length,
+        method_bytecode,
+        string_preprocess,
+        no_load_classes))
     {
       return true;
     }
@@ -605,7 +612,8 @@ bool java_bytecode_languaget::typecheck(
         get_message_handler(),
         max_user_array_length,
         method_bytecode,
-        string_preprocess))
+        string_preprocess,
+        no_load_classes))
     {
       return true;
     }

src/java_bytecode/java_bytecode_language.h

@@ -37,7 +37,8 @@ Author: Daniel Kroening, [email protected]
   "(java-cp-include-files):"                                                   \
   "(lazy-methods)"                                                             \
   "(lazy-methods-extra-entry-point):"                                          \
-  "(java-load-class):"
+  "(java-load-class):"                                                         \
+  "(java-no-load-class):"
 
 #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/                                          \
   " --no-core-models                 don't load internally provided models for core classes in\n"/* NOLINT(*) */ \
@@ -181,6 +182,8 @@ class java_bytecode_languaget:public languaget
   synthetic_methods_mapt synthetic_methods;
   stub_global_initializer_factoryt stub_global_initializer_factory;
   class_hierarchyt class_hierarchy;
+  // List of classes to never load
+  std::unordered_set<std::string> no_load_classes;
 };
 
 std::unique_ptr<languaget> new_java_bytecode_language();