Implement constant propagation of ID_cprover_string_concat_func

This is required to allow constant propagation of StringBuilder.append() and
String concatenation with +.

Author: danpoe

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation/Main.class

@@ -0,0 +1,8 @@
+public class Main {
+    public void test() {
+        StringBuilder sb = new StringBuilder("abc");
+        sb.append("xyz");
+        String s = sb.toString();
+        assert s.startsWith("abcxyz");
+    }
+}

jbmc/regression/jbmc-strings/StringBuilderAppendConstantEvaluation/Main.java

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,8 @@
+public class Main {
+    public void test() {
+        String s1 = "abc";
+        String s2 = "xyz";
+        String s3 = s1 + s2;
+        assert s3.startsWith("abcxyz");
+    }
+}

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation/Main.class

@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.test --property "java::Main.test:()V.assertion.1"
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/StringConcatenationConstantEvaluation/Main.java

@@ -444,6 +444,55 @@ bool symex_assignt::constant_propagate_empty_string(
   return true;
 }
 
+bool symex_assignt::constant_propagate_concat(
+  const function_application_exprt &f_l1,
+  const function_application_exprt &f_l2)
+{
+  const refined_string_exprt &s1 = to_string_expr(f_l2.arguments().at(2));
+  const auto s1_data_opt = try_get_string_data_array(s1, ns);
+
+  if(!s1_data_opt)
+    return false;
+
+  const array_exprt &s1_data = s1_data_opt->get();
+
+  const refined_string_exprt &s2 = to_string_expr(f_l2.arguments().at(3));
+  const auto s2_data_opt = try_get_string_data_array(s2, ns);
+
+  if(!s2_data_opt)
+    return false;
+
+  const array_exprt &s2_data = s2_data_opt->get();
+
+  const std::size_t new_size =
+    s1_data.operands().size() + s2_data.operands().size();
+
+  const constant_exprt new_char_array_length =
+    from_integer(new_size, length_type);
+
+  array_typet new_char_array_type(
+    char_type,
+    new_char_array_length);
+
+  exprt::operandst operands(s1_data.operands());
+  operands.insert(
+    operands.end(),
+    s2_data.operands().begin(),
+    s2_data.operands().end());
+
+  array_exprt new_char_array(
+    std::move(operands),
+    new_char_array_type);
+
+  assign_constants(
+    to_ssa_expr(f_l1.arguments().at(0)),
+    new_char_array_length,
+    to_ssa_expr(f_l1.arguments().at(1)),
+    new_char_array);
+
+  return true;
+}
+
 void symex_assignt::assign_non_struct_symbol(
   const ssa_exprt &lhs, // L1
   const expr_skeletont &full_lhs,
@@ -493,7 +542,11 @@ void symex_assignt::assign_non_struct_symbol(
 
         int ret = false;
 
-        if(func_id == ID_cprover_string_empty_string_func)
+        if(func_id == ID_cprover_string_concat_func)
+        {
+          ret = constant_propagate_concat(f_l1, f_l2);
+        }
+        else if(func_id == ID_cprover_string_empty_string_func)
         {
           ret = constant_propagate_empty_string(f_l1);
         }

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

@@ -119,6 +119,10 @@ class symex_assignt
   bool constant_propagate_empty_string(
     const function_application_exprt &f_l1);
 
+  bool constant_propagate_concat(
+    const function_application_exprt &f_l1,
+    const function_application_exprt &f_l2);
+
   void assign_constants(
     const ssa_exprt &length,
     const constant_exprt &new_length,

src/goto-symex/symex_assign.cpp

@@ -64,11 +64,6 @@ struct simplify_expr_cachet
 simplify_expr_cachet simplify_expr_cache;
 #endif
 
-static optionalt<std::reference_wrapper<const array_exprt>>
-try_get_string_data_array(
-  const refined_string_exprt &s,
-  const namespacet &ns);
-
 simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
 {
   if(expr.op().is_constant())
@@ -1924,7 +1919,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
 /// \return array expression representing the char sequence which forms the
 ///   content of the refined string expression, empty optional if the content
 ///   cannot be determined
-static optionalt<std::reference_wrapper<const array_exprt>>
+optionalt<std::reference_wrapper<const array_exprt>>
   try_get_string_data_array(
     const refined_string_exprt &s,
     const namespacet &ns)

src/goto-symex/symex_assign.h

@@ -10,8 +10,12 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_SIMPLIFY_EXPR_H
 #define CPROVER_UTIL_SIMPLIFY_EXPR_H
 
+class array_exprt;
 class exprt;
 class namespacet;
+class refined_string_exprt;
+
+#include <util/optional.h>
 
 //
 // simplify an expression
@@ -27,4 +31,9 @@ bool simplify(
 // this is the preferred interface
 exprt simplify_expr(exprt src, const namespacet &ns);
 
+optionalt<std::reference_wrapper<const array_exprt>>
+try_get_string_data_array(
+  const refined_string_exprt &s,
+  const namespacet &ns);
+
 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_H