From 60183a3d44280cb6ac3fe88328741e803929304a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 10 Apr 2018 14:36:13 +0100
Subject: [PATCH 1/2] Assign string at malloc site

This is much more efficient than assigning to the object in the case the
object is an element of an array.
---
 src/java_bytecode/java_object_factory.cpp | 12 +++++++-----
 src/java_bytecode/java_object_factory.h   |  2 +-
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index cad25eb6a16..713ffd88566 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/src/java_bytecode/java_object_factory.cpp
@@ -248,7 +248,8 @@ exprt allocate_dynamic_object(
 /// \param symbol_table: symbol table
 /// \param loc: location in the source
 /// \param output_code: code block to which the necessary code is added
-void allocate_dynamic_object_with_decl(
+/// \return the dynamic object created
+exprt allocate_dynamic_object_with_decl(
   const exprt &target_expr,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,
@@ -257,8 +258,7 @@ void allocate_dynamic_object_with_decl(
   std::vector<const symbolt *> symbols_created;
   code_blockt tmp_block;
   const typet &allocate_type=target_expr.type().subtype();
-  // We will not use the malloc site and can safely ignore it
-  (void) allocate_dynamic_object(
+  const exprt dynamic_object = allocate_dynamic_object(
     target_expr,
     allocate_type,
     symbol_table,
@@ -278,6 +278,7 @@ void allocate_dynamic_object_with_decl(
 
   for(const exprt &code : tmp_block.operands())
     output_code.add(to_code(code));
+  return dynamic_object;
 }
 
 /// Installs a new symbol in the symbol table, pushing the corresponding symbolt
@@ -701,11 +702,12 @@ static bool add_nondet_string_pointer_initialization(
   if(!struct_type.has_component("data") || !struct_type.has_component("length"))
     return true;
 
-  allocate_dynamic_object_with_decl(expr, symbol_table, loc, code);
+  const exprt malloc_site =
+    allocate_dynamic_object_with_decl(expr, symbol_table, loc, code);
 
   code.add(
     initialize_nondet_string_struct(
-      dereference_exprt(expr, struct_type),
+      dereference_exprt(malloc_site, struct_type),
       max_nondet_string_length,
       loc,
       symbol_table,
diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h
index 7262f7dc652..9a5da141344 100644
--- a/src/java_bytecode/java_object_factory.h
+++ b/src/java_bytecode/java_object_factory.h
@@ -146,7 +146,7 @@ exprt allocate_dynamic_object(
   std::vector<const symbolt *> &symbols_created,
   bool cast_needed = false);
 
-void allocate_dynamic_object_with_decl(
+exprt allocate_dynamic_object_with_decl(
   const exprt &target_expr,
   symbol_table_baset &symbol_table,
   const source_locationt &loc,

From c2071069c953260f4f37304807af58b78698f4bb Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 11 Apr 2018 08:06:47 +0100
Subject: [PATCH 2/2] Test with array of strings

This checks that jbmc correctly analyze functions that take arrays of
strings as inputs.
With the changes assigning strings directly at malloc site, this example
can be analyzed by jbmc approximately 15 times faster.
---
 .../jbmc-strings/StringArray/Test.class       | Bin 0 -> 925 bytes
 regression/jbmc-strings/StringArray/Test.java |  26 ++++++++++++++++++
 regression/jbmc-strings/StringArray/test.desc |   8 ++++++
 3 files changed, 34 insertions(+)
 create mode 100644 regression/jbmc-strings/StringArray/Test.class
 create mode 100644 regression/jbmc-strings/StringArray/Test.java
 create mode 100644 regression/jbmc-strings/StringArray/test.desc

diff --git a/regression/jbmc-strings/StringArray/Test.class b/regression/jbmc-strings/StringArray/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..067f88236ecba04538c2bb0aa77f7f94c91773c8
GIT binary patch
literal 925
zcmZ`%TTc@~6#k~&Ten+!;a1d2RkSytTG7Om5Eb>sq7Nk|Vq&swC$O;Y*4?d%KSdsW
z@wIAFj3oF-;*TPp*;3j>&2G+|Irr~7^ZV@Q34k@+*O5d{!&ME78uB`>;d%@S+)%Nk
zLq$%-O&u}hgt#R{K}AtV31t-(hUq2K_qi8XuH!$ke6wZq4g=d^P}VKS3N{#`#nLMV
zY18d+hGfHX_>11V7WcMAFoWFQ<Lv{6Lh(&w-~3=!ZPVGUHUrOccI&0TO$>=<V73po
z%x+jg#WI7o-nP%%=}ouiwfQqk6pw9lKUfuI4P-FQpgTR=&YPZRek5<;x_N)k^#X=?
z=<vg~RMNl-Rt=<(X2_1mdNcz2)bm`AVSelyPW-rM*&Xf~sN%MPJE#$IF@uV`2GM<w
zAvI2U+1lrA>OEl^Rw4HI`<`k0470@v3Wf>wlAzb@cDX}buS^E~m$vh{>O@uGj+)FA
z|H*H1JmIEI>t&ehaNqKH=K?-$An1{UcDqAQCP9w~V5zJijI=12pqu0j-Ewp?I_2^a
z*jEvVS&~X<q%B|$^Q4Q=ABaGr^KJPQN+!}TpU9s{iT2CUny^ShX_TefR%LkrdE*<D
zLnJGwh#y0JeFW{-(31N!wj3iy9=$R^oO0p=7=7vx31_ImAYG=O3O#m}fM^6kOr&Fh
zZaGX5yfg|l-2=*ajx2qk7+KY{Gc2lDpr55F@6rX}wGbJQ&LjqyI)o~HffW4?MSveR
S9)TCdWJHXIf}+cz`^q2Pio*T?

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/StringArray/Test.java b/regression/jbmc-strings/StringArray/Test.java
new file mode 100644
index 00000000000..6b270b4a768
--- /dev/null
+++ b/regression/jbmc-strings/StringArray/Test.java
@@ -0,0 +1,26 @@
+public class Test {
+
+    public static String check(String[] array) {
+        // Filter
+        if(array == null)
+            return "null array";
+        if(array.length < 2)
+            return "too short";
+        if(array[0] == null)
+            return "null string";
+
+        // Arrange
+        String s0 = array[0];
+        String s1 = array[1];
+
+        // Act
+        boolean b = s0.equals(s1);
+
+        // Assert
+        assert(s0 != null);
+        assert(!b);
+
+        // Return
+        return s0 + s1;
+    }
+}
diff --git a/regression/jbmc-strings/StringArray/test.desc b/regression/jbmc-strings/StringArray/test.desc
new file mode 100644
index 00000000000..84195a84d46
--- /dev/null
+++ b/regression/jbmc-strings/StringArray/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --function Test.check --string-max-input-length 1000
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion\.1\].* line 20.* SUCCESS$
+^\[.*assertion\.2\].* line 21.* FAILURE$
+--