From 9d255633d61ebfa2626cf64a0b5b12986d1d0450 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 24 Jun 2026 10:33:05 -0700 Subject: [PATCH 1/3] Port SARIF and regex differential tests from Python to Lean tests Move two CI test scripts in-process as StrataPythonTestExtra Lean tests, following the CpythonDiffTest precedent, and fix a related lakefile bug. SARIF (replaces run_py_analyze_sarif.py + validate_sarif.py): StrataPythonTestExtra/SarifTest.lean spawns strata_python.gen to compile each tests/test_*.py to Ion, runs StrataPython.Pipeline.runPyAnalyzePipeline (the same path `pyAnalyzeLaurel --sarif` drives), builds the SARIF document via Core.Sarif.vcResultsToSarif, and asserts on the typed SarifDocument directly. Most of the Python validator's checks now hold by construction; the per-test checks, tool name, and SKIP_TESTS set are ported. Drops a `lake exe` subprocess and the JSON parse/re-validate round trip. Regex (replaces Regex/diff_test.py): StrataPythonTestExtra/RegexDiffTest.lean runs Strata's SMT regex backend in-process (lifting checkMatch from DiffTestCore.lean) and compares against Python's `re`, which has no in-process equivalent and stays a subprocess: Regex/regex_oracle.py reads the corpus on stdin, spawned once. The 534-case corpus moves to Regex/corpus.tsv. Verdict classification matches the Python driver; counts are identical (468 agree, 0 bugs, 66 known gaps, 0 investigate). The DiffTestCore executable is kept (it has a --log-dir debugging feature). lakefile: treat the PythonDialectIon input_file as binary (drop `text = true`); the dialect Ion file is binary and reading it as text is incorrect. CI: build_and_test_lean runs both via `lake test -- `; the build_python matrix excludes them (SMT-heavy and version-independent, run once not per Python version). Co-Authored-By: Claude Opus 4.8 --- .github/workflows/ci.yml | 25 +- StrataPythonTest/Regex/corpus.tsv | 534 +++++++++++++ StrataPythonTest/Regex/diff_test.py | 975 ----------------------- StrataPythonTest/Regex/regex_oracle.py | 50 ++ StrataPythonTest/run_py_analyze_sarif.py | 96 --- StrataPythonTest/validate_sarif.py | 57 -- StrataPythonTestExtra/RegexDiffTest.lean | 229 ++++++ StrataPythonTestExtra/SarifTest.lean | 186 +++++ lakefile.toml | 1 - 9 files changed, 1015 insertions(+), 1138 deletions(-) create mode 100644 StrataPythonTest/Regex/corpus.tsv delete mode 100644 StrataPythonTest/Regex/diff_test.py create mode 100644 StrataPythonTest/Regex/regex_oracle.py delete mode 100755 StrataPythonTest/run_py_analyze_sarif.py delete mode 100755 StrataPythonTest/validate_sarif.py create mode 100644 StrataPythonTestExtra/RegexDiffTest.lean create mode 100644 StrataPythonTestExtra/SarifTest.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 46a4e4d..53d5bb1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -52,16 +52,21 @@ jobs: shell: bash run: ./run_py_interpret.sh - name: Run pyAnalyze SARIF tests - working-directory: StrataPythonTest - shell: bash - run: python run_py_analyze_sarif.py + # SarifTest is the StrataPythonTestExtra Lean port of the old + # run_py_analyze_sarif.py: it runs the analysis pipeline in-process and + # asserts on the SARIF document. Excluded from the build_python matrix + # below so the (SMT-heavy) suite runs once here rather than per version. + run: PYTHON=python lake test -- SarifTest - name: Run pyAnalyze golden-file tests working-directory: StrataPythonTest shell: bash run: ./run_py_analyze.sh - name: Run regex differential tests - working-directory: StrataPythonTest/Regex - run: python diff_test.py + # RegexDiffTest is the StrataPythonTestExtra Lean port of the old + # Regex/diff_test.py: it runs Strata's SMT regex backend in-process and + # compares against the Python `re` oracle (spawned once). Excluded from + # the build_python matrix below so the (SMT-heavy) suite runs once here. + run: PYTHON=python lake test -- RegexDiffTest - name: Save lake cache uses: ./.github/actions/save-lake-cache with: @@ -174,10 +179,12 @@ jobs: with: install-to: system - name: Run PySpec and dispatch tests - # Excludes the CPython differential test, which is run separately below - # against a full CPython checkout; here it would be a no-op anyway since - # CPYTHON_DIR is unset. - run: PYTHON=python lake test -- --exclude CpythonDiffTest + # Excludes: + # - CpythonDiffTest: run separately below against a full CPython checkout + # (here it would be a no-op anyway since CPYTHON_DIR is unset). + # - SarifTest, RegexDiffTest: SMT-heavy and version-independent, run once + # in build_and_test_lean rather than per Python version. + run: PYTHON=python lake test -- --exclude CpythonDiffTest --exclude SarifTest --exclude RegexDiffTest - name: Run CPython differential tests # Clones CPython at the matrix version and round-trips its whole test # suite through the Strata generator + Ion (de)serializer. The round-trip diff --git a/StrataPythonTest/Regex/corpus.tsv b/StrataPythonTest/Regex/corpus.tsv new file mode 100644 index 0000000..4f020d5 --- /dev/null +++ b/StrataPythonTest/Regex/corpus.tsv @@ -0,0 +1,534 @@ +a a fullmatch +a b fullmatch +ab ab fullmatch +ab a fullmatch +ab abc fullmatch +a abc match +a bcd match +ab abc match +ab bcd match +. a fullmatch +. fullmatch +. ab fullmatch +.+ abc fullmatch +[a-z] a fullmatch +[a-z] z fullmatch +[a-z] A fullmatch +[abc] b fullmatch +[abc] d fullmatch +[a-z]+ hello fullmatch +[a-z]+ Hello fullmatch +[^a-z] A fullmatch +[^a-z] a fullmatch +[^b] a fullmatch +[^b] b fullmatch +[^A-Z]+ hello fullmatch +[^A-Z]+ Hello fullmatch +[^a] fullmatch +[^a] bc fullmatch +[^a] bb fullmatch +[^b]+ fullmatch +a* fullmatch +a* aaa fullmatch +a* b fullmatch +a+ fullmatch +a+ a fullmatch +a+ aaa fullmatch +((((((a+)+)+)+)+)+)+ a fullmatch +((((((a+)+)+)+)+)+)+ b fullmatch +((((((a+)+)+)+)+)+)+ aab match +((((((a+)+)+)+)+)+)+ bab search +(a+)* fullmatch +(a+)* a fullmatch +(a+)* aaa fullmatch +(a+)* b fullmatch +(a+)* ab match +(a+)* bab search +(a*)+ fullmatch +(a*)+ a fullmatch +(a*)+ aaa fullmatch +(a*)+ b fullmatch +(a*)+ ab match +(a*)+ bab search +(a+b+)+ fullmatch +(a+b+)+ ab fullmatch +(a+b+)+ aabb fullmatch +(a+b+)+ abab fullmatch +(a+b+)+ a fullmatch +(a+b+)+ ba fullmatch +(a+b+)+ abx match +(a+b+)+ xab search +(a+|b+)+ fullmatch +(a+|b+)+ a fullmatch +(a+|b+)+ b fullmatch +(a+|b+)+ aabb fullmatch +(a+|b+)+ abba fullmatch +(a+|b+)+ c fullmatch +(a+|b+)+ ac match +(a+|b+)+ cab search +a? fullmatch +a? a fullmatch +a? aa fullmatch +a{2,4} a fullmatch +a{2,4} aa fullmatch +a{2,4} aaaa fullmatch +a{2,4} aaaaa fullmatch +a{3} aaa fullmatch +a{3} aa fullmatch +a{0} fullmatch +a{0} a fullmatch +a{1} a fullmatch +a{1} aa fullmatch +a{0,1} fullmatch +a{0,1} a fullmatch +a{0,1} aa fullmatch +(ab){2} abab fullmatch +(ab){2} ab fullmatch +(ab){2} ababab fullmatch +(ab){2,3} abab fullmatch +(ab){2,3} ababab fullmatch +(ab){2,3} ab fullmatch +(ab){2,3} abababab fullmatch +[a-z0-9.\-]{1,10} test-str-1 fullmatch +[a-z0-9.\-]{1,10} test-str! fullmatch +[a-z0-9.\-]{1,10} fullmatch +[a-z0-9.\-]{1,10} 0123456789a fullmatch +a{2} xaax search +a{2} xa search +(ab){2} xababx search +(ab){2} xabx search +^a{3}$ aaa fullmatch +^a{3}$ aa fullmatch +^a{3}$ aaaa fullmatch +^a{2,4}$ a fullmatch +^a{2,4}$ aa fullmatch +^a{2,4}$ aaaa fullmatch +^a{2,4}$ aaaaa fullmatch +^a{3}$ aaa match +^a{3}$ aaab match +a{3} aaab match +a|b a fullmatch +a|b b fullmatch +a|b c fullmatch +a|b|c c fullmatch +a|b|c d fullmatch +(ab)+ ab fullmatch +(ab)+ abab fullmatch +(ab)+ aba fullmatch +(a|b)+ abba fullmatch +(a|b)+ abbc fullmatch +^a a fullmatch +^a ba fullmatch +a$ a fullmatch +a$ ab fullmatch +^a$ a fullmatch +^a$ ab fullmatch +^a$ ba fullmatch +^a a match +^a ab match +^a ba match +^a$ a match +^a$ ab match +^$ fullmatch +^$ a fullmatch +^$ match +^$ a match +^$ search +^$ a search + fullmatch + a fullmatch +a xax search +a xyz search +^a$ a search +^a$ xa search +^a$ ax search +^a abc search +^a xabc search +^a a search +a$ ba search +a$ ab search +a$ xyzba search +a$ xyzbax search +^a|b$ a fullmatch +^a|b$ b fullmatch +^a|b$ ab fullmatch +^a|b$ a match +^a|b$ b match +^a|b$ ab match +^a|b$ xb match +^a|b$ axyz search +^a|b$ xyzb search +^a|b$ xyzc search +^a|b$ axyzb search +^(a|b)$ a fullmatch +^(a|b)$ b fullmatch +^(a|b)$ ab fullmatch +^(a|b)$ a match +^(a|b)$ b match +^(a|b)$ ab match +^(a|b)$ a search +^(a|b)$ ab search +(^a$)|(^b$) a fullmatch +(^a$)|(^b$) b fullmatch +(^a$)|(^b$) c fullmatch +^a$|^$b a fullmatch +^a$|^$b fullmatch +a$.* a fullmatch +a$.* ab fullmatch +a$.* a match +a$.* ab match +a$.* ba search +a$.* ab search +a$b* a fullmatch +a$b* ab fullmatch +a$b? a fullmatch +a$b? ab fullmatch +a$.+ a match +a$.+ ab match +a$b+ a fullmatch +a$b+ ab fullmatch +a$$ a match +a$$ ab match +a$ a match +a$ ab match +a$ ba match +a$ aab match +a.*$ axyz match +a.*$ a match +a.*$ b match +a.*b axyzb match +a.*b ab match +a.*b axyz match +a.*b baxyzb match +ab$.* ab fullmatch +ab$.* abc fullmatch +ab$.* ab match +ab$.* abc match +ab$.* xab search +ab$.* xabc search +[a-z]$.* a fullmatch +[a-z]$.* ab fullmatch +[a-z]$.* xa search +[a-z]$.* xa1 search +(ab)$.* ab fullmatch +(ab)$.* abc fullmatch +(ab)$.* ab match +.*^a a match +.*^a ab match +.*^a ba match +.*^a a search +.*^a ba search +.*^a xa search +a?(^b) b fullmatch +a?(^b) ab fullmatch +a?(^b) b match +a?(^b) ba match +a?(^b) ab match +a?(^b) b search +a?(^b) xb search +a?(^b) ab search +a?(^b) xab search +a?(^b) ba search +a?(^b) bx search +^?(^b) b search +^?(^b) xb search +^?(^b) ab search +a?^b b fullmatch +a?^b a fullmatch +a?^b ab fullmatch +a?^b b match +a?^b ba match +a?^b ab match +a?^b? fullmatch +a?^b? b fullmatch +a?^b? a fullmatch +a?^b? ab fullmatch +a?^b? match +a?^b? b match +a?^b? a match +a$b ab match +(^a)* fullmatch +(^a)* a fullmatch +(^a)* aa fullmatch +(^a)* a match +(^a)* aa match +(a$)* fullmatch +(a$)* a fullmatch +(a$)* aa fullmatch +(a$)* a match +(a$)* ab match +(^a$)* fullmatch +(^a$)* a fullmatch +(^a$)* aa fullmatch +(^a){2} aa fullmatch +(^a){2} a fullmatch +(a$){2} aa fullmatch +(a$){2} a fullmatch +(^a){0,2} fullmatch +(^a){0,2} a fullmatch +(^a){0,2} aa fullmatch +(a$){0,2} fullmatch +(a$){0,2} a fullmatch +(a$){0,2} aa fullmatch +(^a){1,2} a fullmatch +(^a){1,2} aa fullmatch +(a$){1,2} a fullmatch +(a$){1,2} aa fullmatch +(a?)* fullmatch +(a?)* a fullmatch +(a?)* aaa fullmatch +(^a?)* fullmatch +(^a?)* a fullmatch +(^a?)* aa fullmatch +(a?$)* fullmatch +(a?$)* a fullmatch +(a?$)* aa fullmatch +(a?){0,2} fullmatch +(a?){0,2} a fullmatch +(a?){0,2} aa fullmatch +(a?){0,2} aaa fullmatch +(^a?){0,2} fullmatch +(^a?){0,2} a fullmatch +(^a?){0,2} aa fullmatch +(a?$){0,2} fullmatch +(a?$){0,2} a fullmatch +(a?$){0,2} aa fullmatch +x(^a) xa fullmatch +x(^a) a fullmatch +x(^a|b) xb fullmatch +x(^a|b) xa fullmatch +(a$)b ab fullmatch +(a$)(b) ab fullmatch +(a$)b ab match +(a$|b)c ac fullmatch +(a$|b)c bc fullmatch +(a$|b)c abc fullmatch +(a|b$)c ac fullmatch +(a|b$)c bc fullmatch +(^a)(^b) ab fullmatch +(^a)(^b) a fullmatch +(a$)(b$) ab fullmatch +(a$)(b$) a fullmatch +(^|$)c c fullmatch +(^|$)c xc fullmatch +a(^|$)b ab fullmatch +c(^a|b$)d cad fullmatch +c(^a|b$)d cbd fullmatch +c(^a|b$)d ccd fullmatch +(^a|b$)(^c|d$) ac fullmatch +(^a|b$)(^c|d$) bd fullmatch +(^a|b$)(^c|d$) bc fullmatch +(^a)(b) ab search +(^a)(b) xab search +(a)(b$) ab search +(a)(b$) abx search +(^a)(b$) ab search +(^a)(b$) xab search +(^a)(b$) abx search +(a$|b)c bc match +(a$|b)c bcd match +a?$b? fullmatch +a?$b? a fullmatch +a?$b? b fullmatch +a?$b? ab fullmatch +a?$b? match +a?$b? a match +a?$b? b match +a?$b? ab match +a?$b? a search +a?$b? b search +a?$b? xb search +a?$b? ab search +(a?$)b? fullmatch +(a?$)b? a fullmatch +(a?$)b? ab fullmatch +(a?$)b? b fullmatch +abc abc fullmatch +abc ab fullmatch +abc abcd fullmatch +abc ABC fullmatch +abc abc match +abc abcd match +abc xabc match +abc xabc search +abc xabcx search +abc xabx search +abc|def abc fullmatch +abc|def def fullmatch +abc|def abcdef fullmatch +abc|def abd fullmatch +abc|def xdef search +abc|def xabx search +(abc)+ abc fullmatch +(abc)+ abcabc fullmatch +(abc)+ abcab fullmatch +(abc){2} abcabc fullmatch +(abc){2} abc fullmatch +(abc){2} abcabcabc fullmatch +(abc){1,3} abc fullmatch +(abc){1,3} abcabcabc fullmatch +(abc){1,3} abcabcabcabc fullmatch +(ab|cd)+ abcd fullmatch +(ab|cd)+ cdab fullmatch +(ab|cd)+ abce fullmatch +(ab|cd)+ xabcdy search +(ab|cd)+ xacx search +[a-z][0-9] a1 fullmatch +[a-z][0-9] a12 fullmatch +[a-z][0-9] 11 fullmatch +[a-z][0-9]+ a123 fullmatch +[a-z][0-9]+ a fullmatch +[a-z]{2}[0-9]{2} ab12 fullmatch +[a-z]{2}[0-9]{2} a12 fullmatch +[a-z]{2}[0-9]{2} ab1 fullmatch +[a-z]{2}[0-9]{2} xab12y search +[a-z]{2}[0-9]{2} xab1y search +^abc$ abc fullmatch +^abc$ xabc fullmatch +^abc$ abcx fullmatch +^abc abcxyz search +^abc xabc search +abc$ xyzabc search +abc$ abcx search +^abc$ abc search +^abc$ xabc search +^abc$ abcx search +abc.*def abcdef fullmatch +abc.*def abcXXdef fullmatch +abc.*def abcdef search +abc.*def xabcXXdefy search +abc.*def abcXXdeg fullmatch +abc.+def abcdef fullmatch +abc.+def abcXdef fullmatch +ab ababab search +ab bbbabb search +ab aabb search +ab ba search +abc aabbc search +abc aabcbc search +a:b a:b fullmatch +a:b ab fullmatch +a:b a:b:c fullmatch +a:b a:b match +a:b a:bc match +a:b xa:b match +a:b xa:by search +a:b xaby search +[a-z]+:[0-9]+ foo:42 fullmatch +[a-z]+:[0-9]+ foo42 fullmatch +[a-z]+:[0-9]+ foo:42 match +[a-z]+:[0-9]+ foo:42x match +[a-z]+:[0-9]+ foo:42 search +[a-z]+:[0-9]+ xfoo:42y search +(a:b)+ a:b fullmatch +(a:b)+ a:ba:b fullmatch +(a:b)+ a:ba: fullmatch +(a:b)+ a:b match +(a:b)+ a:bx match +^[a-z]+:[0-9]+$ foo:42 fullmatch +^[a-z]+:[0-9]+$ foo:42 match +^[a-z]+:[0-9]+$ foo:42x match +^[a-z]+:[0-9]+$ foo:42 search +^[a-z]+:[0-9]+$ xfoo:42 search +a\.b a.b fullmatch +a\.b axb fullmatch +a\.b a.b match +a\.b a.bc match +a\.b a.b search +a\.b xaxbx search +a\+b a+b fullmatch +a\+b ab fullmatch +a\+b a+b match +a\+b a+bc match +a\*b a*b fullmatch +a\*b aab fullmatch +a\*b a*b match +a\?b a?b fullmatch +a\?b ab fullmatch +a\?b a?b match +a\(b\) a(b) fullmatch +a\(b\) ab fullmatch +a\(b\) a(b) match +a\[b\] a[b] fullmatch +a\[b\] ab fullmatch +a\[b\] a[b] match +a\\b a\b fullmatch +a\\b ab fullmatch +a\\b a\b match +a\\b a\bc match +a\\b xa\by search +a\\b xaby search +[\.-z]+ abc fullmatch +[\.-z]+ ABC fullmatch +[\.-z]+ - fullmatch +[\.-z]+ . fullmatch +[\.-z]+ abc search +\w+:\d+\.\d+ foo:3.14 fullmatch +\w+:\d+\.\d+ foo:3x14 fullmatch +\w+:\d+\.\d+ foo:3.14 match +\w+:\d+\.\d+ foo:3.14x match +\w+:\d+\.\d+ xfoo:3.14y search +\w+:\d+\.\d+ xfoo:3x14y search +x{100,2} x fullmatch +(abc abc fullmatch +a** a fullmatch +a(?=b) ab match +a(?!b) ac match +(?<=a)b ab match +(?a) a fullmatch +(?Pa) b fullmatch +(?Pa)(?Pb) ab fullmatch +(?i)hello HELLO fullmatch +(?i)hello Hello fullmatch +(?i)hello world fullmatch +(?i)[a-z]+ ABC fullmatch +(?s)a.b axb fullmatch +(?m)^a a search +(a)\1 aa fullmatch +(a)\1 ab fullmatch +(a|b)\1 aa fullmatch +(a|b)\1 bb fullmatch +(a|b)\1 ab fullmatch +(.)\1 aa fullmatch +(.)\1 ab fullmatch diff --git a/StrataPythonTest/Regex/diff_test.py b/StrataPythonTest/Regex/diff_test.py deleted file mode 100644 index 0b5f3b4..0000000 --- a/StrataPythonTest/Regex/diff_test.py +++ /dev/null @@ -1,975 +0,0 @@ -#!/usr/bin/env python3 -""" -Differential testing: Python re module vs Strata SMT-based regex checker. - -Usage: - python diff_test.py [--lake-exe ] - -For each test case in the corpus, runs the regex+string pair through both -Python's re module and Strata's DiffTestCore tool, then reports discrepancies -according to the agreement logic. - -Agreement logic: - agree Python match + Strata match - Python noMatch + Strata noMatch - Python error + Strata parseError (patternError or unimplemented) - - bug Python match + Strata noMatch (false negative) - Python noMatch + Strata match (false positive) - Python error + Strata match/noMatch (Strata accepts invalid regex) - Python match/noMatch + Strata parseError:patternError - (Strata rejects valid regex) - - known_gap Python match/noMatch + Strata parseError:unimplemented - (feature not yet supported) - - investigate Strata smtError, or any other combination -""" - -import re -import subprocess -import sys -import os -import argparse - -# ── Test corpus ──────────────────────────────────────────────────────────────── -# Each entry is (python_regex, test_string, mode). -# mode is one of: "match", "fullmatch", "search". -# Every comment ends with the Python ground-truth answer: # match / # noMatch / # error. - -CORPUS = [ - - # ── Literals ──────────────────────────────────────────────────────────────── - - ("a", "a", "fullmatch"), # match - ("a", "b", "fullmatch"), # noMatch - ("ab", "ab", "fullmatch"), # match - ("ab", "a", "fullmatch"), # noMatch — too short - ("ab", "abc", "fullmatch"), # noMatch — too long - - # match mode: anchored at start, trailing content allowed - ("a", "abc", "match"), # match - ("a", "bcd", "match"), # noMatch — doesn't start with a - ("ab", "abc", "match"), # match - ("ab", "bcd", "match"), # noMatch - - # ── Character atoms ───────────────────────────────────────────────────────── - - # Dot (anychar): matches exactly one character - (".", "a", "fullmatch"), # match - (".", "", "fullmatch"), # noMatch — needs exactly one char - (".", "ab", "fullmatch"), # noMatch — two chars - (".+", "abc", "fullmatch"), # match - - # Character ranges - ("[a-z]", "a", "fullmatch"), # match - ("[a-z]", "z", "fullmatch"), # match - ("[a-z]", "A", "fullmatch"), # noMatch — uppercase - ("[abc]", "b", "fullmatch"), # match - ("[abc]", "d", "fullmatch"), # noMatch - ("[a-z]+", "hello", "fullmatch"), # match - ("[a-z]+", "Hello", "fullmatch"), # noMatch — H is uppercase - - # Negated classes [^...]: complement intersected with allchar - ("[^a-z]", "A", "fullmatch"), # match - ("[^a-z]", "a", "fullmatch"), # noMatch - (r"[^b]", "a", "fullmatch"), # match - (r"[^b]", "b", "fullmatch"), # noMatch - (r"[^A-Z]+","hello", "fullmatch"), # match - (r"[^A-Z]+","Hello", "fullmatch"), # noMatch — H is uppercase - # Complement must be single-char, not multi-char or empty - (r"[^a]", "", "fullmatch"), # noMatch — must be exactly 1 char - (r"[^a]", "bc", "fullmatch"), # noMatch — 2 chars, not 1 - (r"[^a]", "bb", "fullmatch"), # noMatch — 2 chars - (r"[^b]+", "", "fullmatch"), # noMatch — below min (1) - - # ── Quantifiers ───────────────────────────────────────────────────────────── - - # * (star): zero or more - ("a*", "", "fullmatch"), # match - ("a*", "aaa", "fullmatch"), # match - ("a*", "b", "fullmatch"), # noMatch - - # + (plus = concat r (star r)): one or more - ("a+", "", "fullmatch"), # noMatch - ("a+", "a", "fullmatch"), # match - ("a+", "aaa", "fullmatch"), # match - - # deeply nested plus — a few cases to verify recursion depth, not re-testing a+ semantics - ("((((((a+)+)+)+)+)+)+", "a", "fullmatch"), # match - ("((((((a+)+)+)+)+)+)+", "b", "fullmatch"), # noMatch - ("((((((a+)+)+)+)+)+)+", "aab", "match"), # match — trailing b ok - ("((((((a+)+)+)+)+)+)+", "bab", "search"), # match — found in middle - - # (a+)* — plus inside star: equivalent to a* - ("(a+)*", "", "fullmatch"), # match — zero groups - ("(a+)*", "a", "fullmatch"), # match - ("(a+)*", "aaa", "fullmatch"), # match - ("(a+)*", "b", "fullmatch"), # noMatch - ("(a+)*", "ab", "match"), # match — trailing b ok - ("(a+)*", "bab", "search"), # match — found in middle - - # (a*)+ — star inside plus: equivalent to a* - ("(a*)+", "", "fullmatch"), # match — one empty group - ("(a*)+", "a", "fullmatch"), # match - ("(a*)+", "aaa", "fullmatch"), # match - ("(a*)+", "b", "fullmatch"), # noMatch - ("(a*)+", "ab", "match"), # match — trailing b ok - ("(a*)+", "bab", "search"), # match — found in middle - - # (a+b+)+ — concat of pluses inside plus - ("(a+b+)+", "", "fullmatch"), # noMatch - ("(a+b+)+", "ab", "fullmatch"), # match - ("(a+b+)+", "aabb", "fullmatch"), # match — two chars each - ("(a+b+)+", "abab", "fullmatch"), # match — two groups - ("(a+b+)+", "a", "fullmatch"), # noMatch — no b - ("(a+b+)+", "ba", "fullmatch"), # noMatch — wrong order - ("(a+b+)+", "abx", "match"), # match — trailing x ok - ("(a+b+)+", "xab", "search"), # match — found after x - - # (a+|b+)+ — alternation of pluses inside plus - ("(a+|b+)+", "", "fullmatch"), # noMatch - ("(a+|b+)+", "a", "fullmatch"), # match - ("(a+|b+)+", "b", "fullmatch"), # match - ("(a+|b+)+", "aabb", "fullmatch"), # match — aa then bb - ("(a+|b+)+", "abba", "fullmatch"), # match — a, bb, a - ("(a+|b+)+", "c", "fullmatch"), # noMatch - ("(a+|b+)+", "ac", "match"), # match — trailing c ok - ("(a+|b+)+", "cab", "search"), # match — found after c - - # ? (optional = union empty r): zero or one - ("a?", "", "fullmatch"), # match - ("a?", "a", "fullmatch"), # match - ("a?", "aa", "fullmatch"), # noMatch - - # {n,m} and exact {n} - ("a{2,4}", "a", "fullmatch"), # noMatch — too few - ("a{2,4}", "aa", "fullmatch"), # match - ("a{2,4}", "aaaa", "fullmatch"), # match - ("a{2,4}", "aaaaa", "fullmatch"), # noMatch — too many - ("a{3}", "aaa", "fullmatch"), # match - ("a{3}", "aa", "fullmatch"), # noMatch - - # Zero and exact counts - ("a{0}", "", "fullmatch"), # match — 0 reps = empty string - ("a{0}", "a", "fullmatch"), # noMatch - ("a{1}", "a", "fullmatch"), # match - ("a{1}", "aa", "fullmatch"), # noMatch - ("a{0,1}", "", "fullmatch"), # match — same language as a? - ("a{0,1}", "a", "fullmatch"), # match - ("a{0,1}", "aa", "fullmatch"), # noMatch - - # Group loops - ("(ab){2}", "abab", "fullmatch"), # match - ("(ab){2}", "ab", "fullmatch"), # noMatch — too few - ("(ab){2}", "ababab", "fullmatch"), # noMatch — too many - ("(ab){2,3}", "abab", "fullmatch"), # match — 2 reps - ("(ab){2,3}", "ababab", "fullmatch"), # match — 3 reps - ("(ab){2,3}", "ab", "fullmatch"), # noMatch — 1 rep - ("(ab){2,3}", "abababab","fullmatch"), # noMatch — 4 reps - - # Multi-char class with loop: ok_chars-style identifier check - (r"[a-z0-9.\-]{1,10}", "test-str-1", "fullmatch"), # match - (r"[a-z0-9.\-]{1,10}", "test-str!", "fullmatch"), # noMatch — ! not in class - (r"[a-z0-9.\-]{1,10}", "", "fullmatch"), # noMatch — below min - (r"[a-z0-9.\-]{1,10}", "0123456789a", "fullmatch"), # noMatch — 11 chars, over limit - - # Loops in search mode - ("a{2}", "xaax", "search"), # match — aa found in middle - ("a{2}", "xa", "search"), # noMatch — only one a - ("(ab){2}", "xababx", "search"), # match - ("(ab){2}", "xabx", "search"), # noMatch — only one ab - - # Anchored loops: ^ and $ alongside {n,m} - ("^a{3}$", "aaa", "fullmatch"), # match - ("^a{3}$", "aa", "fullmatch"), # noMatch - ("^a{3}$", "aaaa", "fullmatch"), # noMatch - ("^a{2,4}$", "a", "fullmatch"), # noMatch - ("^a{2,4}$", "aa", "fullmatch"), # match - ("^a{2,4}$", "aaaa", "fullmatch"), # match - ("^a{2,4}$", "aaaaa", "fullmatch"), # noMatch - ("^a{3}$", "aaa", "match"), # match — $ blocks trailing content - ("^a{3}$", "aaab", "match"), # noMatch — $ blocks trailing b - ("a{3}", "aaab", "match"), # match — no $, trailing b allowed - - # ── Alternation ───────────────────────────────────────────────────────────── - - ("a|b", "a", "fullmatch"), # match - ("a|b", "b", "fullmatch"), # match - ("a|b", "c", "fullmatch"), # noMatch - ("a|b|c", "c", "fullmatch"), # match - ("a|b|c", "d", "fullmatch"), # noMatch - - # ── Groups ────────────────────────────────────────────────────────────────── - - ("(ab)+", "ab", "fullmatch"), # match - ("(ab)+", "abab", "fullmatch"), # match - ("(ab)+", "aba", "fullmatch"), # noMatch - ("(a|b)+", "abba", "fullmatch"), # match - ("(a|b)+", "abbc", "fullmatch"), # noMatch — c not in [ab] - - # ── Anchors: basic behavior ────────────────────────────────────────────────── - - # fullmatch: ^ and $ are effectively redundant (whole string must match anyway) - ("^a", "a", "fullmatch"), # match - ("^a", "ba", "fullmatch"), # noMatch - ("a$", "a", "fullmatch"), # match - ("a$", "ab", "fullmatch"), # noMatch - ("^a$", "a", "fullmatch"), # match - ("^a$", "ab", "fullmatch"), # noMatch - ("^a$", "ba", "fullmatch"), # noMatch - - # match mode: ^ is a no-op (match already anchors at start); $ cuts off trailing content - ("^a", "a", "match"), # match - ("^a", "ab", "match"), # match — trailing b allowed - ("^a", "ba", "match"), # noMatch - ("^a$", "a", "match"), # match - ("^a$", "ab", "match"), # noMatch — $ blocks trailing b - - # ^$ matches only the empty string, across all modes - ("^$", "", "fullmatch"), # match - ("^$", "a", "fullmatch"), # noMatch - ("^$", "", "match"), # match - ("^$", "a", "match"), # noMatch - ("^$", "", "search"), # match - ("^$", "a", "search"), # noMatch - - # Empty pattern: same language as ^$ - ("", "", "fullmatch"), # match - ("", "a", "fullmatch"), # noMatch - - # search mode basics - ("a", "xax", "search"), # match - ("a", "xyz", "search"), # noMatch - ("^a$", "a", "search"), # match - ("^a$", "xa", "search"), # noMatch - ("^a$", "ax", "search"), # noMatch - - # ^ in search: prevents a free prefix - ("^a", "abc", "search"), # match - ("^a", "xabc", "search"), # noMatch - ("^a", "a", "search"), # match - - # $ in search: prevents a free suffix - ("a$", "ba", "search"), # match - ("a$", "ab", "search"), # noMatch - ("a$", "xyzba", "search"), # match - ("a$", "xyzbax","search"), # noMatch — a is not at end - - # Alternation with anchors across all modes - ("^a|b$", "a", "fullmatch"), # match — ^a covers "a" - ("^a|b$", "b", "fullmatch"), # match — b$ covers "b" - ("^a|b$", "ab", "fullmatch"), # noMatch — neither "a" nor "b" alone - ("^a|b$", "a", "match"), # match - ("^a|b$", "b", "match"), # match - ("^a|b$", "ab", "match"), # match — ^a fires, b is trailing - ("^a|b$", "xb", "match"), # noMatch - ("^a|b$", "axyz", "search"), # match — ^a fires - ("^a|b$", "xyzb", "search"), # match — b$ fires - ("^a|b$", "xyzc", "search"), # noMatch - ("^a|b$", "axyzb", "search"), # match — ^a fires at start - - # Group with both anchors, across all modes - ("^(a|b)$", "a", "fullmatch"), # match - ("^(a|b)$", "b", "fullmatch"), # match - ("^(a|b)$", "ab", "fullmatch"), # noMatch - ("^(a|b)$", "a", "match"), # match - ("^(a|b)$", "b", "match"), # match - ("^(a|b)$", "ab", "match"), # noMatch — $ prevents trailing b - ("^(a|b)$", "a", "search"), # match - ("^(a|b)$", "ab", "search"), # noMatch - - # Anchors inside groups / alternation - ("(^a$)|(^b$)", "a", "fullmatch"), # match - ("(^a$)|(^b$)", "b", "fullmatch"), # match - ("(^a$)|(^b$)", "c", "fullmatch"), # noMatch - ("^a$|^$b", "a", "fullmatch"), # match — first branch covers "a" - ("^a$|^$b", "", "fullmatch"), # noMatch — ^$b: ^, $, then b — unmatchable - - # ── Anchors: $ followed by non-consuming suffix (concat | true, false => branch) ── - # - # When r1 always consumes and r2 may be empty, $ in r1 can still fire if - # r2 = "". Strata splits into: Case 1 (r2 = "", $ fires) | Case 2 (r2 ≠ ""). - - # a$.*: a (always-consuming) followed by .* (non-consuming) - ("a$.*", "a", "fullmatch"), # match — $ fires, .* = "" - ("a$.*", "ab", "fullmatch"), # noMatch — b after a blocks $ - ("a$.*", "a", "match"), # match - ("a$.*", "ab", "match"), # noMatch - ("a$.*", "ba", "search"), # match — a at end, $ fires - ("a$.*", "ab", "search"), # noMatch - - # $ followed by b* or b?: b*/b? can match "", so $ can still fire - ("a$b*", "a", "fullmatch"), # match - ("a$b*", "ab", "fullmatch"), # noMatch - ("a$b?", "a", "fullmatch"), # match - ("a$b?", "ab", "fullmatch"), # noMatch - - # $ followed by always-consuming suffix: $ is forced unmatchable (concat | true,true =>) - ("a$.+", "a", "match"), # noMatch — .+ needs ≥1 char after $ - ("a$.+", "ab", "match"), # noMatch - ("a$b+", "a", "fullmatch"), # noMatch - ("a$b+", "ab", "fullmatch"), # noMatch - - # Double $: second is redundant - ("a$$", "a", "match"), # match - ("a$$", "ab", "match"), # noMatch - - # $ in match mode: terminates the match, no trailing content allowed - ("a$", "a", "match"), # match - ("a$", "ab", "match"), # noMatch — b follows $ - ("a$", "ba", "match"), # noMatch — match anchors at start - ("a$", "aab", "match"), # noMatch - - # a.*$ in match mode: .* followed by $ - ("a.*$", "axyz", "match"), # match - ("a.*$", "a", "match"), # match — .* = "", $ fires - ("a.*$", "b", "match"), # noMatch - - # a.*b in match mode: must start with a and reach b; trailing content allowed - ("a.*b", "axyzb","match"), # match - ("a.*b", "ab", "match"), # match - ("a.*b", "axyz", "match"), # noMatch — never reaches b - ("a.*b", "baxyzb","match"), # noMatch — doesn't start with a - - # Multi-char consuming prefix before $ - ("ab$.*", "ab", "fullmatch"), # match - ("ab$.*", "abc", "fullmatch"), # noMatch — c after $ blocked - ("ab$.*", "ab", "match"), # match - ("ab$.*", "abc", "match"), # noMatch - ("ab$.*", "xab", "search"), # match — ab at end - ("ab$.*", "xabc", "search"), # noMatch - - # Range prefix before $ - ("[a-z]$.*", "a", "fullmatch"), # match - ("[a-z]$.*", "ab", "fullmatch"), # noMatch - ("[a-z]$.*", "xa", "search"), # match — lowercase at end - ("[a-z]$.*", "xa1", "search"), # noMatch — digit at end, not in [a-z] - - # Group prefix before $ - ("(ab)$.*", "ab", "fullmatch"), # match - ("(ab)$.*", "abc", "fullmatch"), # noMatch - ("(ab)$.*", "ab", "match"), # match - - # ── Anchors: ^ preceded by non-consuming content (concat | false, true => branch) ─ - # - # When r1 may be empty and r2 always consumes with ^, Strata splits into: - # Case 1 (r1 = "", ^ fires at original position) | Case 2 (r1 ≠ "", ^ blocked). - - # .*^a: .* may be empty, so ^ can still fire at position 0 - (".*^a", "a", "match"), # match — .* = "", ^ fires, a matches - (".*^a", "ab", "match"), # match — .* = "", ^ fires, trailing b ok - (".*^a", "ba", "match"), # noMatch — no way to make .* empty AND ^ fire at a - - # .*^a in search: dotStar wrapper means ^ must still fire at position 0 - (".*^a", "a", "search"), # match - (".*^a", "ba", "search"), # noMatch - (".*^a", "xa", "search"), # noMatch - - # a?(^b): a? non-consuming with content, (^b) always-consuming with ^ - ("a?(^b)", "b", "fullmatch"), # match — a? = "", ^ fires, b matches - ("a?(^b)", "ab", "fullmatch"), # noMatch — a? = "a" → ^ past start; a? = "" → b ≠ a - ("a?(^b)", "b", "match"), # match - ("a?(^b)", "ba", "match"), # match — a? = "", ^ fires, b matches, trailing a ok - ("a?(^b)", "ab", "match"), # noMatch - - # a?(^b) in search: core_ft/core_ff have atStart=false; ^ must not fire mid-string - ("a?(^b)", "b", "search"), # match — pos 0: a?="", ^ fires, b matches - ("a?(^b)", "xb", "search"), # noMatch - ("a?(^b)", "ab", "search"), # noMatch - ("a?(^b)", "xab", "search"), # noMatch - ("a?(^b)", "ba", "search"), # match — pos 0: a?="", ^ fires, b matches - ("a?(^b)", "bx", "search"), # match — pos 0: a?="", ^ fires, b matches - - # ^?(^b) in search: r1=^? has no non-anchor content → split doesn't fire → simple path. - # The fix (passing atStart instead of true to r2) matters here: with atStart=false in - # core_ft/core_ff, ^ in r2 must be blocked even though the split condition was not met. - ("^?(^b)", "b", "search"), # match — pos 0: ^?="", ^ fires, b matches - ("^?(^b)", "xb", "search"), # noMatch — ^ can only fire at pos 0; b≠x - ("^?(^b)", "ab", "search"), # noMatch - - # ── Anchors: concat(false, false) — both sides may be empty ───────────────── - # - # When both sides may be empty and r2 contains ^, Strata splits into: - # Case 1 (r1 = "", ^ fires) | Case 2 (r1 ≠ "", ^ blocked). - - # a?^b: parses as concat(concat(a?,^),b); inner false,false; ^ fires only when a? = "" - ("a?^b", "b", "fullmatch"), # match — a? = "", ^ fires, b matches - ("a?^b", "a", "fullmatch"), # noMatch — a? = "" → b ≠ a; a? = "a" → ^ past start - ("a?^b", "ab", "fullmatch"), # noMatch - ("a?^b", "b", "match"), # match - ("a?^b", "ba", "match"), # match — a? = "", ^ fires, trailing a ok - ("a?^b", "ab", "match"), # noMatch - - # a?^b?: outer concat(a?, concat(^,b?)) — false,false with ^ in r2 and content in r1 - ("a?^b?", "", "fullmatch"), # match — a? = "", ^ fires, b? = "" - ("a?^b?", "b", "fullmatch"), # match — a? = "", ^ fires, b? = "b" - ("a?^b?", "a", "fullmatch"), # noMatch — a? = "a" → ^ past start; a? = "" → b? ≠ a - ("a?^b?", "ab", "fullmatch"), # noMatch - ("a?^b?", "", "match"), # match - ("a?^b?", "b", "match"), # match - ("a?^b?", "a", "match"), # match — a? = "", ^ fires, b? = "", trailing a ok - - # $ in the middle with always-consuming suffix: unmatchable - ("a$b", "ab", "match"), # noMatch - - # ── Anchors: inside quantified expressions ─────────────────────────────────── - # - # For star/loop, Strata splits the iterations into first (atStart), middle - # (false,false), and last (atEnd) when the inner regex is always-consuming - # or contains an anchor. - - # (^a)*: ^ only fires for the first iteration; subsequent iterations get atStart=false - ("(^a)*", "", "fullmatch"), # match — 0 iterations - ("(^a)*", "a", "fullmatch"), # match — 1 iteration: ^ at 0 - ("(^a)*", "aa", "fullmatch"), # noMatch — 2nd ^ fails at pos 1 - ("(^a)*", "a", "match"), # match — 1 iteration, trailing content allowed - ("(^a)*", "aa", "match"), # match — 1 iteration enough, trailing a allowed - - # (a$)*: $ only fires for the last iteration; earlier iterations get atEnd=false - ("(a$)*", "", "fullmatch"), # match — 0 iterations - ("(a$)*", "a", "fullmatch"), # match — 1 iteration: $ at end - ("(a$)*", "aa", "fullmatch"), # noMatch — $ after 1st a blocked by 2nd a - ("(a$)*", "a", "match"), # match - ("(a$)*", "ab", "match"), # match — 0 iterations match "" at position 0 - - # (^a$)*: both anchors — only 1 iteration possible - ("(^a$)*", "", "fullmatch"), # match — 0 iterations - ("(^a$)*", "a", "fullmatch"), # match — 1 iteration - ("(^a$)*", "aa", "fullmatch"), # noMatch — 2 iterations impossible - - # Anchor inside loop: repeated iteration blocked - ("(^a){2}", "aa", "fullmatch"), # noMatch — 2nd ^ is past start - ("(^a){2}", "a", "fullmatch"), # noMatch - ("(a$){2}", "aa", "fullmatch"), # noMatch — $ after 1st a blocks 2nd iteration - ("(a$){2}", "a", "fullmatch"), # noMatch - - # (^a){0,2}: loop(0,m) with always-consuming anchored inner — first/middle/last split - ("(^a){0,2}", "", "fullmatch"), # match — 0 reps - ("(^a){0,2}", "a", "fullmatch"), # match — 1 rep: ^ at 0 - ("(^a){0,2}", "aa", "fullmatch"), # noMatch — 2nd ^ fails at pos 1 - - # (a$){0,2}: loop(0,m) with always-consuming anchored inner - ("(a$){0,2}", "", "fullmatch"), # match — 0 reps - ("(a$){0,2}", "a", "fullmatch"), # match — 1 rep: $ at end - ("(a$){0,2}", "aa", "fullmatch"), # noMatch — $ blocked - - # {n,m} with n≥1: recursed via concat; anchor handling falls to concat cases - ("(^a){1,2}", "a", "fullmatch"), # match — 1 rep: ^ at 0 - ("(^a){1,2}", "aa", "fullmatch"), # noMatch — 2nd ^ fails at pos 1 - ("(a$){1,2}", "a", "fullmatch"), # match — 1 rep: $ at end - ("(a$){1,2}", "aa", "fullmatch"), # noMatch — $ blocked - - # star with non-consuming inner — simple path (no anchor split needed) - ("(a?)*", "", "fullmatch"), # match - ("(a?)*", "a", "fullmatch"), # match - ("(a?)*", "aaa", "fullmatch"), # match - - # star with anchored non-consuming inner — split still required - ("(^a?)*", "", "fullmatch"), # match — 0 iterations - ("(^a?)*", "a", "fullmatch"), # match — 1 iter: ^ fires, a? = "a" - ("(^a?)*", "aa", "fullmatch"), # noMatch — ^ fails at pos 1 - ("(a?$)*", "", "fullmatch"), # match — 0 iterations - ("(a?$)*", "a", "fullmatch"), # match — 1 iter: a? = "a", $ at end - ("(a?$)*", "aa", "fullmatch"), # noMatch — $ after 1st a blocked - - # loop(0,m) with non-consuming inner — simple path - ("(a?){0,2}", "", "fullmatch"), # match - ("(a?){0,2}", "a", "fullmatch"), # match - ("(a?){0,2}", "aa", "fullmatch"), # match - ("(a?){0,2}", "aaa", "fullmatch"), # noMatch — exceeds max - - # loop(0,m) with anchored non-consuming inner — split required - ("(^a?){0,2}", "", "fullmatch"), # match — 0 reps - ("(^a?){0,2}", "a", "fullmatch"), # match — 1 rep: ^ fires, a? = "a" - ("(^a?){0,2}", "aa", "fullmatch"), # noMatch — ^ fails at pos 1 - ("(a?$){0,2}", "", "fullmatch"), # match — 0 reps - ("(a?$){0,2}", "a", "fullmatch"), # match — 1 rep: a? = "a", $ at end - ("(a?$){0,2}", "aa", "fullmatch"), # noMatch — $ blocked - - # ── Anchors: unusual / unmatchable positions ───────────────────────────────── - - # ^ after an always-consuming prefix: ^ is past the start - ("x(^a)", "xa", "fullmatch"), # noMatch — ^ after x: past start - ("x(^a)", "a", "fullmatch"), # noMatch - ("x(^a|b)", "xb", "fullmatch"), # match — ^a fails, b branch works - ("x(^a|b)", "xa", "fullmatch"), # noMatch — ^a fails, b ≠ a - - # $ blocked by following content - ("(a$)b", "ab", "fullmatch"), # noMatch — $ before b is unmatchable - ("(a$)(b)", "ab", "fullmatch"), # noMatch - ("(a$)b", "ab", "match"), # noMatch - - # Alternation where one branch has a context-killed anchor - ("(a$|b)c", "ac", "fullmatch"), # noMatch — a$ then c: $ blocked; b ≠ a - ("(a$|b)c", "bc", "fullmatch"), # match — b branch works - ("(a$|b)c", "abc", "fullmatch"), # noMatch - ("(a|b$)c", "ac", "fullmatch"), # match — a branch works - ("(a|b$)c", "bc", "fullmatch"), # noMatch — b$c: $ before c → unmatchable - - # Two anchors that cannot both fire - ("(^a)(^b)", "ab", "fullmatch"), # noMatch — 2nd ^ is past start - ("(^a)(^b)", "a", "fullmatch"), # noMatch - ("(a$)(b$)", "ab", "fullmatch"), # noMatch — 1st $ requires end but b follows - ("(a$)(b$)", "a", "fullmatch"), # noMatch - - # ^ or $ at a position where it can't fire cleanly - ("(^|$)c", "c", "fullmatch"), # match — ^ fires → "c" matches - ("(^|$)c", "xc", "fullmatch"), # noMatch — neither fires - ("a(^|$)b", "ab", "fullmatch"), # noMatch — after a: ^ past start, $ blocked by b - - # Anchors blocked by surrounding always-consuming chars - ("c(^a|b$)d", "cad", "fullmatch"), # noMatch - ("c(^a|b$)d", "cbd", "fullmatch"), # noMatch - ("c(^a|b$)d", "ccd", "fullmatch"), # noMatch - ("(^a|b$)(^c|d$)", "ac", "fullmatch"), # noMatch - ("(^a|b$)(^c|d$)", "bd", "fullmatch"), # noMatch - ("(^a|b$)(^c|d$)", "bc", "fullmatch"), # noMatch - - # Search mode: anchor inside group restricts positional freedom - ("(^a)(b)", "ab", "search"), # match — ^a forces start - ("(^a)(b)", "xab", "search"), # noMatch — ^ blocks - ("(a)(b$)", "ab", "search"), # match — b$ forces end - ("(a)(b$)", "abx", "search"), # noMatch — $ blocked by x - ("(^a)(b$)", "ab", "search"), # match — both anchors: exactly "ab" - ("(^a)(b$)", "xab", "search"), # noMatch — ^ blocks - ("(^a)(b$)", "abx", "search"), # noMatch — $ blocks - - # Match mode: $ inside group cuts off trailing content - ("(a$|b)c", "bc", "match"), # match - ("(a$|b)c", "bcd", "match"), # match — trailing d allowed - - # ── $ in (false,false) concat — atEnd case-split ──────────────────────────── - # - # a?$b?: both sides may be empty. $ in r1 should only fire when r2="". - # Without the atEnd split, $ fires even when b? matches non-empty. - # The split fires at the inner concat($, b?) level. - - ("a?$b?", "", "fullmatch"), # match — a?="", $ fires, b?="" - ("a?$b?", "a", "fullmatch"), # match — a?="a", $ fires, b?="" - ("a?$b?", "b", "fullmatch"), # noMatch — $ at pos 0 but string non-empty; no valid split - ("a?$b?", "ab", "fullmatch"), # noMatch — $ can't fire: b? non-empty after $ - ("a?$b?", "", "match"), # match - ("a?$b?", "a", "match"), # match - ("a?$b?", "b", "match"), # noMatch - ("a?$b?", "ab", "match"), # noMatch — $ can't fire with b? non-empty - ("a?$b?", "a", "search"), # match — pos 1: a?="", $ fires at end, b?="" - ("a?$b?", "b", "search"), # match — pos 1: a?="", $ fires at end, b?="" - ("a?$b?", "xb", "search"), # match — pos 2: $ fires at end of string - ("a?$b?", "ab", "search"), # match — pos 2: $ fires at end of string - - # (a?$)b?: semantically identical to a?$b? but the $-split fires at the outer - # concat level (r1=group(a?$) contains $, r2=b? has non-anchor content), exercising - # the false,false $-split path at a different point in the tree. - ("(a?$)b?", "", "fullmatch"), # match — group matches "", $ fires, b?="" - ("(a?$)b?", "a", "fullmatch"), # match — group matches "a", $ fires, b?="" - ("(a?$)b?", "ab", "fullmatch"), # noMatch — $ blocked by non-empty b? - ("(a?$)b?", "b", "fullmatch"), # noMatch — group can't match at end with "b" remaining - - # ── Multi-char literals and patterns ───────────────────────────────────────── - - # Basic multi-char literals - ("abc", "abc", "fullmatch"), # match - ("abc", "ab", "fullmatch"), # noMatch — too short - ("abc", "abcd", "fullmatch"), # noMatch — too long - ("abc", "ABC", "fullmatch"), # noMatch — case mismatch - ("abc", "abc", "match"), # match - ("abc", "abcd", "match"), # match — trailing d allowed - ("abc", "xabc", "match"), # noMatch — doesn't start with a - ("abc", "xabc", "search"), # match — found in middle - ("abc", "xabcx", "search"), # match - ("abc", "xabx", "search"), # noMatch — no abc substring - - # Multi-char alternation - ("abc|def", "abc", "fullmatch"), # match - ("abc|def", "def", "fullmatch"), # match - ("abc|def", "abcdef", "fullmatch"), # noMatch — too long - ("abc|def", "abd", "fullmatch"), # noMatch - ("abc|def", "xdef", "search"), # match - ("abc|def", "xabx", "search"), # noMatch - - # Multi-char groups with quantifiers - ("(abc)+", "abc", "fullmatch"), # match - ("(abc)+", "abcabc", "fullmatch"), # match - ("(abc)+", "abcab", "fullmatch"), # noMatch — incomplete last rep - ("(abc){2}", "abcabc", "fullmatch"), # match - ("(abc){2}", "abc", "fullmatch"), # noMatch — only 1 rep - ("(abc){2}", "abcabcabc", "fullmatch"), # noMatch — 3 reps - ("(abc){1,3}", "abc", "fullmatch"), # match — 1 rep - ("(abc){1,3}", "abcabcabc", "fullmatch"), # match — 3 reps - ("(abc){1,3}", "abcabcabcabc", "fullmatch"), # noMatch — 4 reps - - # Multi-char alternation inside groups - ("(ab|cd)+", "abcd", "fullmatch"), # match — ab then cd - ("(ab|cd)+", "cdab", "fullmatch"), # match — cd then ab - ("(ab|cd)+", "abce", "fullmatch"), # noMatch — ce not in group - ("(ab|cd)+", "xabcdy", "search"), # match - ("(ab|cd)+", "xacx", "search"), # noMatch - - # Multi-char character class sequences - ("[a-z][0-9]", "a1", "fullmatch"), # match - ("[a-z][0-9]", "a12", "fullmatch"), # noMatch — too long - ("[a-z][0-9]", "11", "fullmatch"), # noMatch — first char not [a-z] - ("[a-z][0-9]+", "a123", "fullmatch"), # match - ("[a-z][0-9]+", "a", "fullmatch"), # noMatch — no digit - ("[a-z]{2}[0-9]{2}", "ab12", "fullmatch"), # match - ("[a-z]{2}[0-9]{2}", "a12", "fullmatch"), # noMatch — only 1 letter - ("[a-z]{2}[0-9]{2}", "ab1", "fullmatch"), # noMatch — only 1 digit - ("[a-z]{2}[0-9]{2}", "xab12y", "search"), # match - ("[a-z]{2}[0-9]{2}", "xab1y", "search"), # noMatch - - # Multi-char patterns with anchors - ("^abc$", "abc", "fullmatch"), # match - ("^abc$", "xabc", "fullmatch"), # noMatch - ("^abc$", "abcx", "fullmatch"), # noMatch - ("^abc", "abcxyz", "search"), # match — ^ forces start - ("^abc", "xabc", "search"), # noMatch — ^ blocks - ("abc$", "xyzabc", "search"), # match — $ forces end - ("abc$", "abcx", "search"), # noMatch — $ blocked by x - ("^abc$", "abc", "search"), # match — both anchors: exactly "abc" - ("^abc$", "xabc", "search"), # noMatch - ("^abc$", "abcx", "search"), # noMatch - - # Multi-char with .* wildcard - ("abc.*def", "abcdef", "fullmatch"), # match — .* = "" - ("abc.*def", "abcXXdef", "fullmatch"), # match — .* = "XX" - ("abc.*def", "abcdef", "search"), # match - ("abc.*def", "xabcXXdefy","search"), # match - ("abc.*def", "abcXXdeg", "fullmatch"), # noMatch — ends with g not f - ("abc.+def", "abcdef", "fullmatch"), # noMatch — .+ needs ≥1 char between - ("abc.+def", "abcXdef", "fullmatch"), # match - - # Multi-char search: overlapping candidates - ("ab", "ababab", "search"), # match — first ab at pos 0 - ("ab", "bbbabb", "search"), # match — ab at pos 3 - ("ab", "aabb", "search"), # match — ab at pos 1 - ("ab", "ba", "search"), # noMatch — no ab substring - ("abc", "aabbc", "search"), # noMatch — no abc substring - ("abc", "aabcbc", "search"), # match — abc at pos 1 - - # ── Special characters: colon, backslash, and escaped metacharacters ───────── - - # Literal colon - ("a:b", "a:b", "fullmatch"), # match - ("a:b", "ab", "fullmatch"), # noMatch — missing colon - ("a:b", "a:b:c", "fullmatch"), # noMatch — too long - ("a:b", "a:b", "match"), # match - ("a:b", "a:bc", "match"), # match — trailing c allowed - ("a:b", "xa:b", "match"), # noMatch — doesn't start with a - ("a:b", "xa:by", "search"), # match - ("a:b", "xaby", "search"), # noMatch - ("[a-z]+:[0-9]+", "foo:42", "fullmatch"), # match - ("[a-z]+:[0-9]+", "foo42", "fullmatch"), # noMatch — no colon - ("[a-z]+:[0-9]+", "foo:42", "match"), # match - ("[a-z]+:[0-9]+", "foo:42x", "match"), # match — trailing x allowed - ("[a-z]+:[0-9]+", "foo:42", "search"), # match - ("[a-z]+:[0-9]+", "xfoo:42y","search"), # match - ("(a:b)+", "a:b", "fullmatch"), # match — 1 rep - ("(a:b)+", "a:ba:b", "fullmatch"), # match — 2 reps - ("(a:b)+", "a:ba:", "fullmatch"), # noMatch — incomplete last rep - ("(a:b)+", "a:b", "match"), # match - ("(a:b)+", "a:bx", "match"), # match — trailing x allowed - ("^[a-z]+:[0-9]+$", "foo:42", "fullmatch"), # match - ("^[a-z]+:[0-9]+$", "foo:42", "match"), # match — $ blocks trailing - ("^[a-z]+:[0-9]+$", "foo:42x", "match"), # noMatch — $ blocks x - ("^[a-z]+:[0-9]+$", "foo:42", "search"), # match - ("^[a-z]+:[0-9]+$", "xfoo:42", "search"), # noMatch — ^ blocks - - # Escaped metacharacters as literals - (r"a\.b", "a.b", "fullmatch"), # match — \. matches literal dot - (r"a\.b", "axb", "fullmatch"), # noMatch — x is not a dot - (r"a\.b", "a.b", "match"), # match - (r"a\.b", "a.bc", "match"), # match — trailing c allowed - (r"a\.b", "a.b", "search"), # match - (r"a\.b", "xaxbx", "search"), # noMatch - (r"a\+b", "a+b", "fullmatch"), # match — \+ matches literal + - (r"a\+b", "ab", "fullmatch"), # noMatch - (r"a\+b", "a+b", "match"), # match - (r"a\+b", "a+bc", "match"), # match — trailing c allowed - (r"a\*b", "a*b", "fullmatch"), # match — \* matches literal * - (r"a\*b", "aab", "fullmatch"), # noMatch - (r"a\*b", "a*b", "match"), # match - (r"a\?b", "a?b", "fullmatch"), # match — \? matches literal ? - (r"a\?b", "ab", "fullmatch"), # noMatch - (r"a\?b", "a?b", "match"), # match - (r"a\(b\)", "a(b)", "fullmatch"), # match — escaped parens are literals - (r"a\(b\)", "ab", "fullmatch"), # noMatch - (r"a\(b\)", "a(b)", "match"), # match - (r"a\[b\]", "a[b]", "fullmatch"), # match — escaped brackets are literals - (r"a\[b\]", "ab", "fullmatch"), # noMatch - (r"a\[b\]", "a[b]", "match"), # match - (r"a\\b", "a\\b", "fullmatch"), # match — \\ matches literal backslash - (r"a\\b", "ab", "fullmatch"), # noMatch - (r"a\\b", "a\\b", "match"), # match - (r"a\\b", "a\\bc", "match"), # match — trailing c allowed - (r"a\\b", "xa\\by", "search"), # match - (r"a\\b", "xaby", "search"), # noMatch - - # Escaped metacharacter as range start: [\.-z] = range from '.' to 'z' - (r"[\.-z]+", "abc", "fullmatch"), # match — a,b,c all in range .-z - (r"[\.-z]+", "ABC", "fullmatch"), # noMatch — A,B,C below '.' - (r"[\.-z]+", "-", "fullmatch"), # noMatch — '-' (ASCII 45) below '.' (46) - (r"[\.-z]+", ".", "fullmatch"), # match — '.' is start of range - (r"[\.-z]+", "abc", "search"), # match - - # Mixed: colon and escaped metacharacters together - (r"\w+:\d+\.\d+", "foo:3.14", "fullmatch"), # match - (r"\w+:\d+\.\d+", "foo:3x14", "fullmatch"), # noMatch — x not a dot - (r"\w+:\d+\.\d+", "foo:3.14", "match"), # match - (r"\w+:\d+\.\d+", "foo:3.14x", "match"), # match — trailing x allowed - (r"\w+:\d+\.\d+", "xfoo:3.14y", "search"), # match - (r"\w+:\d+\.\d+", "xfoo:3x14y", "search"), # noMatch - - # ── Error cases ────────────────────────────────────────────────────────────── - - ("x{100,2}", "x", "fullmatch"), # error — invalid bounds: lo > hi - ("(abc", "abc", "fullmatch"), # error — unmatched parenthesis - ("a**", "a", "fullmatch"), # error — nothing to repeat - - # ── Unimplemented: lookahead / lookbehind ──────────────────────────────────── - - (r"a(?=b)", "ab", "match"), # match - (r"a(?!b)", "ac", "match"), # match - (r"(?<=a)b", "ab", "match"), # noMatch — re.match at pos 0: nothing precedes b - (r"(?...) ──────────────────────────────── - - (r"(?Pa)", "a", "fullmatch"), # match - (r"(?Pa)", "b", "fullmatch"), # noMatch - (r"(?Pa)(?Pb)", "ab", "fullmatch"), # match - - # ── Unimplemented: inline flags (?i) (?m) (?s) ────────────────────────────── - - (r"(?i)hello", "HELLO", "fullmatch"), # match — case-insensitive - (r"(?i)hello", "Hello", "fullmatch"), # match - (r"(?i)hello", "world", "fullmatch"), # noMatch - (r"(?i)[a-z]+", "ABC", "fullmatch"), # match - (r"(?s)a.b", "axb", "fullmatch"), # match — (?s): . also matches \n - (r"(?m)^a", "a", "search"), # match — (?m): ^ matches per-line - - # ── Unimplemented: backreferences ──────────────────────────────────────────── - - (r"(a)\1", "aa", "fullmatch"), # match — group 1 repeated - (r"(a)\1", "ab", "fullmatch"), # noMatch - (r"(a|b)\1", "aa", "fullmatch"), # match - (r"(a|b)\1", "bb", "fullmatch"), # match - (r"(a|b)\1", "ab", "fullmatch"), # noMatch — mismatch - (r"(.)\1", "aa", "fullmatch"), # match — any char repeated - (r"(.)\1", "ab", "fullmatch"), # noMatch -] - -# ── Python oracle ────────────────────────────────────────────────────────────── - -def run_python(regex: str, string: str, mode: str) -> str: - """Returns 'match', 'noMatch', or 'error:'.""" - fn = {"match": re.match, "fullmatch": re.fullmatch, "search": re.search}[mode] - try: - return "match" if fn(regex, string) is not None else "noMatch" - except re.error as e: - return f"error:{e}" - -# ── Strata oracle ────────────────────────────────────────────────────────────── - -# Path to the StrataPython package root, inferred from this script's location. -# Script is at StrataPython/StrataPythonTest/Regex/diff_test.py, so package root is 2 dirs up. -_SCRIPT_DIR = os.path.dirname(os.path.abspath(__file__)) -_STRATA_PYTHON_DIR = os.path.abspath(os.path.join(_SCRIPT_DIR, "..", "..")) - - -def run_strata(cases: list[tuple[str, str, str]], lake_exe: str, - log_dir: str | None = None) -> dict: - """ - Pipes all test cases to DiffTestCore in one subprocess call. - Returns a dict keyed by (regex, string, mode) → result string. - If log_dir is given, passes --log-dir to DiffTestCore so each generated - .core.st program is written to /_.core.st. - """ - stdin_data = "".join(f"{r}\t{s}\t{m}\n" for r, s, m in cases) - cmd = [lake_exe, "exe", "DiffTestCore"] - if log_dir: - cmd += ["--log-dir", log_dir] - proc = subprocess.run( - cmd, - input=stdin_data, - capture_output=True, - text=True, - cwd=_STRATA_PYTHON_DIR, - ) - results = {} - for line in proc.stdout.splitlines(): - parts = line.split("\t", 3) - if len(parts) == 4: - regex, string, mode, result = parts - results[(regex, string, mode)] = result - else: - print(f" [WARNING] unexpected DiffTestCore output: {line!r}", - file=sys.stderr) - if proc.returncode != 0 and proc.stderr: - print(f"[DiffTestCore stderr]\n{proc.stderr}", file=sys.stderr) - return results - -# ── Agreement logic ──────────────────────────────────────────────────────────── - -def classify(py_result: str, st_result: str) -> str: - """ - Returns one of: 'agree', 'bug', 'known_gap', 'investigate'. - """ - py_match = (py_result == "match") - py_nomatch = (py_result == "noMatch") - py_error = py_result.startswith("error:") - - st_match = (st_result == "match") - st_nomatch = (st_result == "noMatch") - st_pattern_error = (st_result == "parseError:patternError") - st_unimpl = (st_result == "parseError:unimplemented") - st_parse_error = st_pattern_error or st_unimpl - st_smt_error = st_result.startswith("smtError:") - - # Agreement - if py_match and st_match: return "agree" - if py_nomatch and st_nomatch: return "agree" - if py_error and st_parse_error: return "agree" - - # Bugs - if py_match and st_nomatch: return "bug" - if py_nomatch and st_match: return "bug" - if py_error and (st_match or st_nomatch): return "bug" # Strata accepted an invalid regex - if (py_match or py_nomatch) and st_pattern_error: return "bug" # Strata rejected a valid regex - - # Known gap: Strata says unimplemented for a regex Python accepts - if (py_match or py_nomatch) and st_unimpl: return "known_gap" - - # Anything else (smtError, missing output, etc.) - return "investigate" - -# ── Driver ───────────────────────────────────────────────────────────────────── - -def main() -> int: - parser = argparse.ArgumentParser( - description="Differential regex test: Python re module vs Strata SMT backend" - ) - parser.add_argument( - "--lake-exe", default="lake", - help="Path to the lake executable (default: lake)" - ) - parser.add_argument( - "--log-dir", default=None, metavar="PATH", - help="Directory to write generated .core.st programs for debugging" - ) - args = parser.parse_args() - - print(f"Running {len(CORPUS)} test cases against Strata (package dir: {_STRATA_PYTHON_DIR})...") - if args.log_dir: - print(f"Logging .core.st programs to: {args.log_dir}") - - strata_results = run_strata(CORPUS, args.lake_exe, log_dir=args.log_dir) - if len(strata_results) != len(CORPUS): - print(f"ERROR: expected {len(CORPUS)} results from DiffTestCore, got {len(strata_results)}.", - file=sys.stderr) - return 2 - - counts: dict[str, int] = {"agree": 0, "bug": 0, "known_gap": 0, "investigate": 0} - bugs, gaps, investigations = [], [], [] - - for idx, (regex, string, mode) in enumerate(CORPUS, start=1): - py = run_python(regex, string, mode) - st = strata_results.get((regex, string, mode), "smtError:missing_output") - verdict = classify(py, st) - counts[verdict] += 1 - entry = (idx, regex, string, mode, py, st) - if verdict == "bug": - bugs.append(entry) - elif verdict == "known_gap": - gaps.append(entry) - elif verdict == "investigate": - investigations.append(entry) - - # ── Report ───────────────────────────────────────────────────────────────── - print(f"\n{'─' * 62}") - print(f" agree: {counts['agree']:3} bugs: {counts['bug']:3} " - f"known gaps: {counts['known_gap']:3} investigate: {counts['investigate']:3}") - print(f"{'─' * 62}") - - if bugs: - print(f"\n🐛 BUGS ({len(bugs)}) — Strata and Python disagree on a valid regex:") - for idx, regex, string, mode, py, st in bugs: - print(f" [#{idx}] regex={regex!r} string={string!r} mode={mode!r}") - print(f" Python : {py}") - print(f" Strata : {st}") - - if gaps: - print(f"\n⚠️ KNOWN GAPS ({len(gaps)}) — Strata says 'unimplemented':") - for idx, regex, string, mode, py, st in gaps: - print(f" [#{idx}] regex={regex!r} string={string!r} mode={mode!r} python={py}") - - if investigations: - print(f"\n🔍 INVESTIGATE ({len(investigations)}):") - for idx, regex, string, mode, py, st in investigations: - print(f" [#{idx}] regex={regex!r} string={string!r} mode={mode!r}") - print(f" Python : {py}") - print(f" Strata : {st}") - - if not bugs and not investigations: - print("\n✅ All cases either agree or are known gaps.") - - return 1 if bugs or investigations else 0 - - -if __name__ == "__main__": - sys.exit(main()) diff --git a/StrataPythonTest/Regex/regex_oracle.py b/StrataPythonTest/Regex/regex_oracle.py new file mode 100644 index 0000000..d421a66 --- /dev/null +++ b/StrataPythonTest/Regex/regex_oracle.py @@ -0,0 +1,50 @@ +#!/usr/bin/env python3 +"""Python `re` oracle for the regex differential test. + +Reads tab-separated `\t\t` triples from stdin (one per +line) and writes `\t\t\t` to stdout, where + is one of: + match + noMatch + error: + + is one of match / fullmatch / search. This mirrors the output contract +of the Strata-side DiffTestCore tool so the Lean test can classify the two +result streams symmetrically. The corpus is guaranteed tab- and newline-free +(see RegexDiffTest.lean), so a plain split on tab is safe. +""" + +import re +import sys + +_FNS = {"match": re.match, "fullmatch": re.fullmatch, "search": re.search} + + +def run(regex: str, string: str, mode: str) -> str: + fn = _FNS.get(mode) + if fn is None: + return f"error:unknown mode {mode}" + try: + return "match" if fn(regex, string) is not None else "noMatch" + except re.error as e: + return f"error:{e}" + + +def main() -> int: + out = [] + for line in sys.stdin: + line = line.rstrip("\n") + if not line: + continue + parts = line.split("\t") + if len(parts) != 3: + out.append(f"\t\t\terror:bad_input_format") + continue + regex, string, mode = parts + out.append(f"{regex}\t{string}\t{mode}\t{run(regex, string, mode)}") + sys.stdout.write("\n".join(out) + ("\n" if out else "")) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/StrataPythonTest/run_py_analyze_sarif.py b/StrataPythonTest/run_py_analyze_sarif.py deleted file mode 100755 index 7d03564..0000000 --- a/StrataPythonTest/run_py_analyze_sarif.py +++ /dev/null @@ -1,96 +0,0 @@ -#!/usr/bin/env python3 -"""Test SARIF output for pyAnalyzeLaurel. - -Runs pyAnalyzeLaurel --sarif on selected test files and validates the SARIF -output. Run from StrataPython/StrataPythonTest/ (same as run_py_analyze.sh). -""" - -import subprocess -import sys -from pathlib import Path - -from validate_sarif import validate - -REPO_ROOT = Path(__file__).resolve().parent.parent.parent -TEST_DIR = Path(__file__).resolve().parent -STRATA_PYTHON_DIR = Path(__file__).resolve().parent.parent -TEST_FILES = sorted( - f"tests/{p.name}" for p in (Path(__file__).resolve().parent / "tests").glob("test_*.py") -) - -SKIP_TESTS = { - "test_foo_client_folder", - "test_invalid_client_type", - "test_unsupported_config", - "test_with_void_enter", - "test_class_no_init_extra_args", # No SARIF output because does not run SMT analysis - "test_user_error_metadata", # No SARIF output because does not run SMT analysis - "test_is_non_none", # No SARIF output because does not run SMT analysis - "test_is_not_non_none", # No SARIF output because does not run SMT analysis - "test_list", # Module-level asserts cause "asserts not supported in functions" error -} - - -def run(test_file: str) -> bool: - test_path = TEST_DIR / test_file - if not test_path.exists(): - return True - - base_name = Path(test_file).stem - if base_name in SKIP_TESTS: - print(f"Skipping: {base_name}") - return True - - ion_rel = f"StrataPythonTest/tests/{base_name}.python.st.ion" - ion_abs = STRATA_PYTHON_DIR / ion_rel - sarif_abs = STRATA_PYTHON_DIR / f"{ion_rel}.sarif" - - print(f"Testing SARIF output for pyAnalyzeLaurel {base_name}...") - - # Generate Ion file - subprocess.run( - [ - sys.executable, "-m", "strata_python.gen", "py_to_strata", - "--dialect", "dialects/Python.dialect.st.ion", - str(test_path), - str(ion_abs), - ], - cwd=STRATA_PYTHON_DIR / "Tools" / "strata-python", - check=True, - ) - - # Run analysis with --sarif (lake exe builds the binary on demand) - subprocess.run( - ["lake", "exe", "pyAnalyzeLaurel", "--sarif", ion_rel], - cwd=STRATA_PYTHON_DIR, - stdout=subprocess.DEVNULL, - ) - - ok = True - if not sarif_abs.exists(): - print(f"ERROR: SARIF file not created for {base_name} (expected {sarif_abs})") - ok = False - else: - result = validate(str(sarif_abs), base_name) - if result != "OK": - print(f"ERROR: SARIF validation failed for {base_name}: {result}") - ok = False - else: - print(f"Test passed: {base_name}") - - # Clean up generated files - ion_abs.unlink(missing_ok=True) - sarif_abs.unlink(missing_ok=True) - return ok - - -def main() -> int: - failed = 0 - for tf in TEST_FILES: - if not run(tf): - failed = 1 - return failed - - -if __name__ == "__main__": - sys.exit(main()) diff --git a/StrataPythonTest/validate_sarif.py b/StrataPythonTest/validate_sarif.py deleted file mode 100755 index 12cbade..0000000 --- a/StrataPythonTest/validate_sarif.py +++ /dev/null @@ -1,57 +0,0 @@ -#!/usr/bin/env python3 -"""Validate a SARIF file produced by Strata's pyAnalyze --sarif.""" - -import json -import sys - - -def validate(sarif_path: str, base_name: str) -> str: - with open(sarif_path) as f: - d = json.load(f) - - errors = [] - if d.get("version") != "2.1.0": - errors.append("wrong version") - if "runs" not in d or len(d["runs"]) != 1: - errors.append("missing or wrong runs") - return "FAIL: " + "; ".join(errors) - - run = d["runs"][0] - if run.get("tool", {}).get("driver", {}).get("name") != "Strata": - errors.append("wrong tool name") - results = run.get("results", []) - for r in results: - if r.get("level") not in ("none", "error", "warning", "note"): - errors.append(f"invalid level: {r.get('level')}") - if "ruleId" not in r: - errors.append("missing ruleId") - if "message" not in r or "text" not in r.get("message", {}): - errors.append("missing message text") - - error_results = [r for r in results if r.get("level") == "error"] - located_results = [r for r in results if r.get("locations")] - - if base_name == "test_precondition_verification": - if len(error_results) < 1: - errors.append( - f"expected errors, got {len(error_results)} error-level results" - ) - - if base_name == "test_arithmetic": - if len(error_results) != 0: - errors.append(f"expected 0 errors, got {len(error_results)}") - if len(located_results) < 1: - errors.append( - f"expected results with locations, got {len(located_results)}" - ) - - return "FAIL: " + "; ".join(errors) if errors else "OK" - - -if __name__ == "__main__": - if len(sys.argv) != 3: - print(f"Usage: {sys.argv[0]} ", file=sys.stderr) - sys.exit(2) - result = validate(sys.argv[1], sys.argv[2]) - print(result) - sys.exit(0 if result == "OK" else 1) diff --git a/StrataPythonTestExtra/RegexDiffTest.lean b/StrataPythonTestExtra/RegexDiffTest.lean new file mode 100644 index 0000000..7cc8ac1 --- /dev/null +++ b/StrataPythonTestExtra/RegexDiffTest.lean @@ -0,0 +1,229 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +meta import StrataPythonTest.Util.Python -- shake: keep +meta import StrataPython.Regex.ReToCore +meta import StrataDDM.Elab +meta import StrataDDM.BuiltinDialects +public meta import Strata.Languages.Core.Verifier +public meta import Strata.Languages.Core + +/-! ## Regex differential test: Strata SMT backend vs Python `re` + +Ports `StrataPythonTest/Regex/diff_test.py` to a Lean test. The test corpus — +`(regex, string, mode)` triples — lives in `StrataPythonTest/Regex/corpus.tsv`, +one tab-separated triple per line. + +For each case the test: +1. Runs the regex through Strata's SMT backend in-process (the same path + `DiffTestCore` uses: `pythonRegexToCore` then `Core.verify`). +2. Gets the Python `re` result from the `regex_oracle.py` helper, spawned once + over the whole corpus. +3. Classifies the pair as agree / bug / known_gap / investigate and fails the + test on any bug or investigate, matching the Python driver. + +This is a runtime test (needs Python on PATH, plus the SMT solvers cvc5 and z3), +run from `StrataPythonTestExtra/` via `lake test`. The Strata side moved +in-process; the Python `re` oracle stays a subprocess because there is no +in-process equivalent. +-/ + +open Strata +open StrataPython (MatchMode pythonRegexToCore) +open StrataDDM.Elab (LoadedDialects elabProgram) + +namespace StrataPython.RegexDiffTest + +meta section + +def corpusFile : System.FilePath := "StrataPythonTest/Regex/corpus.tsv" +def oracleScript : System.FilePath := "StrataPythonTest/Regex/regex_oracle.py" + +def parseMode (s : String) : Option MatchMode := + match s with + | "match" => some .match + | "fullmatch" => some .fullmatch + | "search" => some .search + | _ => none + +/-- Strata-side result, mirroring `DiffTestCore`'s output vocabulary. -/ +inductive StrataResult where + | match + | noMatch + | parseError (kind : String) -- "patternError" or "unimplemented" + | smtError (msg : String) + +def StrataResult.toStr : StrataResult → String + | .match => "match" + | .noMatch => "noMatch" + | .parseError kind => s!"parseError:{kind}" + | .smtError msg => s!"smtError:{msg}" + +/-- Escape a string for embedding as a double-quoted Core string literal. -/ +def escapeForCore (s : String) : String := + s.foldl (fun acc c => acc ++ match c with + | '\\' => "\\\\" + | '"' => "\\\"" + | '\n' => "\\n" + | '\r' => "\\r" + | '\t' => "\\t" + | _ => toString c) "" + +/-- Build a Core program asserting `str.in.re(testStr, regexExpr)`. -/ +def mkProgText (testStr regexStr : String) : String := + "program Core;\n" ++ + "procedure main() {\n" ++ + s!" assert [match_check]: (str.in.re(\"{escapeForCore testStr}\", {regexStr}));\n" ++ + "};" + +/-- Check whether `testStr` matches `pyRegex` (in `mode`) via Strata's SMT + backend. Lifted from `DiffTestCore.checkMatch` (without the `--log-dir` + path, which the test does not need). -/ +def checkMatch (pyRegex testStr : String) (mode : MatchMode) : IO StrataResult := do + let (regexExpr, parseErr) := pythonRegexToCore pyRegex mode + match parseErr with + | some (.patternError ..) => return .parseError "patternError" + | some (.unimplemented ..) => return .parseError "unimplemented" + | none => + let regexStr := toString (Core.formatExprs [regexExpr]) + let progText := mkProgText testStr regexStr + let inputCtx := Lean.Parser.mkInputContext progText "" + let dctx := LoadedDialects.builtin.addDialect! Core + let leanEnv ← Lean.mkEmptyEnvironment 0 + match elabProgram dctx leanEnv inputCtx with + | .error errors => + let msgs ← errors.toList.mapM (·.toString) + return .smtError s!"elab: {String.intercalate "; " msgs}" + | .ok pgm => + let vcResults ← Strata.Core.verify pgm inputCtx none .quiet + match vcResults[0]? with + | none => return .smtError "no VCs generated" + | some vc => + if vc.isSuccess then return .match + else if vc.isFailure then return .noMatch + else return match vc.outcome with + | .error err => .smtError s!"impl: {err}" + | _ => .smtError "unknown" + +/-- Verdict for a (python, strata) result pair. Mirrors `classify` in + `diff_test.py`. -/ +inductive Verdict where + | agree + | bug + | knownGap + | investigate + +/-- Classify a Python `re` result string against a Strata result. `pyResult` + is one of `match`, `noMatch`, or `error:` (from `regex_oracle.py`). -/ +def classify (pyResult : String) (st : StrataResult) : Verdict := + let pyMatch := pyResult == "match" + let pyNoMatch := pyResult == "noMatch" + let pyError := pyResult.startsWith "error:" + match st with + -- Agreement + | .match => if pyMatch then .agree else if pyNoMatch then .bug + else /- pyError -/ .bug -- Strata accepted an invalid regex + | .noMatch => if pyNoMatch then .agree else if pyMatch then .bug + else /- pyError -/ .bug -- Strata accepted an invalid regex + | .parseError "unimplemented" => + if pyError then .agree + else /- pyMatch || pyNoMatch -/ .knownGap + | .parseError _ /- patternError -/ => + if pyError then .agree + else /- Strata rejected a valid regex -/ .bug + | .smtError _ => .investigate + +/-- One classified corpus entry, kept for reporting. -/ +structure Entry where + idx : Nat + regex : String + str : String + mode : String + py : String + st : String + verdict : Verdict + +/-- Read the corpus as `(regex, string, mode)` triples. -/ +def readCorpus : IO (Array (String × String × String)) := do + let contents ← IO.FS.readFile corpusFile + let mut out := #[] + for line in contents.splitOn "\n" do + if line.isEmpty then continue + match line.splitOn "\t" with + | [r, s, m] => out := out.push (r, s, m) + | _ => throw <| .userError s!"Malformed corpus line: {line}" + return out + +/-- Run all corpus cases through the Python `re` oracle in one subprocess, + returning a map from `(regex, string, mode)` to the result string. -/ +def runOracle (pythonCmd : System.FilePath) + (cases : Array (String × String × String)) : IO (Std.HashMap (String × String × String) String) := do + let stdinData := String.intercalate "\n" (cases.toList.map (fun (r, s, m) => s!"{r}\t{s}\t{m}")) ++ "\n" + let child ← IO.Process.spawn { + cmd := pythonCmd.toString + args := #[oracleScript.toString] + stdin := .piped, stdout := .piped, stderr := .piped + } + let (stdinH, child) ← child.takeStdin + stdinH.putStr stdinData + stdinH.flush + let stdout ← child.stdout.readToEnd + let stderr ← child.stderr.readToEnd + let exitCode ← child.wait + if exitCode ≠ 0 then + throw <| .userError s!"regex_oracle.py failed (exit {exitCode}): {stderr}" + let mut m : Std.HashMap (String × String × String) String := {} + for line in stdout.splitOn "\n" do + if line.isEmpty then continue + match line.splitOn "\t" with + | [r, s, mode, res] => m := m.insert (r, s, mode) res + | _ => pure () + return m + +def main : IO Unit := do + withPython fun pythonCmd => do + let cases ← readCorpus + IO.println s!"Running {cases.size} regex differential cases..." + let oracle ← runOracle pythonCmd cases + + let mut entries : Array Entry := #[] + let mut idx := 0 + for (regex, str, mode) in cases do + idx := idx + 1 + let some mm := parseMode mode + | throw <| .userError s!"Unknown mode in corpus: {mode}" + let st ← checkMatch regex str mm + let py := oracle.getD (regex, str, mode) "error:missing_oracle_output" + entries := entries.push { + idx, regex, str, mode, py, st := st.toStr, verdict := classify py st } + + let count (v : Verdict → Bool) := entries.filter (fun e => v e.verdict) |>.size + let agree := count (· matches .agree) + let bugs := entries.filter (fun e => e.verdict matches .bug) + let gaps := count (· matches .knownGap) + let investigations := entries.filter (fun e => e.verdict matches .investigate) + + IO.println s!" agree: {agree} bugs: {bugs.size} known gaps: {gaps} investigate: {investigations.size}" + + let report (e : Entry) : String := + s!" [#{e.idx}] regex={e.regex} string={e.str} mode={e.mode}\n Python: {e.py}\n Strata: {e.st}" + unless bugs.isEmpty do + IO.println s!"\nBUGS ({bugs.size}) — Strata and Python disagree on a valid regex:" + for e in bugs do IO.println (report e) + unless investigations.isEmpty do + IO.println s!"\nINVESTIGATE ({investigations.size}):" + for e in investigations do IO.println (report e) + + if !bugs.isEmpty || !investigations.isEmpty then + throw <| .userError s!"{bugs.size} bug(s), {investigations.size} investigate — regex differential test failed." + IO.println "All cases either agree or are known gaps." + +end + +end StrataPython.RegexDiffTest + +#eval StrataPython.RegexDiffTest.main diff --git a/StrataPythonTestExtra/SarifTest.lean b/StrataPythonTestExtra/SarifTest.lean new file mode 100644 index 0000000..a748903 --- /dev/null +++ b/StrataPythonTestExtra/SarifTest.lean @@ -0,0 +1,186 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +meta import StrataPythonTest.Util.Python -- shake: keep +meta import StrataPython +meta import StrataPython.Pipeline.PyAnalyzeLaurel +meta import Strata.Languages.Core.SarifOutput + +import Strata.Languages.Core.Verifier + +/-! ## SARIF output tests for `pyAnalyzeLaurel` + +Ports `run_py_analyze_sarif.py` + `validate_sarif.py` to a Lean test. For each +`tests/test_*.py` file the test: + +1. Spawns `strata_python.gen py_to_strata` to compile the Python source to Ion. +2. Runs `StrataPython.Pipeline.runPyAnalyzePipeline` in-process — the same + pipeline `pyAnalyzeLaurel --sarif` drives — and builds the SARIF document + via `Core.Sarif.vcResultsToSarif`. +3. Asserts the SARIF document is well-formed. + +Unlike the Python version this runs entirely in-process: it inspects the typed +`Strata.Sarif.SarifDocument` directly rather than serializing to JSON and +re-parsing, so most of `validate_sarif.py`'s structural checks (version, +single run, valid `level`, present `ruleId`/`message`) are guaranteed by the +types. The remaining checks — tool name, the per-test expectations for +`test_precondition_verification` and `test_arithmetic` — are asserted below. + +This is a runtime test (needs Python with `strata_python.gen`, plus the SMT +solvers cvc5 and z3 on PATH), run from `StrataPythonTestExtra/` via `lake test`. +-/ + +open Strata +open StrataPython (withPython) + +namespace StrataPython.SarifTest + +meta section + +/-- Test files that produce no usable SARIF output and are skipped, mirroring + `SKIP_TESTS` in the original `run_py_analyze_sarif.py`. -/ +def skipTests : Std.HashSet String := Std.HashSet.ofList [ + "test_foo_client_folder", + "test_invalid_client_type", + "test_unsupported_config", + "test_with_void_enter", + "test_class_no_init_extra_args", -- No SARIF output: does not run SMT analysis + "test_user_error_metadata", -- No SARIF output: does not run SMT analysis + "test_is_non_none", -- No SARIF output: does not run SMT analysis + "test_is_not_non_none", -- No SARIF output: does not run SMT analysis + "test_list" -- Module-level asserts: "asserts not supported" error +] + +def testsDir : System.FilePath := "StrataPythonTest/tests" + +/-- Compile a Python source file to a `.python.st.ion` Ion file in `outDir`. -/ +def compilePython (pythonCmd dialectFile pyFile outDir : System.FilePath) + : IO System.FilePath := do + let some stem := pyFile.fileStem + | throw <| .userError s!"No stem for {pyFile}" + let ionPath := outDir / s!"{stem}.python.st.ion" + let child ← IO.Process.spawn { + cmd := pythonCmd.toString + args := #["-m", "strata_python.gen", "py_to_strata", + "--dialect", dialectFile.toString, + pyFile.toString, ionPath.toString] + inheritEnv := true + stdin := .null, stdout := .null, stderr := .piped + } + let stderr ← child.stderr.readToEnd + let exitCode ← child.wait + if exitCode ≠ 0 then + throw <| .userError s!"py_to_strata failed for {pyFile} (exit {exitCode}): {stderr}" + return ionPath + +/-- Run the analysis pipeline on a compiled Ion file and return the SARIF + document, mirroring the `pyAnalyzeLaurel --sarif` path: deductive mode, + `entryPoint = .all`, quiet output. `pyFile` is the original Python source, + used (as the CLI does) both as the pipeline `sourcePath` and to build the + `files` map so SARIF locations resolve. Returns `none` if the pipeline did + not reach verification (e.g. aborted), matching the Python script's "no + SARIF file created" failure. -/ +def analyzeToSarif (ionFile pyFile specDir : System.FilePath) + : IO (Option Strata.Sarif.SarifDocument) := do + let options : Core.VerifyOptions := + { Core.VerifyOptions.default with + verbose := .quiet, removeIrrelevantAxioms := .Precise, + checkMode := .deductive } + let (outcome, _stats, _pctx) ← StrataPython.Pipeline.runPyAnalyzePipeline { + filePath := ionFile.toString + specDir + sourcePath := some pyFile.toString + verifyOptions := options + entryPoint := .all + isBugFinding := false + outputMode := .quiet + } + match outcome with + | .verified vcResults _coreProgram => + -- Build the source file map so VC metadata file-ranges resolve to + -- SARIF locations, keyed by the same URI the pipeline stamps on them. + let srcText ← IO.FS.readFile pyFile + let files := Map.empty.insert (Strata.Uri.file pyFile.toString) + (Lean.FileMap.ofString srcText) + pure (some (Core.Sarif.vcResultsToSarif options.checkMode files vcResults)) + | .failed => pure none + +/-- Validate a SARIF document for `baseName`, mirroring `validate_sarif.py`. + Returns an error message, or `none` if valid. Structural invariants + (version, single run, valid `level` enum, present `ruleId`/`message`) hold + by construction of `SarifDocument`; we check the remaining properties. -/ +def validate (doc : Strata.Sarif.SarifDocument) (baseName : String) : Option String := Id.run do + if doc.version != "2.1.0" then + return some s!"wrong version: {doc.version}" + if doc.runs.size != 1 then + return some s!"expected 1 run, got {doc.runs.size}" + let run := doc.runs[0]! + if run.tool.driver.name != "Strata" then + return some s!"wrong tool name: {run.tool.driver.name}" + let results := run.results + let errorResults := results.filter (·.level == .error) + let locatedResults := results.filter (·.locations.size > 0) + + if baseName == "test_precondition_verification" then + if errorResults.size < 1 then + return some s!"expected error-level results, got {errorResults.size}" + + if baseName == "test_arithmetic" then + if errorResults.size != 0 then + return some s!"expected 0 errors, got {errorResults.size}" + if locatedResults.size < 1 then + return some s!"expected results with locations, got {locatedResults.size}" + + return none + +/-- Recursively unused: tests live directly under `testsDir`; collect `test_*.py`. -/ +def findTestFiles : IO (Array System.FilePath) := do + let mut results := #[] + for entry in ← testsDir.readDir do + let p := entry.path + if p.extension == some "py" then + if let some stem := p.fileStem then + if stem.startsWith "test_" then + results := results.push p + return results.qsort (·.toString < ·.toString) + +def main : IO Unit := do + withPython fun pythonCmd => do + IO.FS.withTempDir fun tmpDir => do + let dialectFile := tmpDir / "Python.dialect.st.ion" + IO.FS.writeBinFile dialectFile Python.toIon + + let files ← findTestFiles + let mut failures := 0 + for pyFile in files do + let some stem := pyFile.fileStem + | continue + if skipTests.contains stem then + IO.println s!"Skipping: {stem}" + continue + IO.println s!"Testing SARIF output for {stem}..." + let ionFile ← compilePython pythonCmd dialectFile pyFile tmpDir + match ← analyzeToSarif ionFile pyFile tmpDir with + | none => + IO.println s!"ERROR: pipeline produced no SARIF output for {stem}" + failures := failures + 1 + | some doc => + match validate doc stem with + | some err => + IO.println s!"ERROR: SARIF validation failed for {stem}: {err}" + failures := failures + 1 + | none => + IO.println s!"Test passed: {stem}" + + if failures > 0 then + throw <| .userError s!"{failures} SARIF test failure(s)." + +end + +end StrataPython.SarifTest + +#eval StrataPython.SarifTest.main diff --git a/lakefile.toml b/lakefile.toml index 3ca85f5..11150dc 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,7 +10,6 @@ git = "https://github.com/strata-org/Strata.git" [[input_file]] name = "PythonDialectIon" path = "Tools/strata-python/dialects/Python.dialect.st.ion" -text = true [[lean_lib]] name = "StrataPython" From 884b6cf050220e6daf5319b118dc3f61025ed975 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 24 Jun 2026 16:13:17 -0700 Subject: [PATCH 2/3] Port pyInterpret golden tests from shell to a Lean test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace run_py_interpret.sh with StrataPythonTestExtra/InterpretTest.lean. For each tests/test_*.py it spawns strata_python.gen to compile to Ion, then runs the interpreter pipeline in-process — the same path Cli.lean's pyInterpret drives (pythonAndSpecToLaurel -> translateCombinedLaurel -> typeCheck -> core.run + runCall __main__) — and checks expected_interpret/: no .expected/.skip means run to completion; a .expected means fail with matching text; a .skip means skip. The committed patterns are escaped literals, so the match reduces to substring containment after unescaping \X -> X (no regex engine needed). Running in-process replaces 219 `lake exe pyInterpret` subprocess spawns (the shell version times out past 10 min locally). Update 4 expected files (test_class_no_init_extra_args, test_is_non_none, test_is_not_non_none, test_user_error_metadata): they matched only the generic CLI hint "Run strata --help for additional help." — a Cli framework artifact the in-process path doesn't emit — so they now assert the actual, stable interpreter error for each, making the checks strictly stronger. CI: build_and_test_lean runs it via `lake test -- InterpretTest`; the build_python matrix excludes it alongside the other in-process suites. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/ci.yml | 12 +- .../test_class_no_init_extra_args.expected | 2 +- .../test_is_non_none.expected | 2 +- .../test_is_not_non_none.expected | 2 +- .../test_user_error_metadata.expected | 2 +- StrataPythonTest/run_py_interpret.sh | 141 ------------- StrataPythonTestExtra/InterpretTest.lean | 187 ++++++++++++++++++ 7 files changed, 198 insertions(+), 150 deletions(-) delete mode 100755 StrataPythonTest/run_py_interpret.sh create mode 100644 StrataPythonTestExtra/InterpretTest.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 53d5bb1..18c6591 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -48,9 +48,11 @@ jobs: pip install ./.lake/packages/Strata/Tools/Python-base pip install ./Tools/strata-python - name: Run pyInterpret golden-file tests - working-directory: StrataPythonTest - shell: bash - run: ./run_py_interpret.sh + # InterpretTest is the StrataPythonTestExtra Lean port of the old + # run_py_interpret.sh: it runs the interpreter pipeline in-process per + # tests/test_*.py and checks outcomes against expected_interpret/. + # Excluded from the build_python matrix below so it runs once here. + run: PYTHON=python lake test -- InterpretTest - name: Run pyAnalyze SARIF tests # SarifTest is the StrataPythonTestExtra Lean port of the old # run_py_analyze_sarif.py: it runs the analysis pipeline in-process and @@ -182,9 +184,9 @@ jobs: # Excludes: # - CpythonDiffTest: run separately below against a full CPython checkout # (here it would be a no-op anyway since CPYTHON_DIR is unset). - # - SarifTest, RegexDiffTest: SMT-heavy and version-independent, run once + # - SarifTest, RegexDiffTest, InterpretTest: version-independent, run once # in build_and_test_lean rather than per Python version. - run: PYTHON=python lake test -- --exclude CpythonDiffTest --exclude SarifTest --exclude RegexDiffTest + run: PYTHON=python lake test -- --exclude CpythonDiffTest --exclude SarifTest --exclude RegexDiffTest --exclude InterpretTest - name: Run CPython differential tests # Clones CPython at the matrix version and round-trips its whole test # suite through the Strata generator + Ion (de)serializer. The round-trip diff --git a/StrataPythonTest/expected_interpret/test_class_no_init_extra_args.expected b/StrataPythonTest/expected_interpret/test_class_no_init_extra_args.expected index c77f7e4..01570f7 100644 --- a/StrataPythonTest/expected_interpret/test_class_no_init_extra_args.expected +++ b/StrataPythonTest/expected_interpret/test_class_no_init_extra_args.expected @@ -1 +1 @@ -Run strata --help for additional help\. +'NoInit' called with too many positional arguments: expected at most 0, got 1 diff --git a/StrataPythonTest/expected_interpret/test_is_non_none.expected b/StrataPythonTest/expected_interpret/test_is_non_none.expected index c77f7e4..6d04400 100644 --- a/StrataPythonTest/expected_interpret/test_is_non_none.expected +++ b/StrataPythonTest/expected_interpret/test_is_non_none.expected @@ -1 +1 @@ -Run strata --help for additional help\. +Unsupported construct: `is` is only supported with None diff --git a/StrataPythonTest/expected_interpret/test_is_not_non_none.expected b/StrataPythonTest/expected_interpret/test_is_not_non_none.expected index c77f7e4..a5c5fa2 100644 --- a/StrataPythonTest/expected_interpret/test_is_not_non_none.expected +++ b/StrataPythonTest/expected_interpret/test_is_not_non_none.expected @@ -1 +1 @@ -Run strata --help for additional help\. +Unsupported construct: `is not` is only supported with None diff --git a/StrataPythonTest/expected_interpret/test_user_error_metadata.expected b/StrataPythonTest/expected_interpret/test_user_error_metadata.expected index c77f7e4..9925350 100644 --- a/StrataPythonTest/expected_interpret/test_user_error_metadata.expected +++ b/StrataPythonTest/expected_interpret/test_user_error_metadata.expected @@ -1 +1 @@ -Run strata --help for additional help\. +Unknown method 'nonexistent_method' diff --git a/StrataPythonTest/run_py_interpret.sh b/StrataPythonTest/run_py_interpret.sh deleted file mode 100755 index d52023e..0000000 --- a/StrataPythonTest/run_py_interpret.sh +++ /dev/null @@ -1,141 +0,0 @@ -#!/bin/bash - -# Usage: ./run_py_interpret.sh [--filter ] [--fuel ] [--keep-all-files ] [--verbose] [--update] -# -# Runs pyInterpret on all test_*.py files and reports pass/fail. -# -# Expected outcomes are controlled by files in expected_interpret/: -# - No .expected/.skip → run test, assert exit code 0 (PASS) -# - .expected file → run test, assert non-zero exit and output matches -# the regex pattern in the file -# - .skip file → skip test (file contents used as reason) -# -# Options: -# --filter Only run tests whose name contains -# --fuel Set the interpreter fuel limit (default: 100000) -# --verbose Show full interpreter output on failure -# --update Regenerate .expected files from actual output - -set -o pipefail - -SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" -TESTS_DIR="$SCRIPT_DIR/tests" -EXPECTED_DIR="$SCRIPT_DIR/expected_interpret" -STRATA_PYTHON_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" - -passed=0 -errors=0 -skipped=0 -filter="" -keepAllFiles="" -fuel="" -verbose=0 -update=0 - -while [ $# -gt 0 ]; do - case "$1" in - --filter) filter="$2"; shift ;; - --keep-all-files) keepAllFiles="--keep-all-files $2"; shift ;; - --fuel) fuel="--fuel $2"; shift ;; - --verbose) verbose=1 ;; - --update) update=1 ;; - *) echo "Unknown option: $1"; exit 1 ;; - esac - shift -done - -# Ensure pyInterpret is built (lake exe will build on demand, but pre-build for cleaner output) -(cd "$STRATA_PYTHON_DIR" && lake build pyInterpret > /dev/null 2>&1) - -for test_file in "$TESTS_DIR"/test_*.py; do - [ -f "$test_file" ] || continue - base_name=$(basename "$test_file" .py) - - # Apply name filter if specified - if [ -n "$filter" ] && [[ "$base_name" != *"$filter"* ]]; then - continue - fi - - expected_file="$EXPECTED_DIR/${base_name}.expected" - skip_file="$EXPECTED_DIR/${base_name}.skip" - ion_file="$TESTS_DIR/${base_name}.python.st.ion" - - # Check for skip file - if [ -f "$skip_file" ]; then - reason=$(cat "$skip_file") - echo "SKIP: $base_name — $reason" - skipped=$((skipped + 1)) - continue - fi - - # Compile Python to Ion - if ! (cd "$STRATA_PYTHON_DIR/Tools/strata-python" && python3 -m strata_python.gen py_to_strata \ - --dialect "dialects/Python.dialect.st.ion" \ - "$test_file" "$ion_file") 2>/dev/null; then - echo "SKIP (parse): $base_name" - skipped=$((skipped + 1)) - continue - fi - - # Run interpreter - rel_ion="StrataPythonTest/tests/${base_name}.python.st.ion" - output=$(cd "$STRATA_PYTHON_DIR" && lake exe pyInterpret $fuel $keepAllFiles \ - "$rel_ion" 2>&1) - exit_code=$? - - # Clean up Ion file - rm -f "$ion_file" - - if [ -f "$expected_file" ]; then - # Expected file exists → test should fail, output should match regex - pattern=$(cat "$expected_file") - - if [ $update -eq 1 ]; then - if [ $exit_code -ne 0 ]; then - echo "$output" | grep -oE "$pattern" | head -1 > "$expected_file" - echo "Updated: $base_name" - else - rm -f "$expected_file" - echo "Updated: $base_name (now passes, removed expected file)" - fi - passed=$((passed + 1)) - elif [ $exit_code -eq 0 ]; then - echo "ERR: $base_name (expected failure matching /$pattern/ but test passed)" - errors=$((errors + 1)) - elif echo "$output" | grep -qE "$pattern"; then - echo "OK: $base_name (expected failure)" - passed=$((passed + 1)) - else - echo "ERR: $base_name (output does not match expected pattern /$pattern/)" - if [ $verbose -eq 1 ]; then - echo "$output" | sed 's/^/ /' - fi - errors=$((errors + 1)) - fi - else - # No expected file → test should pass - if [ $update -eq 1 ] && [ $exit_code -ne 0 ]; then - # Test fails unexpectedly; create expected file with regex-escaped error - reason=$(echo "$output" | grep -v "^$" | grep -v "backtrace:" | grep -v "^ [0-9]" | grep -v "^trace:" | tail -1) - escaped=$(echo "$reason" | sed 's/[][(){}.*+?^$\\|]/\\&/g') - echo "$escaped" > "$expected_file" - echo "Created: $base_name — $reason" - passed=$((passed + 1)) - elif [ $exit_code -eq 0 ]; then - echo "OK: $base_name" - passed=$((passed + 1)) - else - reason=$(echo "$output" | grep -v "^$" | grep -v "backtrace:" | grep -v "^ [0-9]" | grep -v "^trace:" | tail -1) - echo "ERR: $base_name (expected pass but failed) — $reason" - if [ $verbose -eq 1 ]; then - echo "$output" | grep -v "backtrace:" | grep -v "^ [0-9]" | grep -v "^$" | sed 's/^/ /' - fi - errors=$((errors + 1)) - fi - fi -done - -echo "" -echo "Results: $passed passed, $skipped skipped, $errors errors" - -[ "$errors" -eq 0 ] diff --git a/StrataPythonTestExtra/InterpretTest.lean b/StrataPythonTestExtra/InterpretTest.lean new file mode 100644 index 0000000..784c761 --- /dev/null +++ b/StrataPythonTestExtra/InterpretTest.lean @@ -0,0 +1,187 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +meta import StrataPythonTest.Util.Python -- shake: keep +meta import StrataPython +meta import StrataPython.PySpecPipeline +meta import StrataPython.PyFactory +public meta import Strata.Languages.Core.StatementEval +public meta import Strata.Languages.Core.ProgramEval + +/-! ## pyInterpret golden tests + +Ports `StrataPythonTest/run_py_interpret.sh` to a Lean test. For each +`tests/test_*.py` the test spawns `strata_python.gen py_to_strata` to compile +the source to Ion, then runs the interpreter pipeline in-process — the same +path `Cli.lean`'s `pyInterpret` command drives (Python → Laurel → Core → +execute `__main__`) — and checks the outcome against `expected_interpret/`: + +- No `.expected`/`.skip` file → the program must run to completion. +- A `.expected` file → the program must fail, and the failure text must + contain the file's pattern. All committed patterns are escaped literals + (every metacharacter is backslash-escaped), so "matches" reduces to + substring containment after unescaping `\X → X`; no regex engine is needed. +- A `.skip` file → skip (the contents are the reason). + +This is a runtime test (needs Python with `strata_python.gen`), run from +`StrataPythonTestExtra/` via `lake test`. Unlike the shell version it runs the +interpreter in-process rather than via `lake exe pyInterpret`. +-/ + +open Strata +open StrataPython (withPython) + +namespace StrataPython.InterpretTest + +meta section + +def testsDir : System.FilePath := "StrataPythonTest/tests" +def expectedDir : System.FilePath := "StrataPythonTest/expected_interpret" + +/-- Default interpreter fuel, matching `run_py_interpret.sh`. -/ +def defaultFuel : Nat := 100000 + +/-- Compile a Python source file to a `.python.st.ion` Ion file in `outDir`. + Returns `none` on a parse failure (the shell script's "SKIP (parse)"). -/ +def compilePython (pythonCmd dialectFile pyFile outDir : System.FilePath) + : IO (Option System.FilePath) := do + let some stem := pyFile.fileStem + | return none + let ionPath := outDir / s!"{stem}.python.st.ion" + let child ← IO.Process.spawn { + cmd := pythonCmd.toString + args := #["-m", "strata_python.gen", "py_to_strata", + "--dialect", dialectFile.toString, + pyFile.toString, ionPath.toString] + inheritEnv := true + stdin := .null, stdout := .null, stderr := .null + } + let exitCode ← child.wait + if exitCode ≠ 0 then return none + return some ionPath + +/-- Interpret a compiled Python Ion program, mirroring `Cli.lean`'s + `pyInterpretCommand`. Returns `.ok ()` when `__main__` runs to completion, + or `.error msg` with the formatted failure text otherwise (the same text + the CLI prints, which the `.expected` patterns match against). -/ +def interpret (ionFile : System.FilePath) : IO (Except String Unit) := do + let quietCtx ← Strata.Pipeline.PipelineContext.create (outputMode := .quiet) + let coreOpt ← + match ← (StrataPython.pythonAndSpecToLaurel ionFile.toString (specDir := ".")).run quietCtx + |>.toBaseIO with + | .ok laurel => + match ← StrataPython.translateCombinedLaurel laurel with + | (some core, _diags) => pure (Except.ok core) + | (none, diags) => pure (Except.error s!"Laurel to Core translation failed: {diags}") + | .error () => + let msgs ← quietCtx.getMessages + pure (Except.error (match msgs.back? with | some m => m.message | none => "Pipeline aborted")) + match coreOpt with + | .error msg => return .error msg + | .ok core => + match Core.typeCheck Core.VerifyOptions.quiet core (moreFns := StrataPython.ReFactory) with + | .error e => return .error s!"Core type checking failed: {e.message}" + | .ok core => + match core.run with + | .error diag => return .error s!"Error: {diag}" + | .ok E => + let mainProc := Core.Program.Procedure.find? core ⟨"__main__", ()⟩ + let outputNames := match mainProc with + | some p => p.header.outputs.keys.map (·.name) + | none => [] + let (lhs, exprEnv) := Core.Env.genVars outputNames E.exprEnv + let E := { E with exprEnv } + let E := Core.Statement.Command.runCall lhs "__main__" [] defaultFuel E + match E.error with + | none => return .ok () + | some e => return .error (toString (Std.format e)) + +/-- Unescape a committed `.expected` pattern (`\X → X`) so a literal substring + check is equivalent to the original POSIX-regex match. -/ +def unescapePattern (s : String) : String := + let rec go (cs : List Char) (acc : String) : String := + match cs with + | [] => acc + | '\\' :: c :: rest => go rest (acc.push c) + | c :: rest => go rest (acc.push c) + go s.toList "" + +structure Outcome where + passed : Nat := 0 + skipped : Nat := 0 + errors : Nat := 0 + +def collectTestFiles : IO (Array System.FilePath) := do + let mut out := #[] + for entry in ← testsDir.readDir do + let p := entry.path + if p.extension == some "py" then + if let some stem := p.fileStem then + if stem.startsWith "test_" then + out := out.push p + return out.qsort (·.toString < ·.toString) + +def main : IO Unit := do + withPython fun pythonCmd => do + IO.FS.withTempDir fun tmpDir => do + let dialectFile := tmpDir / "Python.dialect.st.ion" + IO.FS.writeBinFile dialectFile Python.toIon + + let files ← collectTestFiles + let mut o : Outcome := {} + for pyFile in files do + let some baseName := pyFile.fileStem + | continue + let expectedFile := expectedDir / s!"{baseName}.expected" + let skipFile := expectedDir / s!"{baseName}.skip" + + if ← skipFile.pathExists then + let reason := (← IO.FS.readFile skipFile).trimAscii.toString + IO.println s!"SKIP: {baseName} — {reason}" + o := { o with skipped := o.skipped + 1 } + continue + + match ← compilePython pythonCmd dialectFile pyFile tmpDir with + | none => + IO.println s!"SKIP (parse): {baseName}" + o := { o with skipped := o.skipped + 1 } + | some ionFile => + let result ← interpret ionFile + if ← expectedFile.pathExists then + -- Expected failure: result must be an error containing the pattern. + let pattern := unescapePattern (← IO.FS.readFile expectedFile).trimAscii.toString + match result with + | .ok () => + IO.println s!"ERR: {baseName} (expected failure matching /{pattern}/ but test passed)" + o := { o with errors := o.errors + 1 } + | .error output => + if (output.splitOn pattern).length > 1 then + IO.println s!"OK: {baseName} (expected failure)" + o := { o with passed := o.passed + 1 } + else + IO.println s!"ERR: {baseName} (output does not match expected pattern /{pattern}/)" + IO.println s!" got: {output}" + o := { o with errors := o.errors + 1 } + else + -- No expected file: the program must run to completion. + match result with + | .ok () => + IO.println s!"OK: {baseName}" + o := { o with passed := o.passed + 1 } + | .error output => + IO.println s!"ERR: {baseName} (expected pass but failed) — {output}" + o := { o with errors := o.errors + 1 } + + IO.println s!"\nResults: {o.passed} passed, {o.skipped} skipped, {o.errors} errors" + if o.errors > 0 then + throw <| .userError s!"{o.errors} pyInterpret test failure(s)." + +end + +end StrataPython.InterpretTest + +#eval StrataPython.InterpretTest.main From 6bb4618783f7fe8d50cc588a229055b2e1522f1f Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 24 Jun 2026 16:26:52 -0700 Subject: [PATCH 3/3] Remove standalone Script exes with no remaining caller MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Delete the Scripts/ executable wrappers and their lean_exe targets for pyInterpret, pyAnalyzeToGoto, pyTranslateLaurel, pySpecToLaurel, pyResolveOverloads, and pySpecs. None are invoked by any script, workflow, or test: pyInterpret's only caller (run_py_interpret.sh) was ported to the InterpretTest Lean test, and the other five had no caller. The underlying StrataPython.Cli.*Command definitions are untouched — the standalone Strata-CLI repo wires all of them into its unified `strata` binary, so only the per-command standalone exes are removed here. Kept: pyAnalyzeLaurel (used by run_py_analyze.sh) and pyAnalyzeLaurelToGoto (used by py_ion_to_cbmc.sh). Co-Authored-By: Claude Opus 4.8 --- README.md | 2 +- Scripts/pyAnalyzeToGoto.lean | 10 ---------- Scripts/pyInterpret.lean | 10 ---------- Scripts/pyResolveOverloads.lean | 10 ---------- Scripts/pySpecToLaurel.lean | 10 ---------- Scripts/pySpecs.lean | 10 ---------- Scripts/pyTranslateLaurel.lean | 10 ---------- lakefile.toml | 30 ------------------------------ 8 files changed, 1 insertion(+), 91 deletions(-) delete mode 100644 Scripts/pyAnalyzeToGoto.lean delete mode 100644 Scripts/pyInterpret.lean delete mode 100644 Scripts/pyResolveOverloads.lean delete mode 100644 Scripts/pySpecToLaurel.lean delete mode 100644 Scripts/pySpecs.lean delete mode 100644 Scripts/pyTranslateLaurel.lean diff --git a/README.md b/README.md index 5faf4f6..da62594 100644 --- a/README.md +++ b/README.md @@ -60,7 +60,7 @@ The package is the repository root: │ │ └── ReToCore.lean # Regex → Core SMT translation │ └── Pipeline/ │ └── PyAnalyzeLaurel.lean # Full analysis pipeline (Python → Laurel → Core → SMT) -├── Scripts/ # Executable entry points (pyInterpret, pyAnalyzeLaurel, etc.) +├── Scripts/ # Executable entry points (pyAnalyzeLaurel, pyAnalyzeLaurelToGoto) ├── Tools/ │ └── strata-python/ # Python tooling package (Ion reader, dialect generator) ├── StrataPythonTest/ # Compile-time tests (built with lake build) diff --git a/Scripts/pyAnalyzeToGoto.lean b/Scripts/pyAnalyzeToGoto.lean deleted file mode 100644 index 377f540..0000000 --- a/Scripts/pyAnalyzeToGoto.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module -import StrataPython.Cli - -public def main (args : List String) : IO Unit := - runCommand StrataPython.Cli.pyAnalyzeToGotoCommand args diff --git a/Scripts/pyInterpret.lean b/Scripts/pyInterpret.lean deleted file mode 100644 index bc7eb38..0000000 --- a/Scripts/pyInterpret.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module -import StrataPython.Cli - -public def main (args : List String) : IO Unit := - runCommand StrataPython.Cli.pyInterpretCommand args diff --git a/Scripts/pyResolveOverloads.lean b/Scripts/pyResolveOverloads.lean deleted file mode 100644 index a683aa5..0000000 --- a/Scripts/pyResolveOverloads.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module -import StrataPython.Cli - -public def main (args : List String) : IO Unit := - runCommand StrataPython.Cli.pyResolveOverloadsCommand args diff --git a/Scripts/pySpecToLaurel.lean b/Scripts/pySpecToLaurel.lean deleted file mode 100644 index bead8ba..0000000 --- a/Scripts/pySpecToLaurel.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module -import StrataPython.Cli - -public def main (args : List String) : IO Unit := - runCommand StrataPython.Cli.pySpecToLaurelCommand args diff --git a/Scripts/pySpecs.lean b/Scripts/pySpecs.lean deleted file mode 100644 index f4984cd..0000000 --- a/Scripts/pySpecs.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module -import StrataPython.Cli - -public def main (args : List String) : IO Unit := - runCommand StrataPython.Cli.pySpecsCommand args diff --git a/Scripts/pyTranslateLaurel.lean b/Scripts/pyTranslateLaurel.lean deleted file mode 100644 index 815dc5a..0000000 --- a/Scripts/pyTranslateLaurel.lean +++ /dev/null @@ -1,10 +0,0 @@ -/- - Copyright Strata Contributors - - SPDX-License-Identifier: Apache-2.0 OR MIT --/ -module -import StrataPython.Cli - -public def main (args : List String) : IO Unit := - runCommand StrataPython.Cli.pyTranslateLaurelCommand args diff --git a/lakefile.toml b/lakefile.toml index 11150dc..6086cb1 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -36,37 +36,7 @@ name = "pyAnalyzeLaurel" root = "Scripts.pyAnalyzeLaurel" needs = ["StrataPython"] -[[lean_exe]] -name = "pyAnalyzeToGoto" -root = "Scripts.pyAnalyzeToGoto" -needs = ["StrataPython"] - -[[lean_exe]] -name = "pyTranslateLaurel" -root = "Scripts.pyTranslateLaurel" -needs = ["StrataPython"] - [[lean_exe]] name = "pyAnalyzeLaurelToGoto" root = "Scripts.pyAnalyzeLaurelToGoto" needs = ["StrataPython"] - -[[lean_exe]] -name = "pySpecToLaurel" -root = "Scripts.pySpecToLaurel" -needs = ["StrataPython"] - -[[lean_exe]] -name = "pyResolveOverloads" -root = "Scripts.pyResolveOverloads" -needs = ["StrataPython"] - -[[lean_exe]] -name = "pyInterpret" -root = "Scripts.pyInterpret" -needs = ["StrataPython"] - -[[lean_exe]] -name = "pySpecs" -root = "Scripts.pySpecs" -needs = ["StrataPython"]