From c6c9368a0099f12ca6283ca16ae8523e207948e3 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 12 Apr 2019 17:07:27 +0100
Subject: [PATCH] Remove Character.toChars, highSurrogate, lowSurrogate models

Character.toChars was malformed (it tried to address a java::array[char] * like it was
a raw char[], and tried to return an if_exprt of two arrays of differing type), and there
is already an implementation in the models library with a perfectly good implementation.

Character.highSurrogate and lowSurrogate were type unsound (creating additions of mixed type).
Again, they add nothing on top of the shipped models library.
---
 .../jbmc-strings/CharacterToChars/C.class     | Bin 0 -> 960 bytes
 .../jbmc-strings/CharacterToChars/C.java      |  20 +++++++
 .../CharacterToChars/should_fail.desc         |  10 ++++
 .../jbmc-strings/CharacterToChars/test.desc   |   8 +++
 .../character_refine_preprocess.cpp           |  56 ------------------
 5 files changed, 38 insertions(+), 56 deletions(-)
 create mode 100644 jbmc/regression/jbmc-strings/CharacterToChars/C.class
 create mode 100644 jbmc/regression/jbmc-strings/CharacterToChars/C.java
 create mode 100644 jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc
 create mode 100644 jbmc/regression/jbmc-strings/CharacterToChars/test.desc

diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/C.class b/jbmc/regression/jbmc-strings/CharacterToChars/C.class
new file mode 100644
index 0000000000000000000000000000000000000000..6763c2bc8f0b993504a08e1208cd9955cd1f1410
GIT binary patch
literal 960
zcmaKpOK;Oa6ot?D5ht!oQYYz)M;{bOn$m*g9TlPqR3N3WD5^w}K#pS(7ZX>u17gST
z=!PY0K%xkwvga4DV9l?n5NDE*Myga>8qd8x_s)0b{`~vx2!MlC6JwY&F^`2Da#%EQ
z*@T8U6#`I!Uvl{k14|~Z;HrUZ0>vdaN&GksqE2!*NZe-Vw*<tlKxRGY1nF%7wNl*?
z(CSgk7sxk)j{mUxs_Dm%rC7jjM4lV&xN#ukK~hWGLBi5T{T548KS|lt6HuPk1#;<|
z=y~%kvjXGWsq4Mma`$_M2Brkeq#bp`)}|YT0@-yh9B`Q1Q8)Jd%|M=-sju$2uU!l0
zkT+1VP{pzZ3*!RQ^2b`}c3!M){P%V*j-!|ebptgEE4VIDIFUVS?)e@Gizlgi+l^f>
z^;u-3k&FndR~}TQf&7Rr<oyXuw)`ZB{nqe6+Dg0f1}fEEEN~iQ9FZtYOGNH8j)de~
z3yjwI<%pm!A3}WOM!^KvOfShB=HBWHP(+E5KzUgFhic9h-RxH=jZaVyFi|_w-ec@L
zv?qtqfAn&8O?9#(NjpRNR$snyq>udR<%%n+V;iTlnq!Z4k+5nHb`e?bHRyb2h`!3$
zq3`=J@r>?MT98KO`>+EeI`%P%DH?LHfobj(R)Zb&W6T(sE%iU;G9~ASp5IZXP<FFW
zI@5HKrVFhR7bm<nS;2-GPGFYj-5{Oho9s6p@MTaN@JXs1lw-`2s!VeihBOY@<TGLC
ezQ8<yp?!d+eujE_l(LHs#kwO0evyHKOaB1!yQYx<

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/C.java b/jbmc/regression/jbmc-strings/CharacterToChars/C.java
new file mode 100644
index 00000000000..13b0a4c6c29
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/CharacterToChars/C.java
@@ -0,0 +1,20 @@
+public class C {
+
+    public void test() {
+        char[] c = Character.toChars(5);
+        assert c.length == 1;
+        assert c[0] == 5;
+
+        char[] two_bytes = Character.toChars(0x10000);
+        assert two_bytes.length == 2;
+        assert two_bytes[0] == '\ud800';
+        assert two_bytes[1] == '\udc00';
+    }
+
+    public void shouldFail() {
+        char[] c = Character.toChars(20);
+        assert c.length == 1;
+        assert c[0] == 100;
+    }
+
+}
diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc b/jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc
new file mode 100644
index 00000000000..9576aaffcef
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/CharacterToChars/should_fail.desc
@@ -0,0 +1,10 @@
+CORE
+C.class
+--function C.shouldFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::C\.shouldFail:\(\)V\.assertion.1\] line 16 assertion at file C\.java line 16 function java::C\.shouldFail:\(\)V bytecode-index 12: SUCCESS
+\[java::C\.shouldFail:\(\)V\.assertion.2\] line 17 assertion at file C\.java line 17 function java::C\.shouldFail:\(\)V bytecode-index 23: FAILURE
+--
+^warning: ignoring
diff --git a/jbmc/regression/jbmc-strings/CharacterToChars/test.desc b/jbmc/regression/jbmc-strings/CharacterToChars/test.desc
new file mode 100644
index 00000000000..bdfb1ce7ebe
--- /dev/null
+++ b/jbmc/regression/jbmc-strings/CharacterToChars/test.desc
@@ -0,0 +1,8 @@
+CORE
+C.class
+--function C.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
index 130f0b4fa5e..cf242141a71 100644
--- a/jbmc/src/java_bytecode/character_refine_preprocess.cpp
+++ b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
@@ -321,15 +321,6 @@ exprt character_refine_preprocesst::expr_of_high_surrogate(
   return std::move(high_surrogate);
 }
 
-/// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.highSurrogate:(C)Z
-codet character_refine_preprocesst::convert_high_surrogate(
-  conversion_inputt &target)
-{
-  return convert_char_function(
-    &character_refine_preprocesst::expr_of_high_surrogate, target);
-}
-
 /// Determines if the specified character is an ASCII lowercase character.
 /// \param chr: An expression of type character
 /// \param type: A type for the output
@@ -1141,16 +1132,6 @@ exprt character_refine_preprocesst::expr_of_low_surrogate(
   return plus_exprt(uDC00, mod_exprt(chr, u0400));
 }
 
-/// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.lowSurrogate:(I)C
-/// \param target: a position in a goto program
-codet character_refine_preprocesst::convert_low_surrogate(
-  conversion_inputt &target)
-{
-  return convert_char_function(
-    &character_refine_preprocesst::expr_of_low_surrogate, target);
-}
-
 /// Returns the value obtained by reversing the order of the bytes in the
 /// specified char value.
 /// \param chr: An expression of type character
@@ -1174,37 +1155,6 @@ codet character_refine_preprocesst::convert_reverse_bytes(
     &character_refine_preprocesst::expr_of_reverse_bytes, target);
 }
 
-/// Converts the specified character (Unicode code point) to its UTF-16
-/// representation stored in a char array. If the specified code point is a BMP
-/// (Basic Multilingual Plane or Plane 0) value, the resulting char array has
-/// the same value as codePoint. If the specified code point is a supplementary
-/// code point, the resulting char array has the corresponding surrogate pair.
-/// \param chr: An expression of type character
-/// \param type: A type for the output
-/// \return A character array expression of the given type
-exprt character_refine_preprocesst::expr_of_to_chars(
-  const exprt &chr, const typet &type)
-{
-  array_typet array_type=to_array_type(type);
-  const typet &char_type=array_type.subtype();
-  exprt low_surrogate=expr_of_low_surrogate(chr, char_type);
-  array_exprt case1({low_surrogate}, array_type);
-  exprt high_surrogate = expr_of_high_surrogate(chr, char_type);
-  array_exprt case2(
-    {std::move(low_surrogate), std::move(high_surrogate)}, array_type);
-  return if_exprt(
-    expr_of_is_bmp_code_point(chr, type), std::move(case1), std::move(case2));
-}
-
-/// Converts function call to an assignment of an expression corresponding to
-/// the java method Character.toChars:(I)[C
-/// \param target: a position in a goto program
-codet character_refine_preprocesst::convert_to_chars(conversion_inputt &target)
-{
-  return convert_char_function(
-    &character_refine_preprocesst::expr_of_to_chars, target);
-}
-
 /// Converts function call to an assignment of an expression corresponding to
 /// the java method Character.toCodePoint:(CC)I
 /// \param target: a position in a goto program
@@ -1433,8 +1383,6 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_get_type_int;
   conversion_table["java::java.lang.Character.hashCode:()I"]=
       &character_refine_preprocesst::convert_hash_code;
-  conversion_table["java::java.lang.Character.highSurrogate:(I)C"]=
-      &character_refine_preprocesst::convert_high_surrogate;
   conversion_table["java::java.lang.Character.isAlphabetic:(I)Z"]=
       &character_refine_preprocesst::convert_is_alphabetic;
   conversion_table["java::java.lang.Character.isBmpCodePoint:(I)Z"]=
@@ -1523,8 +1471,6 @@ void character_refine_preprocesst::initialize_conversion_table()
       &character_refine_preprocesst::convert_is_whitespace_char;
   conversion_table["java::java.lang.Character.isWhitespace:(I)Z"]=
       &character_refine_preprocesst::convert_is_whitespace_int;
-  conversion_table["java::java.lang.Character.lowSurrogate:(I)C"]=
-      &character_refine_preprocesst::convert_is_low_surrogate;
 
   // Not supported "java::java.lang.Character.offsetByCodePoints:([CIIII)I"
   // Not supported "java::java.lang.Character.offsetByCodePoints:"
@@ -1532,8 +1478,6 @@ void character_refine_preprocesst::initialize_conversion_table()
 
   conversion_table["java::java.lang.Character.reverseBytes:(C)C"]=
       &character_refine_preprocesst::convert_reverse_bytes;
-  conversion_table["java::java.lang.Character.toChars:(I)[C"]=
-      &character_refine_preprocesst::convert_to_chars;
 
   // Not supported "java::java.lang.Character.toChars:(I[CI)I"