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,18 @@
+public class Main {
+  public void test1(StringBuilder sb) {
+    String s = sb.substring(0);
+    assert s.startsWith("xyz");
+  }
+
+  public void test2(int i) {
+    StringBuilder sb = new StringBuilder("abc");
+
+    String s = sb.substring(i);
+    assert s.startsWith("xyz");
+  }
+
+  public void test3(StringBuilder sb, int i) {
+    String s = sb.substring(i);
+    assert s.startsWith("xyz");
+  }
+}

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test1 --property "java::Main.test1:(Ljava/lang/StringBuilder;)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test2 --property "java::Main.test2:(I)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

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

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,18 @@
+public class Main {
+  public void test1(String s1) {
+    String s2 = s1.substring(0);
+    assert s2.startsWith("xyz");
+  }
+
+  public void test2(int i) {
+    String s1 = "abc";
+
+    String s2 = s1.substring(i);
+    assert s2.startsWith("xyz");
+  }
+
+  public void test3(String s1, int i) {
+    String s2 = s1.substring(i);
+    assert s2.startsWith("xyz");
+  }
+}

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

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

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

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure
+Main.class
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1"
+^Generated 1 VCC\(s\), 1 remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

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

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

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

@@ -181,6 +181,10 @@ 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);
+      }
     }
   }
 
@@ -310,6 +314,26 @@ goto_symext::try_evaluate_constant_string(
   return try_get_string_data_array(s_pointer_opt->get(), ns);
 }
 
+optionalt<std::reference_wrapper<const constant_exprt>>
+goto_symext::try_evaluate_constant(const statet &state, const exprt &expr)
+{
+  if(expr.id() != ID_symbol)
+  {
+    return {};
+  }
+
+  const auto constant_expr_opt =
+    state.propagation.find(to_symbol_expr(expr).get_identifier());
+
+  if(!constant_expr_opt || constant_expr_opt->get().id() != ID_constant)
+  {
+    return {};
+  }
+
+  return optionalt<std::reference_wrapper<const constant_exprt>>(
+    to_constant_expr(constant_expr_opt->get()));
+}
+
 void goto_symext::constant_propagate_empty_string(
   statet &state,
   symex_assignt &symex_assign,
@@ -387,3 +411,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 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_l1.arguments().at(2));
+  const auto s_data_opt = try_evaluate_constant_string(state, s.content());
+
+  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_opt =
+      try_evaluate_constant(state, f_l1.arguments().at(4));
+
+    if(!end_index_expr_opt)
+    {
+      return false;
+    }
+
+    end_index =
+      numeric_cast_v<mp_integer>(to_constant_expr(*end_index_expr_opt));
+
+    if(end_index < 0 || end_index > s_data.operands().size())
+    {
+      return false;
+    }
+  }
+  else
+  {
+    end_index = s_data.operands().size();
+  }
+
+  const auto start_index_expr_opt =
+    try_evaluate_constant(state, f_l1.arguments().at(3));
+
+  if(!start_index_expr_opt)
+  {
+    return false;
+  }
+
+  const mp_integer start_index =
+    numeric_cast_v<mp_integer>(to_constant_expr(*start_index_expr_opt));
+
+  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);
+
+  const 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)));
+
+  const 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

@@ -568,6 +568,19 @@ class goto_symext
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// 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
+  /// \return true if the operation could be evaluated to a constant string,
+  ///   false otherwise
+  bool constant_propagate_string_substring(
+    statet &state,
+    symex_assignt &symex_assign,
+    const function_application_exprt &f_l1);
+
   /// Assign constant string length and string data given by a char array to
   /// given ssa variables
   ///
@@ -627,6 +640,13 @@ class goto_symext
   optionalt<std::reference_wrapper<const array_exprt>>
   try_evaluate_constant_string(const statet &state, const exprt &content);
 
+  // clang-format off
+  static optionalt<std::reference_wrapper<const constant_exprt>>
+  try_evaluate_constant(
+    const statet &state,
+    const exprt &expr);
+  // clang-format on
+
   // havocs the given object
   void havoc_rec(statet &state, const guardt &guard, const exprt &dest);