From b236ee4738602140cab93b29b47ea122161b8991 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Sat, 4 Mar 2017 12:00:51 +0100 Subject: [PATCH 1/6] allow regex to limit class files loaded from JAR --- src/cbmc/cbmc_parse_options.cpp | 1 + src/cbmc/cbmc_parse_options.h | 1 + src/java_bytecode/jar_file.cpp | 23 ++++++++++++------ src/java_bytecode/jar_file.h | 25 +++++++++++++------- src/java_bytecode/java_bytecode_language.cpp | 5 ++++ src/java_bytecode/java_bytecode_language.h | 1 + src/java_bytecode/java_class_loader.h | 4 ++++ 7 files changed, 44 insertions(+), 16 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 7364752d093..e0e3b7db70e 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 of class files to load\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/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index d679f21c070..f7cb0726494 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -9,8 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - #include "jar_file.h" +#include /*******************************************************************\ @@ -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 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(); diff --git a/src/java_bytecode/jar_file.h b/src/java_bytecode/jar_file.h index 53f673102bf..7670cbf6a8b 100644 --- a/src/java_bytecode/jar_file.h +++ b/src/java_bytecode/jar_file.h @@ -15,27 +15,26 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include 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 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); @@ -45,18 +44,25 @@ class jar_filet protected: mz_zip_archive zip; bool mz_ok; + std::string matcher; + std::map 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 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..6a0327968b1 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/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")) 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.h b/src/java_bytecode/java_class_loader.h index b2a4953445a..8e8f5c5b82c 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/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 class_mapt; From ed34a739d8be7e8e1af67b5f0a935e8b388e243a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 7 Mar 2017 13:04:24 +0100 Subject: [PATCH 2/6] support class load configuration via JSON file e.g. ``` { "jar": [ "A.jar", "B.jar" ], "classFiles": [ "jarfile3$A.class", "jarfile3.class" ] } ``` --- src/cbmc/Makefile | 3 +- src/cbmc/cbmc_parse_options.cpp | 2 +- src/cegis/Makefile | 3 +- src/goto-cc/Makefile | 3 +- src/goto-diff/Makefile | 3 +- src/goto-instrument/Makefile | 3 +- src/java_bytecode/jar_file.cpp | 50 ++++++++++++++++++++++----- src/java_bytecode/jar_file.h | 6 ++-- src/java_bytecode/java_class_loader.h | 1 + src/symex/Makefile | 3 +- 10 files changed, 60 insertions(+), 17 deletions(-) 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 e0e3b7db70e..5ed5d28054e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1155,7 +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-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/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 f7cb0726494..0f45af67d33 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 "jar_file.h" #include - +#include /*******************************************************************\ Function: jar_filet::open @@ -24,7 +25,9 @@ Function: jar_filet::open \*******************************************************************/ -void jar_filet::open(std::string &java_cp_include_files, const std::string &filename) +void jar_filet::open( + std::string &java_cp_include_files, + const std::string &filename) { if(!mz_ok) { @@ -35,6 +38,32 @@ void jar_filet::open(std::string &java_cp_include_files, const std::string &file 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"; + assert(json_cp_config.is_object() && "JSON has wrong format"); + jsont include_files=json_cp_config["classFiles"]; + assert(include_files.is_array() && "JSON has 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); @@ -47,11 +76,16 @@ void jar_filet::open(std::string &java_cp_include_files, const std::string &file 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")) + + // non-class files are loaded in any case + bool add_file=!has_suffix(file_name, ".class"); + // load .class file only if they match regex + if(regex_match) + add_file|=std::regex_match(file_name, string_matcher, regex_matcher); + // load .class file only if it is in the match set + else + add_file|=set_matcher.count(file_name)>0; + if(add_file) { index.push_back(file_name); filtered_jar[filtered_index]=i; diff --git a/src/java_bytecode/jar_file.h b/src/java_bytecode/jar_file.h index 7670cbf6a8b..a1ff04bb933 100644 --- a/src/java_bytecode/jar_file.h +++ b/src/java_bytecode/jar_file.h @@ -16,8 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include -class jar_filet +class jar_filet:public messaget { public: jar_filet():mz_ok(false) { } @@ -48,7 +49,7 @@ class jar_filet std::map index_map; }; -class jar_poolt +class jar_poolt:public messaget { public: void set_java_cp_include_files(std::string &_java_cp_include_files) @@ -62,6 +63,7 @@ class jar_poolt if(it==file_map.end()) { jar_filet &jar_file=file_map[file_name]; + jar_file.set_message_handler(get_message_handler()); jar_file.open(java_cp_include_files, file_name); return jar_file; } diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index 8e8f5c5b82c..e76d5894860 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -23,6 +23,7 @@ class java_class_loadert:public messaget void set_java_cp_include_files(std::string &java_cp_include_files) { jar_pool.set_java_cp_include_files(java_cp_include_files); + jar_pool.set_message_handler(get_message_handler()); } // maps class names to the parse trees 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 .. From 469897f051b799212c5ca18eb3e60f09b80fa541 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 7 Mar 2017 13:32:27 +0100 Subject: [PATCH 3/6] add jars from JSON config to classpath --- src/java_bytecode/java_bytecode_language.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 6a0327968b1..923a7efcf8d 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 @@ -59,6 +60,25 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) java_cp_include_files=cmd.get_value("java-cp-include-files"); else 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"; + assert(json_cp_config.is_object() && "JSON has wrong format"); + jsont include_files=json_cp_config["jar"]; + assert(include_files.is_array() && "JSON has 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); + } + } } /*******************************************************************\ From 3d009a9e8a459421bf916a6d5491a537b2e08e9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 7 Mar 2017 14:51:08 +0100 Subject: [PATCH 4/6] add regression test --- regression/cbmc-java/jar-file4/A.jar | Bin 0 -> 721 bytes regression/cbmc-java/jar-file4/B.jar | Bin 0 -> 721 bytes regression/cbmc-java/jar-file4/C.jar | Bin 0 -> 934 bytes regression/cbmc-java/jar-file4/jar.json | 12 ++++++++++++ regression/cbmc-java/jar-file4/test.desc | 10 ++++++++++ 5 files changed, 22 insertions(+) create mode 100644 regression/cbmc-java/jar-file4/A.jar create mode 100644 regression/cbmc-java/jar-file4/B.jar create mode 100644 regression/cbmc-java/jar-file4/C.jar create mode 100644 regression/cbmc-java/jar-file4/jar.json create mode 100644 regression/cbmc-java/jar-file4/test.desc diff --git a/regression/cbmc-java/jar-file4/A.jar b/regression/cbmc-java/jar-file4/A.jar new file mode 100644 index 0000000000000000000000000000000000000000..e721e6f32f945341ca9aafca44a794bb16cfeb02 GIT binary patch literal 721 zcmWIWW@Zs#;Nak3$Pf4PVn70%3@i-3t|5-Po_=on|4uP5Ff#;rvvYt{FhP|C;M6Pv zQ~}rQ>*(j{<{BKL=j-;__snS@Z(Y5MyxzK6=gyqp9At3C_`%a6JuhD!Pv48Bt5`TA zUPvC1mXg%U_#v*U_I!z!#dC4dC*rEp7_Mf2D*9N&2zG^l;4&o_pdGG2jBrIdnim9s zvRR2mX_+~x#ww0_$vKI|#jgIo-iI9oYA>t!?p9O#8lCUNZ`vBR!Q6F1Q-DTQz@Ge9 ztE3-^O$zxFE!Xwnp!|b=p>*bhhozrA-fM1bzd!yygPO&wL#{dx7N&33mAAJ0#`)#k z48dDhyY+rAXE8jV@^MLVY1z5E+_@#Co*eA|-%e(4vW~UWax%H@c6Uu&aOj=WCeQnJ zM6c^=-F0mnhxA#E$@xYO>~|TM*coqqsFg9=oA_n@4?Z^oV>i*uG1Hc6ac>E6$vE ze0%0HG0}sPH<+z@1&;seJ8r*CB8U6P#@HjG)}OZV_A!P#r$zWp;kmxxiSXJZv4?-I z=u~tM?3bNZH7EDlG{JALIO}_I-!%OL2i}6vmH++&gC>v>6nKnGA`GZ002aNV6o3lg zQ3^^A=vtBE1Qh=WU<+izwIZbkWD`JfhwLy=+#$eWAQL?%1H4(;Kq{Dla5snnb~gZw CHqIXa literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/jar-file4/B.jar b/regression/cbmc-java/jar-file4/B.jar new file mode 100644 index 0000000000000000000000000000000000000000..d381e413e74f2aa5d1f92381ec7fe608679b7e81 GIT binary patch literal 721 zcmWIWW@Zs#;Nak3C=U1YVn70%3@i-3t|5-Po_=on|4uP5Ff#;rvvYt{FhP|C;M6Pv zQ~}rQ>*(j{<{BKL=j-;__snS@Z(Y5MyxzK6=gyqp9At3C_`%a6JuhD!Pv48Bt5`TA zUPvC1mXg%U_#v*U_I!z!#dC4dC*rEp7_Mf2D*9N&2zG^l;4&o_pdGG2jBrIdnim9s zvRR2mX_+~x#wt#F$vKI|#jgIo-iI9oYA-Lln|61`kH3Y&RVy^NG~E;77i)34*!-wA zIQ*_aut(6x{7Q``_WA~UuQ|Ld{P{Ebzu!Ca=TBWNv&G?s{QMJL*roMui`)>qp?twQ z+3Q7^{^b@9qQIepCtu>P_P*wY%PRA_JeQrmG^OPP=kb~6 z<{#hgne|L`p=|;C7b(TQA9MNs-$>e^E8v)Or~%rTH#=kQTIYU6gN z-;34QWKwO#biP_fuh(^cb4~c4MDz{Dzl@+Lv^lv+>OU}O0vSPp$H*kYfSLke(F;le zr~n?Np!9&Q6**2o@s9wuKqg!(Qffdp0Tg%04g*(j{<{BKL=j-;__snS@Z(Y5MyxzK6=gyqp9At3C_`%a6JuhD!Pv48Bt5`TA zUPvC1mXg%U_#v*U_I!z!#dC4dC*rEp7_Mf2D*9N&2zG^l;4&o_pdGG2jBv&AXjCuo z0cEoii_$W4QjPVJa}tY-eS>2Cg&jp~H{UJWEkD(1={5c%UKd##XPubMqPxOV*iOzs z?ZdWQ_RU-K&c3uq&??>SSR&rJv ziT4i4va`JsduL@3xcy<$LA6U8HoRESQ90Yd{JYGZ_WVRohaAp|w;GeOss)a0?BU$X zqQ$#6(9@#lQF@|G3EQUQXC^u%D)$^p308QnzgNg$d%LZs!B%0nqWmx0l&^aGs(qi~ zxqq$Y(q@$x`)=~yTdKKhiDTmn2TX z?49N|O)EjJ&w%(^$lVXOM%fRp!H`EL8T6;>I$ulW4QyGAB(U1oJpk-#p=bDQs+ zEfkIUd^%kq-b66;T&u{H$5L6(uk`Df?zEFUY@uSi-MVdM^PhX+B7OmpmaVCEP1bH7 zKk$58|Nq4+%{ix6h#3Y=)cQ1M{efd5bEiJM{7`N2YZqII`Y-o)BtCqm^Z(3R?&Ggl z>Lyej`^)#fWzzh_XZsc!SXvaX=RbA$!#pmvXP3U@W;IH&MHjAIYpl2Rs68lU{uE0H zyurx8a1@w41H2iTL>N#LHZ0YG5;iJ;r&LffN7ss+)IiA^0c?RxxK^Y@j%)%bNg_K8 clq3=0Fp!CwKm)v4*+BBlK)4e~UkAGy09`dfUjP6A literal 0 HcmV?d00001 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 From b473638813d33a3439f45f6768f092bd29ac3bec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 10 Mar 2017 11:18:52 +0100 Subject: [PATCH 5/6] take comments into account --- src/java_bytecode/jar_file.cpp | 14 ++++--- src/java_bytecode/jar_file.h | 9 ++-- src/java_bytecode/java_bytecode_language.cpp | 43 ++++++++++++-------- src/java_bytecode/java_class_loader.h | 1 + 4 files changed, 38 insertions(+), 29 deletions(-) diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index 0f45af67d33..0980e1466ea 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -8,11 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include -#include "jar_file.h" + +#include #include -#include +#include "jar_file.h" /*******************************************************************\ Function: jar_filet::open @@ -54,9 +54,11 @@ void jar_filet::open( get_message_handler(), json_cp_config)) throw "cannot read JSON input configuration for JAR loading"; - assert(json_cp_config.is_object() && "JSON has wrong format"); + if(!json_cp_config.is_object()) + throw "the JSON file has a wrong format"; jsont include_files=json_cp_config["classFiles"]; - assert(include_files.is_array() && "JSON has wrong format"); + 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()); @@ -84,7 +86,7 @@ void jar_filet::open( add_file|=std::regex_match(file_name, string_matcher, regex_matcher); // load .class file only if it is in the match set else - add_file|=set_matcher.count(file_name)>0; + add_file|=set_matcher.find(file_name)!=set_matcher.end(); if(add_file) { index.push_back(file_name); diff --git a/src/java_bytecode/jar_file.h b/src/java_bytecode/jar_file.h index a1ff04bb933..c168b8b4199 100644 --- a/src/java_bytecode/jar_file.h +++ b/src/java_bytecode/jar_file.h @@ -22,14 +22,13 @@ class jar_filet:public messaget { public: jar_filet():mz_ok(false) { } - inline explicit jar_filet(const std::string &file_name) { } ~jar_filet(); 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 mz_ok; } + explicit operator bool() const { return mz_ok; } typedef std::vector indext; indext index; @@ -45,8 +44,6 @@ class jar_filet:public messaget protected: mz_zip_archive zip; bool mz_ok; - std::string matcher; - std::map index_map; }; class jar_poolt:public messaget @@ -56,9 +53,11 @@ class jar_poolt:public messaget { 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"); + 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()) { diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 923a7efcf8d..0e2eb25d0ec 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -56,29 +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"); - else - 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"; - assert(json_cp_config.is_object() && "JSON has wrong format"); - jsont include_files=json_cp_config["jar"]; - assert(include_files.is_array() && "JSON has wrong format"); - // add jars from JSON config file to classpath - for(const jsont &file_entry : include_files.array) + java_cp_include_files=cmd.get_value("java-cp-include-files"); + // load file list from JSON file + if(java_cp_include_files[0]=='@') { - assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar")); - config.java.classpath.push_back(file_entry.value); + 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=".*"; } /*******************************************************************\ diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index e76d5894860..dfd57ac9ac7 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -20,6 +20,7 @@ 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); From 53fad70f4408487780748985a02d5df32b96a39d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Fri, 10 Mar 2017 14:10:38 +0100 Subject: [PATCH 6/6] change from vector indices to map --- src/java_bytecode/jar_file.cpp | 36 +++++++++---------------- src/java_bytecode/jar_file.h | 6 ++--- src/java_bytecode/java_class_loader.cpp | 11 ++++---- src/java_bytecode/java_class_loader.h | 2 +- 4 files changed, 20 insertions(+), 35 deletions(-) diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index 0980e1466ea..07d7719e500 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -69,7 +69,6 @@ void jar_filet::open( std::size_t number_of_files= mz_zip_reader_get_num_files(&zip); - size_t filtered_index=0; 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, real_index, &file_stat); @@ -173,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 c168b8b4199..9407e711128 100644 --- a/src/java_bytecode/jar_file.h +++ b/src/java_bytecode/jar_file.h @@ -30,13 +30,11 @@ class jar_filet:public messaget // Test for error; 'true' means we are good. 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; + 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(); 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