diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class new file mode 100644 index 00000000000..4ecf201f185 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java new file mode 100644 index 00000000000..1af7317bca5 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/Test.java @@ -0,0 +1,68 @@ +public class Test +{ + public static String checkDet() + { + String tmp = String.valueOf(1000000); + tmp = String.valueOf(1000001); + tmp = String.valueOf(1000002); + tmp = String.valueOf(1000003); + tmp = String.valueOf(1000004); + tmp = String.valueOf(1000005); + tmp = String.valueOf(-1000001); + tmp = String.valueOf(-1000002); + tmp = String.valueOf(-1000003); + tmp = String.valueOf(1000004); + tmp = String.valueOf(1000005); + tmp = String.valueOf(-1000001); + tmp = String.valueOf(-1000002); + tmp = String.valueOf(1000003); + tmp = String.valueOf(1000004); + tmp = String.valueOf(1000005); + tmp = String.valueOf(1000001); + tmp = String.valueOf(-1000002); + tmp = String.valueOf(-1000003); + tmp = String.valueOf(1000004); + tmp = String.valueOf(1000005); + return tmp; + } + + public static String checkNonDet(int i) + { + String tmp = String.valueOf(1000000); + tmp = String.valueOf(i + 1); + tmp = String.valueOf(i + 2); + tmp = String.valueOf(i + 3); + tmp = String.valueOf(i + 4); + tmp = String.valueOf(i + 5); + tmp = String.valueOf(i - 1); + tmp = String.valueOf(i - 2); + tmp = String.valueOf(i - 3); + tmp = String.valueOf(i - 4); + tmp = String.valueOf(i - 5); + tmp += " "; + tmp += String.valueOf(i); + tmp += " "; + tmp += String.valueOf(i + 2); + tmp += " "; + tmp += String.valueOf(i + 3); + tmp += " "; + tmp += String.valueOf(-i); + tmp += " "; + tmp += String.valueOf(-i + 1); + tmp += " "; + tmp += String.valueOf(-i - 2); + return tmp; + } + + public static void checkWithDependency(boolean b) + { + String s = String.valueOf(12); + if (b) { + assert(s.startsWith("12")); + } + else { + assert(!s.startsWith("12")); + } + } + +} diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc new file mode 100644 index 00000000000..18c4b3b0f9a --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.checkWithDependency --depth 10000 +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 61 .*: SUCCESS +assertion at file Test.java line 64 .*: FAILURE +-- +-- +Check that when a dependency is present, the correct constraints are added diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc new file mode 100644 index 00000000000..8fc14e7e524 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.checkDet --verbosity 10 --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 25 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc new file mode 100644 index 00000000000..7342d08a711 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.checkNonDet --verbosity 10 --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 53 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/src/solvers/README.md b/src/solvers/README.md index e2f06856aff..4fb75cebaad 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -281,7 +281,7 @@ allocates a new string before calling a primitive. \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink * `cprover_string_of_int` : \copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) - \link string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) More... \endlink + \link string_constraint_generatort::add_axioms_for_string_of_int(const function_application_exprt &f) More... \endlink * `cprover_string_of_float` : \copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) \link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 39bb9d4c782..234f5d4749c 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -122,19 +122,25 @@ optionalt> eval_string( return result; } -array_string_exprt -make_string(const std::vector &array, const array_typet &array_type) +template +static array_string_exprt +make_string(Iter begin, Iter end, const array_typet &array_type) { const typet &char_type = array_type.subtype(); array_exprt array_expr(array_type); const auto &insert = std::back_inserter(array_expr.operands()); - std::transform( - array.begin(), array.end(), insert, [&](const mp_integer &i) { // NOLINT - return from_integer(i, char_type); - }); + std::transform(begin, end, insert, [&](const mp_integer &i) { + return from_integer(i, char_type); + }); return to_array_string_expr(array_expr); } +static array_string_exprt +make_string(const std::vector &array, const array_typet &array_type) +{ + return make_string(array.begin(), array.end(), array_type); +} + std::vector string_concatenation_builtin_functiont::eval( const std::vector &input1_value, const std::vector &input2_value, @@ -216,6 +222,84 @@ optionalt string_insertion_builtin_functiont::eval( return make_string(result_value, type); } +/// Constructor from arguments of a function application. +/// The arguments in `fun_args` should be in order: +/// an integer `result.length`, a character pointer `&result[0]`, +/// an expression `arg` which is to be converted to a string. +/// Other arguments are ignored by this constructor. +string_creation_builtin_functiont::string_creation_builtin_functiont( + const exprt &return_code, + const std::vector &fun_args, + array_poolt &array_pool) + : string_builtin_functiont(return_code) +{ + PRECONDITION(fun_args.size() >= 3); + result = array_pool.find(fun_args[1], fun_args[0]); + arg = fun_args[2]; +} + +optionalt string_of_int_builtin_functiont::eval( + const std::function &get_value) const +{ + const auto arg_value = numeric_cast(get_value(arg)); + if(!arg_value) + return {}; + static std::string digits = "0123456789abcdefghijklmnopqrstuvwxyz"; + const auto radix_value = numeric_cast(get_value(radix)); + if(!radix_value || *radix_value > digits.length()) + return {}; + + mp_integer current_value = *arg_value; + std::vector right_to_left_characters; + if(current_value < 0) + current_value = -current_value; + if(current_value == 0) + right_to_left_characters.emplace_back('0'); + while(current_value > 0) + { + const auto digit_value = (current_value % *radix_value).to_ulong(); + right_to_left_characters.emplace_back(digits.at(digit_value)); + current_value /= *radix_value; + } + if(*arg_value < 0) + right_to_left_characters.emplace_back('-'); + + const auto length = right_to_left_characters.size(); + const auto length_expr = from_integer(length, result.length().type()); + const array_typet type(result.type().subtype(), length_expr); + return make_string( + right_to_left_characters.rbegin(), right_to_left_characters.rend(), type); +} + +exprt string_of_int_builtin_functiont::length_constraint() const +{ + const typet &type = result.length().type(); + const auto radix_opt = numeric_cast(radix); + const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2; + const std::size_t upper_bound = + max_printed_string_length(arg.type(), radix_value); + const exprt negative_arg = + binary_relation_exprt(arg, ID_le, from_integer(0, type)); + const exprt absolute_arg = + if_exprt(negative_arg, unary_minus_exprt(arg), arg); + + exprt size_expr = from_integer(1, type); + exprt min_int_with_current_size = from_integer(1, radix.type()); + for(std::size_t current_size = 2; current_size <= upper_bound + 1; + ++current_size) + { + min_int_with_current_size = mult_exprt(radix, min_int_with_current_size); + const exprt at_least_current_size = + binary_relation_exprt(absolute_arg, ID_ge, min_int_with_current_size); + size_expr = if_exprt( + at_least_current_size, from_integer(current_size, type), size_expr); + } + + const exprt size_expr_with_sign = if_exprt( + negative_arg, plus_exprt(size_expr, from_integer(1, type)), size_expr); + return equal_exprt(result.length(), size_expr_with_sign); +} + string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt( const exprt &return_code, const function_application_exprt &f, diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h index e29bc075d6f..c2b00f0f4d3 100644 --- a/src/solvers/refinement/string_builtin_function.h +++ b/src/solvers/refinement/string_builtin_function.h @@ -264,8 +264,12 @@ class string_creation_builtin_functiont : public string_builtin_functiont { public: array_string_exprt result; - std::vector args; - exprt return_code; + exprt arg; + + string_creation_builtin_functiont( + const exprt &return_code, + const std::vector &fun_args, + array_poolt &array_pool); optionalt string_result() const override { @@ -278,6 +282,43 @@ class string_creation_builtin_functiont : public string_builtin_functiont } }; +/// String creation from integer types +class string_of_int_builtin_functiont : public string_creation_builtin_functiont +{ +public: + string_of_int_builtin_functiont( + const exprt &return_code, + const std::vector &fun_args, + array_poolt &array_pool) + : string_creation_builtin_functiont(return_code, fun_args, array_pool) + { + PRECONDITION(fun_args.size() <= 4); + if(fun_args.size() == 4) + radix = fun_args[3]; + else + radix = from_integer(10, arg.type()); + }; + + optionalt + eval(const std::function &get_value) const override; + + std::string name() const override + { + return "string_of_int"; + } + + exprt add_constraints(string_constraint_generatort &generator) const override + { + return generator.add_axioms_for_string_of_int_with_radix( + result, arg, radix); + } + + exprt length_constraint() const override; + +private: + exprt radix; +}; + /// String test class string_test_builtin_functiont : public string_builtin_functiont { diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index ac2b081cde7..8a7ac5ae20e 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -165,6 +165,11 @@ class string_constraint_generatort final const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset); + exprt add_axioms_for_string_of_int_with_radix( + const array_string_exprt &res, + const exprt &input_int, + const exprt &radix, + size_t max_size = 0); private: symbol_exprt fresh_boolean(const irep_idt &prefix); @@ -258,15 +263,10 @@ class string_constraint_generatort final const exprt &guard); exprt add_axioms_from_literal(const function_application_exprt &f); exprt add_axioms_from_int(const function_application_exprt &f); - exprt add_axioms_from_int( + exprt add_axioms_for_string_of_int( const array_string_exprt &res, const exprt &input_int, size_t max_size = 0); - exprt add_axioms_from_int_with_radix( - const array_string_exprt &res, - const exprt &input_int, - const exprt &radix, - size_t max_size = 0); exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i); exprt add_axioms_from_int_hex(const function_application_exprt &f); exprt add_axioms_from_long(const function_application_exprt &f); diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 54afb59ca0d..839aec70b77 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -214,7 +214,7 @@ exprt string_constraint_generatort::add_axioms_for_string_of_float( const array_string_exprt integer_part_str = fresh_string(index_type, char_type); const exprt return_code2 = - add_axioms_from_int(integer_part_str, integer_part, 8); + add_axioms_for_string_of_int(integer_part_str, integer_part, 8); return add_axioms_for_concat(res, integer_part_str, fractional_part_str); } @@ -423,8 +423,8 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation( array_string_exprt string_expr_integer_part = fresh_string(index_type, char_type); - exprt return_code1 = - add_axioms_from_int(string_expr_integer_part, dec_significand_int, 3); + exprt return_code1 = add_axioms_for_string_of_int( + string_expr_integer_part, dec_significand_int, 3); minus_exprt fractional_part( dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); @@ -467,7 +467,7 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation( const array_string_exprt exponent_string = fresh_string(index_type, char_type); const exprt return_code6 = - add_axioms_from_int(exponent_string, decimal_exponent, 3); + add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3); // string_expr = concat(string_expr_with_E, exponent_string) return add_axioms_for_concat(res, string_expr_with_E, exponent_string); diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index 20b9d332472..9b7664e4fd9 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/refinement/string_constraint_generator_format.cpp @@ -269,7 +269,7 @@ string_constraint_generatort::add_axioms_for_format_specifier( { case format_specifiert::DECIMAL_INTEGER: return_code = - add_axioms_from_int(res, get_component_in_struct(arg, ID_int)); + add_axioms_for_string_of_int(res, get_component_in_struct(arg, ID_int)); return res; case format_specifiert::HEXADECIMAL_INTEGER: return_code = @@ -293,8 +293,8 @@ string_constraint_generatort::add_axioms_for_format_specifier( case format_specifiert::STRING: return get_string_expr(get_component_in_struct(arg, "string_expr")); case format_specifiert::HASHCODE: - return_code = - add_axioms_from_int(res, get_component_in_struct(arg, "hashcode")); + return_code = add_axioms_for_string_of_int( + res, get_component_in_struct(arg, "hashcode")); return res; case format_specifiert::LINE_SEPARATOR: // TODO: the constant should depend on the system: System.lineSeparator() diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index 64e380db7f7..ba9f79d8cce 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -144,7 +144,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_int( const typet &index_type = s1.length().type(); const typet &char_type = s1.content().type().subtype(); array_string_exprt s2 = fresh_string(index_type, char_type); - exprt return_code = add_axioms_from_int(s2, f.arguments()[4]); + exprt return_code = add_axioms_for_string_of_int(s2, f.arguments()[4]); return add_axioms_for_insert(res, s1, s2, offset); } diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 6ba8f324554..c0e795d0dc8 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -31,17 +31,17 @@ exprt string_constraint_generatort::add_axioms_from_int( const array_string_exprt res = char_array_of_pointer(f.arguments()[1], f.arguments()[0]); if(f.arguments().size() == 4) - return add_axioms_from_int_with_radix( + return add_axioms_for_string_of_int_with_radix( res, f.arguments()[2], f.arguments()[3]); else // f.arguments.size()==3 - return add_axioms_from_int(res, f.arguments()[2]); + return add_axioms_for_string_of_int(res, f.arguments()[2]); } /// 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 /// \return a new string expression -DEPRECATED("should use add_axioms_from_int instead") +DEPRECATED("should use add_axioms_for_string_of_int instead") exprt string_constraint_generatort::add_axioms_from_long( const function_application_exprt &f) { @@ -49,10 +49,10 @@ exprt string_constraint_generatort::add_axioms_from_long( const array_string_exprt res = char_array_of_pointer(f.arguments()[1], f.arguments()[0]); if(f.arguments().size() == 4) - return add_axioms_from_int_with_radix( + return add_axioms_for_string_of_int_with_radix( res, f.arguments()[2], f.arguments()[3]); else - return add_axioms_from_int(res, f.arguments()[2]); + return add_axioms_for_string_of_int(res, f.arguments()[2]); } /// Add axioms corresponding to the String.valueOf(Z) java function. @@ -124,13 +124,14 @@ exprt string_constraint_generatort::add_axioms_from_bool( /// \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") /// \return code 0 on success -exprt string_constraint_generatort::add_axioms_from_int( +exprt string_constraint_generatort::add_axioms_for_string_of_int( const array_string_exprt &res, const exprt &input_int, size_t max_size) { const constant_exprt radix=from_integer(10, input_int.type()); - return add_axioms_from_int_with_radix(res, input_int, radix, max_size); + return add_axioms_for_string_of_int_with_radix( + res, input_int, radix, max_size); } /// Add axioms enforcing that the string corresponds to the result @@ -142,7 +143,7 @@ exprt string_constraint_generatort::add_axioms_from_int( /// \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") /// \return code 0 on success -exprt string_constraint_generatort::add_axioms_from_int_with_radix( +exprt string_constraint_generatort::add_axioms_for_string_of_int_with_radix( const array_string_exprt &res, const exprt &input_int, const exprt &radix, @@ -204,7 +205,8 @@ exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) /// \param res: string expression for the result /// \param i: an integer argument /// \return code 0 on success -DEPRECATED("use add_axioms_from_int which takes a radix argument instead") +DEPRECATED( + "use add_axioms_for_string_of_int which takes a radix argument instead") exprt string_constraint_generatort::add_axioms_from_int_hex( const array_string_exprt &res, const exprt &i) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 20292000a7c..e9227ebf865 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -224,6 +224,10 @@ static std::unique_ptr to_string_builtin_function( return util_make_unique( return_code, fun_app.arguments(), array_pool); + if(id == ID_cprover_string_of_int_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + return util_make_unique( return_code, fun_app, array_pool); }