diff --git a/regression/strings-smoke-tests/java_parseint/test.desc b/regression/strings-smoke-tests/java_parseint/test.desc deleted file mode 100644 index 3b38dc2c575..00000000000 --- a/regression/strings-smoke-tests/java_parseint/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -test_parseint.class ---refine-strings -^EXIT=10$ -^SIGNAL=0$ -^\[.*assertion.1\].* line 8.* SUCCESS$ -^\[.*assertion.2\].* line 9.* FAILURE$ diff --git a/regression/strings-smoke-tests/java_parseint/test_parseint.class b/regression/strings-smoke-tests/java_parseint/test_parseint.class deleted file mode 100644 index 0f021d000fa..00000000000 Binary files a/regression/strings-smoke-tests/java_parseint/test_parseint.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parseint/test_parseint.java b/regression/strings-smoke-tests/java_parseint/test_parseint.java deleted file mode 100644 index d9b84914c7c..00000000000 --- a/regression/strings-smoke-tests/java_parseint/test_parseint.java +++ /dev/null @@ -1,12 +0,0 @@ -public class test_parseint -{ - public static void main(String[] args) - { - if (args.length == 1) { - String twelve = new String("12"); - int parsed1 = Integer.parseInt(twelve); - assert(parsed1 == 12); - assert(parsed1 != 12); - } - } -} diff --git a/regression/strings-smoke-tests/java_parseint_1/Test.class b/regression/strings-smoke-tests/java_parseint_1/Test.class new file mode 100644 index 00000000000..81304601f47 Binary files /dev/null and b/regression/strings-smoke-tests/java_parseint_1/Test.class differ diff --git a/regression/strings-smoke-tests/java_parseint_1/Test.java b/regression/strings-smoke-tests/java_parseint_1/Test.java new file mode 100644 index 00000000000..8831b817489 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint_1/Test.java @@ -0,0 +1,19 @@ +public class Test +{ + public static void foo(int i) + { + if (i == 1) { + String twelve = new String("12"); + int parsed1 = Integer.parseInt(twelve); + assert(parsed1 == 12); + assert(parsed1 != 12); + } + else if (i == 2) { + // 2^31-1, max value of Integer + String max_int = new String("2147483647"); + int parsed2 = Integer.parseInt(max_int); + assert(parsed2 == 2147483647); + assert(parsed2 != 2147483647); + } + } +} diff --git a/regression/strings-smoke-tests/java_parseint_1/test.desc b/regression/strings-smoke-tests/java_parseint_1/test.desc new file mode 100644 index 00000000000..b0e5d799277 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint_1/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.foo --refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 8.* SUCCESS$ +^\[.*assertion.2\].* line 9.* FAILURE$ +^\[.*assertion.3\].* line 15.* SUCCESS$ +^\[.*assertion.4\].* line 16.* FAILURE$ diff --git a/regression/strings-smoke-tests/java_parseint_2/Test.class b/regression/strings-smoke-tests/java_parseint_2/Test.class new file mode 100644 index 00000000000..58992e04a96 Binary files /dev/null and b/regression/strings-smoke-tests/java_parseint_2/Test.class differ diff --git a/regression/strings-smoke-tests/java_parseint_2/Test.java b/regression/strings-smoke-tests/java_parseint_2/Test.java new file mode 100644 index 00000000000..a32036c75ab --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint_2/Test.java @@ -0,0 +1,10 @@ +public class Test +{ + public static void foo(String input_string) + { + int parsed1 = Integer.parseInt(input_string); + if (parsed1 == 2) { + assert(false); + } + } +} diff --git a/regression/strings-smoke-tests/java_parseint_2/test.desc b/regression/strings-smoke-tests/java_parseint_2/test.desc new file mode 100644 index 00000000000..60c72ba9b36 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint_2/test.desc @@ -0,0 +1,6 @@ +THOROUGH +Test.class +--function Test.foo --refine-strings +^EXIT=10$ +^SIGNAL=0$ +^\[.*assertion.1\].* line 7.* FAILURE$ diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/Test.class b/regression/strings-smoke-tests/java_parseint_knownbug/Test.class new file mode 100644 index 00000000000..dd9c4886962 Binary files /dev/null and b/regression/strings-smoke-tests/java_parseint_knownbug/Test.class differ diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/Test.java b/regression/strings-smoke-tests/java_parseint_knownbug/Test.java new file mode 100644 index 00000000000..bb63540ad96 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint_knownbug/Test.java @@ -0,0 +1,12 @@ +public class Test +{ + public static void foo() + { + // -2^31, min value of Integer, and longest string we could have without + // leading zeroes + String min_int = new String("-2147483648"); + int parsed3 = Integer.parseInt(min_int); + assert(parsed3 == -2147483648); + assert(parsed3 != -2147483648); + } +} diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc index f543e2d900b..c8084216052 100644 --- a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc +++ b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc @@ -1,12 +1,10 @@ KNOWNBUG -test_parseint.class ---refine-strings +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ ^\[.*assertion.2\].* line 10.* FAILURE$ -^\[.*assertion.3\].* line 17.* SUCCESS$ -^\[.*assertion.4\].* line 18.* FAILURE$ -- -- Issue #664 is about turning these tests on diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.class b/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.class deleted file mode 100644 index 59932ae0cd7..00000000000 Binary files a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java b/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java deleted file mode 100644 index d2283bbfccd..00000000000 --- a/regression/strings-smoke-tests/java_parseint_knownbug/test_parseint.java +++ /dev/null @@ -1,21 +0,0 @@ -public class test_parseint -{ - public static void main(String[] args) - { - if (args.length == 2) { - // 2^31-1, max value of Integer - String max_int = new String("2147483647"); - int parsed2 = Integer.parseInt(max_int); - assert(parsed2 == 2147483647); - assert(parsed2 != 2147483647); - } - else if (args.length == 3) { - // -2^31, min value of Integer, and longest string we could have without - // leading zeroes - String min_int = new String("-2147483648"); - int parsed3 = Integer.parseInt(min_int); - assert(parsed3 == -2147483648); - assert(parsed3 != -2147483648); - } - } -} diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/Test.class b/regression/strings-smoke-tests/java_parseint_with_radix/Test.class new file mode 100644 index 00000000000..26bc43a8c10 Binary files /dev/null and b/regression/strings-smoke-tests/java_parseint_with_radix/Test.class differ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.java b/regression/strings-smoke-tests/java_parseint_with_radix/Test.java similarity index 77% rename from regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.java rename to regression/strings-smoke-tests/java_parseint_with_radix/Test.java index 978bf9fb320..29716aa2486 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.java +++ b/regression/strings-smoke-tests/java_parseint_with_radix/Test.java @@ -1,32 +1,32 @@ -public class test_parseint_with_radix +public class Test { - public static void main(String[] args) + public static void foo(int i) { - if (args.length == 1) { + if (i == 1) { String str1 = new String("F"); int parsed1 = Integer.parseInt(str1, 16); assert(parsed1 == 15); assert(parsed1 != 15); } - else if (args.length == 2) { + else if (i == 2) { String str2 = new String("123"); int parsed2 = Integer.parseInt(str2, 10); assert(parsed2 == 123); assert(parsed2 != 123); } - else if (args.length == 3) { + else if (i == 3) { String str3 = new String("77"); int parsed3 = Integer.parseInt(str3, 8); assert(parsed3 == 63); assert(parsed3 != 63); } - else if (args.length == 4) { + else if (i == 4) { String str4 = new String("-101"); int parsed4 = Integer.parseInt(str4, 2); assert(parsed4 == -5); assert(parsed4 != -5); } - else if (args.length == 5) { + else if (i == 5) { String str5 = new String("00aB"); int parsed5 = Integer.parseInt(str5, 16); assert(parsed5 == 171); diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test.desc index e6138767e20..8b4a846fa3b 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix/test.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix/test.desc @@ -1,6 +1,6 @@ CORE -test_parseint_with_radix.class ---refine-strings +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.class b/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.class deleted file mode 100644 index 22a393e7d10..00000000000 Binary files a/regression/strings-smoke-tests/java_parseint_with_radix/test_parseint_with_radix.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.class b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.class new file mode 100644 index 00000000000..507c0f9f16b Binary files /dev/null and b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.class differ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.java b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.java similarity index 78% rename from regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.java rename to regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.java index 7279127d053..e7cbf6df57b 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.java +++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/Test.java @@ -1,15 +1,15 @@ -public class test_parseint_with_radix +public class Test { - public static void main(String[] args) + public static void foo(int i) { - if (args.length == 1) { + if (i == 1) { // 2^31-1, max value of Integer String str1 = new String("7FFFFFFF"); int parsed1 = Integer.parseInt(str1, 16); assert(parsed1 == 2147483647); assert(parsed1 != 2147483647); } - else if (args.length == 2) { + else if (i == 2) { // -2^31, min value of Integer, and longest string we could have String str2 = new String("-100000000000000000000000000000000"); int parsed2 = Integer.parseInt(str2, 2); diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output new file mode 100644 index 00000000000..e9cde4a8842 --- /dev/null +++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output @@ -0,0 +1,164 @@ +CBMC version 5.7 64-bit x86_64 linux +Parsing test_parseint_with_radix.class +Java main class: test_parseint_with_radix +Converting +Generating GOTO Program +Adding CPROVER library (x86_64) +Removal of function pointers and virtual functions +Partial Inlining +Generic Property Instrumentation +Starting Bounded Model Checking +Unwinding loop __CPROVER__start.0 iteration 1 thread 0 +Unwinding loop __CPROVER__start.0 iteration 2 thread 0 +Unwinding loop __CPROVER__start.0 iteration 3 thread 0 +Unwinding loop __CPROVER__start.0 iteration 4 thread 0 +Unwinding loop __CPROVER__start.0 iteration 5 thread 0 +Unwinding recursion java::test_parseint_with_radix::clinit_wrapper iteration 1 +Unwinding recursion java::test_parseint_with_radix::clinit_wrapper iteration 1 +size of program expression: 530 steps +simple slicing removed 50 assignments +Generated 68 VCC(s), 9 remaining after simplification +Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier +converting SSA +Running string refinement loop with MiniSAT 2.2.1 without simplifier +BV-Refinement: post-processing +BV-Refinement: iteration 1 +54337 variables, 39117 clauses +SAT checker inconsistent: instance is UNSATISFIABLE +BV-Refinement: got UNSAT, and the proof passes => UNSAT +Total iterations: 1 +BV-Refinement: post-processing +BV-Refinement: iteration 1 +54337 variables, 39117 clauses +SAT checker inconsistent: instance is UNSATISFIABLE +BV-Refinement: got UNSAT, and the proof passes => UNSAT +Total iterations: 1 +Runtime decision procedure: 0.386s + +** Results: +[pointer_dereference.1] reference is null in *stub_ignored_arg1: SUCCESS +[pointer_dereference.2] reference is null in *stub_ignored_arg1->data: SUCCESS +[pointer_dereference.3] reference is null in *cprover_string_array$7: SUCCESS +[pointer_dereference.4] reference is null in *this: SUCCESS +[pointer_dereference.5] reference is null in *stub_ignored_arg0: SUCCESS +[pointer_dereference.6] reference is null in *stub_ignored_arg0->data: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.1] reference is null in *args: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.2] reference is null in *new_tmp0: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.3] reference is null in *new_tmp2: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.1] assertion at file test_parseint_with_radix.java line 9 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 20: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.1] Throw null: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.4] reference is null in *new_tmp3: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.2] assertion at file test_parseint_with_radix.java line 10 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 29: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.2] Throw null: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.5] reference is null in *args: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.6] reference is null in *new_tmp4: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.7] reference is null in *new_tmp6: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.3] assertion at file test_parseint_with_radix.java line 16 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 52: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.3] Throw null: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.8] reference is null in *new_tmp7: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.4] assertion at file test_parseint_with_radix.java line 17 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 61: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.4] Throw null: SUCCESS +[pointer_dereference.7] reference is null in *this: SUCCESS +[array-create-negative-size.1] Array size should be >= 0: SUCCESS +[pointer_dereference.8] reference is null in *cloned_array: SUCCESS +[pointer_dereference.9] reference is null in *cloned_array: SUCCESS +[pointer_dereference.10] reference is null in *this: SUCCESS +[pointer_dereference.11] reference is null in *cloned_array: SUCCESS +[pointer_dereference.12] reference is null in *this: SUCCESS +[pointer_dereference.13] reference is null in *cloned_array: SUCCESS +[pointer_dereference.14] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.15] reference is null in this->data[index]: SUCCESS +[pointer_dereference.16] reference is null in *this: SUCCESS +[array-create-negative-size.2] Array size should be >= 0: SUCCESS +[pointer_dereference.17] reference is null in *cloned_array: SUCCESS +[pointer_dereference.18] reference is null in *cloned_array: SUCCESS +[pointer_dereference.19] reference is null in *this: SUCCESS +[pointer_dereference.20] reference is null in *cloned_array: SUCCESS +[pointer_dereference.21] reference is null in *this: SUCCESS +[pointer_dereference.22] reference is null in *cloned_array: SUCCESS +[pointer_dereference.23] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.24] reference is null in this->data[index]: SUCCESS +[pointer_dereference.25] reference is null in *this: SUCCESS +[array-create-negative-size.3] Array size should be >= 0: SUCCESS +[pointer_dereference.26] reference is null in *cloned_array: SUCCESS +[pointer_dereference.27] reference is null in *cloned_array: SUCCESS +[pointer_dereference.28] reference is null in *this: SUCCESS +[pointer_dereference.29] reference is null in *cloned_array: SUCCESS +[pointer_dereference.30] reference is null in *this: SUCCESS +[pointer_dereference.31] reference is null in *cloned_array: SUCCESS +[pointer_dereference.32] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.33] reference is null in this->data[index]: SUCCESS +[pointer_dereference.34] reference is null in *this: SUCCESS +[array-create-negative-size.4] Array size should be >= 0: SUCCESS +[pointer_dereference.35] reference is null in *cloned_array: SUCCESS +[pointer_dereference.36] reference is null in *cloned_array: SUCCESS +[pointer_dereference.37] reference is null in *this: SUCCESS +[pointer_dereference.38] reference is null in *cloned_array: SUCCESS +[pointer_dereference.39] reference is null in *this: SUCCESS +[pointer_dereference.40] reference is null in *cloned_array: SUCCESS +[pointer_dereference.41] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.42] reference is null in this->data[index]: SUCCESS +[pointer_dereference.43] reference is null in *this: SUCCESS +[array-create-negative-size.5] Array size should be >= 0: SUCCESS +[pointer_dereference.44] reference is null in *cloned_array: SUCCESS +[pointer_dereference.45] reference is null in *cloned_array: SUCCESS +[pointer_dereference.46] reference is null in *this: SUCCESS +[pointer_dereference.47] reference is null in *cloned_array: SUCCESS +[pointer_dereference.48] reference is null in *this: SUCCESS +[pointer_dereference.49] reference is null in *cloned_array: SUCCESS +[pointer_dereference.50] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.51] reference is null in this->data[index]: SUCCESS +[pointer_dereference.52] reference is null in *this: SUCCESS +[array-create-negative-size.6] Array size should be >= 0: SUCCESS +[pointer_dereference.53] reference is null in *cloned_array: SUCCESS +[pointer_dereference.54] reference is null in *cloned_array: SUCCESS +[pointer_dereference.55] reference is null in *this: SUCCESS +[pointer_dereference.56] reference is null in *cloned_array: SUCCESS +[pointer_dereference.57] reference is null in *this: SUCCESS +[pointer_dereference.58] reference is null in *cloned_array: SUCCESS +[pointer_dereference.59] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.60] reference is null in this->data[index]: SUCCESS +[pointer_dereference.61] reference is null in *this: SUCCESS +[array-create-negative-size.7] Array size should be >= 0: SUCCESS +[pointer_dereference.62] reference is null in *cloned_array: SUCCESS +[pointer_dereference.63] reference is null in *cloned_array: SUCCESS +[pointer_dereference.64] reference is null in *this: SUCCESS +[pointer_dereference.65] reference is null in *cloned_array: SUCCESS +[pointer_dereference.66] reference is null in *this: SUCCESS +[pointer_dereference.67] reference is null in *cloned_array: SUCCESS +[pointer_dereference.68] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.69] reference is null in this->data[index]: SUCCESS +[pointer_dereference.70] reference is null in *this: SUCCESS +[array-create-negative-size.8] Array size should be >= 0: SUCCESS +[pointer_dereference.71] reference is null in *cloned_array: SUCCESS +[pointer_dereference.72] reference is null in *cloned_array: SUCCESS +[pointer_dereference.73] reference is null in *this: SUCCESS +[pointer_dereference.74] reference is null in *cloned_array: SUCCESS +[pointer_dereference.75] reference is null in *this: SUCCESS +[pointer_dereference.76] reference is null in *cloned_array: SUCCESS +[pointer_dereference.77] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.78] reference is null in this->data[index]: SUCCESS +[pointer_dereference.79] reference is null in *this: SUCCESS +[array-create-negative-size.9] Array size should be >= 0: SUCCESS +[pointer_dereference.80] reference is null in *cloned_array: SUCCESS +[pointer_dereference.81] reference is null in *cloned_array: SUCCESS +[pointer_dereference.82] reference is null in *this: SUCCESS +[pointer_dereference.83] reference is null in *cloned_array: SUCCESS +[pointer_dereference.84] reference is null in *this: SUCCESS +[pointer_dereference.85] reference is null in *cloned_array: SUCCESS +[pointer_dereference.86] reference is null in cloned_array->data[index]: SUCCESS +[pointer_dereference.87] reference is null in this->data[index]: SUCCESS +[pointer_dereference.88] reference is null in *args: SUCCESS +[pointer_dereference.89] reference is null in *args: SUCCESS +[pointer_dereference.90] reference is null in *args: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.9] reference is null in *args: SUCCESS +[pointer_dereference.91] reference is null in *args: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.10] reference is null in array_data_init$10[array_init_iter$11]: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.11] reference is null in *malloc_site$12: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.12] reference is null in *malloc_site$12: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.13] reference is null in *malloc_site$12: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.14] reference is null in *malloc_site$12: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.15] reference is null in *malloc_site$13: SUCCESS + +** 0 of 123 failed (1 iteration) +VERIFICATION SUCCESSFUL diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc index e3aa52b3cef..62ba98812e5 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc +++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc @@ -1,6 +1,6 @@ KNOWNBUG -test_parseint_with_radix.class ---refine-strings +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 9.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.class b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.class deleted file mode 100644 index 876f33d861b..00000000000 Binary files a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test_parseint_with_radix.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parselong_1/test_parselong.class b/regression/strings-smoke-tests/java_parselong_1/test_parselong.class deleted file mode 100644 index d912ed08003..00000000000 Binary files a/regression/strings-smoke-tests/java_parselong_1/test_parselong.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parselong_2/test_parselong.class b/regression/strings-smoke-tests/java_parselong_2/test_parselong.class deleted file mode 100644 index d0ba8c19bc7..00000000000 Binary files a/regression/strings-smoke-tests/java_parselong_2/test_parselong.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parselong_3/test_parselong.class b/regression/strings-smoke-tests/java_parselong_3/test_parselong.class deleted file mode 100644 index c7cafd723c4..00000000000 Binary files a/regression/strings-smoke-tests/java_parselong_3/test_parselong.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parselong_4/test_parselong.class b/regression/strings-smoke-tests/java_parselong_4/test_parselong.class deleted file mode 100644 index 89e6a99d4ab..00000000000 Binary files a/regression/strings-smoke-tests/java_parselong_4/test_parselong.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parselong_5/test_parselong.class b/regression/strings-smoke-tests/java_parselong_5/test_parselong.class deleted file mode 100644 index deaff359766..00000000000 Binary files a/regression/strings-smoke-tests/java_parselong_5/test_parselong.class and /dev/null differ diff --git a/regression/strings-smoke-tests/java_parselong_binary_1/Test.class b/regression/strings-smoke-tests/java_parselong_binary_1/Test.class new file mode 100644 index 00000000000..199471e4b3e Binary files /dev/null and b/regression/strings-smoke-tests/java_parselong_binary_1/Test.class differ diff --git a/regression/strings-smoke-tests/java_parselong_5/test_parselong.java b/regression/strings-smoke-tests/java_parselong_binary_1/Test.java similarity index 76% rename from regression/strings-smoke-tests/java_parselong_5/test_parselong.java rename to regression/strings-smoke-tests/java_parselong_binary_1/Test.java index ac30cc8af83..00b77873c3e 100644 --- a/regression/strings-smoke-tests/java_parselong_5/test_parselong.java +++ b/regression/strings-smoke-tests/java_parselong_binary_1/Test.java @@ -1,6 +1,6 @@ -public class test_parselong +public class Test { - public static void main(String[] args) + public static void foo() { // -2^35 String str = new String("-100000000000000000000000000000000000"); diff --git a/regression/strings-smoke-tests/java_parselong_3/test.desc b/regression/strings-smoke-tests/java_parselong_binary_1/test.desc similarity index 66% rename from regression/strings-smoke-tests/java_parselong_3/test.desc rename to regression/strings-smoke-tests/java_parselong_binary_1/test.desc index fa8ad9ccc48..d7a85429a93 100644 --- a/regression/strings-smoke-tests/java_parselong_3/test.desc +++ b/regression/strings-smoke-tests/java_parselong_binary_1/test.desc @@ -1,6 +1,6 @@ -THOROUGH -test_parselong.class ---refine-strings +CORE +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong_decimal_1/Test.class b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.class new file mode 100644 index 00000000000..98489907514 Binary files /dev/null and b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.class differ diff --git a/regression/strings-smoke-tests/java_parselong_1/test_parselong.java b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.java similarity index 74% rename from regression/strings-smoke-tests/java_parselong_1/test_parselong.java rename to regression/strings-smoke-tests/java_parselong_decimal_1/Test.java index a328af58250..a46474b1ac4 100644 --- a/regression/strings-smoke-tests/java_parselong_1/test_parselong.java +++ b/regression/strings-smoke-tests/java_parselong_decimal_1/Test.java @@ -1,6 +1,6 @@ -public class test_parselong +public class Test { - public static void main(String[] args) + public static void foo() { // 2^40 String str = new String("1099511627776"); diff --git a/regression/strings-smoke-tests/java_parselong_1/test.desc b/regression/strings-smoke-tests/java_parselong_decimal_1/test.desc similarity index 70% rename from regression/strings-smoke-tests/java_parselong_1/test.desc rename to regression/strings-smoke-tests/java_parselong_decimal_1/test.desc index fa8ad9ccc48..baaacde7d66 100644 --- a/regression/strings-smoke-tests/java_parselong_1/test.desc +++ b/regression/strings-smoke-tests/java_parselong_decimal_1/test.desc @@ -1,6 +1,6 @@ THOROUGH -test_parselong.class ---refine-strings +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong_decimal_2/Test.class b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.class new file mode 100644 index 00000000000..922b885b7b3 Binary files /dev/null and b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.class differ diff --git a/regression/strings-smoke-tests/java_parselong_3/test_parselong.java b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.java similarity index 75% rename from regression/strings-smoke-tests/java_parselong_3/test_parselong.java rename to regression/strings-smoke-tests/java_parselong_decimal_2/Test.java index e05341bdb86..e5578284020 100644 --- a/regression/strings-smoke-tests/java_parselong_3/test_parselong.java +++ b/regression/strings-smoke-tests/java_parselong_decimal_2/Test.java @@ -1,6 +1,6 @@ -public class test_parselong +public class Test { - public static void main(String[] args) + public static void foo() { // -2^41 String str = new String("-2199023255552"); diff --git a/regression/strings-smoke-tests/java_parselong_5/test.desc b/regression/strings-smoke-tests/java_parselong_decimal_2/test.desc similarity index 70% rename from regression/strings-smoke-tests/java_parselong_5/test.desc rename to regression/strings-smoke-tests/java_parselong_decimal_2/test.desc index fa8ad9ccc48..baaacde7d66 100644 --- a/regression/strings-smoke-tests/java_parselong_5/test.desc +++ b/regression/strings-smoke-tests/java_parselong_decimal_2/test.desc @@ -1,6 +1,6 @@ THOROUGH -test_parselong.class ---refine-strings +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 8.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong_hex_1/Test.class b/regression/strings-smoke-tests/java_parselong_hex_1/Test.class new file mode 100644 index 00000000000..33ba81a0406 Binary files /dev/null and b/regression/strings-smoke-tests/java_parselong_hex_1/Test.class differ diff --git a/regression/strings-smoke-tests/java_parselong_2/test_parselong.java b/regression/strings-smoke-tests/java_parselong_hex_1/Test.java similarity index 73% rename from regression/strings-smoke-tests/java_parselong_2/test_parselong.java rename to regression/strings-smoke-tests/java_parselong_hex_1/Test.java index c2e3d60bd11..944597ee24c 100644 --- a/regression/strings-smoke-tests/java_parselong_2/test_parselong.java +++ b/regression/strings-smoke-tests/java_parselong_hex_1/Test.java @@ -1,6 +1,6 @@ -public class test_parselong +public class Test { - public static void main(String[] args) + public static void foo() { String str = new String("+00AbCdEf0123"); long parsed = Long.parseLong(str, 16); diff --git a/regression/strings-smoke-tests/java_parselong_4/test.desc b/regression/strings-smoke-tests/java_parselong_hex_1/test.desc similarity index 66% rename from regression/strings-smoke-tests/java_parselong_4/test.desc rename to regression/strings-smoke-tests/java_parselong_hex_1/test.desc index 17db69e3979..f9ef9a9c0b6 100644 --- a/regression/strings-smoke-tests/java_parselong_4/test.desc +++ b/regression/strings-smoke-tests/java_parselong_hex_1/test.desc @@ -1,6 +1,6 @@ -THOROUGH -test_parselong.class ---refine-strings +CORE +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* SUCCESS$ diff --git a/regression/strings-smoke-tests/java_parselong_octal_1/Test.class b/regression/strings-smoke-tests/java_parselong_octal_1/Test.class new file mode 100644 index 00000000000..73fbc420bb0 Binary files /dev/null and b/regression/strings-smoke-tests/java_parselong_octal_1/Test.class differ diff --git a/regression/strings-smoke-tests/java_parselong_4/test_parselong.java b/regression/strings-smoke-tests/java_parselong_octal_1/Test.java similarity index 74% rename from regression/strings-smoke-tests/java_parselong_4/test_parselong.java rename to regression/strings-smoke-tests/java_parselong_octal_1/Test.java index 67eee61b85a..4dc8f7b712a 100644 --- a/regression/strings-smoke-tests/java_parselong_4/test_parselong.java +++ b/regression/strings-smoke-tests/java_parselong_octal_1/Test.java @@ -1,6 +1,6 @@ -public class test_parselong +public class Test { - public static void main(String[] args) + public static void foo() { String str = new String("7654321076543210"); long parsed = Long.parseLong(str, 8); diff --git a/regression/strings-smoke-tests/java_parselong_2/test.desc b/regression/strings-smoke-tests/java_parselong_octal_1/test.desc similarity index 66% rename from regression/strings-smoke-tests/java_parselong_2/test.desc rename to regression/strings-smoke-tests/java_parselong_octal_1/test.desc index 17db69e3979..f9ef9a9c0b6 100644 --- a/regression/strings-smoke-tests/java_parselong_2/test.desc +++ b/regression/strings-smoke-tests/java_parselong_octal_1/test.desc @@ -1,6 +1,6 @@ -THOROUGH -test_parselong.class ---refine-strings +CORE +Test.class +--refine-strings --function Test.foo ^EXIT=10$ ^SIGNAL=0$ ^\[.*assertion.1\].* line 7.* SUCCESS$ diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index a969ad6594e..659091b7aa6 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -293,9 +293,17 @@ class string_constraint_generatort exprt add_axioms_for_offset_by_code_point( const function_application_exprt &f); - exprt add_axioms_for_parse_int(const function_application_exprt &f); - exprt add_axioms_for_correct_number_format( + exprt add_axioms_for_characters_in_integer_string( + const symbol_exprt& x, + const typet& type, + const typet& char_type, + const typet& index_type, + const string_exprt& str, + const std::size_t max_string_length, + const exprt& radix); + void add_axioms_for_correct_number_format( const string_exprt &str, const exprt &radix, std::size_t max_size); + exprt add_axioms_for_parse_int(const function_application_exprt &f); exprt add_axioms_for_to_char_array(const function_application_exprt &f); exprt add_axioms_for_compare_to(const function_application_exprt &f); diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 2995648dc38..f3338d36f4b 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -364,12 +364,9 @@ string_exprt string_constraint_generatort::add_axioms_for_value_of( /// \param str: string expression /// \param radix: the radix /// \param max_size: maximum number of characters -/// \return a boolean expression saying whether the string does represent a -/// number with the given radix -exprt string_constraint_generatort::add_axioms_for_correct_number_format( - const string_exprt &str, const exprt &radix, std::size_t max_size) +void string_constraint_generatort::add_axioms_for_correct_number_format( + const string_exprt &str, const exprt &radix_char_type, std::size_t max_size) { - symbol_exprt correct=fresh_boolean("correct_number_format"); const refined_string_typet &ref_type=to_refined_string_type(str.type()); const typet &char_type=ref_type.get_char_type(); const typet &index_type=ref_type.get_index_type(); @@ -381,127 +378,162 @@ exprt string_constraint_generatort::add_axioms_for_correct_number_format( exprt chr=str[0]; equal_exprt starts_with_minus(chr, minus_char); equal_exprt starts_with_plus(chr, plus_char); - exprt starts_with_digit=is_digit_with_radix(chr, radix); + exprt starts_with_digit=is_digit_with_radix(chr, radix_char_type); // TODO: we should have implications in the other direction for correct // correct => |str| > 0 exprt non_empty=str.axiom_for_is_longer_than(from_integer(1, index_type)); - axioms.push_back(implies_exprt(correct, non_empty)); + axioms.push_back(non_empty); // correct => (str[0] = '+' or '-' || is_digit_with_radix(str[0], radix)) or_exprt correct_first( or_exprt(starts_with_minus, starts_with_plus), starts_with_digit); - axioms.push_back(implies_exprt(correct, correct_first)); + axioms.push_back(correct_first); // correct => str[0]='+' or '-' ==> |str| > 1 implies_exprt contains_digit( or_exprt(starts_with_minus, starts_with_plus), str.axiom_for_is_longer_than(from_integer(2, index_type))); - axioms.push_back(implies_exprt(correct, contains_digit)); + axioms.push_back(contains_digit); // correct => |str| < max_size - axioms.push_back( - implies_exprt(correct, str.axiom_for_is_shorter_than(max_size))); + axioms.push_back(str.axiom_for_is_shorter_than(max_size)); + + // forall 1 <= i < |str| . correct => is_digit_with_radix(str[i], radix) + // We unfold the above because we know that it will be used for all i up to + // str.length() + for(std::size_t index=1; index is_digit(str[index]) + implies_exprt character_at_index_is_digit( + binary_relation_exprt(index_expr, ID_lt, str.length()), + is_digit_with_radix(str[index], radix_char_type)); + axioms.push_back(character_at_index_is_digit); + } +} + +/// Add axioms connecting the characters in the input string to the value of the +/// output integer +/// \param x: symbol for abs(integer represented by str) +/// \param type: the type for x +/// \param char_type: the type to use for characters +/// \param index_type: the type to use for indexes +/// \param str: input string +/// \param max_string_length: the maximum length str can have +/// \param radix: the radix, with the same type as x +/// \return an expression for the integer represented by the string +exprt string_constraint_generatort::add_axioms_for_characters_in_integer_string( + const symbol_exprt& x, + const typet& type, + const typet& char_type, + const typet& index_type, + const string_exprt& str, + const std::size_t max_string_length, + const exprt& radix) +{ + /// TODO(OJones): Fix the below algorithm to make it work for min_int. There + /// are two problems. (1) Because we build i as positive and then negate it if + /// the first character is '-', we hit overflow for min_int because + /// |min_int| > max_int. (2) radix^63 overflows. I think we'll have to + /// special-case it. + + const exprt zero_expr=from_integer(0, type); + axioms.push_back(binary_relation_exprt(x, ID_ge, zero_expr)); + + const exprt one_index_type=from_integer(1, index_type); + exprt radix_to_power_of_i; + exprt no_overflow; + + for(std::size_t i=0; i is_digit_with_radix(str[qvar], radix) - symbol_exprt qvar=fresh_univ_index("number_format", index_type); - exprt is_digit=is_digit_with_radix(str[qvar], radix); - string_constraintt all_digits( - qvar, from_integer(1, index_type), str.length(), correct, is_digit); - axioms.push_back(all_digits); + if(i==0) + { + no_overflow=true_exprt(); + radix_to_power_of_i=from_integer(1, type); + } + else + { + const exprt radix_to_power_of_i_minus_one=radix_to_power_of_i; + /// Note that power_exprt is probably designed for floating point. Also, + /// it doesn't work when the exponent isn't a constant, hence why this + /// loop is indexed by i instead of j. It is faster than + /// mult_exprt(radix_to_power_of_i, radix). + radix_to_power_of_i=power_exprt(radix, i_expr); + /// The first time there is overflow we will have that + /// radix^i/radix != radix^(i-1) + /// However, that condition may hold in future, so we have to be sure to + /// propagate the first time this fails to all higher values of i + no_overflow=and_exprt( + equal_exprt( + div_exprt(radix_to_power_of_i, radix), radix_to_power_of_i_minus_one), + no_overflow); + } - return correct; + /// If we have already read all characters from the string then we use 0 + /// instead of the value from str[j] + const binary_relation_exprt i_is_valid(i_expr, ID_lt, str.length()); + const if_exprt digit_value( + i_is_valid, + get_numeric_value_from_character(str[j], char_type, type), + zero_expr); + + /// when there is no overflow, str[j] = (x/radix^i)%radix + const equal_exprt contribution_of_str_j( + digit_value, + mod_exprt(div_exprt(x, radix_to_power_of_i), radix)); + + axioms.push_back(implies_exprt(no_overflow, contribution_of_str_j)); + axioms.push_back(implies_exprt( + not_exprt(no_overflow), equal_exprt(digit_value, zero_expr))); + } + + return if_exprt( + equal_exprt(str[0], constant_char('-', char_type)), + unary_minus_exprt(x), + x); } /// add axioms corresponding to the Integer.parseInt java function /// \param f: a function application with either one string expression or one -/// string expression and an expression for the radix +/// string expression and an integer expression for the radix /// \return an integer expression exprt string_constraint_generatort::add_axioms_for_parse_int( const function_application_exprt &f) { PRECONDITION(f.arguments().size()==1 || f.arguments().size()==2); - string_exprt str=get_string_expr(f.arguments()[0]); + const string_exprt str=get_string_expr(f.arguments()[0]); + const typet &type=f.type(); + PRECONDITION(type.id()==ID_signedbv); const exprt radix= f.arguments().size()==1? - static_cast(from_integer(10, f.type())): - static_cast(typecast_exprt(f.arguments()[1], f.type())); + static_cast(from_integer(10, type)): + static_cast(typecast_exprt(f.arguments()[1], type)); - const typet &type=f.type(); - symbol_exprt i=fresh_symbol("parsed_int", type); + const symbol_exprt x=fresh_symbol("abs_parsed_int", type); const refined_string_typet &ref_type=to_refined_string_type(str.type()); const typet &char_type=ref_type.get_char_type(); - exprt minus_char=constant_char('-', char_type); - exprt plus_char=constant_char('+', char_type); - PRECONDITION(type.id()==ID_signedbv); + const typet &index_type=ref_type.get_index_type(); - exprt chr=str[0]; - exprt starts_with_minus=equal_exprt(chr, minus_char); - exprt starts_with_plus=equal_exprt(chr, plus_char); - exprt starts_with_digit= - not_exprt(or_exprt(starts_with_minus, starts_with_plus)); + /// We experimented with making the max_string_length depend on the base, but + /// this did not make any difference to the speed of execution. + const std::size_t max_string_length=to_bitvector_type(type).get_width()+1; /// TODO: we should throw an exception when this does not hold: - const std::size_t max_string_length=40; - const exprt &correct=add_axioms_for_correct_number_format( - str, radix, max_string_length); - axioms.push_back(correct); - - /// TODO(OJones): size should depend on the radix - /// TODO(OJones): we should deal with overflow properly - for(std::size_t size=1; size<=max_string_length; size++) - { - exprt sum=from_integer(0, type); - exprt first_value=get_numeric_value_from_character(chr, char_type, type); - equal_exprt premise=str.axiom_for_has_length(size); - - for(std::size_t j=1; j=max_string_length-1) - { - // We have to be careful about overflows - div_exprt div(sum, radix); - implies_exprt no_overflow(premise, (equal_exprt(div, sum))); - axioms.push_back(no_overflow); - } + /// Note that the only thing stopping us from taking longer strings with many + /// leading zeros is the axioms for correct number format + add_axioms_for_correct_number_format( + str, typecast_exprt(radix, char_type), max_string_length); - sum=plus_exprt_with_overflow_check( - radix_sum, - get_numeric_value_from_character(str[j], char_type, type)); + exprt parsed_int_expr=add_axioms_for_characters_in_integer_string( + x, type, char_type, index_type, str, max_string_length, radix); - mult_exprt first(first_value, radix); - if(j>=max_string_length-1) - { - // We have to be careful about overflows - div_exprt div_first(first, radix); - implies_exprt no_overflow_first( - and_exprt(starts_with_digit, premise), - equal_exprt(div_first, first_value)); - axioms.push_back(no_overflow_first); - } - first_value=first; - } - - // If the length is `size`, we add axioms: - // a1 : starts_with_digit => i=sum+first_value - // a2 : starts_with_plus => i=sum - // a3 : starts_with_minus => i=-sum - - implies_exprt a1( - and_exprt(premise, starts_with_digit), - equal_exprt(i, plus_exprt(sum, first_value))); - axioms.push_back(a1); - - implies_exprt a2(and_exprt(premise, starts_with_plus), equal_exprt(i, sum)); - axioms.push_back(a2); - - implies_exprt a3( - and_exprt(premise, starts_with_minus), - equal_exprt(i, unary_minus_exprt(sum))); - axioms.push_back(a3); - } - return i; + return parsed_int_expr; } /// Check if a character is a digit with respect to the given radix, e.g. if the @@ -509,21 +541,21 @@ exprt string_constraint_generatort::add_axioms_for_parse_int( /// \param chr: the character /// \param radix: the radix /// \return an expression for the condition -exprt is_digit_with_radix(exprt chr, exprt radix) +exprt is_digit_with_radix(exprt chr, exprt radix_char_type) { const typet &char_type=chr.type(); exprt zero_char=from_integer('0', char_type); exprt nine_char=from_integer('9', char_type); exprt a_char=from_integer('a', char_type); exprt A_char=from_integer('A', char_type); + constant_exprt ten_char_type=from_integer(10, char_type); and_exprt is_digit_when_radix_le_10( binary_relation_exprt(chr, ID_ge, zero_char), binary_relation_exprt( - chr, ID_lt, plus_exprt(zero_char, typecast_exprt(radix, char_type)))); + chr, ID_lt, plus_exprt(zero_char, radix_char_type))); - minus_exprt radix_minus_ten( - typecast_exprt(radix, char_type), from_integer(10, char_type)); + minus_exprt radix_minus_ten(radix_char_type, ten_char_type); or_exprt is_digit_when_radix_gt_10( and_exprt( @@ -537,13 +569,13 @@ exprt is_digit_with_radix(exprt chr, exprt radix) binary_relation_exprt(chr, ID_lt, plus_exprt(A_char, radix_minus_ten)))); return if_exprt( - binary_relation_exprt(radix, ID_le, from_integer(10, radix.type())), + binary_relation_exprt(radix_char_type, ID_le, ten_char_type), is_digit_when_radix_le_10, is_digit_when_radix_gt_10); } /// Get the numeric value of a character, assuming that the radix is large -/// enough +/// enough. '+' and '-' yield 0. /// \param chr: the character to get the numeric value of /// \param char_type: the type to use for characters /// \param type: the type to use for the return value @@ -557,16 +589,25 @@ exprt get_numeric_value_from_character( constant_exprt A_char=from_integer('A', char_type); constant_exprt ten_int=from_integer(10, char_type); - binary_relation_exprt upper_case(chr, ID_ge, A_char); + /// There are four cases, which occur in ASCII in the following order: + /// '+' and '-', digits, upper case letters, lower case letters binary_relation_exprt lower_case(chr, ID_ge, a_char); + binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char); + binary_relation_exprt upper_case_lower_case_or_digit(chr, ID_ge, zero_char); + /// return char >= 'a' ? (char - 'a' + 10) : + /// char >= 'A' ? (char - 'A' + 10) : + /// char >= '0' ? (char - '0') : 0 return typecast_exprt( if_exprt( lower_case, plus_exprt(minus_exprt(chr, a_char), ten_int), if_exprt( - upper_case, + upper_case_or_lower_case, plus_exprt(minus_exprt(chr, A_char), ten_int), - minus_exprt(chr, zero_char))), + if_exprt( + upper_case_lower_case_or_digit, + minus_exprt(chr, zero_char), + from_integer(0, char_type)))), type); } diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp index 29bef9bd788..296c8780523 100644 --- a/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp +++ b/unit/solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp @@ -15,27 +15,97 @@ #include #include + + SCENARIO("get_numeric_value_from_character", "[core][solvers][refinement][string_constraint_generator_valueof]") { - typet char_type=unsignedbv_typet(16); - typet int_type=signedbv_typet(32); + const typet char_type_1=unsignedbv_typet(8); + const typet char_type_2=unsignedbv_typet(16); + const typet char_type_3=unsignedbv_typet(32); + const typet int_type_1=signedbv_typet(8); + const typet int_type_2=signedbv_typet(16); + const typet int_type_3=signedbv_typet(32); + const typet int_type_4=signedbv_typet(64); symbol_tablet symtab; - namespacet ns(symtab); - - REQUIRE(from_integer(0, int_type)==simplify_expr( - get_numeric_value_from_character( - from_integer('0', char_type), char_type, int_type),ns)); - REQUIRE(from_integer(9, int_type)==simplify_expr( - get_numeric_value_from_character( - from_integer('9', char_type), - char_type, int_type), ns)); - REQUIRE(from_integer(10, int_type)==simplify_expr( - get_numeric_value_from_character( - from_integer('A', char_type), - char_type, int_type), ns)); - REQUIRE(from_integer(35, int_type)==simplify_expr( - get_numeric_value_from_character( - from_integer('z', char_type), - char_type, int_type), ns)); + const namespacet ns(symtab); + + WHEN("0") + { + mp_integer character='0'; + mp_integer expected_value=0; + const typet& char_type=char_type_1; + const typet& int_type=int_type_1; + constant_exprt expected_value_exprt=from_integer(expected_value, int_type); + exprt actual_value_exprt=simplify_expr( + get_numeric_value_from_character( + from_integer(character, char_type), char_type, int_type), + ns); + REQUIRE(expected_value_exprt==actual_value_exprt); + } + WHEN("9") + { + mp_integer character='9'; + mp_integer expected_value=9; + const typet& char_type=char_type_2; + const typet& int_type=int_type_2; + constant_exprt expected_value_exprt=from_integer(expected_value, int_type); + exprt actual_value_exprt=simplify_expr( + get_numeric_value_from_character( + from_integer(character, char_type), char_type, int_type), + ns); + REQUIRE(expected_value_exprt==actual_value_exprt); + } + WHEN("A") + { + mp_integer character='A'; + mp_integer expected_value=10; + const typet& char_type=char_type_3; + const typet& int_type=int_type_3; + constant_exprt expected_value_exprt=from_integer(expected_value, int_type); + exprt actual_value_exprt=simplify_expr( + get_numeric_value_from_character( + from_integer(character, char_type), char_type, int_type), + ns); + REQUIRE(expected_value_exprt==actual_value_exprt); + } + WHEN("z") + { + mp_integer character='z'; + mp_integer expected_value=35; + const typet& char_type=char_type_1; + const typet& int_type=int_type_4; + constant_exprt expected_value_exprt=from_integer(expected_value, int_type); + exprt actual_value_exprt=simplify_expr( + get_numeric_value_from_character( + from_integer(character, char_type), char_type, int_type), + ns); + REQUIRE(expected_value_exprt==actual_value_exprt); + } + WHEN("+") + { + mp_integer character='+'; + mp_integer expected_value=0; + const typet& char_type=char_type_2; + const typet& int_type=int_type_1; + constant_exprt expected_value_exprt=from_integer(expected_value, int_type); + exprt actual_value_exprt=simplify_expr( + get_numeric_value_from_character( + from_integer(character, char_type), char_type, int_type), + ns); + REQUIRE(expected_value_exprt==actual_value_exprt); + } + WHEN("-") + { + mp_integer character='-'; + mp_integer expected_value=0; + const typet& char_type=char_type_3; + const typet& int_type=int_type_2; + constant_exprt expected_value_exprt=from_integer(expected_value, int_type); + exprt actual_value_exprt=simplify_expr( + get_numeric_value_from_character( + from_integer(character, char_type), char_type, int_type), + ns); + REQUIRE(expected_value_exprt==actual_value_exprt); + } } diff --git a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp index 85a14ff3859..31ca819a600 100644 --- a/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp +++ b/unit/solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp @@ -18,57 +18,38 @@ SCENARIO("is_digit_with_radix", "[core][solvers][refinement][string_constraint_generator_valueof]") { - typet char_type=unsignedbv_typet(16); - typet int_type=signedbv_typet(32); + const typet char_type=unsignedbv_typet(16); symbol_tablet symtab; - namespacet ns(symtab); + const namespacet ns(symtab); WHEN("Radix 10") { - int radix=10; + const constant_exprt radix_expr=from_integer(10, char_type); REQUIRE(true_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('0', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('0', char_type), radix_expr), ns)); REQUIRE(true_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('9', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('9', char_type), radix_expr), ns)); REQUIRE(false_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('a', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('a', char_type), radix_expr), ns)); } WHEN("Radix 8") { - int radix=8; + const constant_exprt radix_expr=from_integer(8, char_type); REQUIRE(true_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('7', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('7', char_type), radix_expr), ns)); REQUIRE(false_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('8', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('8', char_type), radix_expr), ns)); } WHEN("Radix 16") { - int radix=16; + const constant_exprt radix_expr=from_integer(16, char_type); REQUIRE(true_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('a', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('a', char_type), radix_expr), ns)); REQUIRE(true_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('A', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('A', char_type), radix_expr), ns)); REQUIRE(true_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('f', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('f', char_type), radix_expr), ns)); REQUIRE(false_exprt()==simplify_expr( - is_digit_with_radix( - from_integer('g', char_type), - from_integer(radix, int_type)), ns)); + is_digit_with_radix(from_integer('g', char_type), radix_expr), ns)); } }