From 42ecfa274889fe08c654165db8f0671035131130 Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Thu, 5 Apr 2018 12:59:36 +0100 Subject: [PATCH] Add --java-no-load-class option --- .../java_bytecode_convert_class.cpp | 17 +++++++++---- .../java_bytecode_convert_class.h | 4 +++- src/java_bytecode/java_bytecode_language.cpp | 24 ++++++++++++------- src/java_bytecode/java_bytecode_language.h | 5 +++- 4 files changed, 35 insertions(+), 15 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 2d6d2d5d814..711bba8949e 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/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 &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 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 &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 { diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index b94cfc700b2..33edc2b1e09 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H +#include #include #include @@ -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 &no_load_classes); void mark_java_implicitly_generic_class_type( const irep_idt &class_name, diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 6f4ae143fed..4f62931d7d8 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/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 &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; } diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index f051d120d48..9db26385d8f 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -37,7 +37,8 @@ Author: Daniel Kroening, kroening@kroening.com "(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 no_load_classes; }; std::unique_ptr new_java_bytecode_language();