Merge pull request #994 from allredj/pr/string-preprocess-improve-lengths

forejtv · web-flow · commit 2105ee9dcdc4 · 2017-06-14T11:16:48.000+01:00
Improve length handling in string preprocessing
diff --git 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
diff --git 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
diff --git a/regression/strings-smoke-tests/java_length2/test.desc 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
@@ -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;
+    }
+}
+
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1022,8 +1022,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.
 
 \*******************************************************************/
 
@@ -1862,8 +1862,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
@@ -1911,6 +1910,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:
@@ -2110,9 +2155,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"]=
@@ -2305,9 +2355,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"
@@ -2432,9 +2482,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"
@@ -2461,7 +2511,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;
@@ -2473,6 +2523,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
@@ -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,

Original file line number	Diff line number	Diff line change
`@@ -5,5 +5,6 @@ public static void main(/String[] argv/)`
`5`	`5`	`String s = new String("Abc");`
`6`	`6`	`int l = s.length();`
`7`	`7`	`assert(l == 3);`
	`8`	`+ assert(l != 3);`
`8`	`9`	`}`
`9`	`10`	`}`