Add builtin class for string_to_upper_case

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -187,6 +187,12 @@ exprt string_set_char_builtin_functiont::length_constraint() const
     equal_exprt(return_code, return_value));
 }
 
+static bool eval_is_upper_case(const mp_integer &c)
+{
+  return ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
+         (0xd8 <= c && c <= 0xde);
+}
+
 optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
   const std::function<exprt(const exprt &)> &get_value) const
 {
@@ -195,9 +201,7 @@ optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
     return {};
   for(mp_integer &c : input_opt.value())
   {
-    if(
-      ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
-      (0xd8 <= c && c <= 0xde))
+    if(eval_is_upper_case(c))
       c += 0x20;
   }
   const auto length =
@@ -206,6 +210,23 @@ optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
   return make_string(input_opt.value(), type);
 }
 
+optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  auto input_opt = eval_string(input, get_value);
+  if(!input_opt)
+    return {};
+  for(mp_integer &c : input_opt.value())
+  {
+    if(eval_is_upper_case(c - 0x20))
+      c -= 0x20;
+  }
+  const auto length =
+    from_integer(input_opt.value().size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(input_opt.value(), type);
+}
+
 std::vector<mp_integer> string_insertion_builtin_functiont::eval(
   const std::vector<mp_integer> &input1_value,
   const std::vector<mp_integer> &input2_value,

src/solvers/refinement/string_builtin_function.h

@@ -210,6 +210,39 @@ class string_to_lower_case_builtin_functiont
   };
 };
 
+/// Converting each lowercase character of Basic Latin and Latin-1 supplement
+/// to the corresponding uppercase character.
+class string_to_upper_case_builtin_functiont
+  : public string_transformation_builtin_functiont
+{
+public:
+  string_to_upper_case_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
+  {
+  }
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "to_upper_case";
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_to_upper_case(result, input);
+  };
+
+  exprt length_constraint() const override
+  {
+    return equal_exprt(result.length(), input.length());
+  };
+};
+
 /// String inserting a string into another one
 class string_insertion_builtin_functiont : public string_builtin_functiont
 {

src/solvers/refinement/string_constraint_generator.h

@@ -178,6 +178,9 @@ class string_constraint_generatort final
   exprt add_axioms_for_to_lower_case(
     const array_string_exprt &res,
     const array_string_exprt &str);
+  exprt add_axioms_for_to_upper_case(
+    const array_string_exprt &res,
+    const array_string_exprt &expr);
 
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
@@ -338,9 +341,6 @@ class string_constraint_generatort final
   exprt add_axioms_for_substring(const function_application_exprt &f);
   exprt add_axioms_for_to_lower_case(const function_application_exprt &f);
   exprt add_axioms_for_to_upper_case(const function_application_exprt &f);
-  exprt add_axioms_for_to_upper_case(
-    const array_string_exprt &res,
-    const array_string_exprt &expr);
   exprt add_axioms_for_trim(const function_application_exprt &f);
 
   exprt add_axioms_for_code_point(

src/solvers/refinement/string_refinement_util.cpp

@@ -236,6 +236,10 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
     return util_make_unique<string_to_lower_case_builtin_functiont>(
       return_code, fun_app.arguments(), array_pool);
 
+  if(id == ID_cprover_string_to_upper_case_func)
+    return util_make_unique<string_to_upper_case_builtin_functiont>(
+      return_code, fun_app.arguments(), array_pool);
+
   return util_make_unique<string_builtin_function_with_no_evalt>(
     return_code, fun_app, array_pool);
 }