diff --git a/regression/cbmc-java/jar-file4/A.jar b/regression/cbmc-java/jar-file4/A.jar new file mode 100644 index 00000000000..e721e6f32f9 Binary files /dev/null and b/regression/cbmc-java/jar-file4/A.jar differ diff --git a/regression/cbmc-java/jar-file4/B.jar b/regression/cbmc-java/jar-file4/B.jar new file mode 100644 index 00000000000..d381e413e74 Binary files /dev/null and b/regression/cbmc-java/jar-file4/B.jar differ diff --git a/regression/cbmc-java/jar-file4/C.jar b/regression/cbmc-java/jar-file4/C.jar new file mode 100644 index 00000000000..e318db6c413 Binary files /dev/null and b/regression/cbmc-java/jar-file4/C.jar differ diff --git a/regression/cbmc-java/jar-file4/jar.json b/regression/cbmc-java/jar-file4/jar.json new file mode 100644 index 00000000000..09df8008b8c --- /dev/null +++ b/regression/cbmc-java/jar-file4/jar.json @@ -0,0 +1,12 @@ +{ + "jar": + [ + "A.jar", + "B.jar" + ], + "classFiles": + [ + "jarfile3$A.class", + "jarfile3.class" + ] +} diff --git a/regression/cbmc-java/jar-file4/test.desc b/regression/cbmc-java/jar-file4/test.desc new file mode 100644 index 00000000000..5c34bdcd5a8 --- /dev/null +++ b/regression/cbmc-java/jar-file4/test.desc @@ -0,0 +1,10 @@ +CORE +C.jar +--function jarfile3.f --java-cp-include-files "@jar.json" +^EXIT=10$ +^SIGNAL=0$ +.*SUCCESS$ +.*FAILURE$ +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 79224766188..8132097565c 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -28,7 +28,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ ../util/util$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) INCLUDES= -I .. diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7364752d093..5ed5d28054e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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 or JSON list of files to load (with '@' prefix)\n" " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" "\n" "Semantic transformations:\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index adc6e2ee517..a3fc5e7e7d3 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/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) diff --git a/src/cegis/Makefile b/src/cegis/Makefile index 37fe5416953..f1a38ce4915 100644 --- a/src/cegis/Makefile +++ b/src/cegis/Makefile @@ -116,7 +116,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT) \ ../cbmc/fault_localization$(OBJEXT) \ ../cbmc/symex_coverage$(OBJEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) INCLUDES= -I .. diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile index 04261db95f0..3079e7ebb00 100644 --- a/src/goto-cc/Makefile +++ b/src/goto-cc/Makefile @@ -14,7 +14,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ ../assembler/assembler$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) INCLUDES= -I .. diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile index c003d0c96b0..fd18897aaea 100644 --- a/src/goto-diff/Makefile +++ b/src/goto-diff/Makefile @@ -14,7 +14,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ ../util/util$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) INCLUDES= -I .. diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index f79b62d806f..4cbd6121b24 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -38,7 +38,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ ../util/util$(LIBEXT) \ ../solvers/solvers$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) INCLUDES= -I .. diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index d679f21c070..07d7719e500 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -8,10 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include +#include +#include #include "jar_file.h" - /*******************************************************************\ Function: jar_filet::open @@ -24,7 +25,9 @@ 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) { @@ -35,11 +38,37 @@ void jar_filet::open(const std::string &filename) if(mz_ok) { + // '@' signals file reading with list of class files to load + bool regex_match=java_cp_include_files[0]!='@'; + std::regex regex_matcher; + std::smatch string_matcher; + std::unordered_set set_matcher; + jsont json_cp_config; + if(regex_match) + regex_matcher=std::regex(java_cp_include_files); + else + { + assert(java_cp_include_files.length()>1); + if(parse_json( + java_cp_include_files.substr(1), + get_message_handler(), + json_cp_config)) + throw "cannot read JSON input configuration for JAR loading"; + if(!json_cp_config.is_object()) + throw "the JSON file has a wrong format"; + jsont include_files=json_cp_config["classFiles"]; + if(!include_files.is_array()) + throw "the JSON file has a wrong format"; + for(const jsont &file_entry : include_files.array) + { + assert(file_entry.is_string()); + set_matcher.insert(file_entry.value); + } + } + std::size_t number_of_files= mz_zip_reader_get_num_files(&zip); - index.reserve(number_of_files); - for(std::size_t i=0; isecond; 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 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(); @@ -128,24 +174,11 @@ Function: jar_filet::get_manifest jar_filet::manifestt jar_filet::get_manifest() { - std::size_t i=0; - bool found=false; - - for(const auto &e : index) - { - if(e=="META-INF/MANIFEST.MF") - { - found=true; - break; - } - - i++; - } - - if(!found) + auto entry=filtered_jar.find("META-INF/MANIFEST.MF"); + if(entry==filtered_jar.end()) return manifestt(); - std::string dest=get_entry(i); + std::string dest=get_entry(entry->first); std::istringstream in(dest); manifestt manifest; diff --git a/src/java_bytecode/jar_file.h b/src/java_bytecode/jar_file.h index 53f673102bf..9407e711128 100644 --- a/src/java_bytecode/jar_file.h +++ b/src/java_bytecode/jar_file.h @@ -15,29 +15,26 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include -class jar_filet +class jar_filet:public messaget { public: jar_filet():mz_ok(false) { } - inline explicit jar_filet(const std::string &file_name) - { - open(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 - } + explicit operator bool() const { return mz_ok; } - typedef std::vector indext; - indext index; + // map internal index to real index in jar central directory + typedef std::map filtered_jart; + filtered_jart filtered_jar; - std::string get_entry(std::size_t i); + std::string get_entry(const irep_idt &); typedef std::map manifestt; manifestt get_manifest(); @@ -47,16 +44,24 @@ class jar_filet bool mz_ok; }; -class jar_poolt +class jar_poolt:public messaget { 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) { + if(java_cp_include_files.empty()) + throw "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.set_message_handler(get_message_handler()); + jar_file.open(java_cp_include_files, file_name); return jar_file; } else @@ -66,6 +71,7 @@ class jar_poolt protected: typedef std::map file_mapt; file_mapt file_map; + std::string java_cp_include_files; }; #endif // CPROVER_JAVA_BYTECODE_JAR_FILE_H diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 79295995662..0e2eb25d0ec 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -55,6 +56,36 @@ 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"); + // load file list from JSON file + if(java_cp_include_files[0]=='@') + { + jsont json_cp_config; + if(parse_json( + java_cp_include_files.substr(1), + get_message_handler(), + json_cp_config)) + throw "cannot read JSON input configuration for JAR loading"; + + if(!json_cp_config.is_object()) + throw "the JSON file has a wrong format"; + jsont include_files=json_cp_config["jar"]; + if(!include_files.is_array()) + throw "the JSON file has a wrong format"; + + // add jars from JSON config file to classpath + for(const jsont &file_entry : include_files.array) + { + assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar")); + config.java.classpath.push_back(file_entry.value); + } + } + } + else + java_cp_include_files=".*"; } /*******************************************************************\ @@ -129,6 +160,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")) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 643eacd5b7f..77689d6e12a 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/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(); diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index dc4330aa00c..c8e6bbf5bb4 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -98,7 +98,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( debug() << "Getting class `" << class_name << "' from JAR " << jf << eom; - std::string data=jar_pool(jf).get_entry(jm_it->second.index); + std::string data=jar_pool(jf).get_entry(jm_it->second.class_file_name); std::istringstream istream(data); @@ -129,7 +129,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( debug() << "Getting class `" << class_name << "' from JAR " << cp << eom; - std::string data=jar_pool(cp).get_entry(jm_it->second.index); + std::string data=jar_pool(cp).get_entry(jm_it->second.class_file_name); std::istringstream istream(data); @@ -223,11 +223,10 @@ void java_class_loadert::read_jar_file(const irep_idt &file) debug() << "adding JAR file `" << file << "'" << eom; auto &jm=jar_map[file]; - std::size_t number_of_files=jar_file.index.size(); - for(std::size_t i=0; i class_mapt; class_mapt class_map; @@ -42,7 +48,7 @@ class java_class_loadert:public messaget public: struct entryt { - std::size_t index; + std::string class_file_name; }; // class name to index map diff --git a/src/symex/Makefile b/src/symex/Makefile index f177e91bc07..e887ca55352 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -17,7 +17,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ ../path-symex/path-symex$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) + ../miniz/miniz$(OBJEXT) \ + ../json/json$(LIBEXT) INCLUDES= -I ..