diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 31df88c0bba..ee97592c10b 160000 --- 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 index 1cb966074c6..4779e107ffd 100644 --- 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 index 38261f6441e..a98505a2026 100644 --- 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 index 089dff1e273..2ec5fcbf2ea 100644 --- 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 index 73c00e60e6a..8b94e1d2486 100644 --- 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 new file mode 100644 index 00000000000..8ab584c606b Binary files /dev/null and b/jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class differ 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 new file mode 100644 index 00000000000..ece00ea510f --- /dev/null +++ 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 new file mode 100644 index 00000000000..84c7ab2182f --- /dev/null +++ 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 index 1cb966074c6..4779e107ffd 100644 --- 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 index cd1d038f76c..160deb14def 100644 --- 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 index de14d77c44d..df497badb22 100644 --- 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 index 539651ed9e7..59570e81f11 100644 --- 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 index 0c81faf44d4..3dda5185d6d 100644 --- 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 index 07f65d534f3..cf35f361031 100644 --- 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 index d20c1215eb9..e887d1612ff 100644 --- 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 index 1b89ef8987e..03d6c5b3feb 100644 --- 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 index b8dcfbd6229..28a8a979bed 100644 --- 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 index 4ee4647236c..539c655161d 100644 --- 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 index 46724c6ac99..e3f38b1298e 100644 --- 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 new file mode 100644 index 00000000000..04ed12dc642 Binary files /dev/null and b/jbmc/regression/strings-smoke-tests/java_parselong_unknown_radix/Test.class differ 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 new file mode 100644 index 00000000000..bbc288a5fae --- /dev/null +++ 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 new file mode 100644 index 00000000000..ff5e8d11e1f --- /dev/null +++ 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 index 3b03aa7dc39..4748549e0c5 100644 --- 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.:(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 index c6797b219e2..c25c7f9d274 100644 --- 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 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); }