From 80ea46ab0eb2086a12656e835535d11ba54c0d9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 23 Aug 2017 17:22:50 +0200 Subject: [PATCH 1/9] Add war file regression test --- regression/cbmc-java/war-file1/sample.war | Bin 0 -> 4606 bytes regression/cbmc-java/war-file1/test.desc | 8 ++++++++ regression/cbmc-java/war-file1/url.txt | 1 + 3 files changed, 9 insertions(+) create mode 100644 regression/cbmc-java/war-file1/sample.war create mode 100644 regression/cbmc-java/war-file1/test.desc create mode 100644 regression/cbmc-java/war-file1/url.txt diff --git a/regression/cbmc-java/war-file1/sample.war b/regression/cbmc-java/war-file1/sample.war new file mode 100644 index 0000000000000000000000000000000000000000..0a127e6bd1f6991c32f591e577b42a50210c60f7 GIT binary patch literal 4606 zcmaKv2{@Ep8^@nnjKR!Awi4pCGj_>ZgOFupmy9ftrIBSOCQFRTPO_vdq3lVrB(i7A zzEqTK*(+X@-lXIky{~wEeczeud7g94b^q`CKj+MI&iNVYL7?=&R?~|7A^)@U&y5a% z0$5E`HE|sSEy*7p0ATn}C>+qFhEA@7>&{X`U8xrf_4*ZxRWs1h(ljxZz-oQMc6I9O ziA(e&^~6Pcx_ZlurC!KR%y@Na?Ds^U)bBZI21J4cx>xltSEWT6GwT_f5O0gBy~ln= zOd`982?%{wxnR9dEdH_yQ6HnkqV$XjQLHMT;y=q>t|C?a@&f<{lz&@?Q~g+Is{eGp z?HT}1?TKRC6?G18M<6&7B>#6b$8VzDE_>LWyI|+!xJ$R!3u2cJ?_&RdB5A3SE^gFp zJ2v1yO%LCT6XAsbz%v>E5ZIM&+w_i&la6@2yTs4$V@%%|GpjMGLdXc-NZ1PM0SUxX zI%!=R@rO@DxVp{_vt#&pY0FWE!O;lyul#}2QEbQ7KvxnSdly6#+2w91-Bx_AI!bsV zYf~Ta18lp$@E~U!RJ)E{{(B^MGBe=QBM$d#Pwl=qG%A6*gG^ntwXGW8iou0Ah zQl^fzA=>a91eY#ZqVm~J6M@j4{*pXI!9h!AM1W(lfcbEDBz$Nz@|6Aqbm4=|7f97w zgJ+4ZB&MdfUIa0Z!s3x957|SOI>8ziSP6K`vP1dzfqdb@!PDcTcQF-z81qyG-2ljZmQSQ^@>w**Ekh%-L9eeReHIFMsbcj z0*gwn>b?h0)c)au&MrCmA_X62CcWemA)|G@2GuhOHIP{qE-4_$Z^$K;l7eQ?9i)7# zJMG3CVwNgTOL?zaWsOa9&4}0}4vw6kV7Q5^pWnQviE`(SkZgGZ*#%3 z;Uu#HiyXk%-wS-XN(taDOad{?8lup+7PP`0aaXcXO$Kj&0zN=-`^&tXd zew-3N#!aO;qpzmKi3^-@4G`n8=Se^L#>eWCAGSZ}Wp~<_7n(9Ih&HXZA2PukftfmF zO!0R%)kAIbFZ(i3QmVmM^PC+M938490>IyFD^4+cANu$QjIOK%66z6(ri7GDYc}G; z@sX8_E4Vh4lCo4Cg{7(E#DfofPlUW&C?mG9jnR!~DV7vk1h?F)$6<;N%MTkz(nqgQ zv=OKSD!P?cUu8K3YG`~x{b3@AOw1!CQvws8upRizd`?;`*GQXnmo2L7w4i_VWxOq@ zw=hDb_5jHD|3gf@6J1s^?%xg(o+Ae&n$e*&}czY1hPsh69?? zIQb*j0%^Bjb@!Ge$I)JbxCLQfCeby0vGuAXmQd z+IzjCti5Q-Vl8mXyeDdYTk6A{|Er~aYn@FSrfjDpO%KvPedd<E`FP6H z!^hm6NL+R4rK~etIqW}w>0xr#pVG+9#S;r zhV#c^frsvoMjC@J;OjK#y?O> zSP^Z(ySns&R^V}PoSJM(zjG<)cNb29rp5alD$RmtbkayTuktJB zc+8CV>At5mFN@1l884cmw~)p~b?92YQ;9m-kMJs_?^9-;!)gx}%>MZ@n@@iO*x zp=U$b`br69;h;m*Py+Y)@O2b}6MJ`=v*@Ww8WdO3XY~z-jj{TF4@3Sp*v(w(UT}wc zF;R!%pG|}4?sm?ODBj*};bm^wc*;E)8UJQuA$YZt{MGQab>E-nwn&0HB-8?K*|E3N~fe zeoPS1TF&YD1i||X7C<8+DRcmgj*f;Q zB{h|Xh7RVc3XXSAU8NSM3|g9I}(L^ znfT!wkR%mr86LiU5sa~>C1Q-3li&+rFb_{9Jz0%MW|P!NKMR8d@qWl$q{m<5$f$e%h8X<{R0b>xmZX z@!3+nc6N_3lU2NWSWZ{YS;kmUFdv=j2cSq-cnP6={lbNlM?hApm+uKzd*^bL=Gg1_ z65&pw0BSDy65PAyznD+1!Y#5IWup9exA5$>^{WPD=5Qg84Nk8uODsm zDW8jDmPLrmL4N;7!dKW@7@Xm@Cy(4;PNQtrn~1|)yf`+{NZ5EVL|8V?_l-XD^@H`v zrnacF{Ur^-oRiv=z&9n$?e<32NgVdV>*76aWXBs6 zrY_uwi^u@CR(_oYh~|pOBOuFWV@xR*A%a0f-wAAtK45|gGvj_@d;Q@e*}+F=)P&{a z5}60e0O``9q`8}46^KG1Fs7Q&#QrotUA!VRg_raN#0{#1=iLqW%E#QkRC+zgh1;4P z87-++(3NphN@OsIIXW{W%3bCIdNWLe_zveFsUy}7{`9$mA9hpg>%!ySr|*DpP7#;; z#134LcCMKh{h!syTWzC;WJF^MQ=L(tVLroCMS&XNXkTVAr<$E9vma~x9mwYJuzLaM zxU!V*tpAN7CY#7*v!)((_L63F`Qz>e_Cuax}PK&YObfpwF+(dGtTX~b~{G;uoUMokBxNaUQdTEX9_o@FQ zX2uY7bq+0g&93<|2{Ki})3GU*X=`lB4bo>;tbsUjww`tVvaDfJoXCO`_6a$*K6r%a z=FaN3QJuPvRi*VZtXQZ|cmBnR`#>9V%&!Tg@m)-!!n^kFQP|Ufbe3sFi*`}}NXe5; zf3=UbK)RLSZzzKkv(P#^m?Y^NEd!qyLx+yYJUWemf4TFUR834qqmVNWV9X=4ihsDm z=*NtFmPeVba<>w)wKisa8heO86h6;9oNU}zS7r1kw2Kn*>Z0ATq!T?Vwh=rG>zZ%| z`HOTN8syS=bp@96PV!o^sf9dyv|z)Z2fR8DO-8O390-1>kGmI)U?j@(f+y??CT^un zs2yG}xoU~eLZ)P9mg*W9^@p8@V>)3IbXfiwTAgsSu$r|N!LH@V9#IW0?qyb7e?*KM zln)s*TWxV)GIkn1_1ch>pw9785CP@i|KvK4@<0SEGMazmEK?AbP?Z0@sEc?JNNBS~eeQ5dW%aPau`~mCQvu12q_DyndldpU0YhIS#c~19<+bx%9RJzKt2BDJ$ zqOyhuXKoC8_=KK!eqFL)kfiQ^Ek4(%C^SdoHS1%|(m0|ZcMOE&;zJX29%BRJe(9iW zn33tIHS>IILn!qwi}H|rlFB?gI(UZ3&Kxpt*$~t#Gn+~q)rJB?6d$kg2--S4ut;Zj zVN%+Uhjbo14U_E`D66!1#4KN*16F*}C&#~J>Flbr_}#Zf&qJ<&3HxqQ+k@21r<87V zQAI`k#oNF9e#lsu=gJdGlz0l|51%t&zB_Wz03C)*yG$O`56XBYp+p;hOt*_e)o<{< zf%I)H#WlZ|X9n05BI9AA5c7xQtnx`U8_NWv`UM-4Kr@&3iy5!({w1s(_Lg2O!KK)kJooBE2 zE$ZFLqrEH7-weFtf3I?jf_IdjROK%w-WL6yinnFi Date: Wed, 23 Aug 2017 17:23:24 +0200 Subject: [PATCH 2/9] Change to goto-cc/compile.cpp --- src/goto-cc/compile.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 0a6e3c4dd58..a08c622276c 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -632,7 +632,8 @@ bool compilet::parse_source(const std::string &file_name) return true; if((has_suffix(file_name, ".class") || - has_suffix(file_name, ".jar")) && + has_suffix(file_name, ".jar") || + has_suffix(file_name, ".war")) && final()) return true; From 5857165e7fc823f155cbfd4ab37a5d536e64498f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 23 Aug 2017 17:41:15 +0200 Subject: [PATCH 3/9] Remove WAR class prefix --- src/java_bytecode/jar_file.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index bc065d7a0e9..f6b07884072 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -53,6 +53,11 @@ void jar_filet::open( #endif INVARIANT(file_name.size()==filename_len-1, "no \\0 found in file name"); + // remove WAR class prefix + const std::string war_class_prefix("WEB-INF/classes/"); + if(has_prefix(file_name, war_class_prefix)) + file_name=file_name.substr(war_class_prefix.length()); + // non-class files are loaded in any case bool add_file=!has_suffix(file_name, ".class"); // load .class file only if they match regex / are in match set From 3784c17a61df3c5ab8446e1c609ac1f7ff3b3e44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 23 Aug 2017 17:42:50 +0200 Subject: [PATCH 4/9] Add .war suffix to language options --- src/java_bytecode/java_bytecode_language.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index bac7157df5c..bb46ab79120 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -98,7 +98,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) std::set java_bytecode_languaget::extensions() const { - return { "class", "jar" }; + return { "class", "jar", "war" }; } void java_bytecode_languaget::modules_provided(std::set &modules) @@ -130,7 +130,7 @@ bool java_bytecode_languaget::parse( // override main_class main_class=java_class_loadert::file_to_class_name(path); } - else if(has_suffix(path, ".jar")) + else if(has_suffix(path, ".jar") || has_suffix(path, ".war")) { // build an object to potentially limit which classes are loaded java_class_loader_limitt class_loader_limit( From dab7c10a9dd84d716ff1e14372e0aea313f3a698 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 23 Aug 2017 17:45:47 +0200 Subject: [PATCH 5/9] Add .war suffix to class_loader --- src/java_bytecode/java_class_loader.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index 675e137227c..c154b51b009 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -109,7 +109,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( for(const auto &cp : config.java.classpath) { // in a JAR? - if(has_suffix(cp, ".jar")) + if(has_suffix(cp, ".jar") || has_suffix(cp, ".war")) { read_jar_file(class_loader_limit, cp); @@ -119,7 +119,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree( if(jm_it!=jm.entries.end()) { - debug() << "Getting class `" << class_name << "' from JAR " + debug() << "Getting class `" << class_name << "' from {J,W}AR " << cp << eom; std::string data=jar_pool(class_loader_limit, cp) From c62e6822c9e6bad809ac41c14a5d4b39bcef0704 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 23 Aug 2017 17:54:28 +0200 Subject: [PATCH 6/9] Add wiki link as documentation for WAR format --- src/java_bytecode/jar_file.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index f6b07884072..45a095a0e98 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -54,6 +54,7 @@ void jar_filet::open( INVARIANT(file_name.size()==filename_len-1, "no \\0 found in file name"); // remove WAR class prefix + // cf. https://en.wikipedia.org/wiki/WAR_(file_format) const std::string war_class_prefix("WEB-INF/classes/"); if(has_prefix(file_name, war_class_prefix)) file_name=file_name.substr(war_class_prefix.length()); From 7489e8867ef8d82ed45d094093028cd744378206 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 24 Aug 2017 09:44:49 +0200 Subject: [PATCH 7/9] Support empty jar/war JSON array --- src/java_bytecode/jar_file.cpp | 1 + src/java_bytecode/java_bytecode_language.cpp | 36 +++++++++++++++----- 2 files changed, 28 insertions(+), 9 deletions(-) diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp index 45a095a0e98..ab04aa46d14 100644 --- a/src/java_bytecode/jar_file.cpp +++ b/src/java_bytecode/jar_file.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include void jar_filet::open( diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index bb46ab79120..469423f88be 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -74,19 +74,37 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) java_cp_include_files.substr(1), get_message_handler(), json_cp_config)) - throw "cannot read JSON input configuration for JAR loading"; + throw "cannot read JSON input configuration for JAR/WAR 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) + jsont include_jar_files=json_cp_config["jar"]; + if(!include_jar_files.is_null()) + { + if(!include_jar_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_jar_files.array) + { + assert(file_entry.is_string() && + has_suffix(file_entry.value, ".jar")); + config.java.classpath.push_back(file_entry.value); + } + } + jsont include_war_files=json_cp_config["war"]; + if(!include_war_files.is_null()) { - assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar")); - config.java.classpath.push_back(file_entry.value); + if(!include_war_files.is_array()) + throw "the JSON file has a wrong format"; + + // add wars from JSON config file to classpath + for(const jsont &file_entry : include_war_files.array) + { + assert(file_entry.is_string() && + has_suffix(file_entry.value, ".war")); + config.java.classpath.push_back(file_entry.value); + } } } } From 40b647fd92a697c442aa0bbd5c1e1324235dcaf4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 24 Aug 2017 12:44:27 +0200 Subject: [PATCH 8/9] Restructure java_bytecode_language --- src/java_bytecode/java_bytecode_language.cpp | 82 ++++++++++---------- src/java_bytecode/java_bytecode_language.h | 1 + 2 files changed, 44 insertions(+), 39 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 469423f88be..bb7bb1f170a 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -68,45 +68,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) 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/WAR loading"; - - if(!json_cp_config.is_object()) - throw "the JSON file has a wrong format"; - jsont include_jar_files=json_cp_config["jar"]; - if(!include_jar_files.is_null()) - { - if(!include_jar_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_jar_files.array) - { - assert(file_entry.is_string() && - has_suffix(file_entry.value, ".jar")); - config.java.classpath.push_back(file_entry.value); - } - } - jsont include_war_files=json_cp_config["war"]; - if(!include_war_files.is_null()) - { - if(!include_war_files.is_array()) - throw "the JSON file has a wrong format"; - - // add wars from JSON config file to classpath - for(const jsont &file_entry : include_war_files.array) - { - assert(file_entry.is_string() && - has_suffix(file_entry.value, ".war")); - config.java.classpath.push_back(file_entry.value); - } - } - } + load_from_archive_files(java_cp_include_files.substr(1)); } else java_cp_include_files=".*"; @@ -480,3 +442,45 @@ bool java_bytecode_languaget::to_expr( java_bytecode_languaget::~java_bytecode_languaget() { } + +void java_bytecode_languaget::load_from_archive_files( + const std::string &json_config) +{ + jsont json_cp_config; + if(parse_json( + json_config, + get_message_handler(), + json_cp_config)) + throw "cannot read JSON input configuration for JAR/WAR loading"; + + if(!json_cp_config.is_object()) + throw "the JSON file has a wrong format"; + jsont include_jar_files=json_cp_config["jar"]; + if(!include_jar_files.is_null()) + { + if(!include_jar_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_jar_files.array) + { + assert(file_entry.is_string() && + has_suffix(file_entry.value, ".jar")); + config.java.classpath.push_back(file_entry.value); + } + } + jsont include_war_files=json_cp_config["war"]; + if(!include_war_files.is_null()) + { + if(!include_war_files.is_array()) + throw "the JSON file has a wrong format"; + + // add wars from JSON config file to classpath + for(const jsont &file_entry : include_war_files.array) + { + assert(file_entry.is_string() && + has_suffix(file_entry.value, ".war")); + config.java.classpath.push_back(file_entry.value); + } + } +} diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index a688440e64d..afa94f03792 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -139,6 +139,7 @@ class java_bytecode_languaget:public languaget protected: bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &); const select_pointer_typet &get_pointer_type_selector() const; + void load_from_archive_files(const std::string &); irep_idt main_class; std::vector main_jar_classes; From 4f42f7f049c6d5478918df5f39a084135f6a882c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Thu, 24 Aug 2017 15:01:55 +0200 Subject: [PATCH 9/9] Update WAR file regression test --- regression/cbmc-java/war-file1/test.desc | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-java/war-file1/test.desc b/regression/cbmc-java/war-file1/test.desc index f169cc69c08..3f64bfbb2bd 100644 --- a/regression/cbmc-java/war-file1/test.desc +++ b/regression/cbmc-java/war-file1/test.desc @@ -1,8 +1,9 @@ CORE sample.war ---function mypackage.Hello.doGet +--function mypackage.Hello.doGet --cover location ^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL +\*\* 25 of 26 covered -- -^warning: ignoring +-- +war file source https://tomcat.apache.org/tomcat-6.0-doc/appdev/sample/