diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class new file mode 100644 index 00000000000..08c0c549955 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java new file mode 100644 index 00000000000..552cfeb835e --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java @@ -0,0 +1,62 @@ +public class Test { + public String det() + { + StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz"); + builder.setCharAt(3, '!'); + builder.setCharAt(5, '!'); + builder.setCharAt(7, '!'); + builder.setCharAt(9, '!'); + builder.setCharAt(13, '!'); + builder.setCharAt(15, '!'); + builder.setCharAt(17, '!'); + builder.setCharAt(19, '!'); + builder.setCharAt(4, ':'); + builder.setCharAt(5, ':'); + builder.setCharAt(6, ':'); + builder.setCharAt(9, ':'); + builder.setCharAt(10, ':'); + builder.setCharAt(11, ':'); + builder.setCharAt(16, ':'); + builder.setCharAt(18, ':'); + return builder.toString(); + } + + public String nonDet(String s, char c, int i) + { + StringBuilder builder = new StringBuilder(s); + if(i + 5 >= s.length() || 19 >= s.length() || i < 0) + return "Out of bounds"; + builder.setCharAt(i, c); + builder.setCharAt(i+5, 'x'); + builder.setCharAt(7, '!'); + builder.setCharAt(9, '!'); + builder.setCharAt(13, '!'); + builder.setCharAt(15, '!'); + builder.setCharAt(17, '!'); + builder.setCharAt(19, '!'); + builder.setCharAt(4, ':'); + builder.setCharAt(5, ':'); + builder.setCharAt(6, c); + builder.setCharAt(9, ':'); + builder.setCharAt(10, ':'); + builder.setCharAt(11, ':'); + builder.setCharAt(16, ':'); + builder.setCharAt(18, ':'); + return builder.toString(); + } + + public String withDependency(boolean b) + { + StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz"); + builder.setCharAt(3, '!'); + builder.setCharAt(5, '!'); + + if(b) { + assert builder.toString().startsWith("abc!"); + } else { + assert !builder.toString().startsWith("abc!"); + } + return builder.toString(); + } + +} diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc new file mode 100644 index 00000000000..668e84a1adc --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_dependency.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--function Test.withDependency --max-nondet-string-length 1000 +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 55 .*: SUCCESS +assertion at file Test.java line 57 .*: FAILURE +-- +-- +Check that when a dependency is present, the correct constraints are added + + diff --git a/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc new file mode 100644 index 00000000000..270ef7d2867 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_det.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.det --verbosity 10 --cover location +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 21 .*: 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/StringBuilderSetCharAt/test_nondet.desc b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc new file mode 100644 index 00000000000..a76880a6c16 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringBuilderSetCharAt/test_nondet.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.nonDet --verbosity 10 --cover location --max-nondet-string-length 1000 +^EXIT=0$ +^SIGNAL=0$ +coverage.* file Test.java line 45 .*: SATISFIED +-- +adding lemma .*nondet_infinite_array +-- +Check that using the string dependence informations, no lemma involving arrays is added diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 234f5d4749c..3739d6e85c2 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -29,33 +29,6 @@ string_transformation_builtin_functiont:: const auto arg1 = expr_checked_cast(fun_args[2]); input = array_pool.find(arg1.op1(), arg1.op0()); result = array_pool.find(fun_args[1], fun_args[0]); - args.insert(args.end(), fun_args.begin() + 3, fun_args.end()); -} - -optionalt string_transformation_builtin_functiont::eval( - const std::function &get_value) const -{ - const auto &input_value = eval_string(input, get_value); - if(!input_value.has_value()) - return {}; - - std::vector arg_values; - const auto &insert = std::back_inserter(arg_values); - const mp_integer unknown('?'); - std::transform( - args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT - if(const auto val = numeric_cast(get_value(e))) - return *val; - INVARIANT( - get_value(e).id() == ID_unknown, - "array valuation should only contain constants and unknown"); - return unknown; - }); - - const auto result_value = eval(*input_value, arg_values); - const auto length = from_integer(result_value.size(), result.length().type()); - const array_typet type(result.type().subtype(), length); - return make_string(result_value, type); } string_insertion_builtin_functiont::string_insertion_builtin_functiont( @@ -162,14 +135,56 @@ std::vector string_concatenation_builtin_functiont::eval( return result; } -std::vector string_concat_char_builtin_functiont::eval( - const std::vector &input_value, - const std::vector &args_value) const +optionalt string_concat_char_builtin_functiont::eval( + const std::function &get_value) const { - PRECONDITION(args_value.size() == 1); - std::vector result(input_value); - result.push_back(args_value[0]); - return result; + auto input_opt = eval_string(input, get_value); + if(!input_opt.has_value()) + return {}; + const mp_integer char_val = [&] { + if(const auto val = numeric_cast(get_value(character))) + return *val; + INVARIANT( + get_value(character).id() == ID_unknown, + "character valuation should only contain constants and unknown"); + return mp_integer(CHARACTER_FOR_UNKNOWN); + }(); + input_opt.value().push_back(char_val); + const auto length = + from_integer(input_opt.value().size(), result.length().type()); + const array_typet type(result.type().subtype(), length); + return make_string(input_opt.value(), type); +} + +optionalt string_set_char_builtin_functiont::eval( + const std::function &get_value) const +{ + auto input_opt = eval_string(input, get_value); + const auto char_opt = numeric_cast(get_value(character)); + const auto position_opt = numeric_cast(get_value(position)); + if(!input_opt || !char_opt || !position_opt) + return {}; + if(0 <= *position_opt && *position_opt < input_opt.value().size()) + input_opt.value()[numeric_cast_v(*position_opt)] = *char_opt; + const auto length = + from_integer(input_opt.value().size(), result.length().type()); + const array_typet type(result.type().subtype(), length); + return make_string(input_opt.value(), type); +} + +exprt string_set_char_builtin_functiont::length_constraint() const +{ + const exprt out_of_bounds = or_exprt( + binary_relation_exprt(position, ID_ge, input.length()), + binary_relation_exprt( + position, ID_le, from_integer(0, input.length().type()))); + const exprt return_value = if_exprt( + out_of_bounds, + from_integer(1, return_code.type()), + from_integer(0, return_code.type())); + return and_exprt( + equal_exprt(result.length(), input.length()), + equal_exprt(return_code, return_value)); } std::vector string_insertion_builtin_functiont::eval( diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h index c2b00f0f4d3..0480b5d3d65 100644 --- a/src/solvers/refinement/string_builtin_function.h +++ b/src/solvers/refinement/string_builtin_function.h @@ -11,6 +11,8 @@ class array_poolt; +#define CHARACTER_FOR_UNKNOWN '?' + /// Base class for string functions that are built in the solver class string_builtin_functiont { @@ -68,7 +70,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont public: array_string_exprt result; array_string_exprt input; - std::vector args; /// Constructor from arguments of a function application. /// The arguments in `fun_args` should be in order: @@ -88,15 +89,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont { return {input}; } - - /// Evaluate the result from a concrete valuation of the arguments - virtual std::vector eval( - const std::vector &input_value, - const std::vector &args_value) const = 0; - - optionalt - eval(const std::function &get_value) const override; - bool maybe_testing_function() const override { return false; @@ -108,6 +100,8 @@ class string_concat_char_builtin_functiont : public string_transformation_builtin_functiont { public: + exprt character; + /// 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]`, @@ -118,11 +112,12 @@ class string_concat_char_builtin_functiont array_poolt &array_pool) : string_transformation_builtin_functiont(return_code, fun_args, array_pool) { + PRECONDITION(fun_args.size() == 4); + character = fun_args[3]; } - std::vector eval( - const std::vector &input_value, - const std::vector &args_value) const override; + optionalt + eval(const std::function &get_value) const override; std::string name() const override { @@ -131,7 +126,7 @@ class string_concat_char_builtin_functiont exprt add_constraints(string_constraint_generatort &generator) const override { - return generator.add_axioms_for_concat_char(result, input, args[0]); + return generator.add_axioms_for_concat_char(result, input, character); } exprt length_constraint() const override @@ -140,6 +135,48 @@ class string_concat_char_builtin_functiont } }; +/// Setting a character at a particular position of a string +class string_set_char_builtin_functiont + : public string_transformation_builtin_functiont +{ +public: + exprt position; + exprt character; + + /// 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]`, + /// a string `arg1` of type refined_string_typet, a position and a character. + string_set_char_builtin_functiont( + const exprt &return_code, + const std::vector &fun_args, + array_poolt &array_pool) + : string_transformation_builtin_functiont(return_code, fun_args, array_pool) + { + PRECONDITION(fun_args.size() == 5); + position = fun_args[3]; + character = fun_args[4]; + } + + optionalt + eval(const std::function &get_value) const override; + + std::string name() const override + { + return "set_char"; + } + + exprt add_constraints(string_constraint_generatort &generator) const override + { + return generator.add_axioms_for_set_char( + result, input, position, character); + } + + // \todo: length_constraint is not the best possible name because we also + // \todo: add constraint about the return code + exprt length_constraint() const override; +}; + /// String inserting a string into another one class string_insertion_builtin_functiont : public string_builtin_functiont { diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 8a7ac5ae20e..342c563ac5a 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -170,6 +170,11 @@ class string_constraint_generatort final const exprt &input_int, const exprt &radix, size_t max_size = 0); + exprt add_axioms_for_set_char( + const array_string_exprt &res, + const array_string_exprt &str, + const exprt &position, + const exprt &character); private: symbol_exprt fresh_boolean(const irep_idt &prefix); diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 75f9c115477..a4bad2bdaf6 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -380,19 +380,10 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case( } /// Set a character to a specific value at an index of the string -/// -/// Add axioms ensuring that the result `res` is similar to input string `str` -/// where the character at index `pos` is set to `char`. -/// These axioms are: -/// 1. \f$ |{\tt res}| = |{\tt str}|\f$ -/// 2. \f$ {\tt res}[{\tt pos}]={\tt char}\f$ -/// 3. \f$ \forall i < min(|{\tt res}|, pos). {\tt res}[i] = {\tt str}[i]\f$ -/// 4. \f$ \forall pos+1 <= i < |{\tt res}|.\ {\tt res}[i] = {\tt str}[i]\f$ +/// \copydoc string_constraint_generatort::add_axioms_for_set_char /// \param f: function application with arguments integer `|res|`, character /// pointer `&res[0]`, refined_string `str`, integer `pos`, /// and character `char` -/// \return an integer expression which is `1` when `pos` is out of bounds and -/// `0` otherwise exprt string_constraint_generatort::add_axioms_for_char_set( const function_application_exprt &f) { @@ -402,28 +393,52 @@ exprt string_constraint_generatort::add_axioms_for_char_set( char_array_of_pointer(f.arguments()[1], f.arguments()[0]); const exprt &position = f.arguments()[3]; const exprt &character = f.arguments()[4]; + return add_axioms_for_set_char(res, str, position, character); +} +/// Add axioms ensuring that the result `res` is similar to input string `str` +/// where the character at index `pos` is set to `char`. +/// If `pos` is out of bounds the string returned unchanged. +/// +/// These axioms are: +/// 1. res.length = str.length +/// 2. 0 <= pos < res.length ==> res[pos]=char +/// 3. forall i < min(res.length, pos). res[i] = str[i] +/// 4. forall pos+1 <= i < res.length. res[i] = str[i] +/// \return an integer expression which is `1` when `pos` is out of bounds and +/// `0` otherwise +exprt string_constraint_generatort::add_axioms_for_set_char( + const array_string_exprt &res, + const array_string_exprt &str, + const exprt &position, + const exprt &character) +{ const binary_relation_exprt out_of_bounds(position, ID_ge, str.length()); - const equal_exprt a1(res.length(), str.length()); - lemmas.push_back(a1); - const equal_exprt a2(res[position], character); - lemmas.push_back(a2); - - const symbol_exprt q = fresh_univ_index("QA_char_set", position.type()); - const equal_exprt a3_body(res[q], str[q]); - const string_constraintt a3( - q, minimum(zero_if_negative(res.length()), position), a3_body); - constraints.push_back(a3); - - const symbol_exprt q2 = fresh_univ_index("QA_char_set2", position.type()); - const plus_exprt lower_bound(position, from_integer(1, position.type())); - const equal_exprt a4_body(res[q2], str[q2]); - const string_constraintt a4( - q2, lower_bound, zero_if_negative(res.length()), a4_body); - constraints.push_back(a4); - + lemmas.push_back(equal_exprt(res.length(), str.length())); + lemmas.push_back( + implies_exprt( + and_exprt( + binary_relation_exprt( + from_integer(0, position.type()), ID_le, position), + binary_relation_exprt(position, ID_lt, res.length())), + equal_exprt(res[position], character))); + constraints.push_back([&] { + const symbol_exprt q = fresh_univ_index("QA_char_set", position.type()); + const equal_exprt a3_body(res[q], str[q]); + return string_constraintt( + q, minimum(zero_if_negative(res.length()), position), a3_body); + }()); + constraints.push_back([&] { + const symbol_exprt q2 = fresh_univ_index("QA_char_set2", position.type()); + const plus_exprt lower_bound(position, from_integer(1, position.type())); + const equal_exprt a4_body(res[q2], str[q2]); + return string_constraintt( + q2, lower_bound, zero_if_negative(res.length()), a4_body); + }()); return if_exprt( - out_of_bounds, from_integer(1, f.type()), from_integer(0, f.type())); + out_of_bounds, + from_integer(1, get_return_code_type()), + from_integer(0, get_return_code_type())); } /// Convert two expressions to pair of chars diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index ca567a8c7ed..846cc0520ef 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -30,7 +30,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #include #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits::max() -#define CHARACTER_FOR_UNKNOWN '?' class string_refinementt final: public bv_refinementt { diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index e9227ebf865..05791860b35 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -228,6 +228,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_char_set_func) + return util_make_unique( + return_code, fun_app.arguments(), array_pool); + return util_make_unique( return_code, fun_app, array_pool); }