diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class new file mode 100644 index 00000000000..800af2c1930 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java new file mode 100644 index 00000000000..3caa33d3377 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToLowerCase/Test.java @@ -0,0 +1,50 @@ +public class Test { + public String det() + { + StringBuilder builder = new StringBuilder(); + builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase()); + builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toLowerCase()); + builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toLowerCase()); + builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toLowerCase()); + builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toLowerCase()); + return builder.toString(); + } + + public String nonDet(String s) + { + if(s.length() < 20) + return "Short string"; + if(!s.startsWith("A")) + return "String not starting with A"; + + StringBuilder builder = new StringBuilder(); + builder.append(s.toLowerCase()); + builder.append(s.toLowerCase()); + builder.append(":"); + builder.append(s); + builder.append(":"); + builder.append(s.toLowerCase()); + builder.append(s.toLowerCase()); + return builder.toString(); + } + + public String withDependency(String s, boolean b) + { + // Filter + if(s == null || s.length() < 20) + return "Short string"; + if(!s.endsWith("A")) + return "String not ending with A"; + + // Act + String result = s + s.toLowerCase(); + + // Assert + if(b) { + assert(result.endsWith("a")); + } else { + assert(!result.endsWith("a")); + } + return result; + } +} diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc new file mode 100644 index 00000000000..6015585d6e8 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_dependency.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000 +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 44 .*: SUCCESS +assertion at file Test.java line 46 .*: FAILURE +-- +-- +Check that when there are dependencies, axioms are adde correctly. diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc new file mode 100644 index 00000000000..eadefb44241 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_det.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.det --verbosity 10 --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 9 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc b/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc new file mode 100644 index 00000000000..30ef54cd492 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToLowerCase/test_nondet.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000 +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 27 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class new file mode 100644 index 00000000000..91c3f958e3a Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java new file mode 100644 index 00000000000..110eb7a1146 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToUpperCase/Test.java @@ -0,0 +1,50 @@ +public class Test { + public String det() + { + StringBuilder builder = new StringBuilder(); + builder.append("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".toLowerCase()); + builder.append("abcdeghijklmnopfrstuqwxyzABCDvFGHIJKLMENOPQRSTUVWXYZ".toUpperCase()); + builder.append("abcdeghijlmnopqrstvwxyzABCDEFGHIJuKLMNOPQRSfkTUVWXYZ".toUpperCase()); + builder.append("acdefghijklmnopqrsuvwxyzABCDEFbGHIJKLMNOPtQRSTUVWXYZ".toUpperCase()); + builder.append("abcdfghijklmnopqrstuvwxyzABCDEFGHIJeKLMNOPQRSTUVWXYZ".toUpperCase()); + return builder.toString(); + } + + public String nonDet(String s) + { + if(s.length() < 20) + return "Short string"; + if(!s.startsWith("a")) + return "String not starting with a"; + + StringBuilder builder = new StringBuilder(); + builder.append(s.toUpperCase()); + builder.append(s.toUpperCase()); + builder.append(":"); + builder.append(s); + builder.append(":"); + builder.append(s.toUpperCase()); + builder.append(s.toUpperCase()); + return builder.toString(); + } + + public String withDependency(String s, boolean b) + { + // Filter + if(s == null || s.length() < 20) + return "Short string"; + if(!s.endsWith("a")) + return "String not ending with a"; + + // Act + String result = s + s.toUpperCase(); + + // Assert + if(b) { + assert(result.endsWith("A")); + } else { + assert(!result.endsWith("A")); + } + return result; + } +} diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc new file mode 100644 index 00000000000..472de29b000 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToUpperCase/test_dependency.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.withDependency --verbosity 10 --max-nondet-string-length 10000 +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 44 .*: SUCCESS +assertion at file Test.java line 46 .*: FAILURE +-- +-- +Check that when there are dependencies, axioms are added correctly. diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc new file mode 100644 index 00000000000..eadefb44241 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToUpperCase/test_det.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.det --verbosity 10 --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 9 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc b/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc new file mode 100644 index 00000000000..30ef54cd492 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringToUpperCase/test_nondet.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000 +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 27 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 3739d6e85c2..d9e67a685aa 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -8,7 +8,9 @@ #include "string_constraint_generator.h" -/// Get the valuation of the string, given a valuation +/// Given a function `get_value` which gives a valuation to expressions, attempt +/// to find the current value of the array `a`. If the valuation of some +/// characters are missing, then return an empty optional. static optionalt> eval_string( const array_string_exprt &a, const std::function &get_value); @@ -187,6 +189,51 @@ 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) +{ + // Characters between 'A' and 'Z' are upper-case + // Characters between 0xc0 (latin capital A with grave) + // and 0xd6 (latin capital O with diaeresis) are upper-case + // Characters between 0xd8 (latin capital O with stroke) + // and 0xde (latin capital thorn) are upper-case + return ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) || + (0xd8 <= c && c <= 0xde); +} + +optionalt string_to_lower_case_builtin_functiont::eval( + const std::function &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)) + 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); +} + +optionalt string_to_upper_case_builtin_functiont::eval( + const std::function &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 string_insertion_builtin_functiont::eval( const std::vector &input1_value, const std::vector &input2_value, diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h index 0480b5d3d65..72e526ab102 100644 --- a/src/solvers/refinement/string_builtin_function.h +++ b/src/solvers/refinement/string_builtin_function.h @@ -30,6 +30,10 @@ class string_builtin_functiont return {}; } + /// Given a function `get_value` which gives a valuation to expressions, + /// attempt to find the result of the builtin function. + /// If not enough information can be gathered from `get_value`, return an + /// empty optional. virtual optionalt eval(const std::function &get_value) const = 0; @@ -177,6 +181,72 @@ class string_set_char_builtin_functiont exprt length_constraint() const override; }; +/// Converting each uppercase character of Basic Latin and Latin-1 supplement +/// to the corresponding lowercase character. +class string_to_lower_case_builtin_functiont + : public string_transformation_builtin_functiont +{ +public: + string_to_lower_case_builtin_functiont( + const exprt &return_code, + const std::vector &fun_args, + array_poolt &array_pool) + : string_transformation_builtin_functiont(return_code, fun_args, array_pool) + { + } + + optionalt + eval(const std::function &get_value) const override; + + std::string name() const override + { + return "to_lower_case"; + } + + exprt add_constraints(string_constraint_generatort &generator) const override + { + return generator.add_axioms_for_to_lower_case(result, input); + }; + + exprt length_constraint() const override + { + return equal_exprt(result.length(), input.length()); + }; +}; + +/// 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 &fun_args, + array_poolt &array_pool) + : string_transformation_builtin_functiont(return_code, fun_args, array_pool) + { + } + + optionalt + eval(const std::function &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 { diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 342c563ac5a..a7d42c514d2 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -175,6 +175,12 @@ class string_constraint_generatort final const array_string_exprt &str, const exprt &position, const exprt &character); + 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); @@ -335,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( diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 91ec22bb45a..597e909d6c7 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -456,10 +456,6 @@ exprt string_constraint_generatort::add_axioms_for_function_application( res=add_axioms_for_compare_to(expr); else if(id==ID_cprover_string_literal_func) res=add_axioms_from_literal(expr); - else if(id==ID_cprover_string_concat_func) - res=add_axioms_for_concat(expr); - else if(id==ID_cprover_string_concat_char_func) - res=add_axioms_for_concat_char(expr); else if(id==ID_cprover_string_concat_code_point_func) res=add_axioms_for_concat_code_point(expr); else if(id==ID_cprover_string_insert_func) @@ -480,18 +476,10 @@ exprt string_constraint_generatort::add_axioms_for_function_application( res=add_axioms_for_substring(expr); else if(id==ID_cprover_string_trim_func) res=add_axioms_for_trim(expr); - else if(id==ID_cprover_string_to_lower_case_func) - res=add_axioms_for_to_lower_case(expr); - else if(id==ID_cprover_string_to_upper_case_func) - res=add_axioms_for_to_upper_case(expr); - else if(id==ID_cprover_string_char_set_func) - res=add_axioms_for_char_set(expr); else if(id==ID_cprover_string_empty_string_func) res=add_axioms_for_empty_string(expr); else if(id==ID_cprover_string_copy_func) res=add_axioms_for_copy(expr); - else if(id==ID_cprover_string_of_int_func) - res=add_axioms_from_int(expr); else if(id==ID_cprover_string_of_int_hex_func) res=add_axioms_from_int_hex(expr); else if(id==ID_cprover_string_of_float_func) diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index a4bad2bdaf6..3a7c55975dc 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -230,15 +230,7 @@ exprt string_constraint_generatort::add_axioms_for_trim( /// Conversion of a string to lower case /// -/// Add axioms ensuring `res` corresponds to `str` in which uppercase characters -/// have been converted to lowercase. -/// These axioms are: -/// 1. \f$ |{\tt res}| = |{\tt str}| \f$ -/// 2. \f$ \forall i<|{\tt str}|.\ {\tt is\_upper\_case}({\tt str}[i])? -/// {\tt res}[i]={\tt str}[i]+diff : {\tt res}[i]={\tt str}[i] -/// \land {\tt str}[i]<{\tt 0x100} \f$ -/// where `diff` is the difference between lower case and upper case -/// characters: `diff = 'a'-'A' = 0x20`. +/// \copydoc add_axioms_for_to_lower_case(const array_string_exprt &, array_string_exprt &) /// /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `str` @@ -251,71 +243,102 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case( const array_string_exprt res = char_array_of_pointer(f.arguments()[1], f.arguments()[0]); const array_string_exprt str = get_string_expr(f.arguments()[2]); - const refined_string_typet &ref_type = - to_refined_string_type(f.arguments()[2].type()); - const typet &char_type=ref_type.get_char_type(); - const typet &index_type=ref_type.get_index_type(); - const exprt char_A=constant_char('A', char_type); - const exprt char_Z=constant_char('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. - - equal_exprt a1(res.length(), str.length()); - lemmas.push_back(a1); + return add_axioms_for_to_lower_case(res, str); +} - symbol_exprt idx=fresh_univ_index("QA_lower_case", index_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, str[idx]), - binary_relation_exprt(str[idx], ID_le, char_Z))); + 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, char_type), ID_le, str[idx]), - binary_relation_exprt(str[idx], ID_le, from_integer(0xd6, char_type)))); + 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, char_type), ID_le, str[idx]), - binary_relation_exprt(str[idx], ID_le, from_integer(0xde, char_type)))); - - exprt is_upper_case=disjunction(upper_case); - - // The difference between upper-case and lower-case for the basic latin and - // latin-1 supplement is 0x20. - exprt diff=from_integer(0x20, char_type); - equal_exprt converted(res[idx], plus_exprt(str[idx], diff)); - and_exprt non_converted( - equal_exprt(res[idx], str[idx]), - binary_relation_exprt(str[idx], ID_lt, from_integer(0x100, char_type))); - if_exprt conditional_convert(is_upper_case, converted, non_converted); - - string_constraintt a2( - idx, zero_if_negative(res.length()), conditional_convert); - constraints.push_back(a2); + 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); +} - return from_integer(0, f.type()); +/// 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. +exprt string_constraint_generatort::add_axioms_for_to_lower_case( + const array_string_exprt &res, + const array_string_exprt &str) +{ + 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. + + lemmas.push_back(equal_exprt(res.length(), str.length())); + + constraints.push_back([&] { + const symbol_exprt idx = fresh_univ_index("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()); } /// Add axioms ensuring `res` corresponds to `str` in which lowercase characters -/// have been converted to uppercase. +/// of Basic Latin and Latin-1 supplement of unicode have been converted to +/// uppercase. /// /// These axioms are: -/// 1. \f$ |{\tt res}| = |{\tt str}| \f$ -/// 2. \f$ \forall i<|{\tt str}|.\ 'a'\le {\tt str}[i]\le 'z' -/// \Rightarrow {\tt res}[i]={\tt str}[i]+'A'-'a' \f$ -/// 3. \f$ \forall i<|{\tt str}|.\ \lnot ('a'\le {\tt str}[i] \le 'z') -/// \Rightarrow {\tt res}[i]={\tt str}[i] \f$ -/// Note that index expressions are only allowed in the body of universal -/// axioms, so we use a trivial premise and push our premise into the body. +/// 1. res.length = str.length +/// 2. forall i < str.length. +/// is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i] /// -/// \todo We can reduce the number of constraints by merging -/// constraints 2 and 3. /// \param res: array of characters expression /// \param str: array of characters expression /// \return integer expression which is different from `0` when there is an @@ -330,32 +353,20 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( exprt char_A=constant_char('A', char_type); exprt char_z=constant_char('z', char_type); - // \todo Add support for locales using case mapping information - // from the UnicodeData file. - - equal_exprt a1(res.length(), str.length()); - lemmas.push_back(a1); + lemmas.push_back(equal_exprt(res.length(), str.length())); - symbol_exprt idx1=fresh_univ_index("QA_upper_case1", index_type); - const and_exprt is_lower_case( - binary_relation_exprt(char_a, ID_le, str[idx1]), - binary_relation_exprt(str[idx1], ID_le, char_z)); - minus_exprt diff(char_A, char_a); - equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff)); - implies_exprt body1(is_lower_case, convert); - string_constraintt a2(idx1, zero_if_negative(res.length()), body1); - constraints.push_back(a2); + constraints.push_back([&] { + const symbol_exprt idx = fresh_univ_index("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]))); + }()); - symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type); - const not_exprt is_not_lower_case( - and_exprt( - binary_relation_exprt(char_a, ID_le, str[idx2]), - binary_relation_exprt(str[idx2], ID_le, char_z))); - equal_exprt eq(res[idx2], str[idx2]); - implies_exprt body2(is_not_lower_case, eq); - string_constraintt a3(idx2, zero_if_negative(res.length()), body2); - constraints.push_back(a3); - return from_integer(0, signedbv_typet(32)); + return from_integer(0, get_return_code_type()); } /// Conversion of a string to upper case diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 05791860b35..85ac59305f5 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -232,6 +232,14 @@ static std::unique_ptr to_string_builtin_function( return util_make_unique( return_code, fun_app.arguments(), array_pool); + if(id == ID_cprover_string_to_lower_case_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + + if(id == ID_cprover_string_to_upper_case_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + return util_make_unique( return_code, fun_app, array_pool); }