From 72b611a1b4625cc3119b073dc044c8ef4bf4cd4a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 30 May 2017 11:04:04 +0100 Subject: [PATCH 1/2] Improvements on lengths Add CharSequence.length method More direct conversion of length methods --- .../java_string_library_preprocess.cpp | 77 ++++++++++++++++--- .../java_string_library_preprocess.h | 5 ++ 2 files changed, 71 insertions(+), 11 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 067812974e0..82d55d13688 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1024,8 +1024,8 @@ Function: java_string_library_preprocesst:: Output: return the following code: > lhs = { {Object}, length=rhs_length, data=rhs_array } - Purpose: Produce code for an assignemnrt of a string expr to a - Java string, component-wise. + Purpose: Produce code for an assignment of a string expr to a + Java string. \*******************************************************************/ @@ -1864,8 +1864,7 @@ codet java_string_library_preprocesst::make_copy_string_code( /*******************************************************************\ -Function: - java_string_library_preprocesst::make_copy_constructor_code +Function: java_string_library_preprocesst::make_copy_constructor_code Inputs: type - type of the function @@ -1913,6 +1912,52 @@ codet java_string_library_preprocesst::make_copy_constructor_code( /*******************************************************************\ +Function: java_string_library_preprocesst::make_string_length_code + + Inputs: + type - type of the function + loc - location in the source + symbol_table - symbol table + + Outputs: Code corresponding to: + > str_expr = java_string_to_string_expr(this) + > str_expr_sym = str_expr + > return this->length + + Purpose: Generates code for the String.length method + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_string_length_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // Code for the output + code_blockt code; + + code_typet::parameterst params=type.parameters(); + symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); + dereference_exprt deref(arg_this, arg_this.type().subtype()); + + // Create a new string_exprt to be picked up by the solver + string_exprt str_expr=fresh_string_expr(loc, symbol_table, code); + + // Assign this to str_expr + code.add( + code_assign_java_string_to_string_expr(str_expr, arg_this, symbol_table)); + + // Assign str_expr to str_expr_sym for that expression to be present in the + // symbol table in order to be processed by the string solver + exprt str_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assignt(str_expr_sym, str_expr)); + code.add(code_returnt(get_length(deref, symbol_table))); + + return code; +} + +/*******************************************************************\ + Function: java_string_library_preprocesst::code_for_function Inputs: @@ -2112,9 +2157,14 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]= ID_cprover_string_last_index_of_func; - cprover_equivalent_to_java_function + conversion_table ["java::java.lang.String.length:()I"]= - ID_cprover_string_length_func; + std::bind( + &java_string_library_preprocesst::make_string_length_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); // Not supported "java.lang.String.matches" cprover_equivalent_to_java_function ["java::java.lang.String.offsetByCodePoints:(II)I"]= @@ -2307,9 +2357,9 @@ void java_string_library_preprocesst::initialize_conversion_table() "Ljava/lang/StringBuilder;"]= ID_cprover_string_insert_func; // Not supported "java.lang.StringBuilder.lastIndexOf" - cprover_equivalent_to_java_function + conversion_table ["java::java.lang.StringBuilder.length:()I"]= - ID_cprover_string_length_func; + conversion_table["java::java.lang.String.length:()I"]; // Not supported "java.lang.StringBuilder.offsetByCodePoints" // Not supported "java.lang.StringBuilder.replace" // Not supported "java.lang.StringBuilder.reverse" @@ -2434,9 +2484,9 @@ void java_string_library_preprocesst::initialize_conversion_table() "Ljava/lang/StringBuffer;"]= ID_cprover_string_insert_func; // Not supported "java.lang.StringBuffer.lastIndexOf" - cprover_equivalent_to_java_function + conversion_table ["java::java.lang.StringBuffer.length:()I"]= - ID_cprover_string_length_func; + conversion_table["java::java.lang.String.length:()I"]; // Not supported "java.lang.StringBuffer.offsetByCodePoints" // Not supported "java.lang.StringBuffer.replace" // Not supported "java.lang.StringBuffer.reverse" @@ -2463,7 +2513,7 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_3); // Not supported "java.lang.StringBuffer.trimToSize" - // Other libraries + // CharSequence library cprover_equivalent_to_java_function ["java::java.lang.CharSequence.charAt:(I)C"]= ID_cprover_string_char_at_func; @@ -2475,6 +2525,11 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_1, std::placeholders::_2, std::placeholders::_3); + conversion_table + ["java::java.lang.CharSequence.length:()I"]= + conversion_table["java::java.lang.String.length:()I"]; + + // Other libraries conversion_table ["java::java.lang.Float.toString:(F)Ljava/lang/String;"]= std::bind( diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index 16ab5cfc6a9..79507b1bb36 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -146,6 +146,11 @@ class java_string_library_preprocesst:public messaget const source_locationt &loc, symbol_tablet &symbol_table); + codet make_string_length_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + // Auxiliary functions codet code_for_scientific_notation( const exprt &arg, From 1613290045631895c560642dfddc3e959745d77b Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Fri, 9 Jun 2017 15:54:01 +0100 Subject: [PATCH 2/2] Update smoke tests for String.length Update test description of java_length smoke test Now detected if the assertion is missing from the verification. Add new smoke test java_length2 --- .../strings-smoke-tests/java_length/test.desc | 6 ++++-- .../java_length/test_length.class | Bin 630 -> 654 bytes .../java_length/test_length.java | 1 + .../strings-smoke-tests/java_length2/test.class | Bin 0 -> 642 bytes .../strings-smoke-tests/java_length2/test.desc | 10 ++++++++++ .../strings-smoke-tests/java_length2/test.java | 12 ++++++++++++ 6 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 regression/strings-smoke-tests/java_length2/test.class create mode 100644 regression/strings-smoke-tests/java_length2/test.desc create mode 100644 regression/strings-smoke-tests/java_length2/test.java diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc index d7f0e02feca..487700d01fb 100644 --- a/regression/strings-smoke-tests/java_length/test.desc +++ b/regression/strings-smoke-tests/java_length/test.desc @@ -1,7 +1,9 @@ CORE test_length.class --refine-strings -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ +[.*assertion.1] .* line 7 .*: SUCCESS +[.*assertion.2] .* line 8 .*: FAILURE -- diff --git a/regression/strings-smoke-tests/java_length/test_length.class b/regression/strings-smoke-tests/java_length/test_length.class index 9273d09869b9f51a7d8c54ecac00703acfcf3186..9a1bd2977610d20c55be18a8b140d525fcee4c5f 100644 GIT binary patch delta 94 zcmeyy(#N{tG9zam12Y2?0|SHE*xm44e$YKv6CRroRkI>E4G9zag12Y2?0|SHd92>}2A diff --git a/regression/strings-smoke-tests/java_length/test_length.java b/regression/strings-smoke-tests/java_length/test_length.java index 4222414fa80..620bdc448e9 100644 --- a/regression/strings-smoke-tests/java_length/test_length.java +++ b/regression/strings-smoke-tests/java_length/test_length.java @@ -5,5 +5,6 @@ public static void main(/*String[] argv*/) String s = new String("Abc"); int l = s.length(); assert(l == 3); + assert(l != 3); } } diff --git a/regression/strings-smoke-tests/java_length2/test.class b/regression/strings-smoke-tests/java_length2/test.class new file mode 100644 index 0000000000000000000000000000000000000000..8e9d3161fb5b854424e20d3aabd35502b75128d9 GIT binary patch literal 642 zcmZ8e%T60X5Uk#(y)4++JRAt&4Ym((;RcF`AV`r&qR3ICa2u~jW?@;w?wEgp3r8+o z5+oxLDY^4e5j|_bN-i@!JvB8|)enE~e*@S+-Ghh894a1OVJeRtrgin&#f%3BlP=zP zn8lonc|v(fq^V3)*oo8KFcr;6wg_}UaJIrYRBs7pwf2o*?Q~j_P}mP+`Kf!-l*v~O zCfLED42}uo)%_!JF4iLvx7Qmg3FG!=?E_)Bp+s=}QJg;Eb6Y|5#OyUX-6W8Eq2|de znW{BS;bRyh{I6&RE*5+&V#&u4d>_kLAyfw6ynELEK1n(Wi_{!0R((`aBNPY7&&?wl zsDE00jcin&bw!l^=b-;!v!;`XWZYJVSrTlhFksz@I6cBdOQvBWTQ73hvg+~$M|XgE zo`A=bp<+e5;K~HYf)QQ|e462%c(?0!pdT8DBCk%?y$9R5!q6``-|yi5F>kCJh8r1C2^QBj6FEF~o;p`$?pQEpiM5TrDA~x!fzeW~ fhx{d6>l&7M3rnl&lRc}_1U3wRTWcTBt|uM=qP%#& literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_length2/test.desc b/regression/strings-smoke-tests/java_length2/test.desc new file mode 100644 index 00000000000..e473b51d950 --- /dev/null +++ b/regression/strings-smoke-tests/java_length2/test.desc @@ -0,0 +1,10 @@ +FUTURE +test.class +--refine-strings --function test.check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +This test currently fails because we do not handle the case where the argument +'s' is null. This should be handled in the String model. +The issue number for that is: diffblue/test-gen#500 diff --git a/regression/strings-smoke-tests/java_length2/test.java b/regression/strings-smoke-tests/java_length2/test.java new file mode 100644 index 00000000000..e88464536e0 --- /dev/null +++ b/regression/strings-smoke-tests/java_length2/test.java @@ -0,0 +1,12 @@ +public class test +{ + public static int check(String s) + { + if(s.equals("abc")){ + assert s.length() == 3; + return 0; + } + return 1; + } +} +