Add String.toLowerCase() / String.toUpperCase()

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

@@ -0,0 +1,43 @@
+public class Main {
+    public void toLower() {
+        String str = "ABCDE";
+        str = str.toLowerCase();
+        assert str.equals("abcde");
+    }
+
+    public void noLower() {
+        String str = "ABCDE";
+        str = str.toLowerCase();
+        assert !str.equals("abcdE");
+    }
+
+    public void noprop(String str) {
+        str = str.toLowerCase();
+        assert str.equals("ABCDE");
+    }
+
+    public void nondetArg(String str) {
+        str = "dave".toLowerCase();
+        assert !str.equals(str);
+    }
+
+    public void pi() {
+        assert "π".toLowerCase().equals("π");
+    }
+
+    public void nonAlpha() {
+        assert "^£&$1!".toLowerCase().equals("^£&$1!");
+    }
+
+    public void empty() {
+        assert "".toLowerCase().equals("");
+    }
+
+    public void emptyThis() {
+        assert !"".toLowerCase().equals("dave");
+    }
+
+    public void emptyArg() {
+        assert !"dave".toLowerCase().equals("");
+    }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/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/ConstantEvaluationToLowerCase/emptyArg.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.emptyArg --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/ConstantEvaluationToLowerCase/emptyThis.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.emptyThis --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/ConstantEvaluationToLowerCase/noLower.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.noLower --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/ConstantEvaluationToLowerCase/nonAlpha.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.nonAlpha --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=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/nondetArg.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.nondetArg --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/ConstantEvaluationToLowerCase/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/ConstantEvaluationToLowerCase/pi.desc

@@ -0,0 +1,13 @@
+CORE
+Main.class
+--function Main.pi --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=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is technically wrong (as pi has an uppercase) but our current implementation
+only constant props things within the 0 - 128 range due to the tolower/toupper methods
+currently being used. If this ever changes to be a true all-character case change,
+just modify the test.

jbmc/regression/jbmc-strings/ConstantEvaluationToLowerCase/toLower.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.toLower --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/ConstantEvaluationToUpperCase/Main.java

@@ -0,0 +1,43 @@
+public class Main {
+    public void toUpper() {
+        String str = "abcde";
+        str = str.toUpperCase();
+        assert str.equals("ABCDE");
+    }
+
+    public void noUpper() {
+        String str = "abcde";
+        str = str.toUpperCase();
+        assert !str.equals("ABCDe");
+    }
+
+    public void noprop(String str) {
+        str = str.toUpperCase();
+        assert str.equals("ABCDE");
+    }
+
+    public void nondetArg(String str) {
+        str = "dave".toUpperCase();
+        assert !str.equals(str);
+    }
+
+    public void pi() {
+        assert "π".toUpperCase().equals("π");
+    }
+
+    public void nonAlpha() {
+        assert "^£&$1!".toUpperCase().equals("^£&$1!");
+    }
+
+    public void empty() {
+        assert "".toLowerCase().equals("");
+    }
+
+    public void emptyThis() {
+        assert !"".toUpperCase().equals("dave");
+    }
+
+    public void emptyArg() {
+        assert !"dave".toUpperCase().equals("");
+    }
+}

jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/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/ConstantEvaluationToUpperCase/emptyArg.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.emptyArg --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/ConstantEvaluationToUpperCase/emptyThis.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.emptyThis --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/ConstantEvaluationToUpperCase/noUpper.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.noUpper --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/ConstantEvaluationToUpperCase/nonAlpha.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.nonAlpha --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=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--

jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/nondetArg.desc

@@ -0,0 +1,9 @@
+CORE
+Main.class
+--function Main.nondetArg --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/ConstantEvaluationToUpperCase/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/ConstantEvaluationToUpperCase/pi.desc

@@ -0,0 +1,13 @@
+CORE
+Main.class
+--function Main.pi --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=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This is technically wrong (as pi has an uppercase) but our current implementation
+only constant props things within the 0 - 128 range due to the tolower/toupper methods
+currently being used. If this ever changes to be a true all-character case change,
+just modify the test.

jbmc/regression/jbmc-strings/ConstantEvaluationToUpperCase/toUpper.desc

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

@@ -211,6 +211,14 @@ bool goto_symext::constant_propagate_assignment_with_side_effects(
       {
         return constant_propagate_trim(state, symex_assign, f_l1);
       }
+      else if(func_id == ID_cprover_string_to_lower_case_func)
+      {
+        return constant_propagate_case_change(state, symex_assign, f_l1, false);
+      }
+      else if(func_id == ID_cprover_string_to_upper_case_func)
+      {
+        return constant_propagate_case_change(state, symex_assign, f_l1, true);
+      }
     }
   }
 
@@ -927,6 +935,68 @@ bool goto_symext::constant_propagate_set_char_at(
   return true;
 }
 
+bool goto_symext::constant_propagate_case_change(
+  statet &state,
+  symex_assignt &symex_assign,
+  const function_application_exprt &f_l1,
+  bool to_upper)
+{
+  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 string_data = s_data_opt->get();
+
+  auto &operands = string_data.operands();
+  for(auto &operand : operands)
+  {
+    auto &constant_value = to_constant_expr(operand);
+    auto character = numeric_cast_v<unsigned int>(constant_value);
+
+    // Can't guarantee matches against non-ASCII characters.
+    if(character >= 128)
+      return false;
+
+    if(isalpha(character))
+    {
+      if(to_upper)
+      {
+        if(islower(character))
+          constant_value =
+            from_integer(toupper(character), constant_value.type());
+      }
+      else
+      {
+        if(isupper(character))
+          constant_value =
+            from_integer(tolower(character), constant_value.type());
+      }
+    }
+  }
+
+  const constant_exprt new_char_array_length =
+    from_integer(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(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;
+}
+
 bool goto_symext::constant_propagate_trim(
   statet &state,
   symex_assignt &symex_assign,

src/goto-symex/goto_symex.h

@@ -663,6 +663,13 @@ protected:
     symex_assignt &symex_assign,
     const function_application_exprt &f_l1);
 
+  /// Attempt to constant propagate case changes, both upper and lower.
+  bool constant_propagate_case_change(
+    statet &state,
+    symex_assignt &symex_assign,
+    const function_application_exprt &f_l1,
+    bool to_upper);
+
   /// Assign constant string length and string data given by a char array to
   /// given ssa variables
   ///