From af958f02dbc04a978651ca40eb676389b38c453b Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 26 Mar 2018 10:21:09 +0100
Subject: [PATCH 1/2] Correct length field of string literals

The length was initialized before the string was converted to utf-16
sometimes giving incorrect result. For instance for "\u0000" the length
was set to 2 instead of 1.
---
 src/java_bytecode/java_string_literals.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_string_literals.cpp b/src/java_bytecode/java_string_literals.cpp
index 5ec35ac0d6e..ca6832b4f2c 100644
--- a/src/java_bytecode/java_string_literals.cpp
+++ b/src/java_bytecode/java_string_literals.cpp
@@ -106,6 +106,9 @@ symbol_exprt get_or_create_string_literal_symbol(
   // contents as well:
   if(string_refinement_enabled)
   {
+    const array_exprt data =
+      utf16_to_array(utf8_to_utf16_little_endian(id2string(value)));
+
     struct_exprt literal_init(new_symbol.type);
     literal_init.operands().resize(jls_struct.components().size());
     const std::size_t jlo_nb = jls_struct.component_number("@java.lang.Object");
@@ -113,7 +116,7 @@ symbol_exprt get_or_create_string_literal_symbol(
 
     const std::size_t length_nb = jls_struct.component_number("length");
     const typet &length_type = jls_struct.components()[length_nb].type();
-    const exprt length = from_integer(id2string(value).size(), length_type);
+    const exprt length = from_integer(data.operands().size(), length_type);
     literal_init.operands()[length_nb] = length;
 
     // Initialize the string with a constant utf-16 array:
@@ -127,8 +130,7 @@ symbol_exprt get_or_create_string_literal_symbol(
     // These are basically const global data:
     array_symbol.is_static_lifetime = true;
     array_symbol.is_state_var = true;
-    array_symbol.value =
-      utf16_to_array(utf8_to_utf16_little_endian(id2string(value)));
+    array_symbol.value = data;
     array_symbol.type = array_symbol.value.type();
 
     if(symbol_table.add(array_symbol))

From 56c9c02e03fb363b1f0df77afc85226abcc3c8d6 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 26 Mar 2018 10:43:10 +0100
Subject: [PATCH 2/2] Add test for string literals length

---
 regression/jbmc-strings/literal-length/Test.class | Bin 0 -> 623 bytes
 regression/jbmc-strings/literal-length/Test.java  |  12 ++++++++++++
 regression/jbmc-strings/literal-length/test.desc  |   7 +++++++
 3 files changed, 19 insertions(+)
 create mode 100644 regression/jbmc-strings/literal-length/Test.class
 create mode 100644 regression/jbmc-strings/literal-length/Test.java
 create mode 100644 regression/jbmc-strings/literal-length/test.desc

diff --git a/regression/jbmc-strings/literal-length/Test.class b/regression/jbmc-strings/literal-length/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c05034ce3ea7ba648b8365e6055aec3410267545
GIT binary patch
literal 623
zcmY*WOHbQC5dOxGY-~&u5+1>ATA-At1Q!k*C<5`2kSH92D#6WhR>5GL%66(A`#W-h
z8y7CL5=c}6&itmTV%88)wbJbDeBaD`GyCxG<`%#LCT&<4%A;aIVAzI>w*v2Mm>3eM
z+IWu-0waX-xR)d{PJ>pItOto#4`qWu2ZY>G5C!QnL7$rbN-)-14M`|$2a()qpVVc%
zr^p1;Ka~D46Q;JNw+Owp)bo$Oc;7NuV3d$w^26s^cCFQpeYqK^Olwaj>D-a`-E-ie
zm!RGMbYP>0vmA`!BcY<u`Ou4+^Q&E*8*$u<xu41w7<cdq6NKU`bGLpZ{q(<3EscYy
z$wP%QYNm(TP%O6anzR=3A_#*GnFO(HymaGn(l!IUg#(Q8GA-UO6)Q?7dpbyIXZwa<
zRlbRDbLJX!sfZ}B&1FFz7)A84uc$wu@c}-Uv~9P8;a|`@n47(VVVq*(56t~*<nCPK
z>=`O&&>4EVka}Nm0WE9caucOS=N}gASJ{psk44s5V#I>>7gd3>%fbE^!3&u(psysZ
ekncbk=P>l&(3SY7%3blQiV4kGQ6mmy@Zcki@o&ih

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/literal-length/Test.java b/regression/jbmc-strings/literal-length/Test.java
new file mode 100644
index 00000000000..14edc379387
--- /dev/null
+++ b/regression/jbmc-strings/literal-length/Test.java
@@ -0,0 +1,12 @@
+public class Test {
+    public static int check(int i) {
+        String s = "\u0000";
+
+        if (i == 0)
+            assert(s.length() == 1);
+        else if (i == 1)
+            assert(s.length() != 1);
+
+        return s.length();
+    }
+}
diff --git a/regression/jbmc-strings/literal-length/test.desc b/regression/jbmc-strings/literal-length/test.desc
new file mode 100644
index 00000000000..c9e7816e08c
--- /dev/null
+++ b/regression/jbmc-strings/literal-length/test.desc
@@ -0,0 +1,7 @@
+CORE
+Test.class
+--refine-strings  --function Test.check
+assertion at file Test.java line 6 .* SUCCESS
+assertion at file Test.java line 8 .* FAILURE
+^EXIT=10$
+^SIGNAL=0$