Merge pull request #5126 from danpoe/feature/constant-propagation-of-delete-char-at

Constant propagation of deleteCharAt()

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

@@ -0,0 +1,30 @@
+public class Test
+{
+  public void testSuccess()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.deleteCharAt(1);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testNoPropagation(int index)
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.deleteCharAt(index);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testIndexOutOfBounds1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.deleteCharAt(-1);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testIndexOutOfBounds2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    sb.deleteCharAt(3);
+    assert sb.toString().equals("ac");
+  }
+}

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

@@ -0,0 +1,8 @@
+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$
+--
+--

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

@@ -0,0 +1,8 @@
+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$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_no_propagation.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferDeleteCharAt/test_success.desc

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

@@ -0,0 +1,30 @@
+public class Test
+{
+  public void testSuccess()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.deleteCharAt(1);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testNoPropagation(int index)
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.deleteCharAt(index);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testIndexOutOfBounds1()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.deleteCharAt(-1);
+    assert sb.toString().equals("ac");
+  }
+
+  public void testIndexOutOfBounds2()
+  {
+    StringBuilder sb = new StringBuilder("abc");
+    sb.deleteCharAt(3);
+    assert sb.toString().equals("ac");
+  }
+}

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

@@ -0,0 +1,8 @@
+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$
+--
+--

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

@@ -0,0 +1,8 @@
+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$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_no_propagation.desc

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

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderDeleteCharAt/test_success.desc

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

@@ -191,6 +191,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
       {
         return constant_propagate_integer_to_string(state, symex_assign, f_l1);
       }
+      else if(func_id == ID_cprover_string_delete_char_at_func)
+      {
+        return constant_propagate_delete_char_at(state, symex_assign, f_l1);
+      }
     }
   }
 
@@ -588,3 +592,76 @@ bool goto_symext::constant_propagate_integer_to_string(
 
   return true;
 }
+
+bool goto_symext::constant_propagate_delete_char_at(
+  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 char from
+  // - index of char to delete
+  PRECONDITION(f_l1.arguments().size() == 4);
+
+  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 &index_opt = try_evaluate_constant(state, f_l1.arguments().at(3));
+
+  if(!index_opt)
+  {
+    return false;
+  }
+
+  const mp_integer index = numeric_cast_v<mp_integer>(index_opt->get());
+
+  if(index < 0 || index >= s_data.operands().size())
+  {
+    return false;
+  }
+
+  const constant_exprt new_char_array_length =
+    from_integer(s_data.operands().size() - 1, length_type);
+
+  const array_typet new_char_array_type(char_type, new_char_array_length);
+
+  exprt::operandst operands;
+  operands.reserve(s_data.operands().size() - 1);
+
+  const std::size_t i = numeric_cast_v<std::size_t>(index);
+
+  operands.insert(
+    operands.end(),
+    s_data.operands().begin(),
+    std::next(s_data.operands().begin(), i));
+
+  operands.insert(
+    operands.end(),
+    std::next(s_data.operands().begin(), i + 1),
+    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

@@ -597,6 +597,19 @@ protected:
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// Attempt to constant propagate deleting a character 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_char_at_func
+  ///   with l1 renaming applied
+  /// \return true if the operation could be evaluated to a constant string,
+  ///   false otherwise
+  bool constant_propagate_delete_char_at(
+    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
   ///