diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 8e7947d9636..0192c276394 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1957,6 +1957,9 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]= ID_cprover_string_replace_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.replace:(Ljava/lang/CharSequence;Ljava/lang/CharSequence;)Ljava/lang/String;"]= // NOLINT + ID_cprover_string_replace_func; cprover_equivalent_to_java_function ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]= ID_cprover_string_startswith_func; diff --git a/src/solvers/refinement/expr_cast.h b/src/solvers/refinement/expr_cast.h new file mode 100644 index 00000000000..87531bd8dd1 --- /dev/null +++ b/src/solvers/refinement/expr_cast.h @@ -0,0 +1,71 @@ +/*******************************************************************\ + +Module: exprt conversion functions + +Author: Diffblue ltd. All Rights Reserved + +\*******************************************************************/ + +/// \file +/// Abstraction Refinement Loop + +#ifndef CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H +#define CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H + +#include + +/// Convert exprt to a specific type. Remove empty optional if +/// conversion cannot be performed +/// Generic case doesn't exist, specialize for different types accordingly +/// TODO: this should go to util +template +struct expr_cast_implt final { }; + +template<> +struct expr_cast_implt final +{ + optionalt operator()(const exprt &expr) const + { + mp_integer out; + if(to_integer(expr, out)) + return {}; + return out; + } +}; + +template<> +struct expr_cast_implt final +{ + optionalt operator()(const exprt &expr) const + { + if(const auto tmp=expr_cast_implt()(expr)) + if(tmp->is_long() && *tmp>=0) + return tmp->to_long(); + return {}; + } +}; + +template<> +struct expr_cast_implt final +{ + optionalt operator()(const exprt &expr) const + { + if(is_refined_string_type(expr.type())) + return to_string_expr(expr); + return {}; + } +}; + +template +optionalt expr_cast(const exprt& expr) +{ return expr_cast_implt()(expr); } + +template +T expr_cast_v(const exprt &expr) +{ + const auto maybe=expr_cast(expr); + INVARIANT(maybe, "Bad conversion"); + return *maybe; +} + +#endif // CPROVER_SOLVERS_REFINEMENT_EXPR_CAST_H diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 5bbbba82c6c..7a4c0ba8ff1 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -13,6 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#include "expr_cast.h" /// add axioms to say that the returned string expression `res` has length `k` /// and characters at position `i` in `res` are equal to the character at @@ -359,38 +360,70 @@ string_exprt string_constraint_generatort::add_axioms_for_char_set( return res; } -/// add axioms corresponding to the String.replace java function -/// \par parameters: function application with three arguments, the first is a -/// string, -/// the second and the third are characters +/// 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 +/// Otherwise return empty optional +/// \param expr1 First expression +/// \param expr2 Second expression +/// \return Optional pair of two expressions +static optionalt> to_char_pair( + exprt expr1, exprt expr2) +{ + if((expr1.type().id()==ID_unsignedbv + || expr1.type().id()==ID_char) + && (expr2.type().id()==ID_char + || expr2.type().id()==ID_unsignedbv)) + return std::make_pair(expr1, expr2); + const auto expr1_str=to_string_expr(expr1); + const auto expr2_str=to_string_expr(expr2); + const auto expr1_length=expr_cast(expr1_str.length()); + const auto expr2_length=expr_cast(expr2_str.length()); + if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1) + return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0])); + return { }; +} + +/// Add axioms corresponding to the String.replace java function +/// Only supports String.replace(char, char) and +/// String.replace(String, String) for single-character strings +/// Returns original string in every other case (that behaviour is to +/// be fixed in the future) +/// \param f function application with three arguments, the first is a +/// string, the second and the third are either pair of characters or +/// a pair of strings /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_replace( const function_application_exprt &f) { string_exprt str=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(str.type()); - const exprt &old_char=args(f, 3)[1]; - const exprt &new_char=args(f, 3)[2]; - string_exprt res=fresh_string(ref_type); - - // We add axioms: - // a1 : |res| = |str| - // a2 : forall qvar, 0<=qvar<|res|, - // str[qvar]=oldChar => res[qvar]=newChar - // !str[qvar]=oldChar => res[qvar]=str[qvar] - - m_axioms.push_back(res.axiom_for_has_same_length_as(str)); - - symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type()); - implies_exprt case1( - equal_exprt(str[qvar], old_char), - equal_exprt(res[qvar], new_char)); - implies_exprt case2( - not_exprt(equal_exprt(str[qvar], old_char)), - equal_exprt(res[qvar], str[qvar])); - string_constraintt a2(qvar, res.length(), and_exprt(case1, case2)); - m_axioms.push_back(a2); - return res; + if(const auto maybe_chars=to_char_pair(args(f, 3)[1], args(f, 3)[2])) + { + const auto old_char=maybe_chars->first; + const auto new_char=maybe_chars->second; + string_exprt res=fresh_string(ref_type); + + // We add axioms: + // a1 : |res| = |str| + // a2 : forall qvar, 0<=qvar<|res|, + // str[qvar]=oldChar => res[qvar]=newChar + // !str[qvar]=oldChar => res[qvar]=str[qvar] + + m_axioms.push_back(res.axiom_for_has_same_length_as(str)); + + symbol_exprt qvar=fresh_univ_index("QA_replace", ref_type.get_index_type()); + implies_exprt case1( + equal_exprt(str[qvar], old_char), + equal_exprt(res[qvar], new_char)); + implies_exprt case2( + not_exprt(equal_exprt(str[qvar], old_char)), + equal_exprt(res[qvar], str[qvar])); + string_constraintt a2(qvar, res.length(), and_exprt(case1, case2)); + m_axioms.push_back(a2); + return res; + } + return str; } /// add axioms corresponding to the StringBuilder.deleteCharAt java function diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8cd4924ffec..6fdab35a97a 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -26,6 +26,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #include #include +#include "expr_cast.h" static exprt substitute_array_with_expr(const exprt &expr, const exprt &index); @@ -95,63 +96,6 @@ static exprt get_array( const std::function &super_get, const exprt &arr); -/// Convert exprt to a specific type. Throw bad_cast if conversion -/// cannot be performed -/// Generic case doesn't exist, specialize for different types accordingly -/// TODO: this should go to util - -// Tag dispatching struct - -template -struct expr_cast_implt final { }; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - mp_integer out; - if(to_integer(expr, out)) - return {}; - return out; - } -}; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - if(const auto tmp=expr_cast_implt()(expr)) - if(tmp->is_long() && *tmp>=0) - return tmp->to_long(); - return {}; - } -}; - -template<> -struct expr_cast_implt final -{ - optionalt operator()(const exprt &expr) const - { - if(is_refined_string_type(expr.type())) - return to_string_expr(expr); - return {}; - } -}; - -template -optionalt expr_cast(const exprt& expr) -{ return expr_cast_implt()(expr); } - -template -T expr_cast_v(const exprt &expr) -{ - const auto maybe=expr_cast(expr); - INVARIANT(maybe, "Bad conversion"); - return *maybe; -} - /// Convert index-value map to a vector of values. If a value for an /// index is not defined, set it to the value referenced by the next higher /// index. The length of the resulting vector is the key of the map's