Merge pull request #5086 from smowton/smowton/fix/remove-buggy-to-code-point-function

Remove buggy model of Character.toCodePoint

Author: smowton

jbmc/regression/jbmc-strings/toCodePoint/Test.class

@@ -0,0 +1,10 @@
+public class Test {
+
+  public void test(char a, char b) {
+    assert Character.toCodePoint((char)0xD800, (char)0xDC00) == 0x10000;
+    assert Character.toCodePoint((char)0xDBFF, (char)0xDFFF) == 0x10ffff;
+    assert Character.toCodePoint((char)0xD800, (char)0xDFFF) == 0x103ff;
+    assert Character.toCodePoint((char)0xDBFF, (char)0xDC00) == 0x10fc00;
+    assert Character.toCodePoint(a, b) == 0x10000;
+  }
+}

jbmc/regression/jbmc-strings/toCodePoint/Test.java

@@ -0,0 +1,13 @@
+CORE
+Test.class
+--function Test.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^\[java::Test.test:\(CC\)V.assertion\.1\] line 4 .* SUCCESS$
+^\[java::Test.test:\(CC\)V.assertion\.2\] line 5 .* SUCCESS$
+^\[java::Test.test:\(CC\)V.assertion\.3\] line 6 .* SUCCESS$
+^\[java::Test.test:\(CC\)V.assertion\.4\] line 7 .* SUCCESS$
+^\[java::Test.test:\(CC\)V.assertion\.5\] line 8 .* FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

jbmc/regression/jbmc-strings/toCodePoint/test.desc

@@ -1155,34 +1155,6 @@ codet character_refine_preprocesst::convert_reverse_bytes(
     &character_refine_preprocesst::expr_of_reverse_bytes, 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
-codet character_refine_preprocesst::convert_to_code_point(
-  conversion_inputt &target)
-{
-  const code_function_callt &function_call=target;
-  assert(function_call.arguments().size()==2);
-  const exprt &arg0=function_call.arguments()[0];
-  const exprt &arg1=function_call.arguments()[1];
-  const exprt &result=function_call.lhs();
-  const typet &type=result.type();
-
-  // These operations implement the decoding of a unicode symbol encoded
-  // in UTF16 for the supplementary planes (above U+10000).
-  // The low ten bits of the first character give the bits 10 to 19 of
-  // code point and the low ten bits of the second give the bits 0 to 9,
-  // then 0x10000 is added to the result. For more explenations see:
-  //   https://en.wikipedia.org/wiki/UTF-16
-
-  exprt u010000=from_integer(0x010000, type);
-  exprt mask10bit=from_integer(0x03FF, type);
-  shl_exprt m1(bitand_exprt(arg0, mask10bit), from_integer(10, type));
-  bitand_exprt m2(arg1, mask10bit);
-  bitor_exprt pair_value(u010000, bitor_exprt(m1, m2));
-  return code_assignt(result, pair_value);
-}
-
 /// Converts the character argument to lowercase.
 ///
 ///    TODO: For now we only consider ASCII characters but ultimately
@@ -1481,8 +1453,6 @@ void character_refine_preprocesst::initialize_conversion_table()
 
   // Not supported "java::java.lang.Character.toChars:(I[CI)I"
 
-  conversion_table["java::java.lang.Character.toCodePoint:(CC)I"]=
-      &character_refine_preprocesst::convert_to_code_point;
   conversion_table["java::java.lang.Character.toLowerCase:(C)C"]=
       &character_refine_preprocesst::convert_to_lower_case_char;
   conversion_table["java::java.lang.Character.toLowerCase:(I)I"]=

jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -133,7 +133,6 @@ class character_refine_preprocesst
   static codet convert_reverse_bytes(conversion_inputt &target);
   static exprt expr_of_to_chars(const exprt &chr, const typet &type);
   static codet convert_to_chars(conversion_inputt &target);
-  static codet convert_to_code_point(conversion_inputt &target);
   static exprt expr_of_to_lower_case(const exprt &chr, const typet &type);
   static codet convert_to_lower_case_char(conversion_inputt &target);
   static codet convert_to_lower_case_int(conversion_inputt &target);