Merge pull request #5131 from danpoe/feature/constant-propagation-of-delete

Constant propagation of delete() for StringBuilder and StringBuffer

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/Test.java

@@ -0,0 +1,69 @@
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(0, 0);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(0, 3);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess3()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(0, 4);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess4()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(1, 2);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testSuccess5()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(3, 4);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation1(int index)
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(index, 3);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testNoPropagation2(int index)
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(0, index);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testIndexOutOfBounds1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(-1, 3);
+  }
+
+  public void testIndexOutOfBounds2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(4, 5);
+  }
+
+  public void testIndexOutOfBounds3()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.delete(2, 1);
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/test_index_out_of_bounds1.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIndexOutOfBounds1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/test_index_out_of_bounds2.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIndexOutOfBounds2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/test_index_out_of_bounds3.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIndexOutOfBounds3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/test_no_propagation1.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/test_no_propagation2.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDelete/test_success1.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess1 --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/ConstantEvaluationStringBufferDelete/test_success2.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess2 --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/ConstantEvaluationStringBufferDelete/test_success3.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess3 --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/ConstantEvaluationStringBufferDelete/test_success4.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess4 --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/ConstantEvaluationStringBufferDelete/test_success5.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess5 --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/ConstantEvaluationStringBuilderDelete/Test.java

@@ -0,0 +1,69 @@
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(0, 0);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(0, 3);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess3()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(0, 4);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess4()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(1, 2);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testSuccess5()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(3, 4);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation1(int index)
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(index, 3);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testNoPropagation2(int index)
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(0, index);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testIndexOutOfBounds1()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(-1, 3);
+  }
+
+  public void testIndexOutOfBounds2()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(4, 5);
+  }
+
+  public void testIndexOutOfBounds3()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.delete(2, 1);
+  }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDelete/test_index_out_of_bounds1.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIndexOutOfBounds1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDelete/test_index_out_of_bounds2.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIndexOutOfBounds2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDelete/test_index_out_of_bounds3.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testIndexOutOfBounds3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDelete/test_no_propagation1.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDelete/test_no_propagation2.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDelete/test_success1.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess1 --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/ConstantEvaluationStringBuilderDelete/test_success2.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess2 --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/ConstantEvaluationStringBuilderDelete/test_success3.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess3 --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/ConstantEvaluationStringBuilderDelete/test_success4.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess4 --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/ConstantEvaluationStringBuilderDelete/test_success5.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.testSuccess5 --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$
+--
+--

src/goto-symex/goto_symex.cpp

@@ -195,6 +195,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
       {
         return constant_propagate_delete_char_at(state, symex_assign, f_l1);
       }
+      else if(func_id == ID_cprover_string_delete_func)
+      {
+        return constant_propagate_delete(state, symex_assign, f_l1);
+      }
     }
   }
 
@@ -665,3 +669,97 @@ bool goto_symext::constant_propagate_delete_char_at(
 
   return true;
 }
+
+bool goto_symext::constant_propagate_delete(
+  statet &state,
+  symex_assignt &symex_assign,
+  const function_application_exprt &f_l1)
+{
+  // The function application expression f_l1 takes the following arguments:
+  // - result string length (output parameter)
+  // - result string data array (output parameter)
+  // - string to delete substring from
+  // - index of start of substring to delete (inclusive)
+  // - index of end of substring to delete (exclusive)
+  PRECONDITION(f_l1.arguments().size() == 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();
+
+  const auto &start_opt = try_evaluate_constant(state, f_l1.arguments().at(3));
+
+  if(!start_opt)
+  {
+    return false;
+  }
+
+  const mp_integer start = numeric_cast_v<mp_integer>(start_opt->get());
+
+  if(start < 0 || start > s_data.operands().size())
+  {
+    return false;
+  }
+
+  const auto &end_opt = try_evaluate_constant(state, f_l1.arguments().at(4));
+
+  if(!end_opt)
+  {
+    return false;
+  }
+
+  const mp_integer end = numeric_cast_v<mp_integer>(end_opt->get());
+
+  if(start > end)
+  {
+    return false;
+  }
+
+  const std::size_t start_index = numeric_cast_v<std::size_t>(start);
+
+  const std::size_t end_index =
+    std::min(numeric_cast_v<std::size_t>(end), s_data.operands().size());
+
+  const std::size_t new_size =
+    s_data.operands().size() - end_index + start_index;
+
+  const constant_exprt new_char_array_length =
+    from_integer(new_size, length_type);
+
+  const array_typet new_char_array_type(char_type, new_char_array_length);
+
+  exprt::operandst operands;
+  operands.reserve(new_size);
+
+  operands.insert(
+    operands.end(),
+    s_data.operands().begin(),
+    std::next(s_data.operands().begin(), start_index));
+
+  operands.insert(
+    operands.end(),
+    std::next(s_data.operands().begin(), end_index),
+    s_data.operands().end());
+
+  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;
+}

src/goto-symex/goto_symex.h

@@ -610,6 +610,19 @@ protected:
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// Attempt to constant propagate deleting a substring from a string
+  ///
+  /// \param state: goto symex state
+  /// \param symex_assign: object handling symbol assignments
+  /// \param f_l1: application of function ID_cprover_string_delete_func with
+  ///   l1 renaming applied
+  /// \return true if the operation could be evaluated to a constant string,
+  ///   false otherwise
+  bool constant_propagate_delete(
+    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
   ///