Constant propagation of CProverString.setLength()

danpoe · danpoe · commit 8279e91a600d · 2019-09-29T12:55:11.000+01:00
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.setLength(), more comprehensive tests will be added.
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/Test.class b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/Test.class
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/Test.java b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/Test.java
@@ -0,0 +1,65 @@
+import org.cprover.CProverString;
+
+public class Test
+{
+  public void testSuccess1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 0);
+    assert sb.toString().equals("");
+  }
+
+  public void testSuccess2()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 2);
+    assert sb.toString().equals("ab");
+  }
+
+  public void testSuccess3()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 3);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testSuccess4()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 4);
+    assert sb.toString().equals("abc\u0000");
+  }
+
+  public void testSuccess5()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, 5);
+    assert sb.toString().equals("abc\u0000\u0000");
+  }
+
+  public void testSuccess6(StringBuffer sb)
+  {
+    CProverString.setLength(sb, 0);
+    assert sb.toString().equals("");
+  }
+
+  public void testNoPropagation1()
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, -1);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation2(StringBuffer sb)
+  {
+    CProverString.setLength(sb, 3);
+    assert sb.toString().equals("abc");
+  }
+
+  public void testNoPropagation3(int newLength)
+  {
+    StringBuffer sb = new StringBuffer("abc");
+    CProverString.setLength(sb, newLength);
+    assert sb.toString().equals("abc");
+  }
+}
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation1.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation1 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`  --property 'java::Test.testNoPropagation1:()V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation2.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation2 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation2:(Ljava/lang/StringBuffer;)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_no_propagation3.desc
@@ -0,0 +1,8 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--function Test.testNoPropagation3 --show-vcc --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testNoPropagation3:(I)V.assertion.1'
+^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/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$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/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$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/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$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success4.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/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$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success5.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/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$
+--
+--
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success6.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCProverStringSetLength/test_success6.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$
+--
+--
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1531,8 +1531,11 @@ void java_string_library_preprocesst::initialize_conversion_table()
     ["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
       ID_cprover_string_char_set_func;
   cprover_equivalent_to_java_assign_function
-    ["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
+    ["java::org.cprover.CProverString.setLength:(Ljava/lang/StringBuffer;I)V"] =
       ID_cprover_string_set_length_func;
+  cprover_equivalent_to_java_assign_function
+    ["java::org.cprover.CProverString.setLength:(Ljava/lang/"
+     "StringBuilder;I)V"] = ID_cprover_string_set_length_func;
   cprover_equivalent_to_java_string_returning_function
     ["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
      "lang/CharSequence;"] = ID_cprover_string_substring_func;
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
@@ -199,6 +199,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
       {
         return constant_propagate_delete(state, symex_assign, f_l1);
       }
+      else if(func_id == ID_cprover_string_set_length_func)
+      {
+        return constant_propagate_set_length(state, symex_assign, f_l1);
+      }
     }
   }
 
@@ -763,3 +767,84 @@ bool goto_symext::constant_propagate_delete(
 
   return true;
 }
+
+bool goto_symext::constant_propagate_set_length(
+  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
+  // - new length of the string
+  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 auto &new_length_opt =
+    try_evaluate_constant(state, f_l1.arguments().at(3));
+
+  if(!new_length_opt)
+  {
+    return false;
+  }
+
+  const mp_integer new_length =
+    numeric_cast_v<mp_integer>(new_length_opt->get());
+
+  if(new_length < 0)
+  {
+    return false;
+  }
+
+  const std::size_t new_size = numeric_cast_v<std::size_t>(new_length);
+
+  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;
+
+  if(new_size != 0)
+  {
+    operands.reserve(new_size);
+
+    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();
+
+    operands.insert(
+      operands.end(),
+      s_data.operands().begin(),
+      std::next(
+        s_data.operands().begin(),
+        std::min(new_size, s_data.operands().size())));
+
+    operands.insert(
+      operands.end(),
+      new_size - std::min(new_size, s_data.operands().size()),
+      from_integer(0, char_type));
+  }
+
+  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;
+}
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
@@ -623,6 +623,24 @@ class goto_symext
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// Attempt to constant propagate setting the length of a string
+  ///
+  /// If the new length is less than the current length, characters are stripped
+  /// from the end to match  the new length. If the new length is greater than
+  /// the current length, null characters '\\u0000' are appended to match the
+  /// new length.
+  ///
+  /// \param state: goto symex state
+  /// \param symex_assign: object handling symbol assignments
+  /// \param f_l1: application of function ID_cprover_string_set_length_func
+  ///   with l1 renaming applied
+  /// \return true if the operation could be evaluated to a constant string,
+  ///   false otherwise
+  bool constant_propagate_set_length(
+    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
   ///
