From 9e7363bd272cfef869d5cb986ec2ab20f0072574 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 3 Aug 2026 10:08:11 -0700 Subject: [PATCH] fix unsound regex info for the legacy argument form of re.loop (#10370) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `re.loop` has two accepted AST forms: bounds as decl parameters, `((_ re.loop lo hi) r)` (1 argument, 2 parameters), and bounds as arguments, `(re.loop r lo hi)` (3 arguments, 0 parameters). The plugin accepts arities 1, 2 and 3, and `is_loop` has separate overloads for each form. Only the parameter form was recognized downstream. ### The soundness bug `mk_info_rec`'s `OP_RE_LOOP` case read the bounds solely from `get_decl()->get_num_parameters()`, which is 0 for the argument form, so it silently fell back to the locals `lower_bound = 0, upper_bound = UINT_MAX`. `info::loop` computes ```cpp loop_nullable = (nullable == l_true || lower == 0) ? l_true : nullable; ``` so `lower == 0` forces nullability, and `min_length` collapses to `min_length * 0 = 0`. Net effect: `(re.loop (str.to_re "ab") 1 3)` was reported as `nullable = l_true, min_length = 0`. At the SMT level ```smt2 (declare-const x String) (assert (str.in_re x (re.loop (str.to_re "ab") 1 3))) (assert (= (str.len x) 0)) (check-sat) ``` answered **sat** rather than unsat. The indexed form of the same regex correctly answers unsat. `seq_rewriter::mk_re_loop` already normalizes the argument form to `mk_loop_proper`, which is why this was never observable on the usual paths — it only surfaces where the rewriter is bypassed, as in `seq_monadic`. The `info.nullable` fast path added in #10366 didn't create the bug but widened the path that reaches it. ### The performance bug `derive_core` had no case for the argument form either, so the derivative got stuck as an uninterpreted `re.derivative` term. Instrumenting all three sites that can emit a symbolic `re.derivative` showed that **every one of the 4171 stuck terms** in the regex corpus came from this fall-through (the 512-deep recursion cap and the unnormalizable `re.reverse` site never fired), and 4096 of them came from a single legacy-form loop, whose search then burned its full budget before giving up. ### The fix * `mk_info_rec` branches on `get_num_args()`; for the argument form it reads the bounds from `get_arg(1)`/`get_arg(2)` when they are unsigned numerals, and returns `unknown_info` when they are not. * `derive_core` normalizes the numeral argument forms to `mk_loop_proper`/`mk_loop` and recurses. The block is gated on the cheap `re().is_loop(r)` kind check so that regexes falling through to the later cases don't pay for the `rational` locals. Arguably the right long-term place to normalize is the parser, so the legacy form never reaches the AST at all. Keeping the `mk_info_rec` half is still worthwhile as a guard for API-constructed terms, and the regression test builds the term directly via `mk_app`, so it stays meaningful either way. ### Regression test `src/test/seq_rewriter.cpp` gains a case asserting that `get_info` agrees on the two forms (`nullable == l_false`, `min_length == 2`). Verified to actually catch the bug: reverting `seq_decl_plugin.cpp` and rebuilding gives `ASSERTION VIOLATION` with `nullable=l_true min_length=0`. ### Evaluation Full run over 1545 regex benchmarks with declared statuses, in both transition modes: | | light-ant | brz | |---|---|---| | decided (before → after) | 1462 → **1463** | 1464 → **1465** | | soundness mismatches | 0 → 0 | 0 → 0 | | verdict changes | 1 | 1 (same file) | The one changed file is `L4-01-loop-sat.smt2`: **undef @ 8625 ms → sat @ 0.20 ms**. The corpus contains 1 legacy-form file and 236 indexed-form files, which share the modified `OP_RE_LOOP` path, hence the full A/B rather than a spot check. Timing is neutral. Measured with an interleaved base/fix/base/fix protocol over two saved binaries, since same-binary run-to-run variance (±8%) turned out to exceed the effect: paired best-of-2 over the 315 files taking >1 ms gives a **median ratio of 0.998** (p25/p75 = 0.889/1.075), overall 0.976. `tst_seq_rewriter` passes, `seq_monadic` is ALL PASS in both modes, and the 22172-file QF_S corpus shows no verdict changes and no mismatches. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2 --- src/ast/rewriter/seq_derive.cpp | 16 ++++++++++++++++ src/ast/seq_decl_plugin.cpp | 29 ++++++++++++++++++++++++----- src/test/seq_rewriter.cpp | 28 +++++++++++++++++++++++++++- 3 files changed, 67 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 8bfe4bf96b..39f2ea2a44 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -288,6 +288,22 @@ namespace seq { return mk_deriv_concat(d1, tail); } + // Legacy form where the loop bounds are arguments rather than + // decl parameters: (re.loop r lo hi) and (re.loop r lo). The parser + // accepts these and seq_rewriter normalizes them, but unrewritten + // terms reach here directly. Rewrite to the parameterized form. + if (re().is_loop(r)) { + expr* lo_e = nullptr, * hi_e = nullptr; + rational nlo, nhi; + if (re().is_loop(r, r1, lo_e, hi_e) && + m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned() && + m_autil.is_numeral(hi_e, nhi) && nhi.is_unsigned()) + return derive_rec(re().mk_loop_proper(r1, nlo.get_unsigned(), nhi.get_unsigned())); + if (re().is_loop(r, r1, lo_e) && + m_autil.is_numeral(lo_e, nlo) && nlo.is_unsigned()) + return derive_rec(re().mk_loop(r1, nlo.get_unsigned())); + } + // δ(r1 \ r2) = δ(r1) ∩ ~δ(r2) if (re().is_diff(r, r1, r2)) { expr_ref d1 = derive_rec(r1); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index d0f45485dd..36310fd3c3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1733,11 +1733,30 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { return i1.complement(); case OP_RE_LOOP: i1 = get_info_rec(e->get_arg(0)); - if (e->get_decl()->get_num_parameters() >= 1) - lower_bound = e->get_decl()->get_parameter(0).get_int(); - if (e->get_decl()->get_num_parameters() == 2) - upper_bound = e->get_decl()->get_parameter(1).get_int(); - return i1.loop(lower_bound, upper_bound); + if (e->get_num_args() == 1) { + if (e->get_decl()->get_num_parameters() >= 1) + lower_bound = e->get_decl()->get_parameter(0).get_int(); + if (e->get_decl()->get_num_parameters() == 2) + upper_bound = e->get_decl()->get_parameter(1).get_int(); + return i1.loop(lower_bound, upper_bound); + } + else { + // legacy form carrying the bounds as arguments: + // (re.loop r lo) and (re.loop r lo hi) + arith_util autil(m); + rational n; + if (e->get_num_args() != 2 && e->get_num_args() != 3) + return unknown_info; + if (!autil.is_numeral(e->get_arg(1), n) || !n.is_unsigned()) + return unknown_info; + lower_bound = n.get_unsigned(); + if (e->get_num_args() == 3) { + if (!autil.is_numeral(e->get_arg(2), n) || !n.is_unsigned()) + return unknown_info; + upper_bound = n.get_unsigned(); + } + return i1.loop(lower_bound, upper_bound); + } case OP_RE_DIFF: if (e->get_num_args() != 2) return unknown_info; diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index 55c318aa86..ebfdb09e11 100644 --- a/src/test/seq_rewriter.cpp +++ b/src/test/seq_rewriter.cpp @@ -16,7 +16,8 @@ Tests: 18. Solver: (str.in_re x (re.range x x)) unsat when len(x)=2 19. Solver: inverted symbolic bounds make membership unsatisfiable 20. Solver: contradictory constant lexical bounds are unsatisfiable - 22. (Σ*·S)* is flattened to () | Σ*·S + 22. re.loop with bounds as arguments agrees with the indexed form + 23. (Σ*·S)* is flattened to () | Σ*·S --*/ #include "ast/arith_decl_plugin.h" @@ -323,5 +324,30 @@ void tst_seq_rewriter() { } } + // ----------------------------------------------------------------------- + // 22. re.loop with the bounds given as arguments must be interpreted the + // same as the indexed form. get_info used to read the bounds only + // from the decl parameters, which the argument form does not carry, + // so it silently fell back to lo = 0 and reported (ab){1,3} as + // nullable with min_length 0. seq_rewriter normalizes the argument + // form, so this is only observable on paths that bypass it. + // ----------------------------------------------------------------------- + { + arith_util a_util(m); + expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m); + expr_ref indexed(su.re.mk_loop_proper(ab, 1, 3), m); + expr* args[3] = { ab.get(), a_util.mk_int(1), a_util.mk_int(3) }; + expr_ref as_args(m.mk_app(su.get_family_id(), OP_RE_LOOP, 0, nullptr, 3, args), m); + + auto i1 = su.re.get_info(indexed); + auto i2 = su.re.get_info(as_args); + std::cout << "re.loop indexed: " << mk_pp(indexed, m) + << " nullable=" << i1.nullable << " min_length=" << i1.min_length << "\n"; + std::cout << "re.loop arguments: " << mk_pp(as_args, m) + << " nullable=" << i2.nullable << " min_length=" << i2.min_length << "\n"; + ENSURE(i1.nullable == l_false && i1.min_length == 2); + ENSURE(i2.nullable == l_false && i2.min_length == 2); + } + std::cout << "tst_seq_rewriter: all tests passed\n"; }