From 6a156a9f6258302a6deea52e8a3bcf5d0bb30756 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Jun 2017 14:17:27 +0100
Subject: [PATCH 1/3] Making toLowerCase more precise

We extend add_axioms_for_to_lower_case by taking into account latin
characters up to u00FF and adding in the lemmas the property that the
characters should not exceed u00FF, making the axioms correct (we will
not generate wrong assertion violation) but incomplete (we may miss
cases involving characters beyond u00FF).
---
 ...ng_constraint_generator_transformation.cpp | 46 ++++++++++++-------
 1 file changed, 30 insertions(+), 16 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index 599ae3af9dd..55eb79bbdb9 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -216,34 +216,48 @@ string_exprt string_constraint_generatort::add_axioms_for_to_lower_case(
   string_exprt res=fresh_string(ref_type);
   exprt char_a=constant_char('a', char_type);
   exprt char_A=constant_char('A', char_type);
-  exprt char_z=constant_char('z', char_type);
-  exprt char_Z=constant_char('Z', char_type);
 
-  // TODO: add support for locales using case mapping information
-  // from the UnicodeData file.
+  // TODO: for now, only characters in Basic Latin and Latin-1 supplement
+  // are supported (up to 0x100), we should add others using case mapping
+  // information from the UnicodeData file.
 
   // We add axioms:
   // a1 : |res| = |str|
-  // a2 : forall idx<str.length, 'A'<=str[idx]<='Z' => res[idx]=str[idx]+'a'-'A'
-  // a3 : forall idx<str.length, !('a'<=str[idx]<='z') => res[idx]=str[idx]
-  // forall idx<str.length,
-  // this[idx]='A'<=str[idx]<='Z' ? str[idx]+'a'-'A' : str[idx]
+  // a2 : forall idx<str.length,
+  //   is_upper_case(str[idx])?
+  //      res[idx]=str[idx]+'a'-'A' : res[idx]=str[idx]<0x100
 
   exprt a1=res.axiom_for_has_same_length_as(str);
   axioms.push_back(a1);
 
   symbol_exprt idx=fresh_univ_index("QA_lower_case", index_type);
-  exprt is_upper_case=and_exprt(
+  exprt::operandst upper_case;
+  upper_case.push_back(and_exprt(
     binary_relation_exprt(char_A, ID_le, str[idx]),
-    binary_relation_exprt(str[idx], ID_le, char_Z));
-  minus_exprt diff(char_a, char_A);
-  equal_exprt convert(res[idx], plus_exprt(str[idx], diff));
-  string_constraintt a2(idx, res.length(), is_upper_case, convert);
+    binary_relation_exprt(str[idx], ID_le, from_integer('Z', char_type))));
+
+  upper_case.push_back(and_exprt(
+    binary_relation_exprt(from_integer(0xc0, char_type), ID_le, str[idx]),
+    binary_relation_exprt(str[idx], ID_le, from_integer(0xd6, char_type))));
+
+  upper_case.push_back(and_exprt(
+    binary_relation_exprt(from_integer(0xd8, char_type), ID_le, str[idx]),
+    binary_relation_exprt(str[idx], ID_le, from_integer(0xde, char_type))));
+
+  exprt is_upper_case=disjunction(upper_case);
+
+  // The difference between upper-case and lower-case for the basic latin and
+  // latin-1 supplement is 0x20.
+  exprt diff=from_integer(0x20, char_type);
+  equal_exprt converted(res[idx], plus_exprt(str[idx], diff));
+  and_exprt non_converted(
+    equal_exprt(res[idx], str[idx]),
+    binary_relation_exprt(str[idx], ID_lt, from_integer(0x100, char_type)));
+  if_exprt conditional_convert(is_upper_case, converted, non_converted);
+
+  string_constraintt a2(idx, res.length(), conditional_convert);
   axioms.push_back(a2);
 
-  equal_exprt eq(res[idx], str[idx]);
-  string_constraintt a3(idx, res.length(), not_exprt(is_upper_case), eq);
-  axioms.push_back(a3);
   return res;
 }
 

From 5553652efd7c1ddc4213e733d198ea39b3649e0f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Jun 2017 14:22:59 +0100
Subject: [PATCH 2/3] Improving the test for Java case functions

We make it more precise by having some assertion that should hold and
some that should fail.
We also test some non ascii (but in latin-1 supplement) characters.
---
 .../strings-smoke-tests/java_case/test.desc   |   9 +++--
 .../java_case/test_case.class                 | Bin 865 -> 1019 bytes
 .../java_case/test_case.java                  |  33 +++++++++++++-----
 3 files changed, 31 insertions(+), 11 deletions(-)

diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc
index 9a254ae3484..d2508fa3489 100644
--- a/regression/strings-smoke-tests/java_case/test.desc
+++ b/regression/strings-smoke-tests/java_case/test.desc
@@ -1,7 +1,12 @@
 CORE
 test_case.class
 --refine-strings
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+assertion.* file test_case.java line 10 .* SUCCESS$
+assertion.* file test_case.java line 11 .* SUCCESS$
+assertion.* file test_case.java line 12 .* SUCCESS$
+assertion.* file test_case.java line 16 .* FAILURE$
+assertion.* file test_case.java line 20 .* SUCCESS$
+assertion.* file test_case.java line 24 .* FAILURE$
 --
diff --git a/regression/strings-smoke-tests/java_case/test_case.class b/regression/strings-smoke-tests/java_case/test_case.class
index 9f7eaab446cd3578f404528b7c77e09fc18c5ab9..863da75113c20863de00fa0169902a184502cd74 100644
GIT binary patch
delta 645
zcmYL`O-~b16o#KWZD*#_DQyR6YY`AX_$swkDvDp|#*b)afts+<OdCQJLX0#n+|-?J
zNfQ&g>JAeZMvc=%j4o#9k1+9fm=Mp50?FjP=icX@_uO;lxBka?@N@6$cc99GML%N(
z$4yRHXq*h>R3PJVGEA6E2Ae5^X$y-nlcLE?a8xomZBjO<Se)Uk!R*%JoqTli_S8c~
za;fPy)@tsv`)+-GMeMiU7w5C&6zQk#3%9)PZmgD<n$MqXtSYqYb(<_zn{&+BoDXDx
zK>@CS3(U7uYNB+JOA6C}<-hjd_-})->+ksQd`}T?u530RH{4CBblK(#SKBr9tCf+~
zK&A76n?w<ml*x(aWj8FVk~KEnLwyV`azs=Q55<!LLlVnXm6Oz{FmD%a*@^Us-Yt5>
zY9ji*LbS`RPZ%8rW*pNa-XXDzwcKle)8eYs{-6!E){0Kjqpw3fBqV+mVqFSh)?&%A
zC2N}-2TboW60%t*C3T#1=sLd7LzF*6+y4uSZP14n_Ay6N;+Xt1omL7%W?%}isF2_$
zHjn6|L7JC1w1jq~)i2WYQAz7Z-=ktM{O`+VheivMK5{U;YB(jxI2jM8gAv^!8u^TI
W_<;REieE<Fq1o4hd5?w<JoXnFn`tZn

delta 493
zcmYk2O-~w86o#KW1KeR41V%*K3e~n&WmNp2A9mHcwZ?_*0yoV_h_QZz2yyFgFzi^l
zbFC)Oltf+kM>Og0XkvOUrnbq=d+$B(Iq!MT`K^D&Hh$cFzXmG2bIDNDJarg%v6wLM
z%)s+FDPA~Cn$Jtkl#5HzVcKEFgi4ygWtKV3{ORYlOmedo*7nxJ#;0(5zb=ZW--4Aa
zBZ~Cb@Hi~*hle}m&DPQG;f})ku<enh?6JV2$C3e`VIe{xmZ`MI)YRxJUMu3Qdb9PV
z7B)rmjmKM7+70#dASJ#*rSqmvUN%YuM+9^7E6A<nj+T0;3zNvGU~CW+P4W+^XHsel
zx7Ek0`gV`VTB%F)qd;u^65Syiv~R84$*k{niFZi!ajQKNH}_=8Pj(slFKpUbgLXx<
zyrZ(WnCw!EKZih?uS%p!f=9xpvF`{pkMB<|Cpk|Z%vA=4A>*eiUD6$N<eZ3oh5py&
S?@&f9isijGqmK<t6#f9b#6n5{

diff --git a/regression/strings-smoke-tests/java_case/test_case.java b/regression/strings-smoke-tests/java_case/test_case.java
index b3437a6f83e..088ee70803e 100644
--- a/regression/strings-smoke-tests/java_case/test_case.java
+++ b/regression/strings-smoke-tests/java_case/test_case.java
@@ -1,12 +1,27 @@
 public class test_case
 {
-   public static void main(/*String[] argv*/)
-   {
-      String s = new String("Ab");
-      String l = s.toLowerCase();
-      String u = s.toUpperCase();
-      assert(l.equals("ab"));
-      assert(u.equals("AB"));
-      assert(s.equalsIgnoreCase("aB"));
-   }
+    public static void main(int i)
+    {
+        String s = new String("Ab");
+        String l = s.toLowerCase();
+        String u = s.toUpperCase();
+        if(i==1)
+        {
+            assert(l.equals("ab"));
+            assert(u.equals("AB"));
+            assert(s.equalsIgnoreCase("aB"));
+        }
+        else if(i==2)
+        {
+            assert(!u.equals("AB"));
+        }
+        else if(i==3)
+        {
+            assert("ÖÇ".toLowerCase().equals("öç"));
+        }
+        else
+        {
+            assert(!"ÖÇ".toLowerCase().equals("öç"));
+        }
+    }
 }

From 695b3ce4aadcbfee2de145f0b5618b0e4ea66458 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 20 Jun 2017 17:19:19 +0100
Subject: [PATCH 3/3] Add comments about characters transformed by toLowerCase

---
 ...tring_constraint_generator_transformation.cpp | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index 55eb79bbdb9..bde386d3eda 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -214,8 +214,9 @@ string_exprt string_constraint_generatort::add_axioms_for_to_lower_case(
   const typet &char_type=ref_type.get_char_type();
   const typet &index_type=ref_type.get_index_type();
   string_exprt res=fresh_string(ref_type);
-  exprt char_a=constant_char('a', char_type);
-  exprt char_A=constant_char('A', char_type);
+  const exprt char_A=constant_char('A', char_type);
+  const exprt char_Z=constant_char('Z', char_type);
+
 
   // TODO: for now, only characters in Basic Latin and Latin-1 supplement
   // are supported (up to 0x100), we should add others using case mapping
@@ -225,21 +226,28 @@ string_exprt string_constraint_generatort::add_axioms_for_to_lower_case(
   // a1 : |res| = |str|
   // a2 : forall idx<str.length,
   //   is_upper_case(str[idx])?
-  //      res[idx]=str[idx]+'a'-'A' : res[idx]=str[idx]<0x100
+  //      res[idx]=str[idx]+diff : res[idx]=str[idx]<0x100
+  // where diff is the difference between lower case and upper case characters:
+  // diff = 'a'-'A' = 0x20
 
   exprt a1=res.axiom_for_has_same_length_as(str);
   axioms.push_back(a1);
 
   symbol_exprt idx=fresh_univ_index("QA_lower_case", index_type);
   exprt::operandst upper_case;
+  // Characters between 'A' and 'Z' are upper-case
   upper_case.push_back(and_exprt(
     binary_relation_exprt(char_A, ID_le, str[idx]),
-    binary_relation_exprt(str[idx], ID_le, from_integer('Z', char_type))));
+    binary_relation_exprt(str[idx], ID_le, char_Z)));
 
+  // Characters between 0xc0 (latin capital A with grave)
+  // and 0xd6 (latin capital O with diaeresis) are upper-case
   upper_case.push_back(and_exprt(
     binary_relation_exprt(from_integer(0xc0, char_type), ID_le, str[idx]),
     binary_relation_exprt(str[idx], ID_le, from_integer(0xd6, char_type))));
 
+  // Characters between 0xd8 (latin capital O with stroke)
+  // and 0xde (latin capital thorn) are upper-case
   upper_case.push_back(and_exprt(
     binary_relation_exprt(from_integer(0xd8, char_type), ID_le, str[idx]),
     binary_relation_exprt(str[idx], ID_le, from_integer(0xde, char_type))));