From 70d0cb0e0081ec5cf48d29668e3ebaeb63813717 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Jun 2017 09:59:46 +0100 Subject: [PATCH 1/8] Forgotten premise in add_axioms_from_int --- .../refinement/string_constraint_generator_valueof.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 9ad1845c9d0..7b060c1e27b 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -209,9 +209,9 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( /// add axioms to say the string corresponds to the result of String.valueOf(I) /// or String.valueOf(J) java functions applied on the integer expression -/// \par parameters: a signed integer expression, and a maximal size for the -/// string -/// representation +/// \param i: a signed integer expression +/// \param max_size: a maximal size for the string representation +/// \param ref_type: type for refined strings /// \return a string expression string_exprt string_constraint_generatort::add_axioms_from_int( const exprt &i, size_t max_size, const refined_string_typet &ref_type) @@ -299,10 +299,10 @@ string_exprt string_constraint_generatort::add_axioms_from_int( sum=new_sum; } + equal_exprt premise=res.axiom_for_has_length(size); exprt a5=conjunction(digit_constraints); - axioms.push_back(a5); + axioms.push_back(implies_exprt(premise, a5)); - equal_exprt premise=res.axiom_for_has_length(size); implies_exprt a6( and_exprt(premise, starts_with_digit), equal_exprt(i, sum)); axioms.push_back(a6); From 8a803100e9a37d2b0aab7bc81b6113002d0e6c71 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Jun 2017 09:36:27 +0100 Subject: [PATCH 2/8] Correcting when to do overflow check in add_axioms_from_int When the number is positive we have to check for overflow even when the index we look at is max_size-2. --- src/solvers/refinement/string_constraint_generator_valueof.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 7b060c1e27b..92eea0392ae 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -288,7 +288,7 @@ string_exprt string_constraint_generatort::add_axioms_from_int( binary_relation_exprt(res[j], ID_le, nine_char)); digit_constraints.push_back(is_number); - if(j>=max_size-1) + if(j>=max_size-2) { // check for overflows if the size is big and_exprt no_overflow( From 15e88e7367d9c1c35537eac7b7fcbc8d5acf0cfe Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 20 Jun 2017 09:40:48 +0100 Subject: [PATCH 3/8] Making tests for int to string conversion more precise We include both assertion that should hold and some that should fail. --- .../java_int_to_string/test.desc | 7 +++++-- .../java_int_to_string/test_int.class | Bin 859 -> 1074 bytes .../java_int_to_string/test_int.java | 6 +++++- 3 files changed, 10 insertions(+), 3 deletions(-) diff --git a/regression/strings-smoke-tests/java_int_to_string/test.desc b/regression/strings-smoke-tests/java_int_to_string/test.desc index 38fa5289bd2..e8d4260b1e0 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test.desc @@ -1,7 +1,10 @@ CORE test_int.class --refine-strings -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +assertion.* file test_int.java line 6 .* SUCCESS$ +assertion.* file test_int.java line 9 .* SUCCESS$ +assertion.* file test_int.java line 11 .* FAILURE$ +assertion.* file test_int.java line 13 .* FAILURE$ -- diff --git a/regression/strings-smoke-tests/java_int_to_string/test_int.class b/regression/strings-smoke-tests/java_int_to_string/test_int.class index eff0e5a422e2df360086c15be326751bd69c8115..ca4e3be5dc4cbe057e18e8f43a9813c6d11e4e1c 100644 GIT binary patch delta 638 zcmYL{&rTCj6vltI?fmI5Xj7_UOBJn3DaG=qq6i{YFd-?c8jOj?3{8Whb!w)giER1| z#1*W317l6VXrg;x!6$I*ni$WtsVwff=X~e8U%qo@e(7Da^7HT4??9RR7Q^H$u5dNZ z5Z6p5Eb>em6fAUdai%C*Omp3&WH4hf%bdadUS+M5thVY-bIb8vXS>;W7zRZwc<#0p zRyAm}gJ-T6ED83?aXq>68y5wnG5h3(%>p-VPH|chnH6Vcn_Da@Mo)w*?RLWt+?KcQ z`z_z#w#^dD26t>$xT}ax&&`Ycz_7upO@(`(^J-CbN{As@l~y=HeUc=?h(x^yDpHc$ zeFA4VD^;9xj0%#J{Ex7sa_=VWFGQ+cq6eg=lCeXy1BSk#KR&|vk@zjm%`Rr~ka(X{ zOj>feOE?`NniFKVU202U$Vz(mr1Nrt( zWsq(88{Ww_!?DIg>kI61p0t!Y0U5?*vK)^@U`%GaAb5h Rgh|9O4|ifo&NNtjG986<>lFl92$jAYhCClO?h zq{%!B28)uE$r8&Fr(WKR`>)(;O%Oiv-1Cb=_xjj9yR1mk_3vza#UjJ1#Q=i>Etgle zMV7TjN!Y2JMV^ABXtBY;yn8e?up6wNk!}!hRR|4xsi z^*M!vLMggZ9UDm!14m)Yn2e}o0IiEH8SRo(s?xE>m#-M>WdSs6r}uume{cL3uXr~U diff --git a/regression/strings-smoke-tests/java_int_to_string/test_int.java b/regression/strings-smoke-tests/java_int_to_string/test_int.java index f46411ed166..9ddbc332b6f 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test_int.java +++ b/regression/strings-smoke-tests/java_int_to_string/test_int.java @@ -1,11 +1,15 @@ public class test_int { - public static void main(/*String[] argv*/) + public static void main(int i) { String s = Integer.toString(12); assert(s.equals("12")); String t = Integer.toString(-23); System.out.println(t); assert(t.equals("-23")); + if(i==1) + assert(!s.equals("12")); + else if(i==2) + assert(!t.equals("-23")); } } From 7fa229b3d7e5cee995928e7f9f9fd847667f6e71 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 23 Jun 2017 12:59:41 +0100 Subject: [PATCH 4/8] Update comments in add_axioms_from_int to reflect changes in the code --- .../string_constraint_generator_valueof.cpp | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 92eea0392ae..dfbe32ea8a0 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -266,8 +266,18 @@ string_exprt string_constraint_generatort::add_axioms_from_int( for(size_t size=1; size<=max_size; size++) { - // For each possible size, we add axioms: - // a5 : forall 1 <= j < size. '0' <= res[j] <= '9' && sum == 10 * (sum/10) + // For each possible size, we have: + // sum_0 = starts_with_digit ? res[0]-'0' : 0 + // sum_j = 10 * sum_{j-1} + res[i] - '0' + // and add axioms: + // a5 : |res| == size => + // forall 1 <= j < size. + // is_number && (j >= max_size-2 => no_overflow) + // where is_number := '0' <= res[j] <= '9' + // and no_overflow := sum_{j-1} = (10 * sum_{j-1} / 10) + // && sum_j >= sum_{j - 1} + // (the first part avoid overflows in multiplication and + // the second one in additions) // a6 : |res| == size && '0' <= res[0] <= '9' => i == sum // a7 : |res| == size && res[0] == '-' => i == -sum @@ -300,8 +310,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int( } equal_exprt premise=res.axiom_for_has_length(size); - exprt a5=conjunction(digit_constraints); - axioms.push_back(implies_exprt(premise, a5)); + implies_exprt a5(premise, conjunction(digit_constraints)); + axioms.push_back(a5); implies_exprt a6( and_exprt(premise, starts_with_digit), equal_exprt(i, sum)); From fb3ab81c0e071e09dc5b8aad9561436f1f230150 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 23 Jun 2017 13:01:58 +0100 Subject: [PATCH 5/8] Using PRECONDITION instead of assert --- .../refinement/string_constraint_generator_valueof.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index dfbe32ea8a0..8b15bf6cbdc 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -216,9 +216,10 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( string_exprt string_constraint_generatort::add_axioms_from_int( const exprt &i, size_t max_size, const refined_string_typet &ref_type) { + PRECONDITION(i.type().id()==ID_signedbv); + PRECONDITION(max_size::max()); string_exprt res=fresh_string(ref_type); const typet &type=i.type(); - assert(type.id()==ID_signedbv); exprt ten=from_integer(10, type); const typet &char_type=ref_type.get_char_type(); const typet &index_type=ref_type.get_index_type(); @@ -262,8 +263,6 @@ string_exprt string_constraint_generatort::add_axioms_from_int( not_exprt(equal_exprt(res[1], zero_char))); axioms.push_back(a4); - assert(max_size::max()); - for(size_t size=1; size<=max_size; size++) { // For each possible size, we have: From eaad10007287ca7e56c4387ae2e52810af647596 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 26 Jun 2017 10:09:21 +0100 Subject: [PATCH 6/8] Comment on the bound for overflow in int to string conversion An overflow can happen when reaching the last index of a string of maximal size which is max_size for negative numbers and max_size - 1 for positive numbers because of the abscence of a `-` (minus) sign --- .../refinement/string_constraint_generator_valueof.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 8b15bf6cbdc..7416bc1a341 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -297,6 +297,10 @@ string_exprt string_constraint_generatort::add_axioms_from_int( binary_relation_exprt(res[j], ID_le, nine_char)); digit_constraints.push_back(is_number); + // An overflow can happen when reaching the last index of a string of + // maximal size which is `max_size` for negative numbers and + // `max_size - 1` for positive numbers because of the abscence of a `-` + // sign. if(j>=max_size-2) { // check for overflows if the size is big From 4440343e17fde94eee7cb13b05850d86f13b9e1b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 26 Jun 2017 11:22:34 +0100 Subject: [PATCH 7/8] Adding tests for String.valueOf(long) --- .../java_value_of_long/test.class | Bin 0 -> 738 bytes .../java_value_of_long/test.desc | 8 ++++++++ .../java_value_of_long/test.java | 17 +++++++++++++++++ 3 files changed, 25 insertions(+) create mode 100644 regression/strings-smoke-tests/java_value_of_long/test.class create mode 100644 regression/strings-smoke-tests/java_value_of_long/test.desc create mode 100644 regression/strings-smoke-tests/java_value_of_long/test.java diff --git a/regression/strings-smoke-tests/java_value_of_long/test.class b/regression/strings-smoke-tests/java_value_of_long/test.class new file mode 100644 index 0000000000000000000000000000000000000000..b559af818fb5ca1292d999a58f411fb5ee2a4f8a GIT binary patch literal 738 zcmY*X+foxj5IwWm&2Bauav@-hU?4_K&=4>23S~h7R%szT#Ij1>Cdo(*E*sqozu-5R zAK+Q70!yp(-3LF$XUnoDTozuYd*+<(KHWXP{(buappAJO8I%nm{W$pD`eWk~rcy{_ z+QMaZshF6tVWDhc)m*-yirS zt9d?x^r!+RZaBD!CPOZc-R$m&UU=@Q6Z+EIW-#}-8;Q*~3={R|jrBO@h_FCY5$_}J z28wV7K1#XJps{7+pcR*9%P`p&f%HZHR5Ohzj0m8?Zefw` o@4~76_DCp@FQgCP3}Nc~&=X%^#05@zQArGF&XVf5G^&5`Kbaqk(*OVf literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc new file mode 100644 index 00000000000..74c93ab1311 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_long/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--refine-strings +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 11 .* SUCCESS$ +assertion.* file test.java line 16 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_long/test.java b/regression/strings-smoke-tests/java_value_of_long/test.java new file mode 100644 index 00000000000..a9ceaa964a7 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_long/test.java @@ -0,0 +1,17 @@ +public class test +{ + public static void main(int i) + { + long l1=12345678901234L; + if(i == 0) + { + String s = String.valueOf(l1); + assert(s.equals("12345678901234")); + } + else + { + String s = String.valueOf(-l1); + assert(!s.equals("-12345678901234")); + } + } +} From 20f3951729940a97b9bac5dfe7cb054c36faa54b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 26 Jun 2017 15:00:02 +0100 Subject: [PATCH 8/8] Correction of line numbers in valueOf(long) test --- regression/strings-smoke-tests/java_value_of_long/test.desc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/strings-smoke-tests/java_value_of_long/test.desc b/regression/strings-smoke-tests/java_value_of_long/test.desc index 74c93ab1311..f96a114f708 100644 --- a/regression/strings-smoke-tests/java_value_of_long/test.desc +++ b/regression/strings-smoke-tests/java_value_of_long/test.desc @@ -3,6 +3,6 @@ test.class --refine-strings ^EXIT=10$ ^SIGNAL=0$ -assertion.* file test.java line 11 .* SUCCESS$ -assertion.* file test.java line 16 .* FAILURE$ +assertion.* file test.java line 9 .* SUCCESS$ +assertion.* file test.java line 14 .* FAILURE$ --