diff --git a/src/solvers/README.md b/src/solvers/README.md index 994ebaaa8c5..a6e92a17944 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -419,35 +419,35 @@ This is described in more detail \link string_builtin_functiont here. \endlink * `cprover_string_associate_length_to_array` : Link the length of the array with the given integer value. * `cprover_string_char_at` : - \copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_char_at More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_char_at More... \endlink * `cprover_string_length` : - \copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_length More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_length More... \endlink \subsection comparisons Comparisons: * `cprover_string_compare_to` : - \copybrief add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink * `cprover_string_contains` : - \copybrief add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink * `cprover_string_equals` : - \copybrief add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink * `cprover_string_equals_ignore_case` : - \copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink * `cprover_string_is_prefix` : - \copybrief add_axioms_for_is_prefix - \link add_axioms_for_is_prefix More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_is_prefix + \link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink * `cprover_string_index_of` : - \copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f=) + \link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink * `cprover_string_last_index_of` : - \copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink \subsection transformations Transformations: @@ -455,23 +455,23 @@ This is described in more detail \link string_builtin_functiont here. \endlink \copybrief string_set_char_builtin_functiont::constraints \link string_set_char_builtin_functiont::constraints More... \endlink * `cprover_string_concat` : - \copybrief add_axioms_for_concat - \link add_axioms_for_concat More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_concat + \link string_constraint_generatort::add_axioms_for_concat More... \endlink * `cprover_string_delete` : - \copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink * `cprover_string_insert` : \copybrief string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const \link string_insertion_builtin_functiont::constraints(string_constraint_generatort &generator) const More... \endlink * `cprover_string_replace` : - \copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink * `cprover_string_set_length` : - \copybrief add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink * `cprover_string_substring` : - \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 + \copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink * `cprover_string_to_lower_case` : \copybrief string_to_lower_case_builtin_functiont::constraints \link string_to_lower_case_builtin_functiont::constraints More... \endlink @@ -479,8 +479,8 @@ This is described in more detail \link string_builtin_functiont here. \endlink \copybrief string_to_upper_case_builtin_functiont::constraints \link string_to_upper_case_builtin_functiont::constraints 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 + \copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink \subsection conversions Conversions: @@ -488,23 +488,23 @@ This is described in more detail \link string_builtin_functiont here. \endlink \copybrief add_axioms_for_format \link add_axioms_for_format More... \endlink * `cprover_string_from_literal` : - \copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink * `cprover_string_of_int` : - \copybrief add_axioms_for_string_of_int - \link add_axioms_for_string_of_int More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_string_of_int + \link string_constraint_generatort::add_axioms_for_string_of_int More... \endlink * `cprover_string_of_float` : - \copybrief add_axioms_for_string_of_float - \link add_axioms_for_string_of_float More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_string_of_float + \link string_constraint_generatort::add_axioms_for_string_of_float More... \endlink * `cprover_string_of_float_scientific_notation` : - \copybrief add_axioms_from_float_scientific_notation - \link add_axioms_from_float_scientific_notation More... \endlink + \copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation + \link string_constraint_generatort::add_axioms_from_float_scientific_notation More... \endlink * `cprover_string_of_char` : - \copybrief add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool) - \link add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool) More... \endlink + \copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) + \link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink * `cprover_string_parse_int` : - \copybrief add_axioms_for_parse_int - \link add_axioms_for_parse_int More... \endlink + \copybrief string_constraint_generatort::add_axioms_for_parse_int + \link string_constraint_generatort::add_axioms_for_parse_int More... \endlink \subsection solvers-deprecated Deprecated primitives: diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp index c902af0654e..0afee4bcca8 100644 --- a/src/solvers/strings/string_builtin_function.cpp +++ b/src/solvers/strings/string_builtin_function.cpp @@ -407,8 +407,8 @@ optionalt string_of_int_builtin_functiont::eval( string_constraintst string_of_int_builtin_functiont::constraints( string_constraint_generatort &generator) const { - auto pair = add_axioms_for_string_of_int_with_radix( - result, arg, radix, 0, generator.ns, array_pool); + auto pair = + generator.add_axioms_for_string_of_int_with_radix(result, arg, radix, 0); pair.second.existential.push_back(equal_exprt(pair.first, return_code)); return pair.second; } diff --git a/src/solvers/strings/string_concatenation_builtin_function.cpp b/src/solvers/strings/string_concatenation_builtin_function.cpp index 8b109fbd872..914f00dc2dd 100644 --- a/src/solvers/strings/string_concatenation_builtin_function.cpp +++ b/src/solvers/strings/string_concatenation_builtin_function.cpp @@ -43,22 +43,19 @@ string_concatenation_builtin_functiont::string_concatenation_builtin_functiont( /// 2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$ /// 3. \f$\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\f$ /// -/// \param fresh_symbol: generator of fresh symbols /// \param res: an array of characters expression /// \param s1: an array of characters expression /// \param s2: an array of characters expression /// \param start_index: integer expression /// \param end_index: integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression `0` -std::pair add_axioms_for_concat_substr( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_concat_substr( const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, - const exprt &end_index, - array_poolt &array_pool) + const exprt &end_index) { string_constraintst constraints; const typet &index_type = start_index.type(); @@ -153,40 +150,28 @@ exprt length_constraint_for_concat_char( /// `s2`. /// /// \deprecated should use concat_substr instead -/// \param fresh_symbol: generator of fresh symbols /// \param res: string_expression corresponding to the result /// \param s1: the string expression to append to /// \param s2: the string expression to append to the first one -/// \param array_pool: pool of arrays representing strings /// \return an integer expression -std::pair add_axioms_for_concat( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_concat( const array_string_exprt &res, const array_string_exprt &s1, - const array_string_exprt &s2, - array_poolt &array_pool) + const array_string_exprt &s2) { exprt index_zero = from_integer(0, s2.length_type()); return add_axioms_for_concat_substr( - fresh_symbol, - res, - s1, - s2, - index_zero, - array_pool.get_or_create_length(s2), - array_pool); + res, s1, s2, index_zero, array_pool.get_or_create_length(s2)); } /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function /// \deprecated java specific -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with two arguments: a string and a code point -/// \param array_pool: pool of arrays representing strings /// \return an expression -std::pair add_axioms_for_concat_code_point( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_concat_code_point( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 4); const array_string_exprt res = @@ -197,8 +182,8 @@ std::pair add_axioms_for_concat_code_point( const array_string_exprt code_point = array_pool.fresh_string(index_type, char_type); return combine_results( - add_axioms_for_code_point(code_point, f.arguments()[3], array_pool), - add_axioms_for_concat(fresh_symbol, res, s1, code_point, array_pool)); + add_axioms_for_code_point(code_point, f.arguments()[3]), + add_axioms_for_concat(res, s1, code_point)); } std::vector string_concatenation_builtin_functiont::eval( @@ -228,18 +213,11 @@ string_constraintst string_concatenation_builtin_functiont::constraints( { auto pair = [&]() -> std::pair { if(args.size() == 0) - return add_axioms_for_concat( - generator.fresh_symbol, result, input1, input2, array_pool); + return generator.add_axioms_for_concat(result, input1, input2); if(args.size() == 2) { - return add_axioms_for_concat_substr( - generator.fresh_symbol, - result, - input1, - input2, - args[0], - args[1], - array_pool); + return generator.add_axioms_for_concat_substr( + result, input1, input2, args[0], args[1]); } UNREACHABLE; }(); diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index ee8b960d310..a263eb8d577 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -74,351 +74,252 @@ class string_constraint_generatort final exprt associate_length_to_array( const exprt &return_code, const function_application_exprt &f); -}; -// Type used by primitives to signal errors -signedbv_typet get_return_code_type(); +public: + std::pair add_axioms_for_concat( + const array_string_exprt &res, + const array_string_exprt &s1, + const array_string_exprt &s2); + + std::pair add_axioms_for_concat_substr( + const array_string_exprt &res, + const array_string_exprt &s1, + const array_string_exprt &s2, + const exprt &start_index, + const exprt &end_index); + std::pair add_axioms_for_insert( + const array_string_exprt &res, + const array_string_exprt &s1, + const array_string_exprt &s2, + const exprt &offset); + std::pair add_axioms_for_string_of_int_with_radix( + const array_string_exprt &res, + const exprt &input_int, + const exprt &radix, + size_t max_size); + + string_constraintst add_constraint_on_characters( + const array_string_exprt &s, + const exprt &start, + const exprt &end, + const std::string &char_set); + std::pair + add_axioms_for_constrain_characters(const function_application_exprt &f); -std::pair add_axioms_for_concat( - symbol_generatort &fresh_symbol, - const array_string_exprt &res, - const array_string_exprt &s1, - const array_string_exprt &s2, - array_poolt &array_pool); -std::pair add_axioms_for_concat_substr( - symbol_generatort &fresh_symbol, - const array_string_exprt &res, - const array_string_exprt &s1, - const array_string_exprt &s2, - const exprt &start_index, - const exprt &end_index, - array_poolt &array_pool); -std::pair add_axioms_for_insert( - symbol_generatort &fresh_symbol, - const array_string_exprt &res, - const array_string_exprt &s1, - const array_string_exprt &s2, - const exprt &offset, - array_poolt &array_pool); -std::pair add_axioms_for_string_of_int_with_radix( - const array_string_exprt &res, - const exprt &input_int, - const exprt &radix, - size_t max_size, - const namespacet &ns, - array_poolt &array_pool); + // The following functions add axioms for the returned value + // to be equal to the result of the function given as argument. + // They are not accessed directly from other classes: they call + // `add_axioms_for_function_application` which determines which of + // these methods should be called. -string_constraintst add_constraint_on_characters( - symbol_generatort &fresh_symbol, - const array_string_exprt &s, - const exprt &start, - const exprt &end, - const std::string &char_set, - array_poolt &array_pool); -std::pair add_axioms_for_constrain_characters( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); + std::pair + add_axioms_for_char_at(const function_application_exprt &f); + std::pair + add_axioms_for_code_point_at(const function_application_exprt &f); -// The following functions add axioms for the returned value -// to be equal to the result of the function given as argument. -// They are not accessed directly from other classes: they call -// `add_axioms_for_function_application` which determines which of -// these methods should be called. + std::pair + add_axioms_for_code_point_before(const function_application_exprt &f); + std::pair + add_axioms_for_contains(const function_application_exprt &f); + std::pair + add_axioms_for_equals(const function_application_exprt &f); + std::pair + add_axioms_for_equals_ignore_case(const function_application_exprt &f); -std::pair add_axioms_for_char_at( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_code_point_at( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_code_point_before( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_contains( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_equals( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_equals_ignore_case( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); + std::pair + add_axioms_for_is_empty(const function_application_exprt &f); + std::pair add_axioms_for_is_prefix( + const array_string_exprt &prefix, + const array_string_exprt &str, + const exprt &offset); + std::pair add_axioms_for_is_prefix( + const function_application_exprt &f, + bool swap_arguments); + + std::pair add_axioms_for_is_suffix( + const function_application_exprt &f, + bool swap_arguments); + std::pair + add_axioms_for_length(const function_application_exprt &f); + std::pair + add_axioms_for_empty_string(const function_application_exprt &f); -std::pair add_axioms_for_is_empty( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_is_prefix( - symbol_generatort &fresh_symbol, - const array_string_exprt &prefix, - const array_string_exprt &str, - const exprt &offset); -std::pair add_axioms_for_is_prefix( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - bool swap_arguments, - array_poolt &array_pool); -std::pair add_axioms_for_is_suffix( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - bool swap_arguments, - array_poolt &array_pool); -std::pair add_axioms_for_length( - const function_application_exprt &f, - array_poolt &array_pool); -std::pair -add_axioms_for_empty_string(const function_application_exprt &f); + std::pair + add_axioms_for_copy(const function_application_exprt &f); -std::pair add_axioms_for_copy( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); + std::pair + add_axioms_for_concat_code_point(const function_application_exprt &f); + std::pair add_axioms_for_constant( + const array_string_exprt &res, + irep_idt sval, + const exprt &guard = true_exprt()); + + std::pair add_axioms_for_delete( + const array_string_exprt &res, + const array_string_exprt &str, + const exprt &start, + const exprt &end); + std::pair + add_axioms_for_delete(const function_application_exprt &f); + std::pair + add_axioms_for_delete_char_at(const function_application_exprt &expr); -std::pair add_axioms_for_concat_code_point( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_constant( - const array_string_exprt &res, - irep_idt sval, - array_poolt &array_pool, - const exprt &guard = true_exprt()); + std::pair add_axioms_for_cprover_string( + const array_string_exprt &res, + const exprt &arg, + const exprt &guard); + std::pair + add_axioms_from_literal(const function_application_exprt &f); -std::pair add_axioms_for_delete( - symbol_generatort &fresh_symbol, - const array_string_exprt &res, - const array_string_exprt &str, - const exprt &start, - const exprt &end, - array_poolt &array_pool); -std::pair add_axioms_for_delete( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_delete_char_at( - symbol_generatort &fresh_symbol, - const function_application_exprt &expr, - array_poolt &array_pool); + std::pair add_axioms_for_string_of_int( + const array_string_exprt &res, + const exprt &input_int, + size_t max_size); + std::pair + add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i); + std::pair + add_axioms_from_int_hex(const function_application_exprt &f); + std::pair + add_axioms_from_long(const function_application_exprt &f); + std::pair + add_axioms_from_bool(const function_application_exprt &f); + std::pair + add_axioms_from_bool(const array_string_exprt &res, const exprt &b); + std::pair + add_axioms_from_char(const function_application_exprt &f); + std::pair + add_axioms_from_char(const array_string_exprt &res, const exprt &c); + std::pair add_axioms_for_index_of( + const array_string_exprt &str, + const exprt &c, + const exprt &from_index); + std::pair add_axioms_for_index_of_string( + const array_string_exprt &haystack, + const array_string_exprt &needle, + const exprt &from_index); + std::pair + add_axioms_for_index_of(const function_application_exprt &f); + std::pair add_axioms_for_last_index_of_string( + const array_string_exprt &haystack, + const array_string_exprt &needle, + const exprt &from_index); + std::pair add_axioms_for_last_index_of( + const array_string_exprt &str, + const exprt &c, + const exprt &from_index); -std::pair add_axioms_for_cprover_string( - symbol_generatort &fresh_symbol, - const array_string_exprt &res, - const exprt &arg, - const exprt &guard, - array_poolt &array_pool); -std::pair add_axioms_from_literal( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); + std::pair + add_axioms_for_last_index_of(const function_application_exprt &f); -std::pair add_axioms_for_string_of_int( - const array_string_exprt &res, - const exprt &input_int, - size_t max_size, - const namespacet &ns, - array_poolt &array_pool); -std::pair add_axioms_from_int_hex( - const array_string_exprt &res, - const exprt &i, - array_poolt &array_pool); -std::pair add_axioms_from_int_hex( - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_from_long( - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns); -std::pair add_axioms_from_bool( - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_from_bool( - const array_string_exprt &res, - const exprt &b, - array_poolt &array_pool); -std::pair add_axioms_from_char( - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_from_char( - const array_string_exprt &res, - const exprt &c, - array_poolt &array_pool); -std::pair add_axioms_for_index_of( - symbol_generatort &fresh_symbol, - const array_string_exprt &str, - const exprt &c, - const exprt &from_index, - array_poolt &array_pool); -std::pair add_axioms_for_index_of_string( - symbol_generatort &fresh_symbol, - const array_string_exprt &haystack, - const array_string_exprt &needle, - const exprt &from_index, - array_poolt &array_pool); -std::pair add_axioms_for_index_of( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_last_index_of_string( - symbol_generatort &fresh_symbol, - const array_string_exprt &haystack, - const array_string_exprt &needle, - const exprt &from_index, - array_poolt &array_pool); -std::pair add_axioms_for_last_index_of( - symbol_generatort &fresh_symbol, - const array_string_exprt &str, - const exprt &c, - const exprt &from_index, - array_poolt &array_pool); + /// \todo The specifications of these functions is only partial. + /// We currently only specify that the string for NaN is "NaN", for infinity + /// and minus infinity the string are "Infinity" and "-Infinity respectively + /// otherwise the string contains only characters in [0123456789.] and '-' at + /// the start for negative number + std::pair + add_axioms_for_string_of_float(const function_application_exprt &f); + std::pair + add_axioms_for_string_of_float(const array_string_exprt &res, const exprt &f); + std::pair add_axioms_for_fractional_part( + const array_string_exprt &res, + const exprt &int_expr, + size_t max_size); + std::pair + add_axioms_from_float_scientific_notation( + const array_string_exprt &res, + const exprt &f); + std::pair + add_axioms_from_float_scientific_notation( + const function_application_exprt &f); -std::pair add_axioms_for_last_index_of( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); + /// Add axioms corresponding to the String.valueOf(D) java function + /// \todo The specifications is only partial. + std::pair + add_axioms_from_double(const function_application_exprt &f); -/// \todo The specifications of these functions is only partial. -/// We currently only specify that the string for NaN is "NaN", for infinity -/// and minus infinity the string are "Infinity" and "-Infinity respectively -/// otherwise the string contains only characters in [0123456789.] and '-' at -/// the start for negative number -std::pair add_axioms_for_string_of_float( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns); -std::pair add_axioms_for_string_of_float( - symbol_generatort &fresh_symbol, - const array_string_exprt &res, - const exprt &f, - array_poolt &array_pool, - const namespacet &ns); -std::pair add_axioms_for_fractional_part( + std::pair + add_axioms_for_replace(const function_application_exprt &f); + std::pair + add_axioms_for_set_length(const function_application_exprt &f); + + /// \todo The specification may not be correct for the case where the + /// string is shorter than end. An actual java program should throw an + /// exception in that case. + std::pair add_axioms_for_substring( + const array_string_exprt &res, + const array_string_exprt &str, + const exprt &start, + const exprt &end); + std::pair + add_axioms_for_substring(const function_application_exprt &f); + + std::pair + add_axioms_for_trim(const function_application_exprt &f); + + std::pair add_axioms_for_code_point( + const array_string_exprt &res, + const exprt &code_point); + std::pair + add_axioms_for_char_literal(const function_application_exprt &f); + + /// Add axioms corresponding the String.codePointCount java function + /// \todo This function is underspecified, we do not compute the exact value + /// but over approximate it. + /// \deprecated This is Java specific and should be implemented in Java. + DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) + std::pair + add_axioms_for_code_point_count(const function_application_exprt &f); + + /// Add axioms corresponding the String.offsetByCodePointCount java function + /// \todo This function is underspecified, it should return the index within + /// this String that is offset from the given first argument by second + /// argument code points and we approximate this by saying the result is + /// between index + offset and index + 2 * offset. + /// \deprecated This is Java specific and should be implemented in Java. + DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) + std::pair + add_axioms_for_offset_by_code_point(const function_application_exprt &f); + + string_constraintst add_axioms_for_characters_in_integer_string( + const exprt &input_int, + const typet &type, + const bool strict_formatting, + const array_string_exprt &str, + const std::size_t max_string_length, + const exprt &radix, + const unsigned long radix_ul); + string_constraintst add_axioms_for_correct_number_format( + const array_string_exprt &str, + const exprt &radix_as_char, + const unsigned long radix_ul, + const std::size_t max_size, + const bool strict_formatting); + std::pair + add_axioms_for_parse_int(const function_application_exprt &f); + std::pair + add_axioms_for_compare_to(const function_application_exprt &f); + + std::pair combine_results( + std::pair result1, + std::pair result2); +}; + +exprt length_constraint_for_concat_char( const array_string_exprt &res, - const exprt &int_expr, - size_t max_size, + const array_string_exprt &s1, array_poolt &array_pool); -std::pair add_axioms_from_float_scientific_notation( - symbol_generatort &fresh_symbol, +exprt length_constraint_for_concat( const array_string_exprt &res, - const exprt &f, - array_poolt &array_pool, - const namespacet &ns); -std::pair add_axioms_from_float_scientific_notation( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns); - -/// Add axioms corresponding to the String.valueOf(D) java function -/// \todo The specifications is only partial. -std::pair add_axioms_from_double( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns); - -std::pair add_axioms_for_replace( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); -std::pair add_axioms_for_set_length( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, + const array_string_exprt &s1, + const array_string_exprt &s2, array_poolt &array_pool); - -/// \todo The specification may not be correct for the case where the -/// string is shorter than end. An actual java program should throw an -/// exception in that case. -std::pair add_axioms_for_substring( - symbol_generatort &fresh_symbol, +exprt length_constraint_for_concat_substr( const array_string_exprt &res, - const array_string_exprt &str, + const array_string_exprt &s1, + const array_string_exprt &s2, const exprt &start, const exprt &end, array_poolt &array_pool); -std::pair add_axioms_for_substring( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); - -std::pair add_axioms_for_trim( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); - -std::pair add_axioms_for_code_point( - const array_string_exprt &res, - const exprt &code_point, - array_poolt &array_pool); -std::pair -add_axioms_for_char_literal(const function_application_exprt &f); - -/// Add axioms corresponding the String.codePointCount java function -/// \todo This function is underspecified, we do not compute the exact value -/// but over approximate it. -/// \deprecated This is Java specific and should be implemented in Java. -DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) -std::pair add_axioms_for_code_point_count( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); - -/// Add axioms corresponding the String.offsetByCodePointCount java function -/// \todo This function is underspecified, it should return the index within -/// this String that is offset from the given first argument by second -/// argument code points and we approximate this by saying the result is -/// between index + offset and index + 2 * offset. -/// \deprecated This is Java specific and should be implemented in Java. -DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) -std::pair add_axioms_for_offset_by_code_point( - symbol_generatort &fresh_symbol, - const function_application_exprt &f); - -string_constraintst add_axioms_for_characters_in_integer_string( - const exprt &input_int, - const typet &type, - const bool strict_formatting, - const array_string_exprt &str, - const std::size_t max_string_length, - const exprt &radix, - const unsigned long radix_ul, - array_poolt &array_pool); -string_constraintst add_axioms_for_correct_number_format( - const array_string_exprt &str, - const exprt &radix_as_char, - const unsigned long radix_ul, - const std::size_t max_size, - const bool strict_formatting, - array_poolt &array_pool); -std::pair add_axioms_for_parse_int( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns); -std::pair add_axioms_for_compare_to( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool); - -exprt is_digit_with_radix( - const exprt &chr, - const bool strict_formatting, - const exprt &radix_as_char, - const unsigned long radix_ul); - -exprt get_numeric_value_from_character( - const exprt &chr, - const typet &char_type, - const typet &type, - const bool strict_formatting, - unsigned long radix_ul); size_t max_printed_string_length(const typet &type, unsigned long ul_radix); @@ -433,26 +334,22 @@ exprt maximum(const exprt &a, const exprt &b); /// \return Boolean true when the sum of the two expressions overflows exprt sum_overflows(const plus_exprt &sum); -exprt length_constraint_for_concat_char( - const array_string_exprt &res, - const array_string_exprt &s1, - array_poolt &array_pool); -exprt length_constraint_for_concat( - const array_string_exprt &res, - const array_string_exprt &s1, - const array_string_exprt &s2, - array_poolt &array_pool); -exprt length_constraint_for_concat_substr( - const array_string_exprt &res, - const array_string_exprt &s1, - const array_string_exprt &s2, - const exprt &start, - const exprt &end, - array_poolt &array_pool); +// Type used by primitives to signal errors +signedbv_typet get_return_code_type(); exprt zero_if_negative(const exprt &expr); -std::pair combine_results( - std::pair result1, - std::pair result2); +exprt is_digit_with_radix( + const exprt &chr, + const bool strict_formatting, + const exprt &radix_as_char, + const unsigned long radix_ul); + +exprt get_numeric_value_from_character( + const exprt &chr, + const typet &char_type, + const typet &type, + const bool strict_formatting, + unsigned long radix_ul); + #endif diff --git a/src/solvers/strings/string_constraint_generator_code_points.cpp b/src/solvers/strings/string_constraint_generator_code_points.cpp index def8e803c2f..0be58b20ada 100644 --- a/src/solvers/strings/string_constraint_generator_code_points.cpp +++ b/src/solvers/strings/string_constraint_generator_code_points.cpp @@ -16,12 +16,11 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// code point to a utf-16 string /// \param res: array of characters corresponding to the result fo the function /// \param code_point: an expression representing a java code point -/// \param array_pool: pool of arrays representing strings /// \return integer expression equal to zero -std::pair add_axioms_for_code_point( +std::pair +string_constraint_generatort::add_axioms_for_code_point( const array_string_exprt &res, - const exprt &code_point, - array_poolt &array_pool) + const exprt &code_point) { string_constraintst constraints; const typet &char_type = res.content().type().subtype(); @@ -116,15 +115,12 @@ exprt pair_value(exprt char1, exprt char2, typet return_type) } /// add axioms corresponding to the String.codePointAt java function -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments a string and an /// index -/// \param array_pool: pool of arrays representing strings /// \return a integer expression corresponding to a code point -std::pair add_axioms_for_code_point_at( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_code_point_at( + const function_application_exprt &f) { string_constraintst constraints; const typet &return_type = f.type(); @@ -154,10 +150,9 @@ std::pair add_axioms_for_code_point_at( /// \par parameters: function application with two arguments: a string and an /// index /// \return a integer expression corresponding to a code point -std::pair add_axioms_for_code_point_before( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_code_point_before( + const function_application_exprt &f) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 2); @@ -187,15 +182,12 @@ std::pair add_axioms_for_code_point_before( /// add axioms giving approximate bounds on the result of the /// String.codePointCount java function -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with three arguments string `str`, integer /// `begin` and integer `end`. -/// \param array_pool: pool of arrays representing strings /// \return an integer expression -std::pair add_axioms_for_code_point_count( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_code_point_count( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); string_constraintst constraints; @@ -216,12 +208,11 @@ std::pair add_axioms_for_code_point_count( /// add axioms giving approximate bounds on the result of the /// String.offsetByCodePointCount java function. We approximate the result by /// saying the result is between index + offset and index + 2 * offset -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments string `str`, integer `index` /// and integer `offset`. /// \return a new string expression -std::pair add_axioms_for_offset_by_code_point( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_offset_by_code_point( const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); diff --git a/src/solvers/strings/string_constraint_generator_comparison.cpp b/src/solvers/strings/string_constraint_generator_comparison.cpp index 84f92bb4ad1..7ac0c52e007 100644 --- a/src/solvers/strings/string_constraint_generator_comparison.cpp +++ b/src/solvers/strings/string_constraint_generator_comparison.cpp @@ -24,15 +24,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// 2. \f$ \forall i<|s_1|.\ eq \Rightarrow s_1[i]=s_2[i] \f$ /// 3. \f$ \lnot eq \Rightarrow (|s_1| \ne |s_2| \land witness=-1) /// \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `s1` and /// refined_string `s2` -/// \param array_pool: pool of arrays representing strings /// \return Boolean expression `eq` -std::pair add_axioms_for_equals( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_equals( + const function_application_exprt &f) { PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(f.arguments().size() == 2); @@ -131,15 +128,12 @@ static exprt character_equals_ignore_case( /// \ eq \Rightarrow {\tt equal\_ignore\_case}(s_1[i],s_2[i]) \f$ /// 3. \f$ \lnot eq \Rightarrow |s_1| \ne |s_2| \lor (0 \le witness<|s_1| /// \land\lnot {\tt equal\_ignore\_case}(s_1[witness],s_2[witness]) \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `s1` and /// refined_string `s2` -/// \param array_pool: pool of arrays representing strings /// \return Boolean expression `eq` -std::pair add_axioms_for_equals_ignore_case( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_equals_ignore_case( + const function_application_exprt &f) { PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(f.arguments().size() == 2); @@ -206,15 +200,12 @@ std::pair add_axioms_for_equals_ignore_case( /// (|s1|<|s2| \land x=|s1|) \lor (|s1| > |s2| \land x=|s2|) /// \land res=|s1|-|s2|) \f$ /// * \f$ \forall i' add_axioms_for_compare_to( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_compare_to( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); const typet &return_type = f.type(); diff --git a/src/solvers/strings/string_constraint_generator_constants.cpp b/src/solvers/strings/string_constraint_generator_constants.cpp index 6101a6be320..35a1fb8c01f 100644 --- a/src/solvers/strings/string_constraint_generator_constants.cpp +++ b/src/solvers/strings/string_constraint_generator_constants.cpp @@ -18,13 +18,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// equal. /// \param res: array of characters for the result /// \param sval: a string constant -/// \param array_pool: pool of arrays representing strings /// \param guard: condition under which the axiom should apply, true by default /// \return integer expression equal to zero -std::pair add_axioms_for_constant( +std::pair +string_constraint_generatort::add_axioms_for_constant( const array_string_exprt &res, irep_idt sval, - array_poolt &array_pool, const exprt &guard) { string_constraintst constraints; @@ -62,7 +61,8 @@ std::pair add_axioms_for_constant( /// pointer `ptr`. /// \return integer expression equal to zero std::pair -add_axioms_for_empty_string(const function_application_exprt &f) +string_constraint_generatort::add_axioms_for_empty_string( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); string_constraintst constraints; @@ -73,34 +73,28 @@ add_axioms_for_empty_string(const function_application_exprt &f) } /// Convert an expression of type string_typet to a string_exprt -/// \param fresh_symbol: generator of fresh symbols /// \param res: string expression for the result /// \param arg: expression of type string typet /// \param guard: condition under which `res` should be equal to arg -/// \param array_pool: pool of arrays representing strings /// \return 0 if constraints were added, 1 if expression could not be handled /// and no constraint was added. Expression we can handle are of the form /// \f$ e := "" | (expr)? e : e \f$ -std::pair add_axioms_for_cprover_string( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_cprover_string( const array_string_exprt &res, const exprt &arg, - const exprt &guard, - array_poolt &array_pool) + const exprt &guard) { if(const auto if_expr = expr_try_dynamic_cast(arg)) { const and_exprt guard_true(guard, if_expr->cond()); const and_exprt guard_false(guard, not_exprt(if_expr->cond())); return combine_results( - add_axioms_for_cprover_string( - fresh_symbol, res, if_expr->true_case(), guard_true, array_pool), - add_axioms_for_cprover_string( - fresh_symbol, res, if_expr->false_case(), guard_false, array_pool)); + add_axioms_for_cprover_string(res, if_expr->true_case(), guard_true), + add_axioms_for_cprover_string(res, if_expr->false_case(), guard_false)); } else if(const auto constant_expr = expr_try_dynamic_cast(arg)) - return add_axioms_for_constant( - res, constant_expr->get_value(), array_pool, guard); + return add_axioms_for_constant(res, constant_expr->get_value(), guard); else return {from_integer(1, get_return_code_type()), {}}; } @@ -110,19 +104,15 @@ std::pair add_axioms_for_cprover_string( /// Add axioms ensuring that the returned string expression is equal to the /// string literal. /// \todo The name of the function should be changed to reflect what it does. -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with an argument which is a string literal /// that is a constant with a string value. -/// \param array_pool: pool of arrays representing strings /// \return string expression -std::pair add_axioms_from_literal( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_from_literal( + const function_application_exprt &f) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 3); // Bad args to string literal? const array_string_exprt res = array_pool.find(args[1], args[0]); - return add_axioms_for_cprover_string( - fresh_symbol, res, args[2], true_exprt(), array_pool); + return add_axioms_for_cprover_string(res, args[2], true_exprt()); } diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp index 7f207e25212..2afcf9342f2 100644 --- a/src/solvers/strings/string_constraint_generator_float.cpp +++ b/src/solvers/strings/string_constraint_generator_float.cpp @@ -153,36 +153,25 @@ exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) /// String representation of a float value /// /// Add axioms corresponding to the String.valueOf(F) java function -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one float argument -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return an integer expression -std::pair add_axioms_for_string_of_float( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns) +std::pair +string_constraint_generatort::add_axioms_for_string_of_float( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); - return add_axioms_for_string_of_float( - fresh_symbol, res, f.arguments()[2], array_pool, ns); + return add_axioms_for_string_of_float(res, f.arguments()[2]); } /// Add axioms corresponding to the String.valueOf(D) java function -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one double argument -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return an integer expression -std::pair add_axioms_from_double( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns) +std::pair +string_constraint_generatort::add_axioms_from_double( + const function_application_exprt &f) { - return add_axioms_for_string_of_float(fresh_symbol, f, array_pool, ns); + return add_axioms_for_string_of_float(f); } /// Add axioms corresponding to the integer part of m, in decimal form with no @@ -193,19 +182,14 @@ std::pair add_axioms_from_double( /// /// \todo This specification is not correct for negative numbers and /// double precision. -/// \param fresh_symbol: generator of fresh symbols /// \param res: string expression corresponding to the result /// \param f: a float expression, which is positive -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return an integer expression, different from zero if an error should be /// raised -std::pair add_axioms_for_string_of_float( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_string_of_float( const array_string_exprt &res, - const exprt &f, - array_poolt &array_pool, - const namespacet &ns) + const exprt &f) { const floatbv_typet &type = to_floatbv_type(f.type()); const ieee_float_spect float_spec(type); @@ -223,8 +207,8 @@ std::pair add_axioms_for_string_of_float( const mod_exprt fractional_part(shifted, max_non_exponent_notation); const array_string_exprt fractional_part_str = array_pool.fresh_string(index_type, char_type); - auto result1 = add_axioms_for_fractional_part( - fractional_part_str, fractional_part, 6, array_pool); + auto result1 = + add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6); // The axiom added to convert to integer should always be satisfiable even // when the preconditions are not satisfied. @@ -234,11 +218,11 @@ std::pair add_axioms_for_string_of_float( // part of the float. const array_string_exprt integer_part_str = array_pool.fresh_string(index_type, char_type); - auto result2 = add_axioms_for_string_of_int( - integer_part_str, integer_part, 8, ns, array_pool); + auto result2 = + add_axioms_for_string_of_int(integer_part_str, integer_part, 8); - auto result3 = add_axioms_for_concat( - fresh_symbol, res, integer_part_str, fractional_part_str, array_pool); + auto result3 = + add_axioms_for_concat(res, integer_part_str, fractional_part_str); merge(result3.second, std::move(result1.second)); merge(result3.second, std::move(result2.second)); @@ -253,13 +237,12 @@ std::pair add_axioms_for_string_of_float( /// \param int_expr: an integer expression /// \param max_size: a maximal size for the string, this includes the /// potential minus sign and therefore should be greater than 2 -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success -std::pair add_axioms_for_fractional_part( +std::pair +string_constraint_generatort::add_axioms_for_fractional_part( const array_string_exprt &res, const exprt &int_expr, - size_t max_size, - array_poolt &array_pool) + size_t max_size) { PRECONDITION(int_expr.type().id() == ID_signedbv); PRECONDITION(max_size >= 2); @@ -345,18 +328,13 @@ std::pair add_axioms_for_fractional_part( /// \f$log_10(n) = log_10(m) + log_10(2) * e - d\f$ /// \f$n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\f$ /// \todo For now we only consider single precision. -/// \param fresh_symbol: generator of fresh symbols /// \param res: string expression representing the float in scientific notation /// \param float_expr: a float expression, which is positive -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return a integer expression different from 0 to signal an exception -std::pair add_axioms_from_float_scientific_notation( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_from_float_scientific_notation( const array_string_exprt &res, - const exprt &float_expr, - array_poolt &array_pool, - const namespacet &ns) + const exprt &float_expr) { string_constraintst constraints; const ieee_float_spect float_spec = ieee_float_spect::single_precision(); @@ -469,7 +447,7 @@ std::pair add_axioms_from_float_scientific_notation( array_string_exprt string_expr_integer_part = array_pool.fresh_string(index_type, char_type); auto result1 = add_axioms_for_string_of_int( - string_expr_integer_part, dec_significand_int, 3, ns, array_pool); + string_expr_integer_part, dec_significand_int, 3); minus_exprt fractional_part( dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); @@ -489,41 +467,35 @@ std::pair add_axioms_from_float_scientific_notation( array_string_exprt string_fractional_part = array_pool.fresh_string(index_type, char_type); auto result2 = add_axioms_for_fractional_part( - string_fractional_part, fractional_part_shifted, 6, array_pool); + string_fractional_part, fractional_part_shifted, 6); // string_expr_with_fractional_part = // concat(string_with_do, string_fractional_part) const array_string_exprt string_expr_with_fractional_part = array_pool.fresh_string(index_type, char_type); auto result3 = add_axioms_for_concat( - fresh_symbol, string_expr_with_fractional_part, string_expr_integer_part, - string_fractional_part, - array_pool); + string_fractional_part); // string_expr_with_E = concat(string_fraction, string_lit_E) const array_string_exprt stringE = array_pool.fresh_string(index_type, char_type); - auto result4 = add_axioms_for_constant(stringE, "E", array_pool); + auto result4 = add_axioms_for_constant(stringE, "E"); const array_string_exprt string_expr_with_E = array_pool.fresh_string(index_type, char_type); auto result5 = add_axioms_for_concat( - fresh_symbol, - string_expr_with_E, - string_expr_with_fractional_part, - stringE, - array_pool); + string_expr_with_E, string_expr_with_fractional_part, stringE); // exponent_string = string_of_int(decimal_exponent) const array_string_exprt exponent_string = array_pool.fresh_string(index_type, char_type); - auto result6 = add_axioms_for_string_of_int( - exponent_string, decimal_exponent, 3, ns, array_pool); + auto result6 = + add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3); // string_expr = concat(string_expr_with_E, exponent_string) - auto result7 = add_axioms_for_concat( - fresh_symbol, res, string_expr_with_E, exponent_string, array_pool); + auto result7 = + add_axioms_for_concat(res, string_expr_with_E, exponent_string); const exprt return_code = maximum( result1.first, @@ -547,21 +519,15 @@ std::pair add_axioms_from_float_scientific_notation( /// /// Add axioms corresponding to the scientific representation of floating point /// values -/// \param fresh_symbol: generator of fresh symbols /// \param f: a function application expression -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return code 0 on success -std::pair add_axioms_from_float_scientific_notation( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns) +std::pair +string_constraint_generatort::add_axioms_from_float_scientific_notation( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); const array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); const exprt &arg = f.arguments()[2]; - return add_axioms_from_float_scientific_notation( - fresh_symbol, res, arg, array_pool, ns); + return add_axioms_from_float_scientific_notation(res, arg); } diff --git a/src/solvers/strings/string_constraint_generator_indexof.cpp b/src/solvers/strings/string_constraint_generator_indexof.cpp index 8f37d5e2f1f..9a3e1f33633 100644 --- a/src/solvers/strings/string_constraint_generator_indexof.cpp +++ b/src/solvers/strings/string_constraint_generator_indexof.cpp @@ -30,18 +30,15 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// 5. \f$ \forall m, n \in [{\tt from\_index}, |{\tt haystack}|) /// .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle} /// \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param str: an array of characters expression /// \param c: a character expression /// \param from_index: an integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression `index` -std::pair add_axioms_for_index_of( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_index_of( const array_string_exprt &str, const exprt &c, - const exprt &from_index, - array_poolt &array_pool) + const exprt &from_index) { string_constraintst constraints; const typet &index_type = str.length_type(); @@ -104,19 +101,16 @@ std::pair add_axioms_for_index_of( /// .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) /// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$ /// 6. \f$ |{\tt needle}| = 0 \Rightarrow \tt{index} = from_index \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param haystack: an array of character expression /// \param needle: an array of character expression /// \param from_index: an integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression `index` representing the first index of `needle` /// in `haystack` -std::pair add_axioms_for_index_of_string( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_index_of_string( const array_string_exprt &haystack, const array_string_exprt &needle, - const exprt &from_index, - array_poolt &array_pool) + const exprt &from_index) { string_constraintst constraints; const typet &index_type = haystack.length_type(); @@ -207,19 +201,16 @@ std::pair add_axioms_for_index_of_string( /// (\exists m \in [0,|{\tt needle}|) /// .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \f$ /// 6. \f$ |{\tt needle}| = 0 \Rightarrow index = from_index \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param haystack: an array of characters expression /// \param needle: an array of characters expression /// \param from_index: integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression `index` representing the last index of `needle` /// in `haystack` before or at `from_index`, or -1 if there is none -std::pair add_axioms_for_last_index_of_string( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_last_index_of_string( const array_string_exprt &haystack, const array_string_exprt &needle, - const exprt &from_index, - array_poolt &array_pool) + const exprt &from_index) { string_constraintst constraints; const typet &index_type = haystack.length_type(); @@ -293,9 +284,9 @@ std::pair add_axioms_for_last_index_of_string( /// /// If the target is a character: // NOLINTNEXTLINE -/// \copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &) +/// \copybrief add_axioms_for_index_of(const array_string_exprt&,const exprt&,const exprt&) // NOLINTNEXTLINE -/// \link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &) +/// \link add_axioms_for_index_of(const array_string_exprt&,const exprt&,const exprt&) /// (More...) \endlink /// /// If the target is a refined_string: @@ -303,16 +294,13 @@ std::pair add_axioms_for_last_index_of_string( /// \link add_axioms_for_index_of_string (More...) /// \endlink /// \warning slow for string targets -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `haystack`, /// refined_string or character `needle`, and optional integer `from_index` /// with default value `0` -/// \param array_pool: pool of arrays representing strings /// \return integer expression -std::pair add_axioms_for_index_of( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_index_of( + const function_application_exprt &f) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 2 || args.size() == 3); @@ -327,7 +315,7 @@ std::pair add_axioms_for_index_of( if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv) { return add_axioms_for_index_of( - fresh_symbol, str, typecast_exprt(c, char_type), from_index, array_pool); + str, typecast_exprt(c, char_type), from_index); } else { @@ -337,8 +325,7 @@ std::pair add_axioms_for_index_of( "c can only be a (un)signedbv or a refined " "string and the (un)signedbv case is already handled")); array_string_exprt sub = get_string_expr(array_pool, c); - return add_axioms_for_index_of_string( - fresh_symbol, str, sub, from_index, array_pool); + return add_axioms_for_index_of_string(str, sub, from_index); } } @@ -360,19 +347,16 @@ std::pair add_axioms_for_index_of( /// 5. \f$ \forall m \in [0, /// min({\tt from\_index}+1, |{\tt haystack}|)) /// .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}\f$ -/// \param fresh_symbol: generator of fresh symbols /// \param str: an array of characters expression /// \param c: a character expression /// \param from_index: an integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression `index` representing the last index of `needle` /// in `haystack` before or at `from_index`, or `-1` if there is none -std::pair add_axioms_for_last_index_of( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_last_index_of( const array_string_exprt &str, const exprt &c, - const exprt &from_index, - array_poolt &array_pool) + const exprt &from_index) { string_constraintst constraints; const typet &index_type = str.length_type(); @@ -422,9 +406,9 @@ std::pair add_axioms_for_last_index_of( /// /// If the target is a character: // NOLINTNEXTLINE -/// \copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &) +/// \copybrief add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&) // NOLINTNEXTLINE -/// \link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const array_string_exprt&,const exprt&,const exprt&, array_poolt &) +/// \link add_axioms_for_last_index_of(const array_string_exprt&,const exprt&,const exprt&) /// (More...) \endlink /// /// If the target is a refined_string: @@ -432,16 +416,13 @@ std::pair add_axioms_for_last_index_of( /// \link add_axioms_for_last_index_of_string /// (More...) \endlink /// \warning slow for string targets -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `haystack`, /// refined_string or character `needle`, and optional integer /// `from_index` with default value `|haystack|-1` -/// \param array_pool: pool of arrays representing strings /// \return an integer expression -std::pair add_axioms_for_last_index_of( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_last_index_of( + const function_application_exprt &f) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 2 || args.size() == 3); @@ -457,12 +438,11 @@ std::pair add_axioms_for_last_index_of( if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv) { return add_axioms_for_last_index_of( - fresh_symbol, str, typecast_exprt(c, char_type), from_index, array_pool); + str, typecast_exprt(c, char_type), from_index); } else { const array_string_exprt sub = get_string_expr(array_pool, c); - return add_axioms_for_last_index_of_string( - fresh_symbol, str, sub, from_index, array_pool); + return add_axioms_for_last_index_of_string(str, sub, from_index); } } diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index ef35a268c4f..4b9babd63aa 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -25,11 +25,11 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include +#include #include #include #include #include -#include string_constraint_generatort::string_constraint_generatort(const namespacet &ns) : array_pool(fresh_symbol), ns(ns) @@ -117,23 +117,19 @@ void merge(string_constraintst &result, string_constraintst other) /// /// This constraint is /// \f$ \forall i \in [start, end), low\_char \le s[i] \le high\_char \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param s: a string expression /// \param start: index of the first character to constrain /// \param end: index at which we stop adding constraints /// \param char_set: a string of the form "-" where /// `` and `` are two characters, which represents the /// set of characters that are between `low_char` and `high_char`. -/// \param array_pool: pool of arrays representing strings /// \return a string expression that is linked to the argument through axioms /// that are added to the list -string_constraintst add_constraint_on_characters( - symbol_generatort &fresh_symbol, +string_constraintst string_constraint_generatort::add_constraint_on_characters( const array_string_exprt &s, const exprt &start, const exprt &end, - const std::string &char_set, - array_poolt &array_pool) + const std::string &char_set) { // Parse char_set PRECONDITION(char_set.length() == 3); @@ -157,16 +153,13 @@ string_constraintst add_constraint_on_characters( /// `char_set` is given by the string `char_set_string` composed of three /// characters `low_char`, `-` and `high_char`. Character `c` belongs to /// `char_set` if \f$low_char \le c \le high_char\f$. -/// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments: integer `|s|`, character /// pointer `&s[0]`, string `char_set_string`, optional integers `start` and /// `end` -/// \param array_pool: pool of arrays representing strings /// \return integer expression whose value is zero -std::pair add_axioms_for_constrain_characters( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_constrain_characters( + const function_application_exprt &f) { const auto &args = f.arguments(); PRECONDITION(3 <= args.size() && args.size() <= 5); @@ -179,8 +172,8 @@ std::pair add_axioms_for_constrain_characters( args.size() >= 4 ? args[3] : from_integer(0, s.length_type()); const exprt &end = args.size() >= 5 ? args[4] : array_pool.get_or_create_length(s); - auto constraints = add_constraint_on_characters( - fresh_symbol, s, start, end, char_set_string.c_str(), array_pool); + auto constraints = + add_constraint_on_characters(s, start, end, char_set_string.c_str()); return {from_integer(0, get_return_code_type()), std::move(constraints)}; } @@ -223,78 +216,77 @@ string_constraint_generatort::add_axioms_for_function_application( if(id == ID_cprover_char_literal_func) return add_axioms_for_char_literal(expr); else if(id == ID_cprover_string_length_func) - return add_axioms_for_length(expr, array_pool); + return add_axioms_for_length(expr); else if(id == ID_cprover_string_equal_func) - return add_axioms_for_equals(fresh_symbol, expr, array_pool); + return add_axioms_for_equals(expr); else if(id == ID_cprover_string_equals_ignore_case_func) - return add_axioms_for_equals_ignore_case(fresh_symbol, expr, array_pool); + return add_axioms_for_equals_ignore_case(expr); else if(id == ID_cprover_string_is_empty_func) - return add_axioms_for_is_empty(fresh_symbol, expr, array_pool); + return add_axioms_for_is_empty(expr); else if(id == ID_cprover_string_char_at_func) - return add_axioms_for_char_at(fresh_symbol, expr, array_pool); + return add_axioms_for_char_at(expr); else if(id == ID_cprover_string_is_prefix_func) - return add_axioms_for_is_prefix(fresh_symbol, expr, false, array_pool); + return add_axioms_for_is_prefix(expr, false); else if(id == ID_cprover_string_is_suffix_func) - return add_axioms_for_is_suffix(fresh_symbol, expr, false, array_pool); + return add_axioms_for_is_suffix(expr, false); else if(id == ID_cprover_string_startswith_func) - return add_axioms_for_is_prefix(fresh_symbol, expr, true, array_pool); + return add_axioms_for_is_prefix(expr, true); else if(id == ID_cprover_string_endswith_func) - return add_axioms_for_is_suffix(fresh_symbol, expr, true, array_pool); + return add_axioms_for_is_suffix(expr, true); else if(id == ID_cprover_string_contains_func) - return add_axioms_for_contains(fresh_symbol, expr, array_pool); + return add_axioms_for_contains(expr); else if(id == ID_cprover_string_index_of_func) - return add_axioms_for_index_of(fresh_symbol, expr, array_pool); + return add_axioms_for_index_of(expr); else if(id == ID_cprover_string_last_index_of_func) - return add_axioms_for_last_index_of(fresh_symbol, expr, array_pool); + return add_axioms_for_last_index_of(expr); else if(id == ID_cprover_string_parse_int_func) - return add_axioms_for_parse_int(fresh_symbol, expr, array_pool, ns); + return add_axioms_for_parse_int(expr); else if(id == ID_cprover_string_code_point_at_func) - return add_axioms_for_code_point_at(fresh_symbol, expr, array_pool); + return add_axioms_for_code_point_at(expr); else if(id == ID_cprover_string_code_point_before_func) - return add_axioms_for_code_point_before(fresh_symbol, expr, array_pool); + return add_axioms_for_code_point_before(expr); else if(id == ID_cprover_string_code_point_count_func) - return add_axioms_for_code_point_count(fresh_symbol, expr, array_pool); + return add_axioms_for_code_point_count(expr); else if(id == ID_cprover_string_offset_by_code_point_func) - return add_axioms_for_offset_by_code_point(fresh_symbol, expr); + return add_axioms_for_offset_by_code_point(expr); else if(id == ID_cprover_string_compare_to_func) - return add_axioms_for_compare_to(fresh_symbol, expr, array_pool); + return add_axioms_for_compare_to(expr); else if(id == ID_cprover_string_literal_func) - return add_axioms_from_literal(fresh_symbol, expr, array_pool); + return add_axioms_from_literal(expr); else if(id == ID_cprover_string_concat_code_point_func) - return add_axioms_for_concat_code_point(fresh_symbol, expr, array_pool); + return add_axioms_for_concat_code_point(expr); else if(id == ID_cprover_string_substring_func) - return add_axioms_for_substring(fresh_symbol, expr, array_pool); + return add_axioms_for_substring(expr); else if(id == ID_cprover_string_trim_func) - return add_axioms_for_trim(fresh_symbol, expr, array_pool); + return add_axioms_for_trim(expr); else if(id == ID_cprover_string_empty_string_func) return add_axioms_for_empty_string(expr); else if(id == ID_cprover_string_copy_func) - return add_axioms_for_copy(fresh_symbol, expr, array_pool); + return add_axioms_for_copy(expr); else if(id == ID_cprover_string_of_int_hex_func) - return add_axioms_from_int_hex(expr, array_pool); + return add_axioms_from_int_hex(expr); else if(id == ID_cprover_string_of_float_func) - return add_axioms_for_string_of_float(fresh_symbol, expr, array_pool, ns); + return add_axioms_for_string_of_float(expr); else if(id == ID_cprover_string_of_float_scientific_notation_func) - return add_axioms_from_float_scientific_notation( - fresh_symbol, expr, array_pool, ns); + return add_axioms_from_float_scientific_notation(expr); else if(id == ID_cprover_string_of_double_func) - return add_axioms_from_double(fresh_symbol, expr, array_pool, ns); + return add_axioms_from_double(expr); else if(id == ID_cprover_string_of_long_func) - return add_axioms_from_long(expr, array_pool, ns); + return add_axioms_from_long(expr); else if(id == ID_cprover_string_of_bool_func) - return add_axioms_from_bool(expr, array_pool); + return add_axioms_from_bool(expr); else if(id == ID_cprover_string_of_char_func) - return add_axioms_from_char(expr, array_pool); + return add_axioms_from_char(expr); else if(id == ID_cprover_string_set_length_func) - return add_axioms_for_set_length(fresh_symbol, expr, array_pool); + return add_axioms_for_set_length(expr); else if(id == ID_cprover_string_delete_func) - return add_axioms_for_delete(fresh_symbol, expr, array_pool); + return add_axioms_for_delete(expr); else if(id == ID_cprover_string_delete_char_at_func) - return add_axioms_for_delete_char_at(fresh_symbol, expr, array_pool); + return add_axioms_for_delete_char_at(expr); else if(id == ID_cprover_string_replace_func) - return add_axioms_for_replace(fresh_symbol, expr, array_pool); + return add_axioms_for_replace(expr); else if(id == ID_cprover_string_constrain_characters_func) - return add_axioms_for_constrain_characters(fresh_symbol, expr, array_pool); + return add_axioms_for_constrain_characters(expr); else { std::string msg( @@ -308,16 +300,13 @@ string_constraint_generatort::add_axioms_for_function_application( /// add axioms to say that the returned string expression is equal to the /// argument of the function application /// \deprecated should use substring instead -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one argument, which is a string, /// or three arguments: string, integer offset and count -/// \param array_pool: pool of arrays representing strings /// \return a new string expression DEPRECATED(SINCE(2017, 10, 5, "should use substring instead")) -std::pair add_axioms_for_copy( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_copy( + const function_application_exprt &f) { const auto &args = f.arguments(); PRECONDITION(args.size() == 3 || args.size() == 5); @@ -327,19 +316,17 @@ std::pair add_axioms_for_copy( const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3]; const exprt count = args.size() == 3 ? array_pool.get_or_create_length(str) : args[4]; - return add_axioms_for_substring( - fresh_symbol, res, str, offset, plus_exprt(offset, count), array_pool); + return add_axioms_for_substring(res, str, offset, plus_exprt(offset, count)); } /// Length of a string /// /// Returns the length of the string argument of the given function application /// \param f: function application with argument string `str` -/// \param array_pool: pool of arrays representing strings /// \return expression `|str|` -std::pair add_axioms_for_length( - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_length( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 1); const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); @@ -357,7 +344,8 @@ exprt is_positive(const exprt &x) /// \param f: function application with one character argument /// \return a new character expression std::pair -add_axioms_for_char_literal(const function_application_exprt &f) +string_constraint_generatort::add_axioms_for_char_literal( + const function_application_exprt &f) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION( @@ -387,14 +375,11 @@ add_axioms_for_char_literal(const function_application_exprt &f) /// Add axioms stating that the character of the string at position given by /// second argument is equal to the returned value. /// This axiom is \f$ char = str[i] \f$. -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments string `str` and integer `i` -/// \param array_pool: pool of arrays representing strings /// \return character expression `char` -std::pair add_axioms_for_char_at( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_char_at( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); @@ -424,11 +409,12 @@ exprt zero_if_negative(const exprt &expr) /// Combine the results of two `add_axioms` function by taking the maximum of /// the return codes and merging the constraints. -std::pair combine_results( +std::pair +string_constraint_generatort::combine_results( std::pair result1, std::pair result2) { const exprt return_code = maximum(result1.first, result2.first); merge(result2.second, std::move(result1.second)); - return {return_code, std::move(result2.second)}; + return {simplify_expr(return_code, ns), std::move(result2.second)}; } diff --git a/src/solvers/strings/string_constraint_generator_testing.cpp b/src/solvers/strings/string_constraint_generator_testing.cpp index 1be420293ce..d01c106e522 100644 --- a/src/solvers/strings/string_constraint_generator_testing.cpp +++ b/src/solvers/strings/string_constraint_generator_testing.cpp @@ -30,18 +30,15 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// where offset_within_bounds is: /// offset >= 0 && offset <= |str| && |str| - offset >= |prefix| /// -/// \param fresh_symbol: generator of fresh symbols /// \param prefix: an array of characters /// \param str: an array of characters /// \param offset: an integer -/// \param array_pool: pool of arrays representing strings /// \return Boolean expression `isprefix` -std::pair add_axioms_for_is_prefix( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_is_prefix( const array_string_exprt &prefix, const array_string_exprt &str, - const exprt &offset, - array_poolt &array_pool) + const exprt &offset) { string_constraintst constraints; const symbol_exprt isprefix = fresh_symbol("isprefix"); @@ -98,19 +95,16 @@ std::pair add_axioms_for_is_prefix( /// string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset) /// \todo The primitive should be renamed to `starts_with`. /// \todo Get rid of the boolean flag. -/// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments refined_string `s0`, /// refined string `s1` and optional integer argument `offset`whose default /// value is 0 /// \param swap_arguments: a Boolean telling whether the prefix is the second /// argument or the first argument -/// \param array_pool: pool of arrays representing strings /// \return boolean expression `isprefix` -std::pair add_axioms_for_is_prefix( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_is_prefix( const function_application_exprt &f, - bool swap_arguments, - array_poolt &array_pool) + bool swap_arguments) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); @@ -121,23 +115,19 @@ std::pair add_axioms_for_is_prefix( get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]); const exprt offset = args.size() == 2 ? from_integer(0, s0.length_type()) : args[2]; - auto pair = - add_axioms_for_is_prefix(fresh_symbol, s0, s1, offset, array_pool); + auto pair = add_axioms_for_is_prefix(s0, s1, offset); return {typecast_exprt(pair.first, f.type()), std::move(pair.second)}; } /// Add axioms stating that the returned value is true exactly when the argument /// string is empty. /// \deprecated should use `string_length(s)==0` instead -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with a string argument -/// \param array_pool: pool of arrays representing strings /// \return a Boolean expression DEPRECATED(SINCE(2017, 10, 5, "should use `string_length s == 0` instead")) -std::pair add_axioms_for_is_empty( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_is_empty( + const function_application_exprt &f) { PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); PRECONDITION(f.arguments().size() == 1); @@ -169,20 +159,17 @@ std::pair add_axioms_for_is_empty( /// \land s_1[{witness}] \ne s_0[{witness} + |s_0| - |s_1|] \f$ /// /// \todo The primitive should be renamed `ends_with`. -/// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments refined_string `s0` /// and refined_string `s1` /// \param swap_arguments: boolean flag telling whether the suffix is the second /// argument or the first argument -/// \param array_pool: pool of arrays representing strings /// \return Boolean expression `issuffix` /// \deprecated Should use `strings_startwith(s0, s1, s1.length - s0.length)`. DEPRECATED(SINCE(2018, 6, 6, "should use strings_startwith")) -std::pair add_axioms_for_is_suffix( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_is_suffix( const function_application_exprt &f, - bool swap_arguments, - array_poolt &array_pool) + bool swap_arguments) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 2); // bad args to string issuffix? @@ -254,15 +241,12 @@ std::pair add_axioms_for_is_suffix( /// \Rightarrow \exists witness < |s_1|. /// \ s_1[witness] \ne s_0[startpos+witness] \f$ /// \warning slow for target longer than one character -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments refined_string `s0` /// refined_string `s1` -/// \param array_pool: pool of arrays representing strings /// \return Boolean expression `contains` -std::pair add_axioms_for_contains( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_contains( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 2); PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool); diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp index 92ee1e7e639..33a4cddb2a0 100644 --- a/src/solvers/strings/string_constraint_generator_transformation.cpp +++ b/src/solvers/strings/string_constraint_generator_transformation.cpp @@ -30,15 +30,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// 3. \f$ \forall i<|{\tt res}|.\ i \ge |s_1| /// \Rightarrow {\tt res}[i] = 0 \f$ /// \todo We can reduce the number of constraints by merging 2 and 3. -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `s1`, integer `k` -/// \param array_pool: pool of arrays representing strings /// \return integer expression equal to `0` -std::pair add_axioms_for_set_length( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_set_length( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 4); string_constraintst constraints; @@ -78,25 +75,22 @@ std::pair add_axioms_for_set_length( /// Substring of a string between two indices /// // NOLINTNEXTLINE -/// \copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &) +/// \copybrief add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) // NOLINTNEXTLINE -/// \link string_constraint_generatort::add_axioms_for_substring(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &) +/// \link string_constraint_generatort::add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) /// (More...) \endlink /// \warning The specification may not be correct for the case where the string /// is shorter than the end index /// \todo Should return a integer different from zero when the string is shorter /// tan the end index. -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `str`, integer `start`, optional integer /// `end` with default value `|str|`. -/// \param array_pool: pool of arrays representing strings /// \return integer expression which is different from 0 when there is an /// exception to signal -std::pair add_axioms_for_substring( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_substring( + const function_application_exprt &f) { const function_application_exprt::argumentst &args = f.arguments(); PRECONDITION(args.size() == 4 || args.size() == 5); @@ -105,7 +99,7 @@ std::pair add_axioms_for_substring( const exprt &i = args[3]; const exprt j = args.size() == 5 ? args[4] : array_pool.get_or_create_length(str); - return add_axioms_for_substring(fresh_symbol, res, str, i, j, array_pool); + return add_axioms_for_substring(res, str, i, j); } /// Add axioms ensuring that `res` corresponds to the substring of `str` @@ -117,20 +111,17 @@ std::pair add_axioms_for_substring( /// 2. \f$ \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \f$ /// \todo Should return code different from 0 if `start' != start` or /// `end' != end` -/// \param fresh_symbol: generator of fresh symbols /// \param res: array of characters expression /// \param str: array of characters expression /// \param start: integer expression /// \param end: integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression equal to zero -std::pair add_axioms_for_substring( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_substring( const array_string_exprt &res, const array_string_exprt &str, const exprt &start, - const exprt &end, - array_poolt &array_pool) + const exprt &end) { const typet &index_type = str.length_type(); PRECONDITION(start.type() == index_type); @@ -179,16 +170,13 @@ std::pair add_axioms_for_substring( /// 9. \f$ (s[m]>{\tt \lq~\rq} \land s[m+|{\tt res}|-1]>{\tt \lq~\rq}) /// \lor m=|{\tt res}| \f$ /// \note Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `str`. -/// \param array_pool: pool of arrays representing strings /// \return integer expression which is different from 0 when there is an /// exception to signal -std::pair add_axioms_for_trim( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_trim( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); string_constraintst constraints; @@ -308,16 +296,13 @@ static optionalt> to_char_pair( /// 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 fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `str`, character `old_char` and /// character `new_char` -/// \param array_pool: pool of arrays representing strings /// \return an integer expression equal to 0 -std::pair add_axioms_for_replace( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_replace( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 5); string_constraintst constraints; @@ -354,15 +339,12 @@ std::pair add_axioms_for_replace( } /// add axioms corresponding to the StringBuilder.deleteCharAt java function -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with two arguments, the first is a /// string and the second is an index -/// \param array_pool: pool of arrays representing strings /// \return an expression whose value is non null to signal an exception -std::pair add_axioms_for_delete_char_at( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_delete_char_at( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 4); const array_string_exprt res = @@ -370,12 +352,7 @@ std::pair add_axioms_for_delete_char_at( const array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]); exprt index_one = from_integer(1, str.length_type()); return add_axioms_for_delete( - fresh_symbol, - res, - str, - f.arguments()[3], - plus_exprt(f.arguments()[3], index_one), - array_pool); + res, str, f.arguments()[3], plus_exprt(f.arguments()[3], index_one)); } /// Add axioms stating that `res` corresponds to the input `str` @@ -387,20 +364,17 @@ std::pair add_axioms_for_delete_char_at( /// (see \ref add_axioms_for_substring and \ref add_axioms_for_concat_substr). /// \todo Should use add_axioms_for_concat_substr instead /// of add_axioms_for_concat -/// \param fresh_symbol: generator of fresh symbols /// \param res: array of characters expression /// \param str: array of characters expression /// \param start: integer expression /// \param end: integer expression -/// \param array_pool: pool of arrays representing strings /// \return integer expression different from zero to signal an exception -std::pair add_axioms_for_delete( - symbol_generatort &fresh_symbol, +std::pair +string_constraint_generatort::add_axioms_for_delete( const array_string_exprt &res, const array_string_exprt &str, const exprt &start, - const exprt &end, - array_poolt &array_pool) + const exprt &end) { PRECONDITION(start.type() == str.length_type()); PRECONDITION(end.type() == str.length_type()); @@ -412,45 +386,31 @@ std::pair add_axioms_for_delete( array_pool.fresh_string(index_type, char_type); return combine_results( add_axioms_for_substring( - fresh_symbol, - sub1, - str, - from_integer(0, str.length_type()), - start, - array_pool), + sub1, str, from_integer(0, str.length_type()), start), combine_results( add_axioms_for_substring( - fresh_symbol, - sub2, - str, - end, - array_pool.get_or_create_length(str), - array_pool), - add_axioms_for_concat(fresh_symbol, res, sub1, sub2, array_pool))); + sub2, str, end, array_pool.get_or_create_length(str)), + add_axioms_for_concat(res, sub1, sub2))); } /// Remove a portion of a string /// // NOLINTNEXTLINE -/// \copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool) +/// \copybrief add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) // NOLINTNEXTLINE -/// \link add_axioms_for_delete(symbol_generatort &fresh_symbol,const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool) +/// \link add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end) /// (More...) \endlink -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `str`, integer `start` and integer `end` -/// \param array_pool: pool of arrays representing strings /// \return an integer expression whose value is different from 0 to signal /// an exception -std::pair add_axioms_for_delete( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_for_delete( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 5); const array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); const array_string_exprt arg = get_string_expr(array_pool, f.arguments()[2]); - return add_axioms_for_delete( - fresh_symbol, res, arg, f.arguments()[3], f.arguments()[4], array_pool); + return add_axioms_for_delete(res, arg, f.arguments()[3], f.arguments()[4]); } diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp index ff55d56e57b..8badede72c9 100644 --- a/src/solvers/strings/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -39,40 +39,35 @@ static unsigned long to_integer_or_default( /// Add axioms corresponding to the String.valueOf(J) java function. /// \deprecated should use add_axioms_from_int instead /// \param f: function application with one long argument -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return a new string expression DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int instead")) -std::pair add_axioms_from_long( - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns) +std::pair +string_constraint_generatort::add_axioms_from_long( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4); const array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); if(f.arguments().size() == 4) return add_axioms_for_string_of_int_with_radix( - res, f.arguments()[2], f.arguments()[3], 0, ns, array_pool); + res, f.arguments()[2], f.arguments()[3], 0); else - return add_axioms_for_string_of_int( - res, f.arguments()[2], 0, ns, array_pool); + return add_axioms_for_string_of_int(res, f.arguments()[2], 0); } /// Add axioms corresponding to the String.valueOf(Z) java function. /// \deprecated This is Java specific and should be implemented in Java instead /// \param f: function application with a Boolean argument -/// \param array_pool: pool of arrays representing strings /// \return a new string expression DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) -std::pair add_axioms_from_bool( - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_from_bool( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); const array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); - return add_axioms_from_bool(res, f.arguments()[2], array_pool); + return add_axioms_from_bool(res, f.arguments()[2]); } /// Add axioms stating that the returned string equals "true" when the Boolean @@ -80,13 +75,12 @@ std::pair add_axioms_from_bool( /// \deprecated This is Java specific and should be implemented in Java instead /// \param res: string expression for the result /// \param b: Boolean expression -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java")) -std::pair add_axioms_from_bool( +std::pair +string_constraint_generatort::add_axioms_from_bool( const array_string_exprt &res, - const exprt &b, - array_poolt &array_pool) + const exprt &b) { const typet &char_type = res.content().type().subtype(); PRECONDITION(b.type() == bool_typet() || b.type().id() == ID_c_bool); @@ -134,19 +128,16 @@ std::pair add_axioms_from_bool( /// \param input_int: a signed integer expression /// \param max_size: a maximal size for the string representation (default 0, /// which is interpreted to mean "as large as is needed for this type") -/// \param ns: namespace -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success -std::pair add_axioms_for_string_of_int( +std::pair +string_constraint_generatort::add_axioms_for_string_of_int( const array_string_exprt &res, const exprt &input_int, - size_t max_size, - const namespacet &ns, - array_poolt &array_pool) + size_t max_size) { const constant_exprt radix = from_integer(10, input_int.type()); return add_axioms_for_string_of_int_with_radix( - res, input_int, radix, max_size, ns, array_pool); + res, input_int, radix, max_size); } /// Add axioms enforcing that the string corresponds to the result @@ -157,16 +148,13 @@ std::pair add_axioms_for_string_of_int( /// \param radix: the radix to use /// \param max_size: a maximal size for the string representation (default 0, /// which is interpreted to mean "as large as is needed for this type") -/// \param ns: namespace -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success -std::pair add_axioms_for_string_of_int_with_radix( +std::pair +string_constraint_generatort::add_axioms_for_string_of_int_with_radix( const array_string_exprt &res, const exprt &input_int, const exprt &radix, - size_t max_size, - const namespacet &ns, - array_poolt &array_pool) + size_t max_size) { PRECONDITION(max_size < std::numeric_limits::max()); const typet &type = input_int.type(); @@ -189,7 +177,7 @@ std::pair add_axioms_for_string_of_int_with_radix( const bool strict_formatting = true; auto result1 = add_axioms_for_correct_number_format( - res, radix_as_char, radix_ul, max_size, strict_formatting, array_pool); + res, radix_as_char, radix_ul, max_size, strict_formatting); auto result2 = add_axioms_for_characters_in_integer_string( input_int, type, @@ -197,8 +185,7 @@ std::pair add_axioms_for_string_of_int_with_radix( res, max_size, radix_input_type, - radix_ul, - array_pool); + radix_ul); merge(result2, std::move(result1)); return {from_integer(0, get_return_code_type()), std::move(result2)}; } @@ -223,13 +210,12 @@ static exprt int_of_hex_char(const exprt &chr) /// \deprecated use add_axioms_from_int_with_radix instead /// \param res: string expression for the result /// \param i: an integer argument -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int_with_radix")) -std::pair add_axioms_from_int_hex( +std::pair +string_constraint_generatort::add_axioms_from_int_hex( const array_string_exprt &res, - const exprt &i, - array_poolt &array_pool) + const exprt &i) { const typet &type = i.type(); PRECONDITION(type.id() == ID_signedbv); @@ -284,37 +270,35 @@ std::pair add_axioms_from_int_hex( /// Add axioms corresponding to the Integer.toHexString(I) java function /// \param f: function application with an integer argument -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success -std::pair add_axioms_from_int_hex( - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_from_int_hex( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); const array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); - return add_axioms_from_int_hex(res, f.arguments()[2], array_pool); + return add_axioms_from_int_hex(res, f.arguments()[2]); } /// Conversion from char to string /// // NOLINTNEXTLINE -/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c, array_poolt &) +/// \copybrief add_axioms_from_char(const array_string_exprt &res, const exprt &c) // NOLINTNEXTLINE -/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c, array_poolt &) +/// \link add_axioms_from_char(const array_string_exprt &res, const exprt &c) /// (More...) \endlink /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]` and character `c` -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success -std::pair add_axioms_from_char( - const function_application_exprt &f, - array_poolt &array_pool) +std::pair +string_constraint_generatort::add_axioms_from_char( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 3); const array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]); - return add_axioms_from_char(res, f.arguments()[2], array_pool); + return add_axioms_from_char(res, f.arguments()[2]); } /// Add axiom stating that string `res` has length 1 and the character @@ -323,12 +307,11 @@ std::pair add_axioms_from_char( /// This axiom is: \f$ |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \f$. /// \param res: array of characters expression /// \param c: character expression -/// \param array_pool: pool of arrays representing strings /// \return code 0 on success -std::pair add_axioms_from_char( +std::pair +string_constraint_generatort::add_axioms_from_char( const array_string_exprt &res, - const exprt &c, - array_poolt &array_pool) + const exprt &c) { string_constraintst constraints; constraints.existential = {and_exprt( @@ -346,14 +329,13 @@ std::pair add_axioms_from_char( /// \param max_size: maximum number of characters /// \param strict_formatting: if true, don't allow a leading plus, redundant /// zeros or upper case letters -/// \param array_pool: pool of arrays representing strings -string_constraintst add_axioms_for_correct_number_format( +string_constraintst +string_constraint_generatort::add_axioms_for_correct_number_format( const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, - const bool strict_formatting, - array_poolt &array_pool) + const bool strict_formatting) { string_constraintst constraints; const typet &char_type = str.content().type().subtype(); @@ -441,16 +423,15 @@ string_constraintst add_axioms_for_correct_number_format( /// \param radix: the radix, with the same type as input_int /// \param radix_ul: the radix as an unsigned long, or 0 if that can't be /// determined -/// \param array_pool: pool of arrays representing strings -string_constraintst add_axioms_for_characters_in_integer_string( +string_constraintst +string_constraint_generatort::add_axioms_for_characters_in_integer_string( const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, - const unsigned long radix_ul, - array_poolt &array_pool) + const unsigned long radix_ul) { string_constraintst constraints; const typet &char_type = str.content().type().subtype(); @@ -531,17 +512,12 @@ string_constraintst add_axioms_for_characters_in_integer_string( /// /// Add axioms ensuring the value of the returned integer corresponds /// to the value represented by `str` -/// \param fresh_symbol: generator of fresh symbols /// \param f: a function application with arguments refined_string `str` and /// an optional integer for the radix -/// \param array_pool: pool of arrays representing strings -/// \param ns: namespace /// \return integer expression equal to the value represented by `str` -std::pair add_axioms_for_parse_int( - symbol_generatort &fresh_symbol, - const function_application_exprt &f, - array_poolt &array_pool, - const namespacet &ns) +std::pair +string_constraint_generatort::add_axioms_for_parse_int( + const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 1 || f.arguments().size() == 2); const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); @@ -569,12 +545,7 @@ std::pair add_axioms_for_parse_int( /// \note the only thing stopping us from taking longer strings with many /// leading zeros is the axioms for correct number format auto constraints1 = add_axioms_for_correct_number_format( - str, - radix_as_char, - radix_ul, - max_string_length, - strict_formatting, - array_pool); + str, radix_as_char, radix_ul, max_string_length, strict_formatting); auto constraints2 = add_axioms_for_characters_in_integer_string( input_int, @@ -583,8 +554,7 @@ std::pair add_axioms_for_parse_int( str, max_string_length, radix, - radix_ul, - array_pool); + radix_ul); merge(constraints2, std::move(constraints1)); return {input_int, std::move(constraints2)}; diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp index 27b3b9e63bd..266ce461515 100644 --- a/src/solvers/strings/string_format_builtin_function.cpp +++ b/src/solvers/strings/string_format_builtin_function.cpp @@ -106,63 +106,46 @@ static exprt is_null(const array_string_exprt &string, array_poolt &array_pool) /// string expr, int, float, char, boolean, hashcode, date_time. /// The correct type will be retrieved by calling get_arg with an id depending /// on the format specifier. -/// \param fresh_symbol: generator of fresh symbols +/// \param generator: constraint generator /// \param fs: a format specifier /// \param string_arg: format string from argument /// \param index_type: type for indexes in strings /// \param char_type: type of characters -/// \param array_pool: pool of arrays representing strings /// \param message: message handler for warnings -/// \param ns: namespace /// \return String expression representing the output of String.format. static std::pair add_axioms_for_format_specifier( - symbol_generatort &fresh_symbol, + string_constraint_generatort &generator, const format_specifiert &fs, const array_string_exprt &string_arg, const typet &index_type, const typet &char_type, - array_poolt &array_pool, - const messaget &message, - const namespacet &ns) + const messaget &message) { string_constraintst constraints; + array_poolt &array_pool = generator.array_pool; const array_string_exprt res = array_pool.fresh_string(index_type, char_type); std::pair return_code; switch(fs.conversion) { case format_specifiert::DECIMAL_INTEGER: - return_code = add_axioms_for_string_of_int( - res, - format_arg_from_string(string_arg, ID_int, array_pool), - 0, - ns, - array_pool); + return_code = generator.add_axioms_for_string_of_int( + res, format_arg_from_string(string_arg, ID_int, array_pool), 0); return {res, std::move(return_code.second)}; case format_specifiert::HEXADECIMAL_INTEGER: - return_code = add_axioms_for_string_of_int_with_radix( + return_code = generator.add_axioms_for_string_of_int_with_radix( res, format_arg_from_string(string_arg, ID_int, array_pool), from_integer(16, index_type), - 16, - ns, - array_pool); + 16); return {res, std::move(return_code.second)}; case format_specifiert::SCIENTIFIC: - return_code = add_axioms_from_float_scientific_notation( - fresh_symbol, - res, - format_arg_from_string(string_arg, ID_float, array_pool), - array_pool, - ns); + return_code = generator.add_axioms_from_float_scientific_notation( + res, format_arg_from_string(string_arg, ID_float, array_pool)); return {res, std::move(return_code.second)}; case format_specifiert::DECIMAL_FLOAT: - return_code = add_axioms_for_string_of_float( - fresh_symbol, - res, - format_arg_from_string(string_arg, ID_float, array_pool), - array_pool, - ns); + return_code = generator.add_axioms_for_string_of_float( + res, format_arg_from_string(string_arg, ID_float, array_pool)); return {res, std::move(return_code.second)}; case format_specifiert::CHARACTER: { @@ -188,10 +171,8 @@ add_axioms_for_format_specifier( return {res, constraints}; } case format_specifiert::BOOLEAN: - return_code = add_axioms_from_bool( - res, - format_arg_from_string(string_arg, ID_boolean, array_pool), - array_pool); + return_code = generator.add_axioms_from_bool( + res, format_arg_from_string(string_arg, ID_boolean, array_pool)); return {res, std::move(return_code.second)}; case format_specifiert::STRING: { @@ -200,19 +181,15 @@ add_axioms_for_format_specifier( return {std::move(string_expr), {}}; } case format_specifiert::HASHCODE: - return_code = add_axioms_for_string_of_int( - res, - format_arg_from_string(string_arg, "hashcode", array_pool), - 0, - ns, - array_pool); + return_code = generator.add_axioms_for_string_of_int( + res, format_arg_from_string(string_arg, "hashcode", array_pool), 0); return {res, std::move(return_code.second)}; case format_specifiert::LINE_SEPARATOR: // TODO: the constant should depend on the system: System.lineSeparator() - return_code = add_axioms_for_constant(res, "\n", array_pool); + return_code = generator.add_axioms_for_constant(res, "\n"); return {res, std::move(return_code.second)}; case format_specifiert::PERCENT_SIGN: - return_code = add_axioms_for_constant(res, "%", array_pool); + return_code = generator.add_axioms_for_constant(res, "%"); return {res, std::move(return_code.second)}; case format_specifiert::SCIENTIFIC_UPPER: case format_specifiert::GENERAL_UPPER: @@ -226,20 +203,14 @@ add_axioms_for_format_specifier( format_specifiert fs_lower = fs; fs_lower.conversion = tolower(fs.conversion); auto format_specifier_result = add_axioms_for_format_specifier( - fresh_symbol, - fs_lower, - string_arg, - index_type, - char_type, - array_pool, - message, - ns); + generator, fs_lower, string_arg, index_type, char_type, message); const exprt return_code_upper_case = - fresh_symbol("return_code_upper_case", get_return_code_type()); + generator.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, array_pool); - auto upper_case_constraints = upper_case_function.constraints(fresh_symbol); + auto upper_case_constraints = + upper_case_function.constraints(generator.fresh_symbol); merge(upper_case_constraints, std::move(format_specifier_result.second)); return {res, std::move(upper_case_constraints)}; } @@ -311,24 +282,21 @@ static exprt format_arg_from_string( /// Parse `s` and add axioms ensuring the output corresponds to the output of /// String.format. -/// \param fresh_symbol: generator of fresh symbols +/// \param generator: constraint generator /// \param res: string expression for the result of the format function /// \param s: a format string /// \param args: a vector of arguments -/// \param array_pool: pool of arrays representing strings /// \param message: message handler for warnings -/// \param ns: namespace /// \return code, 0 on success static std::pair add_axioms_for_format( - symbol_generatort &fresh_symbol, + string_constraint_generatort &generator, const array_string_exprt &res, const std::string &s, const std::vector &args, - array_poolt &array_pool, - const messaget &message, - const namespacet &ns) + const messaget &message) { string_constraintst constraints; + array_poolt &array_pool = generator.array_pool; const std::vector format_strings = parse_format_string(s); std::vector intermediary_strings; std::size_t arg_count = 0; @@ -366,14 +334,7 @@ static std::pair add_axioms_for_format( } auto result = add_axioms_for_format_specifier( - fresh_symbol, - fs, - string_arg, - index_type, - char_type, - array_pool, - message, - ns); + generator, fs, string_arg, index_type, char_type, message); merge(constraints, std::move(result.second)); intermediary_strings.push_back(result.first); } @@ -381,8 +342,8 @@ static std::pair add_axioms_for_format( { const array_string_exprt str = array_pool.fresh_string(index_type, char_type); - auto result = add_axioms_for_constant( - str, fe.get_format_text().get_content(), array_pool); + auto result = generator.add_axioms_for_constant( + str, fe.get_format_text().get_content()); merge(constraints, result.second); intermediary_strings.push_back(str); } @@ -402,13 +363,11 @@ static std::pair add_axioms_for_format( if(intermediary_strings.size() == 1) { // Copy the first string - auto result = add_axioms_for_substring( - fresh_symbol, + auto result = generator.add_axioms_for_substring( res, str, from_integer(0, index_type), - array_pool.get_or_create_length(str), - array_pool); + generator.array_pool.get_or_create_length(str)); merge(constraints, std::move(result.second)); return {result.first, std::move(constraints)}; } @@ -419,15 +378,14 @@ static std::pair add_axioms_for_format( const array_string_exprt &intermediary = intermediary_strings[i]; const array_string_exprt fresh = array_pool.fresh_string(index_type, char_type); - auto result = - add_axioms_for_concat(fresh_symbol, fresh, str, intermediary, array_pool); + auto result = generator.add_axioms_for_concat(fresh, str, intermediary); return_code = maximum(return_code, result.first); merge(constraints, std::move(result.second)); str = fresh; } - auto result = add_axioms_for_concat( - fresh_symbol, res, str, intermediary_strings.back(), array_pool); + auto result = + generator.add_axioms_for_concat(res, str, intermediary_strings.back()); merge(constraints, std::move(result.second)); return {maximum(result.first, return_code), std::move(constraints)}; } @@ -631,14 +589,12 @@ string_constraintst string_format_builtin_functiont::constraints( null_message_handlert message_handler; auto result_constraint_pair = add_axioms_for_format( - generator.fresh_symbol, + generator, result, format_string.value(), inputs, - generator.array_pool, // TODO: get rid of this argument - messaget{message_handler}, - generator.ns); + messaget{message_handler}); INVARIANT( simplify_expr(result_constraint_pair.first, generator.ns).is_zero(), "add_axioms_for_format should return 0, meaning that formatting was"