From 70cceb4622931e3e9778ea7524c1e24398116362 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Jul 2026 17:33:19 +0000 Subject: [PATCH 1/2] smt2: lower replace_all, from_code, to_code and from_int to SMT-LIB smt2_convt lowers applications of the cprover_string_* built-ins over SMT-LIB strings to the SMT-LIB theory of strings. Add four more built-ins with their SMT-LIB 2.6 counterparts: - replace_all(s, old, new) -> (str.replace_all s old new): replaces every match; s is unchanged if old is "". (replace, which lowers to str.replace, replaces the first match only.) - from_code(i) -> (str.from_code i): the one-character string with code point i, and "" unless 0 <= i <= 196607. - to_code(s) -> (str.to_code s): the code point of s if |s| = 1, and -1 otherwise. - from_int(n) -> (str.from_int n): the decimal representation of n, and "" for n < 0. A front-end that needs a sign can use ite(n < 0, "-" ++ from_int(-n), from_int(n)). The integer operands and results are Int-sorted in SMT-LIB; applications with operands or results of another sort, or with the wrong number of operands, are rejected with an unsupported_operation_exceptiont rather than producing input that the solver rejects. No front-end in this repository emits these built-ins yet: they are meant for front-ends that produce SMT-LIB-string applications, such as a Python front-end in preparation, where Python's str.replace, chr, ord and str of an integer need them. Note that the edge cases above follow SMT-LIB and differ from those languages (e.g. Python's "abc".replace("", "x") is "xaxbxcx"); a front-end has to handle such cases itself. Unit tests check the lowering, the rejection of other sorts and arities, and, using Z3, the values of the four lowerings on concrete operands, including the edge cases above. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 35 ++++++++ src/util/irep_ids.def | 4 + unit/solvers/smt2/smt2_conv.cpp | 152 ++++++++++++++++++++++++++++++++ 3 files changed, 191 insertions(+) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e3abf106e7df..e425e513cddc 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2786,6 +2786,19 @@ void smt2_convt::convert_expr(const exprt &expr) // is_prefix(prefix, s) -> (str.prefixof prefix s) // is_suffix(suffix, s) -> (str.suffixof suffix s) // replace(s, old, new) -> (str.replace s old new) : first match + // only; note that symex constant + // propagation and the SAT string solver + // give replace replace-every-match + // semantics + // replace_all(s, old, new) -> (str.replace_all s old new) : every + // match; s unchanged if old is "" + // from_code(i) -> (str.from_code i) : Int operand; "" + // unless 0 <= i <= 196607 + // to_code(s) -> (str.to_code s) : Int result; -1 + // unless |s| = 1 + // from_int(n) -> (str.from_int n) : Int operand; "" + // for n < 0 (unlike of_int, which + // produces a leading '-') // equal(s, t) -> (= s t) // index_of(s, sub[, off]) -> (str.indexof s sub off) : off defaults 0 // startswith(s, prefix) -> (str.prefixof prefix s) @@ -2826,6 +2839,10 @@ void smt2_convt::convert_expr(const exprt &expr) {ID_cprover_string_is_prefix_func, "str.prefixof"}, {ID_cprover_string_is_suffix_func, "str.suffixof"}, {ID_cprover_string_replace_func, "str.replace"}, + {ID_cprover_string_replace_all_func, "str.replace_all"}, + {ID_cprover_string_from_code_func, "str.from_code"}, + {ID_cprover_string_to_code_func, "str.to_code"}, + {ID_cprover_string_from_int_func, "str.from_int"}, {ID_cprover_string_equal_func, "="}, // regex operators {ID_cprover_string_to_regex_func, "str.to_re"}, @@ -2876,6 +2893,24 @@ void smt2_convt::convert_expr(const exprt &expr) } } + // The code-point and integer conversions are Int-sorted in SMT-LIB; + // reject operands or results of any other sort (e.g. bit-vectors) + // instead of emitting SMT-LIB that the solver rejects. + const bool int_operand = fn_id == ID_cprover_string_from_code_func || + fn_id == ID_cprover_string_from_int_func; + const bool int_result = fn_id == ID_cprover_string_to_code_func; + if( + (int_operand || int_result) && + (args.size() != 1 || + (int_operand && args[0].type().id() != ID_integer) || + (int_result && expr.type().id() != ID_integer))) + { + throw unsupported_operation_exceptiont{ + "string built-in '" + id2string(fn_id) + + "' expects exactly one operand and an Int-sorted (integer) " + "operand or result in the SMT-LIB string lowering"}; + } + if(is_index_of) { // str.indexof requires three operands; default the start offset to the diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 43bf0c5b7c07..f6d8456f090e 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -656,6 +656,10 @@ IREP_ID_ONE(cprover_string_parse_int_func) IREP_ID_ONE(cprover_string_is_valid_int_func) IREP_ID_ONE(cprover_string_is_valid_long_func) IREP_ID_ONE(cprover_string_replace_func) +IREP_ID_ONE(cprover_string_replace_all_func) +IREP_ID_ONE(cprover_string_from_code_func) +IREP_ID_ONE(cprover_string_to_code_func) +IREP_ID_ONE(cprover_string_from_int_func) IREP_ID_ONE(cprover_string_set_length_func) IREP_ID_ONE(cprover_string_startswith_func) IREP_ID_ONE(cprover_string_substring_func) diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index f346e68d3a37..3d4ae34c4a07 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -535,6 +535,56 @@ TEST_CASE( REQUIRE(get_assert(eq) == "(assert (= s1 s2))"); } + SECTION("string operators replace_all/from_code/to_code/from_int") + { + const typet int_type{ID_integer}; + + // replace_all replaces every occurrence (str.replace_all), unlike + // replace (str.replace, first occurrence only). + const auto repl_all = string_builtin_app( + ID_cprover_string_replace_all_func, {s1, s2, s1}, string_type); + const auto c_repl_all = string_builtin_app( + ID_cprover_string_contains_func, {repl_all, s2}, bool_typet{}); + REQUIRE( + get_assert(c_repl_all) == + "(assert (str.contains (str.replace_all s1 s2 s1) s2))"); + + // from_code: the single-char string for a code point (str.from_code). + const auto fc = string_builtin_app( + ID_cprover_string_from_code_func, + {from_integer(102, int_type)}, + string_type); + const auto c_fc = string_builtin_app( + ID_cprover_string_contains_func, {fc, s1}, bool_typet{}); + REQUIRE( + get_assert(c_fc) == "(assert (str.contains (str.from_code 102) s1))"); + + // to_code: the code point of a single-char string, an Int result + // (str.to_code; -1 unless the string has length 1). Composed under an + // Int operand here to exercise nesting. + const auto tc = + string_builtin_app(ID_cprover_string_to_code_func, {s2}, int_type); + const auto at_tc = + string_builtin_app(ID_cprover_string_char_at_func, {s1, tc}, string_type); + const auto c_tc = string_builtin_app( + ID_cprover_string_contains_func, {at_tc, s1}, bool_typet{}); + REQUIRE( + get_assert(c_tc) == + "(assert (str.contains (str.at s1 (str.to_code s2)) s1))"); + + // from_int: the decimal string of a non-negative integer (str.from_int; + // SMT-LIB defines it for naturals only -- negative values yield "" and a + // front-end needing sign support composes it, e.g. + // ite(n < 0, "-" ++ from_int(-n), from_int(n))). + const auto fi = + string_builtin_app(ID_cprover_string_from_int_func, {tc}, string_type); + const auto c_fi = string_builtin_app( + ID_cprover_string_contains_func, {fi, s1}, bool_typet{}); + REQUIRE( + get_assert(c_fi) == + "(assert (str.contains (str.from_int (str.to_code s2)) s1))"); + } + SECTION("regex range/concat/plus/union/inter/comp operators") { const auto re1 = @@ -619,6 +669,108 @@ TEST_CASE( ID_cprover_string_contains_func, {arr, s2}, bool_typet{}); REQUIRE_THROWS(get_assert(contains)); } + + SECTION("Int-sorted string conversions reject other sorts and arities") + { + const signedbv_typet s32{32}; + const auto fc_bv = string_builtin_app( + ID_cprover_string_from_code_func, {from_integer(102, s32)}, string_type); + REQUIRE_THROWS(get_assert(equal_exprt{fc_bv, s1})); + + const auto fc_two = string_builtin_app( + ID_cprover_string_from_code_func, + {from_integer(102, integer_typet{}), from_integer(102, integer_typet{})}, + string_type); + REQUIRE_THROWS(get_assert(equal_exprt{fc_two, s1})); + + const auto tc_bv = + string_builtin_app(ID_cprover_string_to_code_func, {s2}, s32); + REQUIRE_THROWS(get_assert(equal_exprt{tc_bv, from_integer(102, s32)})); + } +} + +/// Decide `lhs != expected` with Z3; UNSAT shows that the lowering of `lhs` +/// evaluates to `expected`. +static decision_proceduret::resultt +z3_disproves(const exprt &lhs, const exprt &expected) +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + null_message_handlert message_handler; + smt2_dect smt2_dec{ + ns, "unit test", "", "ALL", smt2_dect::solvert::Z3, "", message_handler}; + smt2_dec << notequal_exprt{lhs, expected}; + return smt2_dec(); +} + +TEST_CASE( + "smt2_convt string conversions evaluated by Z3", + "[core][solvers][smt2]") +{ + const typet string_type{ID_string}; + const integer_typet int_type; + const auto str = [&](const char *v) + { return constant_exprt{v, string_type}; }; + const auto num = [&](long v) { return from_integer(v, int_type); }; + const auto unsat = decision_proceduret::resultt::D_UNSATISFIABLE; + + // replace_all replaces every match; replace only the first one. + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_replace_all_func, + {str("aXaXa"), str("X"), str("Y")}, + string_type), + str("aYaYa")) == unsat); + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_replace_func, + {str("aXaXa"), str("X"), str("Y")}, + string_type), + str("aYaXa")) == unsat); + // An empty pattern leaves the string unchanged (unlike Java and Python). + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_replace_all_func, + {str("abc"), str(""), str("x")}, + string_type), + str("abc")) == unsat); + + // from_code: "" outside [0, 196607]. + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_from_code_func, {num(102)}, string_type), + str("f")) == unsat); + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_from_code_func, {num(196608)}, string_type), + str("")) == unsat); + + // to_code: -1 unless the string has length 1. + REQUIRE( + z3_disproves( + string_builtin_app(ID_cprover_string_to_code_func, {str("f")}, int_type), + num(102)) == unsat); + REQUIRE( + z3_disproves( + string_builtin_app(ID_cprover_string_to_code_func, {str("ab")}, int_type), + num(-1)) == unsat); + + // from_int: decimal digits, "" for negative values. + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_from_int_func, {num(42)}, string_type), + str("42")) == unsat); + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_from_int_func, {num(-5)}, string_type), + str("")) == unsat); } TEST_CASE( From cdc54a5a8361c19c21f91408a2c756924608c222 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Nov 2026 08:10:24 +0000 Subject: [PATCH 2/2] smt2: lower empty_string and decimal of_int to SMT-LIB smt2_convt lowers applications of the cprover_string_* built-ins over SMT-LIB strings to the SMT-LIB theory of strings, and turns the remaining ones into uninterpreted functions. Two of the latter do have exact SMT-LIB counterparts, and leaving them uninterpreted produced spurious counterexamples: for example, x = empty_string(); assert(x == "") failed with both Z3 and cvc5. - empty_string() -> "" - of_int(n) and of_int(n, 10) -> (ite (>= n 0) (str.from_int n) (str.++ "-" (str.from_int (- n)))) as str.from_int is "" for negative n. of_int with any other radix remains uninterpreted. As for from_int, the operand of of_int must be Int-sorted; other sorts are rejected with an unsupported_operation_exceptiont. Unit tests check the lowering, the rejection of other sorts and arities, that of_int with radix 16 is not lowered, and, using Z3, the values on concrete operands, including negative ones. Co-authored-by: Kiro --- src/solvers/smt2/smt2_conv.cpp | 54 ++++++++++++++++++++++++++++----- unit/solvers/smt2/smt2_conv.cpp | 41 +++++++++++++++++++++++++ 2 files changed, 87 insertions(+), 8 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e425e513cddc..b5b7ae0d1463 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -2799,6 +2799,10 @@ void smt2_convt::convert_expr(const exprt &expr) // from_int(n) -> (str.from_int n) : Int operand; "" // for n < 0 (unlike of_int, which // produces a leading '-') + // of_int(n[, 10]) -> (ite (>= n 0) (str.from_int n) + // (str.++ "-" (str.from_int (- n)))) + // : Int operand, decimal only + // empty_string() -> "" // equal(s, t) -> (= s t) // index_of(s, sub[, off]) -> (str.indexof s sub off) : off defaults 0 // startswith(s, prefix) -> (str.prefixof prefix s) @@ -2807,9 +2811,11 @@ void smt2_convt::convert_expr(const exprt &expr) // and the regex operators map to str.to_re / str.in_re and the re.* family // (re.range, re.++, re.*, re.+, re.opt, re.loop, re.union, re.inter, // re.comp, re.diff, re.all, re.allchar, re.none). Built-ins without an - // exact SMT-LIB theory-of-strings counterpart (e.g. compare_to, of_int, - // parse_int, format, case folding, trim) are intentionally not lowered and - // fall through to the generic function-application handling below. + // exact SMT-LIB theory-of-strings counterpart (e.g. compare_to, of_int with + // a radix other than 10, parse_int, format, case folding, trim) are + // intentionally not lowered and fall through to the generic + // function-application handling below, which makes them uninterpreted + // functions. // // Note: this lowering is specific to the (non-incremental) smt2_convt // back-end. The incremental SMT back-end uses a separate converter @@ -2870,10 +2876,17 @@ void smt2_convt::convert_expr(const exprt &expr) const bool is_endswith = fn_id == ID_cprover_string_endswith_func; const bool is_is_empty = fn_id == ID_cprover_string_is_empty_func; const bool is_regex_loop = fn_id == ID_cprover_regex_loop_func; + const bool is_empty_string = fn_id == ID_cprover_string_empty_string_func; + // of_int with a radix other than 10 has no SMT-LIB counterpart. + const bool is_of_int = + fn_id == ID_cprover_string_of_int_func && + (args.size() == 1 || + (args.size() == 2 && args[1].is_constant() && + numeric_cast(to_constant_expr(args[1])) == mp_integer{10})); if( !smt_name.empty() || is_index_of || is_startswith || is_endswith || - is_is_empty || is_regex_loop) + is_is_empty || is_regex_loop || is_empty_string || is_of_int) { // Soundness guard: this native lowering expects SMT-LIB-native operands. // The same cprover_string_*_func ids are also used with the @@ -2897,18 +2910,19 @@ void smt2_convt::convert_expr(const exprt &expr) // reject operands or results of any other sort (e.g. bit-vectors) // instead of emitting SMT-LIB that the solver rejects. const bool int_operand = fn_id == ID_cprover_string_from_code_func || - fn_id == ID_cprover_string_from_int_func; + fn_id == ID_cprover_string_from_int_func || + is_of_int; const bool int_result = fn_id == ID_cprover_string_to_code_func; if( (int_operand || int_result) && - (args.size() != 1 || + ((!is_of_int && args.size() != 1) || (int_operand && args[0].type().id() != ID_integer) || (int_result && expr.type().id() != ID_integer))) { throw unsupported_operation_exceptiont{ "string built-in '" + id2string(fn_id) + - "' expects exactly one operand and an Int-sorted (integer) " - "operand or result in the SMT-LIB string lowering"}; + "' expects a single Int-sorted (integer) operand or an " + "Int-sorted result in the SMT-LIB string lowering"}; } if(is_index_of) @@ -2938,6 +2952,30 @@ void smt2_convt::convert_expr(const exprt &expr) convert_expr(args[0]); out << ')'; } + else if(is_empty_string) + { + // empty_string() -> "" + if(!args.empty() || expr.type().id() != ID_string) + { + throw unsupported_operation_exceptiont{ + "string built-in '" + id2string(fn_id) + + "' expects no operands and a String result in the SMT-LIB " + "string lowering"}; + } + out << "\"\""; + } + else if(is_of_int) + { + // of_int(n[, 10]): the decimal representation of n, with a leading + // '-' for negative n, whereas str.from_int yields "" for n < 0. + out << "(ite (>= "; + convert_expr(args[0]); + out << " 0) (str.from_int "; + convert_expr(args[0]); + out << ") (str.++ \"-\" (str.from_int (- "; + convert_expr(args[0]); + out << "))))"; + } else if(is_is_empty) { // is_empty(s) -> (= s "") diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index 3d4ae34c4a07..3435f5cfda15 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -686,6 +686,25 @@ TEST_CASE( const auto tc_bv = string_builtin_app(ID_cprover_string_to_code_func, {s2}, s32); REQUIRE_THROWS(get_assert(equal_exprt{tc_bv, from_integer(102, s32)})); + + const auto oi_bv = string_builtin_app( + ID_cprover_string_of_int_func, {from_integer(102, s32)}, string_type); + REQUIRE_THROWS(get_assert(equal_exprt{oi_bv, s1})); + + const auto es_arg = string_builtin_app( + ID_cprover_string_empty_string_func, {s1}, string_type); + REQUIRE_THROWS(get_assert(equal_exprt{es_arg, s1})); + } + + SECTION("of_int with a radix other than 10 is not lowered") + { + const auto oi_hex = string_builtin_app( + ID_cprover_string_of_int_func, + {from_integer(102, integer_typet{}), from_integer(16, integer_typet{})}, + string_type); + REQUIRE( + get_assert(equal_exprt{oi_hex, s1}) == + "(assert (= (cprover_string_of_int_func 102 16) s1))"); } } @@ -771,6 +790,28 @@ TEST_CASE( string_builtin_app( ID_cprover_string_from_int_func, {num(-5)}, string_type), str("")) == unsat); + + // of_int: decimal digits, with a leading '-' for negative values. + for(const auto &[n, digits] : std::vector>{ + {42, "42"}, {0, "0"}, {-5, "-5"}, {-120, "-120"}}) + { + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_of_int_func, {num(n)}, string_type), + str(digits)) == unsat); + REQUIRE( + z3_disproves( + string_builtin_app( + ID_cprover_string_of_int_func, {num(n), num(10)}, string_type), + str(digits)) == unsat); + } + + // empty_string is "" + REQUIRE( + z3_disproves( + string_builtin_app(ID_cprover_string_empty_string_func, {}, string_type), + str("")) == unsat); } TEST_CASE(