Add String.trim()

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

@@ -0,0 +1,50 @@
+public class Main {
+    public void trim() {
+        String str = "   abc   ";
+        str = str.trim();
+        assert str.equals("abc");
+    }
+
+    public void noTrim() {
+        String str = "   abc   ";
+        str = str.trim();
+        assert !str.equals(" abc ");
+    }
+
+    public void trimLeft() {
+        String str = "   abc";
+        str = str.trim();
+        assert str.equals("abc");
+    }
+
+    public void trimRight() {
+        String str = "abc   ";
+        str = str.trim();
+        assert str.equals("abc");
+    }
+
+    public void noprop(String str) {
+        str = str.trim();
+        assert str.equals("abc");
+    }
+
+    public void empty() {
+        String str = "".trim();
+        assert str.equals("");
+    }
+
+    public void tab() {
+        String str = " ".trim();
+        assert str.equals("");
+    }
+
+    public void linebreak() {
+        String str = "\n".trim();
+        assert str.equals("");
+    }
+
+    public void middleWhitespace() {
+        String str = "  hello dave   ".trim();
+        assert str.equals("hello dave");
+    }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/empty.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.empty --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/ConstantEvaluationTrim/linebreak.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.empty --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/ConstantEvaluationTrim/middleWhitespace.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.middleWhitespace --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/ConstantEvaluationTrim/noTrim.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.noTrim --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/ConstantEvaluationTrim/noprop.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/tab.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.empty --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/ConstantEvaluationTrim/trim.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.trim --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/ConstantEvaluationTrim/trimLeft.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.trimLeft --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/ConstantEvaluationTrim/trimRight.desc

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

@@ -207,6 +207,10 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
       {
         return constant_propagate_set_char_at(state, symex_assign, f_l1);
       }
+      else if(func_id == ID_cprover_string_trim_func)
+      {
+        return constant_propagate_trim(state, symex_assign, f_l1);
+      }
     }
   }
 
@@ -922,3 +926,55 @@ bool goto_symext::constant_propagate_set_char_at(
 
   return true;
 }
+
+bool goto_symext::constant_propagate_trim(
+  statet &state,
+  symex_assignt &symex_assign,
+  const function_application_exprt &f_l1)
+{
+  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;
+
+  auto is_not_whitespace = [](const exprt &expr) {
+    auto character = numeric_cast_v<unsigned int>(to_constant_expr(expr));
+    return character > ' ';
+  };
+
+  // Note the points where a trim would trim too.
+  auto &operands = s_data_opt->get().operands();
+  auto end_iter =
+    std::find_if(operands.rbegin(), operands.rend(), is_not_whitespace);
+  auto start_iter =
+    std::find_if(operands.begin(), operands.end(), is_not_whitespace);
+
+  // Then copy in the string with leading/trailing whitespace removed.
+  // Note: if start_iter == operands.end it means the entire string is
+  // whitespace, so we'll trim it to be empty anyway.
+  exprt::operandst new_operands;
+  if(start_iter != operands.end())
+    new_operands = exprt::operandst{start_iter, end_iter.base()};
+
+  const constant_exprt new_char_array_length =
+    from_integer(new_operands.size(), length_type);
+
+  const array_typet new_char_array_type(char_type, new_char_array_length);
+  const array_exprt new_char_array(
+    std::move(new_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

@@ -657,6 +657,12 @@ protected:
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// Attempt to constant propagate trim operations.
+  bool constant_propagate_trim(
+    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
   ///