From 55d36b5e567b34a8728245e20a4995842d091f69 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 26 Mar 2018 16:21:25 +0100 Subject: [PATCH 1/2] Fix code for String.equals This should check that the object is an instance of String before doing any string operation. --- .../java_string_library_preprocess.cpp | 71 ++++++++++--------- 1 file changed, 37 insertions(+), 34 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 207740f3063..30202dc5192 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -930,53 +930,56 @@ java_string_library_preprocesst::string_literal_to_string_expr( /// \param symbol_table: symbol table /// \return Code corresponding to: /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -/// string_expr1 = {this->length; *this->data} -/// string_expr2 = {arg->length; *arg->data} -/// return cprover_string_equal(string_expr1, string_expr2) +/// IF arg->@class_identifier == "java.lang.String" +/// THEN +/// string_expr1 = {this->length; *this->data} +/// string_expr2 = {arg->length; *arg->data} +/// bool string_equals_tmp = cprover_string_equal(string_expr1, string_expr2) +/// return string_equals_tmp +/// ELSE +/// return false /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_equals_function_code( const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) { - code_blockt code; + const typet &return_type = type.return_type(); exprt::operandst ops; for(const auto &p : type.parameters()) { symbol_exprt sym(p.get_identifier(), p.type()); ops.push_back(sym); } - exprt::operandst args=process_equals_function_operands( - ops, loc, symbol_table, code); - - member_exprt class_identifier( - checked_dereference(ops[1], ops[1].type().subtype()), - "@class_identifier", - string_typet()); - - // Check the object argument is a String. - equal_exprt arg_is_string( - class_identifier, constant_exprt("java::java.lang.String", string_typet())); - // Check content equality - const symbolt string_equals_sym = get_fresh_aux_symbol( - java_boolean_type(), "string_equals", "str_eq", loc, ID_java, symbol_table); - const symbol_exprt string_equals = string_equals_sym.symbol_expr(); - code.add(code_declt(string_equals), loc); - code.add( - code_assignt( - string_equals, - make_function_application( - ID_cprover_string_equal_func, args, type.return_type(), symbol_table)), - loc); - - code.add( - code_returnt( - if_exprt( - arg_is_string, - string_equals, - from_integer(false, java_boolean_type()))), - loc); + code_ifthenelset code; + code.cond() = [&] { + const member_exprt class_identifier( + checked_dereference(ops[1], ops[1].type().subtype()), + "@class_identifier", + string_typet()); + return equal_exprt( + class_identifier, + constant_exprt("java::java.lang.String", string_typet())); + }(); + + code.then_case() = [&] { + code_blockt instance_case; + // Check content equality + const symbolt string_equals_sym = get_fresh_aux_symbol( + return_type, "string_equals", "str_eq", loc, ID_java, symbol_table); + const symbol_exprt string_equals = string_equals_sym.symbol_expr(); + instance_case.add(code_declt(string_equals), loc); + const exprt::operandst args = + process_equals_function_operands(ops, loc, symbol_table, instance_case); + const auto fun_app = make_function_application( + ID_cprover_string_equal_func, args, return_type, symbol_table); + instance_case.add(code_assignt(string_equals, fun_app), loc); + instance_case.add(code_returnt(string_equals), loc); + return instance_case; + }(); + + code.else_case() = code_returnt(from_integer(false, return_type)); return code; } From a997ffb0f15c02b28ea274438f447e3b3d3d6a97 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 27 Mar 2018 08:54:14 +0100 Subject: [PATCH 2/2] Add verification test for String.equals We add tests which compare the internal String.equals with a reference implementation which loops over the characters of the string. --- .../jbmc-strings/StringEquals/Test.class | Bin 871 -> 1443 bytes .../jbmc-strings/StringEquals/Test.java | 48 ++++++++++++++++++ .../jbmc-strings/StringEquals/test.desc | 12 ++--- .../StringEquals/test_verify.desc | 11 ++++ .../StringEquals/test_verify_non_null.desc | 6 +++ 5 files changed, 71 insertions(+), 6 deletions(-) create mode 100644 regression/jbmc-strings/StringEquals/test_verify.desc create mode 100644 regression/jbmc-strings/StringEquals/test_verify_non_null.desc diff --git a/regression/jbmc-strings/StringEquals/Test.class b/regression/jbmc-strings/StringEquals/Test.class index a03b132327c926fb10971dc8e7f81e89ef3bd6c6..44b8c52d35c29c2066a3a4ab259208de0ad4009f 100644 GIT binary patch literal 1443 zcma)6%Wl&^6g`u~apJl(Nui`kQ(B&Rv<;8)Y$#L#L=Y{AA`nOjxz02-xOQYzw0s+ZBYdLq=MGjLkAKVxLuz!-zugsEjcMdF+(2i=lU`R;_Z!HEgST%&2N} zCNDFv%M8JSVHxfugFl_Qzz`_fWzNuZ+OYUcZE=n}=S47sq%Uy&IzwN&bo!chQ_Gv0 zRmsn~j$u_M#LezmSJSUgYfIh*;zMK^HadKsJKWNFX>rNqi`;TG!Gd8&`rkZjPR`6- zW&GPDq`qm=sL+w z(;m8LJ0`Uq?eH&IF0XJ$gzZ)lK~%*aj5EYLAyX~kjysO+Fhn{~qk9#5u}{W+6$fxo zMG^xfqhKK8kctTu{<_oXiz3n`p<0mNsA*=EVZ&NE)-)e9xm9r&y!n(E`faC@*Owfd zG{_gvdTWCQ<Y0NLR(hRH}h zWI+~*3vuXI5KKr)-}SUh(aLC*va4XPL?AXagMa|}u@4&?p)5|m4G^{*^G&~l|B|$d zz)Yf!#4@Bhp2U13D+t!{;2q>ks|bBa1fDgqyD?vmut&Jn#-tWDAM=fR*p)UGY+sM$m;Kotz}O zu3{a^6nC4@J0#gdlIt-E_KF0HQ>F-lKgF}{myt*&lZgc7Aj>pV!u_U7h1@5E>yZ2} za~~0&&aOZqeUzu-#6Ou5`{#&fQ*Y2UB0e5)&(B``{uX%I=9?vMpb5xSIgA7`OQN4@ zB{7I?*o55}qJNh`9KsflTNG0G2ckso2N>)74vDU%+T`X*1~I~1_A}(%7r`YfCUZEO zdjoaS6E-rCdfJh0pu;6W)&bI_TEf>CnEPTKA9YKP$uv7Z=Z^n8g@OOSKTn#2EJ zDdv$pK=lsNObXQJ5wC&_%D;*7hv=x~;Bn8tKs469f^~Jsffoq)Uqk9lU07bYSxirY OPdzF;KSUcJhW`Ko-x#m} delta 386 zcmY+9&n^Q|7{$+>nf7*WM@>tsW>o#D8LHBRCUzpRsg(qKDVjzjT`(kK!7Iol7A!0* ztQ(1ig^gWb!2@^-;>_5vxw-c{=XbtyAJd=7)xr1c8-NCu6w+`~a3v-bbd*e(m{cfZ zN@7|;!jYI!m_7M@aPQ7!qYPt4x6H4XW(0~FeKqwn8!kRAxbO8Zu>Nls9IP= zO~CH9&Rg~4R-6Pdj|j3i&K& zNxtY|*&Ie>{WhT5h<5|oocRKE2WdRP(4Ud;`cyUi?H8pbpjqpJP%)Ore*lbX BFdF~> diff --git a/regression/jbmc-strings/StringEquals/Test.java b/regression/jbmc-strings/StringEquals/Test.java index 51e9dfc96e5..2de8e735d42 100644 --- a/regression/jbmc-strings/StringEquals/Test.java +++ b/regression/jbmc-strings/StringEquals/Test.java @@ -1,3 +1,6 @@ +// Uses CProverString, must be compiled with ../cprover/CProverString.java +import org.cprover.*; + public class Test { public static void check(int i, String s) { String t = "Hello World"; @@ -15,4 +18,49 @@ else if (i==4) else if (i==5) assert(s.equals(x)); } + + public static boolean referenceImplementation(String s, Object o) { + if (! (o instanceof String)) + return false; + + String s2 = (String) o; + if (s.length() != s2.length()) + return false; + + for (int i = 0; i < s.length(); i++) { + if (CProverString.charAt(s, i) != CProverString.charAt(s2, i)) + return false; + } + + return true; + } + + public static boolean verifyNonNull(String s, Object o) { + // Filter + if (s == null || o == null) + return false; + + // Act + boolean result = s.equals(o); + boolean referenceResult = referenceImplementation(s, o); + + // Assert + assert result == referenceResult; + + // Return + return result; + } + + public static boolean verify(String s, Object o) { + // Act + boolean result = s.equals(o); + boolean referenceResult = referenceImplementation(s, o); + + // Assert + assert result == referenceResult; + + // Return + return result; + } + } diff --git a/regression/jbmc-strings/StringEquals/test.desc b/regression/jbmc-strings/StringEquals/test.desc index 3e35d340082..1f90caa955f 100644 --- a/regression/jbmc-strings/StringEquals/test.desc +++ b/regression/jbmc-strings/StringEquals/test.desc @@ -3,10 +3,10 @@ Test.class --refine-strings --string-max-length 40 --function Test.check ^EXIT=10$ ^SIGNAL=0$ -assertion at file Test.java line 6 .* SUCCESS -assertion at file Test.java line 8 .* FAILURE -assertion at file Test.java line 10 .* SUCCESS -assertion at file Test.java line 12 .* FAILURE -assertion at file Test.java line 14 .* SUCCESS -assertion at file Test.java line 16 .* FAILURE +assertion at file Test.java line 9 .* SUCCESS +assertion at file Test.java line 11 .* FAILURE +assertion at file Test.java line 13 .* SUCCESS +assertion at file Test.java line 15 .* FAILURE +assertion at file Test.java line 17 .* SUCCESS +assertion at file Test.java line 19 .* FAILURE -- diff --git a/regression/jbmc-strings/StringEquals/test_verify.desc b/regression/jbmc-strings/StringEquals/test_verify.desc new file mode 100644 index 00000000000..f13e27ac930 --- /dev/null +++ b/regression/jbmc-strings/StringEquals/test_verify.desc @@ -0,0 +1,11 @@ +KNOWNBUG +Test.class +--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +assertion at file Test.java line 60 .* SUCCESS +-- +-- +null case not handled currently +TG-2179 + diff --git a/regression/jbmc-strings/StringEquals/test_verify_non_null.desc b/regression/jbmc-strings/StringEquals/test_verify_non_null.desc new file mode 100644 index 00000000000..5e62a087b67 --- /dev/null +++ b/regression/jbmc-strings/StringEquals/test_verify_non_null.desc @@ -0,0 +1,6 @@ +CORE +Test.class +--refine-strings --string-max-input-length 20 --string-max-length 100 --unwind 30 --function Test.verifyNonNull +^EXIT=0$ +^SIGNAL=0$ +assertion at file Test.java line 48 .* SUCCESS