Merge pull request #5226 from smowton/smowton/feature/faster-string-to-int

smowton · web-flow · commit 778fb974411a · 2020-02-07T16:38:29.000Z
String solver: avoid cubic formulas for string-to-int conversions
diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library
@@ -1 +1 @@
-Subproject commit 31df88c0bba7fa5f9c4eeb53a79f8902246f386a
+Subproject commit ee97592c10bb6d8c8c65472e547e9d1e41fa9b8d
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1
---max-nondet-string-length 1000 --function Test1.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2
---max-nondet-string-length 1000 --function Test2.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3
---max-nondet-string-length 1000 --function Test3.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* FAILURE$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test
---max-nondet-string-length 1000 --function Test.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java
@@ -0,0 +1,18 @@
+public class Test {
+
+    public static void testMe(String input, int radix) {
+
+        // Railroad the solver a bit to speed up solving
+        // (note use of > and < to dodge constant propagation)
+        if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30)
+            return;
+
+	int value = Integer.parseInt(input, radix);
+	if(value == 20)
+	    assert false;
+        else
+            assert false;
+
+    }
+
+}
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc
@@ -0,0 +1,9 @@
+CORE
+Test
+--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 12.* FAILURE$
+^\[.*assertion.2\].* line 14.* SUCCESS$
+--
+non equal types
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1
---max-nondet-string-length 1000 --function Test1.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2
---max-nondet-string-length 1000 --function Test2.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3
---max-nondet-string-length 1000 --function Test3.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4
---max-nondet-string-length 1000 --function Test4.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test4.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5
---max-nondet-string-length 1000 --function Test5.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test5.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/jbmc/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
@@ -1,6 +1,6 @@
 CORE
 Test6
---max-nondet-string-length 1000 --function Test6.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test6.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary_min
---max-nondet-string-length 1000 --function Test_binary_min.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_binary_min.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal_max
---max-nondet-string-length 1000 --function Test_decimal_max.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_decimal_max.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal_min
---max-nondet-string-length 1000 --function Test_decimal_min.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_decimal_min.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_hex.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex
---max-nondet-string-length 1000 --function Test_hex.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_hex.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc b/jbmc/regression/strings-smoke-tests/java_parselong/test_octal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal
---max-nondet-string-length 1000 --function Test_octal.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test_octal.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.class b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.class
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.java b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.java
@@ -0,0 +1,18 @@
+public class Test {
+
+    public static void testMe(String input, int radix) {
+
+        // Railroad the solver a bit to speed up solving
+        // (note use of > and < to dodge constant propagation)
+        if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30)
+            return;
+
+	long value = Long.parseLong(input, radix);
+	if(value == 20)
+	    assert false;
+        else
+            assert false;
+
+    }
+
+}
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/test.desc
@@ -0,0 +1,9 @@
+THOROUGH
+Test
+--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 12.* FAILURE$
+^\[.*assertion.2\].* line 14.* SUCCESS$
+--
+non equal types
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1574,6 +1574,12 @@ void java_string_library_preprocesst::initialize_conversion_table()
         std::placeholders::_2,
         std::placeholders::_3,
         std::placeholders::_4);
+  cprover_equivalent_to_java_function
+    ["java::org.cprover.CProverString.parseInt:(Ljava/lang/String;I)I"] =
+      ID_cprover_string_parse_int_func;
+  cprover_equivalent_to_java_function
+    ["java::org.cprover.CProverString.parseLong:(Ljava/lang/String;I)J"] =
+      ID_cprover_string_parse_int_func;
 
   // String library
   conversion_table["java::java.lang.String.<init>:(Ljava/lang/String;)V"] =
@@ -1819,18 +1825,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
       conversion_table["java::java.lang.String.length:()I"];
 
   // Other libraries
-  cprover_equivalent_to_java_function
-    ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]=
-      ID_cprover_string_parse_int_func;
-  cprover_equivalent_to_java_function
-    ["java::java.lang.Integer.parseInt:(Ljava/lang/String;I)I"]=
-      ID_cprover_string_parse_int_func;
-  cprover_equivalent_to_java_function
-    ["java::java.lang.Long.parseLong:(Ljava/lang/String;)J"]=
-      ID_cprover_string_parse_int_func;
-  cprover_equivalent_to_java_function
-    ["java::java.lang.Long.parseLong:(Ljava/lang/String;I)J"]=
-      ID_cprover_string_parse_int_func;
   cprover_equivalent_to_java_string_returning_function
     ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]=
       ID_cprover_string_of_int_hex_func;
diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp
@@ -385,7 +385,6 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string(
 
   const equal_exprt starts_with_minus(str[0], from_integer('-', char_type));
   const constant_exprt zero_expr = from_integer(0, type);
-  exprt::operandst digit_constraints;
 
   exprt sum = get_numeric_value_from_character(
     str[0], char_type, type, strict_formatting, radix_ul);
@@ -407,8 +406,7 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string(
     //   (the first part avoid overflows in the multiplication and the second
     //     one in the addition of the definition of sum_j)
     // For all 1<=size<=max_string_length we add axioms:
-    // a5 : |res| == size =>
-    //        forall max_string_length-2 <= j < size. no_overflow_j
+    // a5 : |res| >= size => no_overflow_j (only added when overflow possible)
     // a6 : |res| == size && res[0] is a digit for radix =>
     //        input_int == sum_{size-1}
     // a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1}
@@ -424,31 +422,33 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string(
     // a digit, which is `max_string_length - 2` because of the space left for
     // a minus sign. That assumes that we were able to identify the radix. If we
     // weren't then we check for overflow on every index.
+    optionalt<exprt> no_overflow;
     if(size - 1 >= max_string_length - 2 || radix_ul == 0)
     {
-      const and_exprt no_overflow(
-        equal_exprt(sum, div_exprt(radix_sum, radix)),
-        binary_relation_exprt(new_sum, ID_ge, radix_sum));
-      digit_constraints.push_back(no_overflow);
+      no_overflow = and_exprt{equal_exprt(sum, div_exprt(radix_sum, radix)),
+                              binary_relation_exprt(new_sum, ID_ge, radix_sum)};
     }
     sum = new_sum;
 
-    const equal_exprt premise =
-      equal_to(array_pool.get_or_create_length(str), size);
+    exprt length_expr = array_pool.get_or_create_length(str);
 
-    if(!digit_constraints.empty())
+    if(no_overflow.has_value())
     {
-      const implies_exprt a5(premise, conjunction(digit_constraints));
+      const binary_predicate_exprt string_length_ge_size{
+        length_expr, ID_ge, from_integer(size, length_expr.type())};
+      const implies_exprt a5(string_length_ge_size, *no_overflow);
       constraints.existential.push_back(a5);
     }
 
+    const equal_exprt string_length_equals_size = equal_to(length_expr, size);
+
     const implies_exprt a6(
-      and_exprt(premise, not_exprt(starts_with_minus)),
+      and_exprt(string_length_equals_size, not_exprt(starts_with_minus)),
       equal_exprt(input_int, sum));
     constraints.existential.push_back(a6);
 
     const implies_exprt a7(
-      and_exprt(premise, starts_with_minus),
+      and_exprt(string_length_equals_size, starts_with_minus),
       equal_exprt(input_int, unary_minus_exprt(sum)));
     constraints.existential.push_back(a7);
   }
