Implement constant propagation for substring operations

This implements constant propagation of ID_cprover_string_substring_func
function application expressions. These are in turn used by the various
substring operations of String and StringBuilder.

Author: danpoe

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

@@ -0,0 +1,25 @@
+public class Main {
+  public void test() {
+    StringBuilder sb = new StringBuilder("abc");
+
+    String s1 = sb.substring(0);
+    assert s1.length() == 3;
+    assert s1.startsWith("abc");
+
+    String s2 = sb.substring(1);
+    assert s2.length() == 2;
+    assert s2.startsWith("bc");
+
+    String s3 = sb.substring(0, 3);
+    assert s3.length() == 3;
+    assert s3.startsWith("abc");
+
+    String s4 = sb.substring(0, 0);
+    assert s4.length() == 0;
+    assert s4.startsWith("");
+
+    String s5 = sb.substring(0, 1);
+    assert s5.length() == 1;
+    assert s5.startsWith("a");
+  }
+}

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

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,14 @@
+public class Main {
+  public void test(StringBuilder sb1, int i) {
+    StringBuilder sb2 = new StringBuilder("abc");
+
+    String s1 = sb1.substring(0);
+    assert s1.startsWith("xyz");
+
+    String s2 = sb2.substring(i);
+    assert s2.startsWith("xyz");
+
+    String s3 = sb1.substring(i);
+    assert s3.startsWith("xyz");
+  }
+}

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

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test --property "java::Main.test:(Ljava/lang/StringBuilder;I)V.assertion.1" --show-vcc
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test --property "java::Main.test:(Ljava/lang/StringBuilder;I)V.assertion.2" --show-vcc
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test --property "java::Main.test:(Ljava/lang/StringBuilder;I)V.assertion.3" --show-vcc
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc

@@ -0,0 +1,20 @@
+public class Main {
+  public void test() {
+    String s = "abc";
+
+    String s1 = s.substring(0);
+    assert s1.equals("abc");
+
+    String s2 = s.substring(1);
+    assert s2.equals("bc");
+
+    String s3 = s.substring(0, 3);
+    assert s3.equals("abc");
+
+    String s4 = s.substring(0, 0);
+    assert s4.equals("");
+
+    String s5 = s.substring(0, 1);
+    assert s5.equals("a");
+  }
+}

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

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

@@ -0,0 +1,14 @@
+public class Main {
+  public void test(String s1, int i) {
+    String s2 = "abc";
+
+    String s3 = s1.substring(0);
+    assert s3.startsWith("xyz");
+
+    String s4 = s2.substring(i);
+    assert s4.startsWith("xyz");
+
+    String s5 = s1.substring(i);
+    assert s5.startsWith("xyz");
+  }
+}

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

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test:(Ljava/lang/String;I)V.assertion.1" --show-vcc
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test:(Ljava/lang/String;I)V.assertion.2" --show-vcc
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test:(Ljava/lang/String;I)V.assertion.3" --show-vcc
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -140,6 +140,11 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
         constant_propagate_empty_string(state, symex_assign, f_l1);
         return true;
       }
+      else if(func_id == ID_cprover_string_substring_func)
+      {
+        return constant_propagate_string_substring(
+          state, symex_assign, f_l1, f_l2);
+      }
     }
   }
 
@@ -287,3 +292,90 @@ bool goto_symext::constant_propagate_string_concat(
 
   return true;
 }
+
+bool goto_symext::constant_propagate_string_substring(
+  statet &state,
+  symex_assignt &symex_assign,
+  const function_application_exprt &f_l1,
+  const function_application_exprt &f_l2)
+{
+  const std::size_t num_operands = f_l1.arguments().size();
+
+  PRECONDITION(num_operands >= 4);
+  PRECONDITION(num_operands <= 5);
+
+  const auto &f_type = to_mathematical_function_type(f_l1.function().type());
+  const auto &length_type = f_type.domain().at(0);
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+
+  const refined_string_exprt &s = to_string_expr(f_l2.arguments().at(2));
+  const auto s_data_opt = try_get_string_data_array(s, ns);
+
+  if(!s_data_opt)
+    return false;
+
+  const array_exprt &s_data = s_data_opt->get();
+
+  mp_integer end_index;
+
+  if(num_operands == 5)
+  {
+    const auto &end_index_expr = f_l2.arguments().at(4);
+
+    if(end_index_expr.id() != ID_constant)
+    {
+      return false;
+    }
+
+    end_index = numeric_cast_v<mp_integer>(to_constant_expr(end_index_expr));
+
+    if(end_index < 0 || end_index > s_data.operands().size())
+    {
+      return false;
+    }
+  }
+  else
+  {
+    end_index = s_data.operands().size();
+  }
+
+  const auto &start_index_expr = f_l2.arguments().at(3);
+
+  if(start_index_expr.id() != ID_constant)
+  {
+    return false;
+  }
+
+  mp_integer start_index =
+    numeric_cast_v<mp_integer>(to_constant_expr(start_index_expr));
+
+  if(start_index < 0 || start_index > end_index)
+  {
+    return false;
+  }
+
+  const constant_exprt new_char_array_length =
+    from_integer(end_index - start_index, length_type);
+
+  array_typet new_char_array_type(char_type, new_char_array_length);
+
+  exprt::operandst operands(
+    std::next(
+      s_data.operands().begin(),
+      numeric_cast_v<std::size_t>(start_index)),
+    std::next(
+      s_data.operands().begin(),
+      numeric_cast_v<std::size_t>(end_index)));
+
+  array_exprt new_char_array(std::move(operands), new_char_array_type);
+
+  assign_string_constant(
+    state,
+    symex_assign,
+    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;
+}

jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc

@@ -566,6 +566,19 @@ class goto_symext
     const function_application_exprt &f_l1,
     const function_application_exprt &f_l2);
 
+  /// Attempt to constant propagate getting a substring of a string
+  ///
+  /// \param state: goto symex state
+  /// \param symex_assign: object handling symbol assignments
+  /// \param f_l1: application of function ID_cprover_string_substring_func with
+  ///   l1 renaming applied
+  /// \param f_l2: same as above but with l2 renaming applied
+  bool constant_propagate_string_substring(
+    statet &state,
+    symex_assignt &symex_assign,
+    const function_application_exprt &f_l1,
+    const function_application_exprt &f_l2);
+
   /// Assign constant string length and string data given by a char array to
   /// given ssa variables
   ///