Merge pull request #2038 from romainbrenguier/bugfix/assign-at-malloc-site

[TG-3173] Assign Strings at malloc site in java object factory

Author: romainbrenguier

regression/jbmc-strings/StringArray/Test.class

@@ -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;
+    }
+}

regression/jbmc-strings/StringArray/Test.java

@@ -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$
+--

regression/jbmc-strings/StringArray/test.desc

@@ -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,

src/java_bytecode/java_object_factory.cpp

@@ -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,