Move add_axioms_for_to_lower/upper_case to builtin functions

Author: romainbrenguier

src/solvers/README.md

@@ -275,11 +275,11 @@ allocates a new string before calling a primitive.
     \copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
     \link add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
   * `cprover_string_to_lower_case` :
-    \copybrief add_axioms_for_to_lower_case
-    \link add_axioms_for_to_lower_case More... \endlink
+    \copybrief string_to_lower_case_builtin_functiont::constraints
+    \link string_to_lower_case_builtin_functiont::constraints More... \endlink
   * `cprover_string_to_upper_case` :
-    \copybrief add_axioms_for_to_upper_case
-    \link add_axioms_for_to_upper_case More... \endlink
+    \copybrief string_to_upper_case_builtin_functiont::constraints(symbol_generatort&)
+    \link string_to_upper_case_builtin_functiont::constraints(symbol_generatort&) More... \endlink
   * `cprover_string_trim` :
     \copybrief add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
     \link add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink

src/solvers/refinement/string_builtin_function.cpp

@@ -315,13 +315,82 @@ optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
   return make_string(input_opt.value(), type);
 }
 
+/// Expression which is true for uppercase characters of the Basic Latin and
+/// Latin-1 supplement of unicode.
+static exprt is_upper_case(const exprt &character)
+{
+  const exprt char_A = from_integer('A', character.type());
+  const exprt char_Z = from_integer('Z', character.type());
+  exprt::operandst upper_case;
+  // Characters between 'A' and 'Z' are upper-case
+  upper_case.push_back(
+    and_exprt(
+      binary_relation_exprt(char_A, ID_le, character),
+      binary_relation_exprt(character, ID_le, char_Z)));
+
+  // Characters between 0xc0 (latin capital A with grave)
+  // and 0xd6 (latin capital O with diaeresis) are upper-case
+  upper_case.push_back(
+    and_exprt(
+      binary_relation_exprt(
+        from_integer(0xc0, character.type()), ID_le, character),
+      binary_relation_exprt(
+        character, ID_le, from_integer(0xd6, character.type()))));
+
+  // Characters between 0xd8 (latin capital O with stroke)
+  // and 0xde (latin capital thorn) are upper-case
+  upper_case.push_back(
+    and_exprt(
+      binary_relation_exprt(
+        from_integer(0xd8, character.type()), ID_le, character),
+      binary_relation_exprt(
+        character, ID_le, from_integer(0xde, character.type()))));
+  return disjunction(upper_case);
+}
+
+/// Expression which is true for lower_case characters of the Basic Latin and
+/// Latin-1 supplement of unicode.
+static exprt is_lower_case(const exprt &character)
+{
+  return is_upper_case(
+    minus_exprt(character, from_integer(0x20, character.type())));
+}
+
+/// Set of constraints ensuring `result` corresponds to `input` in which
+/// uppercase characters have been converted to lowercase.
+/// These constraints are:
+///   1. result.length = input.length && return_code = 0
+///   2. forall i < input.length.
+///        result[i] = is_upper_case(input[i]) ? input[i] + diff : input[i]
+///
+/// Where `diff` is the difference between lower case and upper case
+/// characters: `diff = 'a'-'A' = 0x20` and `is_upper_case` is true for the
+/// upper case characters of Basic Latin and Latin-1 supplement of unicode.
 string_constraintst string_to_lower_case_builtin_functiont::constraints(
   string_constraint_generatort &generator) const
 {
-  auto pair =
-    add_axioms_for_to_lower_case(generator.fresh_symbol, result, input);
-  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-  return pair.second;
+  // \todo for now, only characters in Basic Latin and Latin-1 supplement
+  // are supported (up to 0x100), we should add others using case mapping
+  // information from the UnicodeData file.
+  string_constraintst constraints;
+  constraints.existential.push_back(length_constraint());
+  constraints.universal.push_back([&] {
+    const symbol_exprt idx =
+      generator.fresh_symbol("QA_lower_case", result.length().type());
+    const exprt conditional_convert = [&] {
+      // The difference between upper-case and lower-case for the basic
+      // latin and latin-1 supplement is 0x20.
+      const typet &char_type = result.type().subtype();
+      const exprt diff = from_integer(0x20, char_type);
+      const exprt converted =
+        equal_exprt(result[idx], plus_exprt(input[idx], diff));
+      const exprt non_converted = equal_exprt(result[idx], input[idx]);
+      return if_exprt(is_upper_case(input[idx]), converted, non_converted);
+    }();
+    return string_constraintt(
+      idx, zero_if_negative(result.length()), conditional_convert);
+  }());
+  return constraints;
 }
 
 optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
@@ -349,13 +418,26 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
 ///        is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
 ///
 /// \param fresh_symbol: generator of fresh symbols
+/// \return set of constraints
 string_constraintst string_to_upper_case_builtin_functiont::constraints(
-  string_constraint_generatort &generator) const
+  symbol_generatort &fresh_symbol) const
 {
-  auto pair =
-    add_axioms_for_to_upper_case(generator.fresh_symbol, result, input);
-  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-  return pair.second;
+  string_constraintst constraints;
+  constraints.existential.push_back(length_constraint());
+  constraints.universal.push_back([&] {
+    const symbol_exprt idx =
+      fresh_symbol("QA_upper_case", result.length().type());
+    const typet &char_type = input.content().type().subtype();
+    const exprt converted =
+      minus_exprt(input[idx], from_integer(0x20, char_type));
+    return string_constraintt(
+      idx,
+      zero_if_negative(result.length()),
+      equal_exprt(
+        result[idx],
+        if_exprt(is_lower_case(input[idx]), converted, input[idx])));
+  }());
+  return constraints;
 }
 
 std::vector<mp_integer> string_insertion_builtin_functiont::eval(

src/solvers/refinement/string_builtin_function.h

@@ -7,6 +7,7 @@
 #include <vector>
 #include <util/optional.h>
 #include <util/string_expr.h>
+#include "string_constraint_generator.h"
 
 class array_poolt;
 struct string_constraintst;
@@ -211,7 +212,9 @@ class string_to_lower_case_builtin_functiont
 
   exprt length_constraint() const override
   {
-    return equal_exprt(result.length(), input.length());
+    return and_exprt(
+      equal_exprt(result.length(), input.length()),
+      equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };
 
@@ -229,6 +232,17 @@ class string_to_upper_case_builtin_functiont
   {
   }
 
+  string_to_upper_case_builtin_functiont(
+    exprt return_code,
+    array_string_exprt result,
+    array_string_exprt input)
+    : string_transformation_builtin_functiont(
+        std::move(return_code),
+        std::move(result),
+        std::move(input))
+  {
+  }
+
   optionalt<exprt>
   eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
@@ -237,12 +251,20 @@ class string_to_upper_case_builtin_functiont
     return "to_upper_case";
   }
 
+  string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
+
+  /// \copydoc constraints(class symbol_generatort&)
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override;
+  constraints(string_constraint_generatort &generator) const override
+  {
+    return constraints(generator.fresh_symbol);
+  };
 
   exprt length_constraint() const override
   {
-    return equal_exprt(result.length(), input.length());
+    return and_exprt(
+      equal_exprt(result.length(), input.length()),
+      equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };
 

src/solvers/refinement/string_constraint_generator.h

@@ -485,15 +485,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
   const function_application_exprt &f,
   array_poolt &array_pool);
 
-std::pair<exprt, string_constraintst> add_axioms_for_to_lower_case(
-  symbol_generatort &fresh_symbol,
-  const array_string_exprt &res,
-  const array_string_exprt &str);
-
-std::pair<exprt, string_constraintst> add_axioms_for_to_upper_case(
-  symbol_generatort &fresh_symbol,
-  const array_string_exprt &res,
-  const array_string_exprt &expr);
 std::pair<exprt, string_constraintst> add_axioms_for_trim(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -19,6 +19,7 @@ Date:   May 2017
 #include <util/std_expr.h>
 #include <util/unicode.h>
 
+#include "string_builtin_function.h"
 #include "string_constraint_generator.h"
 
 // Format specifier describes how a value should be printed.
@@ -338,10 +339,14 @@ add_axioms_for_format_specifier(
       array_pool,
       message,
       ns);
-    auto upper_case_result = add_axioms_for_to_upper_case(
-      fresh_symbol, res, format_specifier_result.first);
-    merge(upper_case_result.second, std::move(format_specifier_result.second));
-    return {res, std::move(upper_case_result.second)};
+
+    const exprt return_code_upper_case =
+      fresh_symbol("return_code_upper_case", get_return_code_type());
+    const string_to_upper_case_builtin_functiont upper_case_function(
+      return_code_upper_case, res, format_specifier_result.first);
+    auto upper_case_constraints = upper_case_function.constraints(fresh_symbol);
+    merge(upper_case_constraints, std::move(format_specifier_result.second));
+    return {res, std::move(upper_case_constraints)};
   }
   case format_specifiert::OCTAL_INTEGER:
   /// \todo Conversion of octal is not implemented.

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -245,134 +245,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
   return {from_integer(0, f.type()), constraints};
 }
 
-/// Expression which is true for uppercase characters of the Basic Latin and
-/// Latin-1 supplement of unicode.
-static exprt is_upper_case(const exprt &character)
-{
-  const exprt char_A = from_integer('A', character.type());
-  const exprt char_Z = from_integer('Z', character.type());
-  exprt::operandst upper_case;
-  // Characters between 'A' and 'Z' are upper-case
-  upper_case.push_back(
-    and_exprt(
-      binary_relation_exprt(char_A, ID_le, character),
-      binary_relation_exprt(character, ID_le, char_Z)));
-
-  // Characters between 0xc0 (latin capital A with grave)
-  // and 0xd6 (latin capital O with diaeresis) are upper-case
-  upper_case.push_back(
-    and_exprt(
-      binary_relation_exprt(
-        from_integer(0xc0, character.type()), ID_le, character),
-      binary_relation_exprt(
-        character, ID_le, from_integer(0xd6, character.type()))));
-
-  // Characters between 0xd8 (latin capital O with stroke)
-  // and 0xde (latin capital thorn) are upper-case
-  upper_case.push_back(
-    and_exprt(
-      binary_relation_exprt(
-        from_integer(0xd8, character.type()), ID_le, character),
-      binary_relation_exprt(
-        character, ID_le, from_integer(0xde, character.type()))));
-  return disjunction(upper_case);
-}
-
-/// Expression which is true for lower_case characters of the Basic Latin and
-/// Latin-1 supplement of unicode.
-static exprt is_lower_case(const exprt &character)
-{
-  return is_upper_case(
-    minus_exprt(character, from_integer(0x20, character.type())));
-}
-
-/// Add axioms ensuring `res` corresponds to `str` in which uppercase characters
-/// have been converted to lowercase.
-/// These axioms are:
-///   1. res.length = str.length
-///   2. forall i < str.length.
-///        res[i] = is_upper_case(str[i]) ? str[i] + diff : str[i]
-///
-/// Where `diff` is the difference between lower case and upper case
-/// characters: `diff = 'a'-'A' = 0x20` and `is_upper_case` is true for the
-/// upper case characters of Basic Latin and Latin-1 supplement of unicode.
-std::pair<exprt, string_constraintst> add_axioms_for_to_lower_case(
-  symbol_generatort &fresh_symbol,
-  const array_string_exprt &res,
-  const array_string_exprt &str)
-{
-  string_constraintst constraints;
-  const typet &char_type = res.type().subtype();
-  const typet &index_type = res.length().type();
-  const exprt char_A = from_integer('A', char_type);
-  const exprt char_Z = from_integer('Z', char_type);
-
-  // \todo for now, only characters in Basic Latin and Latin-1 supplement
-  // are supported (up to 0x100), we should add others using case mapping
-  // information from the UnicodeData file.
-
-  constraints.existential.push_back(equal_exprt(res.length(), str.length()));
-
-  constraints.universal.push_back([&] {
-    const symbol_exprt idx = fresh_symbol("QA_lower_case", index_type);
-    const exprt conditional_convert = [&] {
-      // The difference between upper-case and lower-case for the basic latin and
-      // latin-1 supplement is 0x20.
-      const exprt diff = from_integer(0x20, char_type);
-      const exprt converted = equal_exprt(res[idx], plus_exprt(str[idx], diff));
-      const exprt non_converted = equal_exprt(res[idx], str[idx]);
-      return if_exprt(is_upper_case(str[idx]), converted, non_converted);
-    }();
-
-    return string_constraintt(
-      idx, zero_if_negative(res.length()), conditional_convert);
-  }());
-
-  return {from_integer(0, get_return_code_type()), std::move(constraints)};
-}
-
-/// Add axioms ensuring `res` corresponds to `str` in which lowercase characters
-/// of Basic Latin and Latin-1 supplement of unicode have been converted to
-/// uppercase.
-///
-/// These axioms are:
-///   1. res.length = str.length
-///   2. forall i < str.length.
-///        is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
-///
-/// \param fresh_symbol: generator of fresh symbols
-/// \param res: array of characters expression
-/// \param str: array of characters expression
-/// \return integer expression which is different from `0` when there is an
-///         exception to signal
-std::pair<exprt, string_constraintst> add_axioms_for_to_upper_case(
-  symbol_generatort &fresh_symbol,
-  const array_string_exprt &res,
-  const array_string_exprt &str)
-{
-  string_constraintst constraints;
-  const typet &char_type = str.content().type().subtype();
-  const typet &index_type = str.length().type();
-  exprt char_a = from_integer('a', char_type);
-  exprt char_A = from_integer('A', char_type);
-  exprt char_z = from_integer('z', char_type);
-
-  constraints.existential.push_back(equal_exprt(res.length(), str.length()));
-
-  constraints.universal.push_back([&] {
-    const symbol_exprt idx = fresh_symbol("QA_upper_case", index_type);
-    const exprt converted =
-      minus_exprt(str[idx], from_integer(0x20, char_type));
-    return string_constraintt(
-      idx,
-      zero_if_negative(res.length()),
-      equal_exprt(
-        res[idx], if_exprt(is_lower_case(str[idx]), converted, str[idx])));
-  }());
-
-  return {from_integer(0, get_return_code_type()), std::move(constraints)};
-}
-
 /// Convert two expressions to pair of chars
 /// If both expressions are characters, return pair of them
 /// If both expressions are 1-length strings, return first character of each