Constant propagation of CProverString.setCharAt()

Only minimal tests are added at this point. The error conditions (like index out
of bounds) will be handled by the models. Once we have models that use
CProverString.setCharAt(), more comprehensive tests will be added.

Author: danpoe

jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetCharAt/Test.class

@@ -0,0 +1,18 @@
+import org.cprover.CProverString;
+
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, 0, 'd');
+    assert sb.toString().equals("dbc");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setCharAt(sb, 2, 'd');
+    assert sb.toString().equals("abd");
+  }
+}

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

@@ -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/ConstantEvaluationCProverStringSetCharAt/test_success1.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/ConstantEvaluationCProverStringSetCharAt/test_success2.desc

@@ -1528,8 +1528,11 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
      "String;II)I"] = ID_cprover_string_offset_by_code_point_func;
   cprover_equivalent_to_java_assign_function
-    ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
-      ID_cprover_string_char_set_func;
+    ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
+     "StringBuffer;IC)V"] = ID_cprover_string_char_set_func;
+  cprover_equivalent_to_java_assign_function
+    ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/"
+     "StringBuilder;IC)V"] = ID_cprover_string_char_set_func;
   cprover_equivalent_to_java_assign_function
     ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
       ID_cprover_string_set_length_func;

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -203,6 +203,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
       {
         return constant_propagate_set_length(state, symex_assign, f_l1);
       }
+      else if(func_id == ID_cprover_string_char_set_func)
+      {
+        return constant_propagate_set_char_at(state, symex_assign, f_l1);
+      }
     }
   }
 
@@ -843,3 +847,73 @@ bool goto_symext::constant_propagate_set_length(
 
   return true;
 }
+
+bool goto_symext::constant_propagate_set_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)
+  // - current string
+  // - index of char to set
+  // - new char
+  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;
+  }
+
+  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 auto &new_char_opt =
+    try_evaluate_constant(state, f_l1.arguments().at(4));
+
+  if(!new_char_opt)
+  {
+    return false;
+  }
+
+  const constant_exprt new_char_array_length =
+    from_integer(s_data.operands().size(), length_type);
+
+  const array_typet new_char_array_type(char_type, new_char_array_length);
+
+  s_data.operands()[numeric_cast_v<std::size_t>(index)] = new_char_opt->get();
+
+  const array_exprt new_char_array(
+    std::move(s_data.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.cpp

@@ -641,6 +641,19 @@ class goto_symext
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// Attempt to constant propagate setting the char at the given index
+  ///
+  /// \param state: goto symex state
+  /// \param symex_assign: object handling symbol assignments
+  /// \param f_l1: application of function ID_cprover_string_char_set_func with
+  ///   l1 renaming applied
+  /// \return true if the operation could be evaluated to a constant string,
+  ///   false otherwise
+  bool constant_propagate_set_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
   ///