From 4c482183e742744c8488795adc3cd18a52a2f4f2 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Tue, 13 Aug 2019 11:32:31 +0100 Subject: [PATCH 1/2] Move add_axiom methods to string_constraint_generator Also removed all arguments that can now be accessed directly via their fields. --- src/solvers/README.md | 84 +-- .../strings/string_builtin_function.cpp | 4 +- .../string_concatenation_builtin_function.cpp | 52 +- .../strings/string_constraint_generator.h | 583 +++++++----------- ...tring_constraint_generator_code_points.cpp | 37 +- ...string_constraint_generator_comparison.cpp | 27 +- .../string_constraint_generator_constants.cpp | 38 +- .../string_constraint_generator_float.cpp | 106 ++-- .../string_constraint_generator_indexof.cpp | 72 +-- .../string_constraint_generator_main.cpp | 128 ++-- .../string_constraint_generator_testing.cpp | 48 +- ...ng_constraint_generator_transformation.cpp | 108 +--- .../string_constraint_generator_valueof.cpp | 126 ++-- .../string_format_builtin_function.cpp | 116 ++-- 14 files changed, 589 insertions(+), 940 deletions(-) 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..013b7cb9065 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,7 +409,8 @@ 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) { 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" From 303ec4d038700fca1f14adf03d9e95eab095d353 Mon Sep 17 00:00:00 2001 From: johndumbell Date: Thu, 25 Jul 2019 12:34:17 +0100 Subject: [PATCH 2/2] Simplify when combining string-refinement result constraints Due to the improvements in constant prop we increasingly have constraints that are trivially simplified, like: if 5 >= 2 do x else y Also because of the way these conditions are combined - the resulting merged if gets added to all subsequent conditions and values - we end up with expressions like this: if 5 >= 2 then (if 5 >= 2 do x ... else y ...) else (if 5 >= 2 do x ... else y ...) Where the size of the expression increases exponentially to the complexity of the original if statement even if the entire conditional is trivial to prove right/wrong. This could likely be worked out by the SAT solver happily enough but due to the size of the resulting expressions (I've seen ones 1.34 billion nodes deep) it never gets there within a reasonable time-frame. --- src/solvers/strings/string_constraint_generator_main.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index 013b7cb9065..4b9babd63aa 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -416,5 +416,5 @@ string_constraint_generatort::combine_results( { 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)}; }