Regex Decision Procedures in Extended RE#

We develop decision procedures for extended regular expressions in the new ERE# framework that uses span semantics, utilizing the power of symbolic derivatives. We prove a normal form theorem in Lean for ERE# that is closed under all Boolean operations and provides the basis for the given decision procedures. The tool is evaluated on existing SMT benchmarks for regexes that shows it to be the fastest solver to date -often orders of magnitude faster than state-of-the-art -albeit specialized for the single-variable fragment of string theory.

a regex 𝑅 = .*a?𝑘 for a is 𝑅|a?𝑘-1 that can be simplified to 𝑅 because 𝑅 subsumes a?𝑘-1, where a? abbreviates a|𝜀. Omitting such rewrites can quickly lead to a state space explosion up to size 2 𝑘 -observe that 𝑘 = 𝑂 (2 | 𝑅 | ) here! For DFA generation, such subsumption checking must be fast in practice.

Dealing with differences between PCRE and POSIX semantics for a regex is a common problem. 3 In PCRE, also known as backtracking or leftmost-eager semantics, the union operator | is noncommutative where in a regex 𝑅 1 |𝑅 2 , a match for 𝑅 2 is only sought when 𝑅 1 fails to match. Note that this difference is relevant for span semantics that has recently been formalized in Lean [50], but irrelevant for language semantics (IsMatch) that is identical under both PCRE and POSIX. A technique to decide if a union 𝑅 1 |𝑅 2 in PCRE has the same span semantics under POSIX, where union is commutative, is to decide match equivalence between 𝑅 1 |𝑅 2 and

If the span semantics of a regex differs between PCRE and POSIX then the regex may contain unreachable cases under PCRE. E.g., the BurntSushi/rebar benchmarking tool [24] -widely used for industrial PCRE matchers -uses a dictionary benchmark containing unions such as may|mayo. The regex may|mayo will never match "mayo" for any input under PCRE semantics and has the exact same behavior as the regex may. Most industrial regex matchers use PCRE semantics, resulting in different behavior to what is intuitively assumed, as | is not union of languages in PCRE. It is a common programming error to define a regex with unintended behavior this way. For example, by using the above technique, may|mayo& (may_) effectively deletes the alternative mayo from may|mayo while mayo|may would remain intact because may& (mayo_) ≡ may.

The logic ERE#, that is introduced in Section 4, is a novel contribution and fundamental for many decision problems. In particular, it lifts RE# to the status of an Effective Boolean Algebra over spans. RE# is closed only under intersection and each regex admits a linear translation to a core regex of the form (?<=𝑅 1 )𝑅 2 (?=𝑅 3 ) where no 𝑅 𝑖 contains lookarounds. The span semantics

where 𝑢 2 is the main match with 𝑢 1 and 𝑢 3 as the surrounding context. For many decision problems, like subsumption, it became necessary to support regexes like (?<=𝑅 1 )𝑅 2 (?=𝑅 3 )& ((?<=𝑅 ′ 1 )𝑅 ′ 2 (?=𝑅 ′ 3 )) that fall outside the fragment for matching in RE#.

Currently, ERE# semantics is not directly expressible in SMT-LIB as it would require support for lookarounds and span semantics. Section 7 proposes an SMT-LIB format for extending RegLan with lookarounds and span semantics.

Contributions. We introduce an extension ERE# of the RE# class that is Boolean closed and formalize a normal form theorem (Theorem 2) for it in Lean allowing us to develop decision procedures for ERE#, including emptiness, subsumption, and equivalence, that are of primary interest in the ERE# framework, as discussed above. It is also possible to use ERE# for pre-processing in SMT solvers. One can invoke ERE# from the simplifier in Z3 [39], to pre-process