From b054782da6f1b2cff8219ee42fa21aee24e9e0a3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Apr 2026 18:27:15 +0000 Subject: [PATCH 01/13] Add hypothesmith-based fuzz testing for Python front-end MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two test modes: 1. Syntax mode: Uses hypothesmith to generate syntactically valid Python programs, then runs them through the parse -> Ion -> round-trip pipeline. Tests that the parser doesn't crash on arbitrary valid Python. 2. Semantic mode: Custom generator produces typed programs with int arithmetic, comparisons, boolean logic, string concatenation, if/else, floor division, modulo, and negation — all with assertions whose expected values are computed by CPython. Programs are first validated with CPython, then run through pyAnalyzeLaurel. A verification failure on a CPython-passing program indicates a semantic modelling bug. Size control: - --max-nodes filters syntax-mode programs by AST node count - --max-examples controls how many programs to generate - --seed enables reproducible runs Usage: cd Tools/Python && ./scripts/hypothesmith.sh [N [SEED [MODE]]] Co-authored-by: Kiro --- Tools/Python/scripts/gen_random_python.py | 252 ++++++++++++++++++++++ Tools/Python/scripts/hypothesmith.sh | 210 ++++++++++++++++++ 2 files changed, 462 insertions(+) create mode 100644 Tools/Python/scripts/gen_random_python.py create mode 100755 Tools/Python/scripts/hypothesmith.sh diff --git a/Tools/Python/scripts/gen_random_python.py b/Tools/Python/scripts/gen_random_python.py new file mode 100644 index 0000000000..3aa66a2b31 --- /dev/null +++ b/Tools/Python/scripts/gen_random_python.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +# Copyright Strata Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +""" +Generate random Python programs for fuzz-testing Strata's Python front-end. + +Two modes: + --mode syntax Use hypothesmith to generate syntactically valid Python. + Tests the parser pipeline (py_to_strata + Ion round-trip). + --mode semantic Use a custom generator to produce typed programs with + assertions that have known outcomes. Tests that + pyAnalyzeLaurel correctly models Python semantics. + +Size control: + --max-examples N Number of Hypothesis examples to try (default: 100). + --max-nodes N Filter: discard programs with more than N AST nodes (default: 50). + --seed S Fixed Hypothesis seed for reproducibility. +""" + +import argparse +import ast +import os +import random +import sys +from pathlib import Path + + +def gen_syntax(args): + """Generate syntactically valid Python via hypothesmith.""" + import hypothesmith + from hypothesis import given, settings, HealthCheck, Phase + + phases = [Phase.generate] + if args.seed is not None: + phases = [Phase.generate] + + out = Path(args.output_dir) + out.mkdir(parents=True, exist_ok=True) + count = [0] + + health_checks = [HealthCheck.too_slow, HealthCheck.filter_too_much] + + @settings( + max_examples=args.max_examples, + suppress_health_check=health_checks, + database=None, + derandomize=args.seed is not None, + phases=phases, + ) + @given(source_code=hypothesmith.from_grammar(auto_target=True)) + def collect(source_code): + try: + tree = ast.parse(source_code) + nodes = len(list(ast.walk(tree))) + except SyntaxError: + return + if nodes < 2: + return + if nodes > args.max_nodes: + return + idx = count[0] + count[0] += 1 + p = out / f"fuzz_syntax_{idx:04d}.py" + p.write_text(source_code) + + if args.seed is not None: + os.environ["HYPOTHESIS_SEED"] = str(args.seed) + collect() + print(f"Generated {count[0]} syntax-mode programs in {out}") + + +# --------------------------------------------------------------------------- +# Semantic mode: build programs with typed variables and checkable assertions +# --------------------------------------------------------------------------- + +def _rand_int(): + return random.randint(-100, 100) + +def _rand_bool(): + return random.choice([True, False]) + +def _rand_str(): + words = ["hello", "world", "foo", "bar", "", "abc", "x"] + return random.choice(words) + +def _gen_int_arithmetic(): + """Generate an int arithmetic block with a true assertion.""" + a, b = _rand_int(), _rand_int() + op_name, op_sym, result_fn = random.choice([ + ("add", "+", lambda a, b: a + b), + ("sub", "-", lambda a, b: a - b), + ("mul", "*", lambda a, b: a * b), + ]) + result = result_fn(a, b) + return ( + f" a: int = {a}\n" + f" b: int = {b}\n" + f" r: int = a {op_sym} b\n" + f' assert r == {result}, "int {op_name}"\n' + ) + +def _gen_int_comparison(): + """Generate an int comparison with a true assertion.""" + a, b = _rand_int(), _rand_int() + op_sym, result = random.choice([ + ("<", a < b), ("<=", a <= b), (">", a > b), + (">=", a >= b), ("==", a == b), ("!=", a != b), + ]) + return ( + f" a: int = {a}\n" + f" b: int = {b}\n" + f' assert (a {op_sym} b) == {result}, "int cmp"\n' + ) + +def _gen_bool_logic(): + """Generate a boolean logic block with a true assertion.""" + a, b = _rand_bool(), _rand_bool() + op_name, op_sym, result_fn = random.choice([ + ("and", "and", lambda a, b: a and b), + ("or", "or", lambda a, b: a or b), + ]) + result = result_fn(a, b) + return ( + f" a: bool = {a}\n" + f" b: bool = {b}\n" + f" r: bool = a {op_sym} b\n" + f' assert r == {result}, "bool {op_name}"\n' + ) + +def _gen_str_concat(): + """Generate a string concatenation with a true assertion.""" + a, b = _rand_str(), _rand_str() + result = a + b + return ( + f" a: str = {a!r}\n" + f" b: str = {b!r}\n" + f" r: str = a + b\n" + f' assert r == {result!r}, "str concat"\n' + ) + +def _gen_if_else(): + """Generate an if/else with a true assertion about the result.""" + cond_val = _rand_bool() + a, b = _rand_int(), _rand_int() + expected = a if cond_val else b + return ( + f" cond: bool = {cond_val}\n" + f" if cond:\n" + f" r: int = {a}\n" + f" else:\n" + f" r: int = {b}\n" + f' assert r == {expected}, "if_else"\n' + ) + +def _gen_floor_div(): + """Generate floor division with a true assertion.""" + a = _rand_int() + b = random.choice([x for x in range(-10, 11) if x != 0]) + result = a // b + return ( + f" a: int = {a}\n" + f" b: int = {b}\n" + f" r: int = a // b\n" + f' assert r == {result}, "floor div"\n' + ) + +def _gen_modulo(): + """Generate modulo with a true assertion.""" + a = _rand_int() + b = random.choice([x for x in range(-10, 11) if x != 0]) + result = a % b + return ( + f" a: int = {a}\n" + f" b: int = {b}\n" + f" r: int = a % b\n" + f' assert r == {result}, "modulo"\n' + ) + +def _gen_negation(): + """Generate unary negation with a true assertion.""" + a = _rand_int() + return ( + f" a: int = {a}\n" + f" r: int = -a\n" + f' assert r == {-a}, "negation"\n' + ) + +def _gen_not(): + """Generate boolean not with a true assertion.""" + a = _rand_bool() + return ( + f" a: bool = {a}\n" + f" r: bool = not a\n" + f' assert r == {not a}, "bool not"\n' + ) + +GENERATORS = [ + _gen_int_arithmetic, + _gen_int_comparison, + _gen_bool_logic, + _gen_str_concat, + _gen_if_else, + _gen_floor_div, + _gen_modulo, + _gen_negation, + _gen_not, +] + + +def gen_semantic(args): + """Generate typed Python programs with known-true assertions.""" + out = Path(args.output_dir) + out.mkdir(parents=True, exist_ok=True) + + if args.seed is not None: + random.seed(args.seed) + + for i in range(args.max_examples): + # Pick 1-5 random blocks per program + n_blocks = random.randint(1, 5) + blocks = [random.choice(GENERATORS)() for _ in range(n_blocks)] + + # Wrap in a function and call it (matches Strata test convention) + body = "\n".join(blocks) + program = f"def main():\n{body}\nmain()\n" + + p = out / f"fuzz_semantic_{i:04d}.py" + p.write_text(program) + + print(f"Generated {args.max_examples} semantic-mode programs in {out}") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument("--mode", choices=["syntax", "semantic"], required=True) + parser.add_argument("--output-dir", required=True, help="Directory for generated .py files") + parser.add_argument("--max-examples", type=int, default=100) + parser.add_argument("--max-nodes", type=int, default=50, + help="Max AST nodes per program (syntax mode)") + parser.add_argument("--seed", type=int, default=None, + help="Random seed for reproducibility") + args = parser.parse_args() + + if args.mode == "syntax": + gen_syntax(args) + else: + gen_semantic(args) + + +if __name__ == "__main__": + main() diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh new file mode 100755 index 0000000000..01c61b8ebc --- /dev/null +++ b/Tools/Python/scripts/hypothesmith.sh @@ -0,0 +1,210 @@ +#!/bin/bash +# Copyright Strata Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# Fuzz-test Strata's Python front-end with randomly generated programs. +# +# Usage: +# ./hypothesmith.sh [N [SEED [MODE]]] +# +# N Number of programs to generate (default: 10) +# SEED Random seed for reproducibility (default: current timestamp) +# MODE "syntax" or "semantic" or "both" (default: both) +# +# Requires: +# - The venv at Tools/Python/.venv with hypothesmith and strata installed +# - strata built (lake build strata) +# - The Python dialect file at Tools/Python/dialects/Python.dialect.st.ion +# +# Exit codes: +# 0 All tests passed +# 1 At least one test failed (source code is printed for reproduction) + +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" +TOOLS_PY="$REPO_ROOT/Tools/Python" +PYTHON="$TOOLS_PY/.venv/bin/python3" +STRATA="$REPO_ROOT/.lake/build/bin/strata" +DIALECT="$TOOLS_PY/dialects/Python.dialect.st.ion" + +N="${1:-10}" +SEED="${2:-$(date +%s)}" +MODE="${3:-both}" + +# Timeouts (seconds) +PARSE_TIMEOUT=30 +ANALYZE_TIMEOUT=90 + +if [ ! -x "$PYTHON" ]; then + echo "ERROR: Python venv not found at $TOOLS_PY/.venv" + echo "Run: python3 -m venv $TOOLS_PY/.venv && $TOOLS_PY/.venv/bin/pip install -e $TOOLS_PY -e ~/hypothesmith.git" + exit 1 +fi + +if [ ! -f "$STRATA" ]; then + echo "ERROR: strata not built. Run: lake build strata" + exit 1 +fi + +if [ ! -f "$DIALECT" ]; then + echo "ERROR: Python dialect not found at $DIALECT" + exit 1 +fi + +workdir=$(mktemp -d /tmp/strata-fuzz.XXX) +trap 'rm -rf "$workdir"' EXIT + +failures=0 + +run_syntax_tests() { + local gen_dir="$workdir/syntax" + echo "=== Syntax mode: generating $N programs (seed=$SEED) ===" + timeout 120 "$PYTHON" "$SCRIPT_DIR/gen_random_python.py" \ + --mode syntax --output-dir "$gen_dir" \ + --max-examples "$N" --max-nodes 50 --seed "$SEED" 2>&1 + + local count=0 + for pyfile in "$gen_dir"/fuzz_syntax_*.py; do + [ -f "$pyfile" ] || continue + count=$((count + 1)) + local base + base=$(basename "$pyfile" .py) + local ion="$gen_dir/${base}.python.st.ion" + local ion2="$gen_dir/${base}.python.st.ion2" + + # Step 1: Parse Python -> Ion + if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \ + --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then + # Parse failure is acceptable — hypothesmith may generate constructs + # the Strata parser doesn't support yet. Just skip. + echo " SKIP (parse): $base" + continue + fi + + # Step 2: Ion round-trip + if ! timeout "$PARSE_TIMEOUT" "$STRATA" toIon \ + --include "$TOOLS_PY/dialects" "$ion" "$ion2" 2>/dev/null; then + echo " FAIL (toIon): $base" + echo "--- Source code ---" + cat "$pyfile" + echo "---" + failures=$((failures + 1)) + continue + fi + + # Step 3: Diff + if ! "$STRATA" diff --include "$TOOLS_PY/dialects" "$ion" "$ion2" 2>/dev/null; then + echo " FAIL (diff): $base" + echo "--- Source code ---" + cat "$pyfile" + echo "---" + failures=$((failures + 1)) + continue + fi + + echo " OK: $base" + done + echo "Syntax tests: $count processed, $failures failures" +} + +run_semantic_tests() { + local gen_dir="$workdir/semantic" + echo "=== Semantic mode: generating $N programs (seed=$SEED) ===" + "$PYTHON" "$SCRIPT_DIR/gen_random_python.py" \ + --mode semantic --output-dir "$gen_dir" \ + --max-examples "$N" --seed "$SEED" 2>&1 + + local count=0 + local sem_failures=0 + for pyfile in "$gen_dir"/fuzz_semantic_*.py; do + [ -f "$pyfile" ] || continue + count=$((count + 1)) + local base + base=$(basename "$pyfile" .py) + local ion="$gen_dir/${base}.python.st.ion" + + # Step 1: Sanity check — run with CPython to confirm assertions pass + if ! timeout 10 python3 "$pyfile" 2>/dev/null; then + echo " BUG (generator): $base fails under CPython!" + cat "$pyfile" + sem_failures=$((sem_failures + 1)) + continue + fi + + # Step 2: Parse Python -> Ion + if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \ + --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then + echo " FAIL (parse): $base" + echo "--- Source code ---" + cat "$pyfile" + echo "---" + sem_failures=$((sem_failures + 1)) + continue + fi + + # Step 3: Run pyAnalyzeLaurel + local output + local ec=0 + output=$(timeout "$ANALYZE_TIMEOUT" "$STRATA" pyAnalyzeLaurel "$ion" 2>&1) || ec=$? + + if [ $ec -eq 124 ] || [ $ec -eq 137 ]; then + echo " TIMEOUT: $base" + continue + fi + + if [ $ec -ne 0 ]; then + # Non-zero exit from pyAnalyzeLaurel — could be unsupported construct. + # Check if it's an internal error vs. expected limitation. + if echo "$output" | grep -qi "panic\|internal\|assertion.*failed\|LEAK"; then + echo " FAIL (internal error): $base" + echo "--- Source code ---" + cat "$pyfile" + echo "--- Output ---" + echo "$output" | head -20 + echo "---" + sem_failures=$((sem_failures + 1)) + continue + fi + echo " SKIP (unsupported): $base" + continue + fi + + # Step 4: Check that all assertions passed (no "failed" in DETAIL line) + if echo "$output" | grep -qE '[1-9][0-9]* failed'; then + echo " FAIL (verification): $base" + echo " Strata reports a failing assertion on a program that CPython runs correctly." + echo " This indicates a semantic modelling bug in the Python-to-Core pipeline." + echo "--- Source code ---" + cat "$pyfile" + echo "--- pyAnalyzeLaurel output ---" + echo "$output" + echo "---" + sem_failures=$((sem_failures + 1)) + continue + fi + + echo " OK: $base" + done + failures=$((failures + sem_failures)) + echo "Semantic tests: $count processed, $sem_failures failures" +} + +echo "Strata Python front-end fuzz test" +echo "Seed: $SEED N: $N Mode: $MODE" +echo "" + +case "$MODE" in + syntax) run_syntax_tests ;; + semantic) run_semantic_tests ;; + both) run_syntax_tests; echo ""; run_semantic_tests ;; + *) echo "Unknown mode: $MODE"; exit 1 ;; +esac + +echo "" +if [ $failures -ne 0 ]; then + echo "FAILED: $failures failure(s). Seed was: $SEED" + exit 1 +fi +echo "ALL PASSED. Seed was: $SEED" From 04b87e60986e0e0086bbc9ca61e1710106acdf3c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Apr 2026 18:38:52 +0000 Subject: [PATCH 02/13] Add --unrestricted mode for Python fuzz testing Adds gen_unrestricted.py with ~60 generators covering Python constructs well beyond what Strata supports today: - Bitwise ops (&, |, ^, ~, <<, >>), power (**) - Augmented assignment (+=, -=, *=) - List ops (index, slice, append, concat, in, comprehensions) - Dict ops (create, access, in, comprehensions) - String methods (upper, lower, strip, len, index, multiply, format) - For loops (over lists, range), while loops, break, nested loops - Nested if, elif chains, ternary expressions - Tuple unpacking, star unpacking, chained comparisons - None checks, Optional types - Classes (fields, methods), nested function calls - Lambda, list/dict comprehensions - Try/except/else/finally, multiple except clauses, raise - With statement (context managers) - Nonlocal, walrus operator (:=), f-strings - Type conversions (int, str, bool, float, list) - isinstance, recursion, default args, *args, **kwargs - Generators (yield), decorators, async/await - Match statement (Python 3.10+) Usage: ./scripts/hypothesmith.sh 20 42 semantic --unrestricted Programs that hit unsupported Strata constructs are reported as SKIP. Only true internal errors (panics) or semantic mismatches (Strata rejects a CPython-passing assertion) count as failures. Co-authored-by: Kiro --- Tools/Python/scripts/gen_random_python.py | 24 +- Tools/Python/scripts/gen_unrestricted.py | 715 ++++++++++++++++++++++ Tools/Python/scripts/hypothesmith.sh | 14 +- 3 files changed, 748 insertions(+), 5 deletions(-) create mode 100644 Tools/Python/scripts/gen_unrestricted.py diff --git a/Tools/Python/scripts/gen_random_python.py b/Tools/Python/scripts/gen_random_python.py index 3aa66a2b31..7699e3d362 100644 --- a/Tools/Python/scripts/gen_random_python.py +++ b/Tools/Python/scripts/gen_random_python.py @@ -15,6 +15,12 @@ --max-examples N Number of Hypothesis examples to try (default: 100). --max-nodes N Filter: discard programs with more than N AST nodes (default: 50). --seed S Fixed Hypothesis seed for reproducibility. + +Options: + --unrestricted Include generators for Python constructs that may be + beyond what Strata supports today (classes, generators, + comprehensions, try/except, match, async, decorators, + etc.). Useful for discovering gaps in Strata's coverage. """ import argparse @@ -207,6 +213,18 @@ def _gen_not(): ] +def _get_generators(unrestricted): + if not unrestricted: + return GENERATORS + import importlib.util, os + spec = importlib.util.spec_from_file_location( + "gen_unrestricted", + os.path.join(os.path.dirname(__file__), "gen_unrestricted.py")) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return GENERATORS + mod.UNRESTRICTED_GENERATORS + + def gen_semantic(args): """Generate typed Python programs with known-true assertions.""" out = Path(args.output_dir) @@ -215,10 +233,12 @@ def gen_semantic(args): if args.seed is not None: random.seed(args.seed) + generators = _get_generators(args.unrestricted) + for i in range(args.max_examples): # Pick 1-5 random blocks per program n_blocks = random.randint(1, 5) - blocks = [random.choice(GENERATORS)() for _ in range(n_blocks)] + blocks = [random.choice(generators)() for _ in range(n_blocks)] # Wrap in a function and call it (matches Strata test convention) body = "\n".join(blocks) @@ -240,6 +260,8 @@ def main(): help="Max AST nodes per program (syntax mode)") parser.add_argument("--seed", type=int, default=None, help="Random seed for reproducibility") + parser.add_argument("--unrestricted", action="store_true", + help="Include generators beyond what Strata supports today") args = parser.parse_args() if args.mode == "syntax": diff --git a/Tools/Python/scripts/gen_unrestricted.py b/Tools/Python/scripts/gen_unrestricted.py new file mode 100644 index 0000000000..115a217df4 --- /dev/null +++ b/Tools/Python/scripts/gen_unrestricted.py @@ -0,0 +1,715 @@ +"""Unrestricted Python program generators for fuzz testing. + +These generators produce constructs that may be beyond what Strata supports +today. Used when --unrestricted is passed to gen_random_python.py. +""" + +import random + +def _rand_int(): + return random.randint(-100, 100) + +def _rand_bool(): + return random.choice([True, False]) + +def _rand_str(): + return random.choice(["hello", "world", "foo", "bar", "", "abc", "x"]) + +def _nonzero(): + return random.choice([x for x in range(-10, 11) if x != 0]) + +def _rand_var(prefix="v"): + return f"{prefix}{random.randint(0, 99)}" + +# --- Bitwise operations --- + +def gen_bitwise(): + a, b = _rand_int(), _rand_int() + op, sym = random.choice([("and", "&"), ("or", "|"), ("xor", "^")]) + r = eval(f"{a} {sym} {b}") + return f" assert ({a} {sym} {b}) == {r}, \"bitwise {op}\"\n" + +def gen_shift(): + a = random.randint(0, 100) + b = random.randint(0, 8) + op, sym = random.choice([("lshift", "<<"), ("rshift", ">>")]) + r = eval(f"{a} {sym} {b}") + return f" assert ({a} {sym} {b}) == {r}, \"{op}\"\n" + +def gen_bitnot(): + a = _rand_int() + return f" assert ~{a} == {~a}, \"bitnot\"\n" + +# --- Power --- + +def gen_power(): + base = random.randint(0, 5) + exp = random.randint(0, 4) + r = base ** exp + return f" assert {base} ** {exp} == {r}, \"power\"\n" + +# --- Augmented assignment --- + +def gen_augmented_assign(): + a = _rand_int() + b = _rand_int() + op, sym = random.choice([("+", "+="), ("-", "-="), ("*", "*=")]) + r = eval(f"{a} {op} {b}") + return ( + f" x: int = {a}\n" + f" x {sym} {b}\n" + f' assert x == {r}, "augmented {sym}"\n' + ) + +# --- Ternary expression --- + +def gen_ternary(): + cond = _rand_bool() + a, b = _rand_int(), _rand_int() + r = a if cond else b + return f" assert ({a} if {cond} else {b}) == {r}, \"ternary\"\n" + +# --- Multiple assignment / swap --- + +def gen_multi_assign(): + a, b = _rand_int(), _rand_int() + return ( + f" x: int = {a}\n" + f" y: int = {b}\n" + f" x, y = y, x\n" + f' assert x == {b} and y == {a}, "swap"\n' + ) + +# --- List operations --- + +def gen_list_create(): + elems = [_rand_int() for _ in range(random.randint(1, 5))] + return ( + f" lst: list = {elems}\n" + f' assert len(lst) == {len(elems)}, "list len"\n' + ) + +def gen_list_index(): + elems = [_rand_int() for _ in range(random.randint(2, 5))] + idx = random.randint(0, len(elems) - 1) + return ( + f" lst: list = {elems}\n" + f' assert lst[{idx}] == {elems[idx]}, "list index"\n' + ) + +def gen_list_concat(): + a = [_rand_int() for _ in range(random.randint(1, 3))] + b = [_rand_int() for _ in range(random.randint(1, 3))] + return ( + f" a: list = {a}\n" + f" b: list = {b}\n" + f' assert a + b == {a + b}, "list concat"\n' + ) + +def gen_list_slice(): + elems = [_rand_int() for _ in range(random.randint(3, 6))] + i = random.randint(0, len(elems) - 2) + j = random.randint(i + 1, len(elems)) + return ( + f" lst: list = {elems}\n" + f' assert lst[{i}:{j}] == {elems[i:j]}, "list slice"\n' + ) + +def gen_list_in(): + elems = [_rand_int() for _ in range(random.randint(2, 5))] + target = random.choice(elems) + return ( + f" lst: list = {elems}\n" + f' assert {target} in lst, "list in"\n' + ) + +def gen_list_append(): + elems = [_rand_int() for _ in range(random.randint(1, 3))] + v = _rand_int() + return ( + f" lst: list = {elems}\n" + f" lst.append({v})\n" + f' assert lst == {elems + [v]}, "list append"\n' + ) + +# --- Dict operations --- + +def gen_dict_create(): + keys = random.sample(["a", "b", "c", "d", "e"], random.randint(1, 4)) + d = {k: _rand_int() for k in keys} + return ( + f" d: dict = {d}\n" + f' assert len(d) == {len(d)}, "dict len"\n' + ) + +def gen_dict_access(): + keys = random.sample(["a", "b", "c", "d"], random.randint(2, 4)) + d = {k: _rand_int() for k in keys} + k = random.choice(keys) + return ( + f" d: dict = {d}\n" + f' assert d[{k!r}] == {d[k]}, "dict access"\n' + ) + +def gen_dict_in(): + keys = random.sample(["a", "b", "c", "d"], random.randint(2, 4)) + d = {k: _rand_int() for k in keys} + k = random.choice(keys) + return ( + f" d: dict = {d}\n" + f' assert {k!r} in d, "dict in"\n' + ) + +# --- String operations --- + +def gen_str_len(): + s = _rand_str() + return f' assert len({s!r}) == {len(s)}, "str len"\n' + +def gen_str_index(): + s = random.choice(["hello", "world", "foobar", "abc"]) + i = random.randint(0, len(s) - 1) + return f' assert {s!r}[{i}] == {s[i]!r}, "str index"\n' + +def gen_str_multiply(): + s = random.choice(["ab", "x", "hi"]) + n = random.randint(0, 4) + return f' assert {s!r} * {n} == {(s * n)!r}, "str mul"\n' + +def gen_str_methods(): + s = random.choice(["Hello", "WORLD", "foo Bar", "abc"]) + method = random.choice(["upper", "lower", "strip"]) + r = getattr(s, method)() + return f' assert {s!r}.{method}() == {r!r}, "str {method}"\n' + +# --- For loops --- + +def gen_for_sum(): + elems = [random.randint(0, 20) for _ in range(random.randint(2, 5))] + return ( + f" total: int = 0\n" + f" for x in {elems}:\n" + f" total = total + x\n" + f' assert total == {sum(elems)}, "for sum"\n' + ) + +def gen_for_range(): + n = random.randint(1, 10) + return ( + f" total: int = 0\n" + f" for i in range({n}):\n" + f" total = total + i\n" + f' assert total == {sum(range(n))}, "for range"\n' + ) + +# --- While loops --- + +def gen_while_countdown(): + n = random.randint(1, 10) + return ( + f" n: int = {n}\n" + f" count: int = 0\n" + f" while n > 0:\n" + f" count = count + 1\n" + f" n = n - 1\n" + f' assert count == {n}, "while countdown"\n' + ) + +# --- Break / continue --- + +def gen_break(): + elems = list(range(1, random.randint(4, 8))) + stop = random.choice(elems[1:]) + expected = sum(x for x in elems if x < stop) + return ( + f" total: int = 0\n" + f" for x in {elems}:\n" + f" if x == {stop}:\n" + f" break\n" + f" total = total + x\n" + f' assert total == {expected}, "break"\n' + ) + +# --- Nested if --- + +def gen_nested_if(): + a, b = _rand_int(), _rand_int() + if a > 0: + if b > 0: + r = 1 + else: + r = 2 + else: + r = 3 + return ( + f" a: int = {a}\n" + f" b: int = {b}\n" + f" if a > 0:\n" + f" if b > 0:\n" + f" r: int = 1\n" + f" else:\n" + f" r: int = 2\n" + f" else:\n" + f" r: int = 3\n" + f' assert r == {r}, "nested if"\n' + ) + +# --- Elif chains --- + +def gen_elif(): + a = _rand_int() + if a > 0: + r = "pos" + elif a < 0: + r = "neg" + else: + r = "zero" + return ( + f" a: int = {a}\n" + f" if a > 0:\n" + f" r: str = \"pos\"\n" + f" elif a < 0:\n" + f" r: str = \"neg\"\n" + f" else:\n" + f" r: str = \"zero\"\n" + f' assert r == {r!r}, "elif"\n' + ) + +# --- Multiple return values / tuple unpacking --- + +def gen_tuple_unpack(): + a, b, c = _rand_int(), _rand_int(), _rand_int() + return ( + f" a, b, c = {a}, {b}, {c}\n" + f' assert a == {a} and b == {b} and c == {c}, "tuple unpack"\n' + ) + +# --- Chained comparisons --- + +def gen_chained_cmp(): + a, b, c = sorted([_rand_int() for _ in range(3)]) + return f' assert {a} <= {b} <= {c}, "chained cmp"\n' + +# --- None checks --- + +def gen_none_check(): + use_none = _rand_bool() + val = "None" if use_none else str(_rand_int()) + is_none = use_none + return ( + f" x = {val}\n" + f' assert (x is None) == {is_none}, "none check"\n' + ) + +# --- Optional type --- + +def gen_optional(): + from typing import Optional + use_none = _rand_bool() + if use_none: + return ( + f" from typing import Optional\n" + f" x: Optional[int] = None\n" + f' assert x is None, "optional none"\n' + ) + else: + v = _rand_int() + return ( + f" from typing import Optional\n" + f" x: Optional[int] = {v}\n" + f' assert x == {v}, "optional value"\n' + ) + +# --- Classes --- + +def gen_class_basic(): + x = _rand_int() + return ( + f" class Pt:\n" + f" def __init__(self):\n" + f" self.x: int = {x}\n" + f" p = Pt()\n" + f' assert p.x == {x}, "class field"\n' + ) + +def gen_class_method(): + a, b = _rand_int(), _rand_int() + return ( + f" class Adder:\n" + f" def __init__(self):\n" + f" self.val: int = {a}\n" + f" def add(self, n: int) -> int:\n" + f" return self.val + n\n" + f" obj = Adder()\n" + f' assert obj.add({b}) == {a + b}, "class method"\n' + ) + +# --- Nested function calls --- + +def gen_nested_call(): + a, b = _rand_int(), _rand_int() + return ( + f" def add(x: int, y: int) -> int:\n" + f" return x + y\n" + f" def double(x: int) -> int:\n" + f" return x * 2\n" + f' assert double(add({a}, {b})) == {(a + b) * 2}, "nested call"\n' + ) + +# --- Lambda --- + +def gen_lambda(): + a, b = _rand_int(), _rand_int() + return ( + f" f = lambda x, y: x + y\n" + f' assert f({a}, {b}) == {a + b}, "lambda"\n' + ) + +# --- List comprehension --- + +def gen_list_comp(): + n = random.randint(2, 6) + return ( + f" lst = [x * 2 for x in range({n})]\n" + f' assert lst == {[x * 2 for x in range(n)]}, "list comp"\n' + ) + +def gen_list_comp_filter(): + n = random.randint(3, 8) + return ( + f" lst = [x for x in range({n}) if x % 2 == 0]\n" + f' assert lst == {[x for x in range(n) if x % 2 == 0]}, "list comp filter"\n' + ) + +# --- Dict comprehension --- + +def gen_dict_comp(): + n = random.randint(2, 5) + expected = {str(i): i * i for i in range(n)} + return ( + f" d = {{str(i): i * i for i in range({n})}}\n" + f' assert d == {expected}, "dict comp"\n' + ) + +# --- Try/except --- + +def gen_try_except(): + return ( + f" caught: bool = False\n" + f" try:\n" + f" x: int = 1 // 0\n" + f" except ZeroDivisionError:\n" + f" caught = True\n" + f' assert caught, "try except"\n' + ) + +def gen_try_except_else(): + return ( + f" result: int = 0\n" + f" try:\n" + f" result = 42\n" + f" except Exception:\n" + f" result = -1\n" + f" else:\n" + f" result = result + 1\n" + f' assert result == 43, "try else"\n' + ) + +def gen_try_finally(): + return ( + f" cleanup: bool = False\n" + f" try:\n" + f" x: int = 10\n" + f" finally:\n" + f" cleanup = True\n" + f' assert cleanup, "try finally"\n' + ) + +# --- With statement (context manager) --- + +def gen_with_stmt(): + # Use a simple class-based context manager + return ( + f" class CM:\n" + f" def __enter__(self):\n" + f" return 42\n" + f" def __exit__(self, *args):\n" + f" pass\n" + f" with CM() as v:\n" + f" r: int = v\n" + f' assert r == 42, "with stmt"\n' + ) + +# --- Global / nonlocal --- + +def gen_nonlocal(): + return ( + f" x: int = 0\n" + f" def inner():\n" + f" nonlocal x\n" + f" x = 99\n" + f" inner()\n" + f' assert x == 99, "nonlocal"\n' + ) + +# --- Walrus operator --- + +def gen_walrus(): + v = _rand_int() + return ( + f" lst = [{v}]\n" + f" if (n := len(lst)) > 0:\n" + f' assert n == 1, "walrus"\n' + ) + +# --- F-strings --- + +def gen_fstring(): + a = random.randint(0, 50) + return f' assert f"val={{{a}}}" == "val={a}", "fstring"\n' + +# --- Star unpacking --- + +def gen_star_unpack(): + elems = [_rand_int() for _ in range(random.randint(3, 5))] + return ( + f" first, *rest = {elems}\n" + f' assert first == {elems[0]}, "star unpack first"\n' + f' assert rest == {elems[1:]}, "star unpack rest"\n' + ) + +# --- Nested loops --- + +def gen_nested_loop(): + n, m = random.randint(1, 4), random.randint(1, 4) + return ( + f" total: int = 0\n" + f" for i in range({n}):\n" + f" for j in range({m}):\n" + f" total = total + 1\n" + f' assert total == {n * m}, "nested loop"\n' + ) + +# --- Type conversions --- + +def gen_type_conv(): + conv = random.choice([ + ("int(3.7)", 3, "float to int"), + ("str(42)", "42", "int to str"), + ("int('17')", 17, "str to int"), + ("bool(0)", False, "int to bool false"), + ("bool(1)", True, "int to bool true"), + ("float(5)", 5.0, "int to float"), + ("list(range(3))", [0, 1, 2], "range to list"), + ]) + expr, expected, label = conv + return f' assert {expr} == {expected!r}, "{label}"\n' + +# --- String formatting --- + +def gen_str_format(): + a = _rand_int() + return f' assert "x={{}}".format({a}) == "x={a}", "str format"\n' + +# --- Multiple except clauses --- + +def gen_multi_except(): + return ( + f" result: str = \"\"\n" + f" try:\n" + f" x = 1 // 0\n" + f" except TypeError:\n" + f" result = \"type\"\n" + f" except ZeroDivisionError:\n" + f" result = \"zero\"\n" + f' assert result == "zero", "multi except"\n' + ) + +# --- Raise / re-raise --- + +def gen_raise(): + return ( + f" caught: bool = False\n" + f" try:\n" + f" raise ValueError(\"test\")\n" + f" except ValueError as e:\n" + f" caught = True\n" + f' assert str(e) == "test", "raise msg"\n' + f' assert caught, "raise caught"\n' + ) + +# --- Pass statement --- + +def gen_pass(): + return ( + f" if True:\n" + f" pass\n" + f' assert True, "pass"\n' + ) + +# --- Delete --- + +def gen_del(): + return ( + f" lst = [1, 2, 3]\n" + f" del lst[1]\n" + f' assert lst == [1, 3], "del"\n' + ) + +# --- Set operations --- + +def gen_set_ops(): + a = list(set([random.randint(0, 10) for _ in range(4)])) + b = list(set([random.randint(0, 10) for _ in range(4)])) + sa, sb = set(a), set(b) + op = random.choice(["union", "intersection"]) + if op == "union": + r = sorted(sa | sb) + return f" assert sorted(set({a}) | set({b})) == {r}, \"set {op}\"\n" + else: + r = sorted(sa & sb) + return f" assert sorted(set({a}) & set({b})) == {r}, \"set {op}\"\n" + +# --- Isinstance --- + +def gen_isinstance(): + return random.choice([ + f' assert isinstance(42, int), "isinstance int"\n', + f' assert isinstance("hi", str), "isinstance str"\n', + f' assert isinstance(True, bool), "isinstance bool"\n', + f' assert isinstance([1], list), "isinstance list"\n', + f' assert not isinstance(42, str), "isinstance neg"\n', + ]) + +# --- Recursive function --- + +def gen_recursion(): + n = random.randint(1, 8) + def fact(n): + return 1 if n <= 1 else n * fact(n - 1) + return ( + f" def factorial(n: int) -> int:\n" + f" if n <= 1:\n" + f" return 1\n" + f" return n * factorial(n - 1)\n" + f' assert factorial({n}) == {fact(n)}, "recursion"\n' + ) + +# --- Default arguments --- + +def gen_default_args(): + d = _rand_int() + return ( + f" def f(x: int, y: int = {d}) -> int:\n" + f" return x + y\n" + f' assert f(10) == {10 + d}, "default arg"\n' + f' assert f(10, 20) == 30, "override default"\n' + ) + +# --- *args / **kwargs --- + +def gen_varargs(): + return ( + f" def f(*args):\n" + f" return sum(args)\n" + f' assert f(1, 2, 3) == 6, "varargs"\n' + ) + +def gen_kwargs(): + return ( + f" def f(**kwargs):\n" + f" return kwargs.get(\"x\", 0)\n" + f' assert f(x=42) == 42, "kwargs"\n' + ) + +# --- Yield / generator --- + +def gen_generator(): + n = random.randint(2, 5) + return ( + f" def gen():\n" + f" for i in range({n}):\n" + f" yield i\n" + f' assert list(gen()) == {list(range(n))}, "generator"\n' + ) + +# --- Decorator --- + +def gen_decorator(): + return ( + f" def my_dec(fn):\n" + f" def wrapper(*a):\n" + f" return fn(*a) + 1\n" + f" return wrapper\n" + f" @my_dec\n" + f" def f(x: int) -> int:\n" + f" return x\n" + f' assert f(10) == 11, "decorator"\n' + ) + +# --- Async (syntax only, not awaited) --- + +def gen_async_def(): + return ( + f" import asyncio\n" + f" async def coro():\n" + f" return 42\n" + f' assert asyncio.run(coro()) == 42, "async"\n' + ) + +# --- Walrus in while --- + +def gen_walrus_while(): + return ( + f" data = [1, 2, 3, 0, 4]\n" + f" total: int = 0\n" + f" idx: int = 0\n" + f" while (v := data[idx]) != 0:\n" + f" total = total + v\n" + f" idx = idx + 1\n" + f' assert total == 6, "walrus while"\n' + ) + +# --- Match statement (Python 3.10+) --- + +def gen_match(): + v = random.choice([1, 2, 3, "other"]) + if v == 1: + r = "one" + elif v == 2: + r = "two" + else: + r = "other" + return ( + f" val = {v!r}\n" + f" match val:\n" + f" case 1:\n" + f" r = \"one\"\n" + f" case 2:\n" + f" r = \"two\"\n" + f" case _:\n" + f" r = \"other\"\n" + f' assert r == {r!r}, "match"\n' + ) + + +UNRESTRICTED_GENERATORS = [ + gen_bitwise, gen_shift, gen_bitnot, gen_power, + gen_augmented_assign, gen_ternary, gen_multi_assign, + gen_list_create, gen_list_index, gen_list_concat, gen_list_slice, + gen_list_in, gen_list_append, + gen_dict_create, gen_dict_access, gen_dict_in, + gen_str_len, gen_str_index, gen_str_multiply, gen_str_methods, + gen_for_sum, gen_for_range, gen_while_countdown, gen_break, + gen_nested_if, gen_elif, gen_tuple_unpack, gen_chained_cmp, + gen_none_check, gen_optional, + gen_class_basic, gen_class_method, gen_nested_call, + gen_lambda, gen_list_comp, gen_list_comp_filter, gen_dict_comp, + gen_try_except, gen_try_except_else, gen_try_finally, + gen_with_stmt, gen_nonlocal, gen_walrus, gen_fstring, + gen_star_unpack, gen_nested_loop, gen_type_conv, gen_str_format, + gen_multi_except, gen_raise, gen_pass, gen_del, gen_set_ops, + gen_isinstance, gen_recursion, gen_default_args, + gen_varargs, gen_kwargs, gen_generator, gen_decorator, + gen_async_def, gen_walrus_while, gen_match, +] diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index 01c61b8ebc..68343224a2 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -5,11 +5,12 @@ # Fuzz-test Strata's Python front-end with randomly generated programs. # # Usage: -# ./hypothesmith.sh [N [SEED [MODE]]] +# ./hypothesmith.sh [N [SEED [MODE [--unrestricted]]]] # # N Number of programs to generate (default: 10) # SEED Random seed for reproducibility (default: current timestamp) # MODE "syntax" or "semantic" or "both" (default: both) +# --unrestricted Include Python constructs beyond what Strata supports today # # Requires: # - The venv at Tools/Python/.venv with hypothesmith and strata installed @@ -32,6 +33,10 @@ DIALECT="$TOOLS_PY/dialects/Python.dialect.st.ion" N="${1:-10}" SEED="${2:-$(date +%s)}" MODE="${3:-both}" +UNRESTRICTED="" +if [ "${4:-}" = "--unrestricted" ]; then + UNRESTRICTED="--unrestricted" +fi # Timeouts (seconds) PARSE_TIMEOUT=30 @@ -114,7 +119,7 @@ run_semantic_tests() { echo "=== Semantic mode: generating $N programs (seed=$SEED) ===" "$PYTHON" "$SCRIPT_DIR/gen_random_python.py" \ --mode semantic --output-dir "$gen_dir" \ - --max-examples "$N" --seed "$SEED" 2>&1 + --max-examples "$N" --seed "$SEED" $UNRESTRICTED 2>&1 local count=0 local sem_failures=0 @@ -157,7 +162,7 @@ run_semantic_tests() { if [ $ec -ne 0 ]; then # Non-zero exit from pyAnalyzeLaurel — could be unsupported construct. # Check if it's an internal error vs. expected limitation. - if echo "$output" | grep -qi "panic\|internal\|assertion.*failed\|LEAK"; then + if echo "$output" | grep -qi "panic\|LEAK"; then echo " FAIL (internal error): $base" echo "--- Source code ---" cat "$pyfile" @@ -167,6 +172,7 @@ run_semantic_tests() { sem_failures=$((sem_failures + 1)) continue fi + # Translation failures and other non-zero exits are unsupported constructs echo " SKIP (unsupported): $base" continue fi @@ -192,7 +198,7 @@ run_semantic_tests() { } echo "Strata Python front-end fuzz test" -echo "Seed: $SEED N: $N Mode: $MODE" +echo "Seed: $SEED N: $N Mode: $MODE Unrestricted: ${UNRESTRICTED:-no}" echo "" case "$MODE" in From 0186a62d2827b5ea6830f6d30c59c18024fac316 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Apr 2026 18:50:47 +0000 Subject: [PATCH 03/13] Add CI workflow for Python front-end fuzz testing Runs on every PR (not merge queue or push to main). For each run: 1. Picks a fresh random seed (reported in step name and logs) 2. Generates 10 programs in both syntax and semantic modes with --unrestricted (covering constructs beyond current Strata support) 3. On failure, checks out the merge base and re-runs with the same seed: - If merge base also fails: creates a GitHub issue labeled 'fuzz-bug' (pre-existing bug, PR is not blocked) - If merge base passes: CI fails with reproduction instructions (the PR introduced a regression) - If merge base can't build: CI fails as inconclusive The seed is always reported so failures can be reproduced locally: cd Tools/Python ./scripts/hypothesmith.sh 10 both --unrestricted Co-authored-by: Kiro --- .github/workflows/python-fuzz.yml | 183 ++++++++++++++++++++++++++++++ 1 file changed, 183 insertions(+) create mode 100644 .github/workflows/python-fuzz.yml diff --git a/.github/workflows/python-fuzz.yml b/.github/workflows/python-fuzz.yml new file mode 100644 index 0000000000..56e395706e --- /dev/null +++ b/.github/workflows/python-fuzz.yml @@ -0,0 +1,183 @@ +name: Python Fuzz + +on: + pull_request: + branches: [main] + +jobs: + fuzz_python: + name: Fuzz-test Python front-end + runs-on: ubuntu-latest + permissions: + contents: read + issues: write + steps: + - name: Checkout PR + uses: actions/checkout@v6 + with: + fetch-depth: 0 + + - name: Pick random seed + id: seed + run: echo "value=$(date +%s%N | cut -c1-10)" >> $GITHUB_OUTPUT + + - name: Install cvc5 + shell: bash + run: | + ARCH=$(uname -m) + if [ "$ARCH" = "x86_64" ]; then ARCH_NAME="x86_64" + elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then ARCH_NAME="arm64" + else echo "Unsupported architecture: $ARCH"; exit 1; fi + wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip + unzip -q cvc5-Linux-${ARCH_NAME}-static.zip + chmod +x cvc5-Linux-${ARCH_NAME}-static/bin/cvc5 + echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> $GITHUB_PATH + + - name: Restore lake cache + uses: actions/cache/restore@v5 + with: + path: .lake + key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }} + restore-keys: | + lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.st') }} + lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }} + lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }} + + - name: Build Strata executables + uses: leanprover/lean-action@v1 + with: + use-github-cache: false + build-args: 'strata:exe strata' + + - uses: actions/setup-python@v6 + with: + python-version: '3.14' + + - name: Install Python dependencies + run: | + python -m venv Tools/Python/.venv + Tools/Python/.venv/bin/pip install --quiet -e Tools/Python + Tools/Python/.venv/bin/pip install --quiet hypothesmith + + - name: Run fuzz tests on PR (seed=${{ steps.seed.outputs.value }}) + id: fuzz_pr + working-directory: Tools/Python + run: | + echo "::group::Fuzz test output" + set +e + ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted 2>&1 | tee /tmp/fuzz_pr.log + echo "exit_code=${PIPESTATUS[0]}" >> $GITHUB_OUTPUT + echo "::endgroup::" + + - name: Analyse failure against merge base + id: analyse + if: steps.fuzz_pr.outputs.exit_code != '0' + run: | + echo "PR fuzz tests failed with seed ${{ steps.seed.outputs.value }}" + echo "" + + # Save the fuzz scripts from the PR branch — they may not exist at the merge base + cp -r Tools/Python/scripts /tmp/fuzz_scripts + + # Check out the merge base and re-run with the same seed + MERGE_BASE=$(git merge-base HEAD origin/${{ github.base_ref }}) + echo "Merge base: $MERGE_BASE" + git checkout "$MERGE_BASE" + + # Restore the fuzz scripts into the merge-base tree + cp /tmp/fuzz_scripts/gen_random_python.py Tools/Python/scripts/ + cp /tmp/fuzz_scripts/gen_unrestricted.py Tools/Python/scripts/ + cp /tmp/fuzz_scripts/hypothesmith.sh Tools/Python/scripts/ + chmod +x Tools/Python/scripts/hypothesmith.sh + + # Rebuild strata at merge base (only executables, skip proofs) + # This may fail if the toolchain changed significantly; treat that as inconclusive. + if ! lake build strata:exe strata 2>&1 | tail -10; then + echo "result=inconclusive" >> $GITHUB_OUTPUT + echo "⚠️ Could not build merge base. Cannot determine if this is a regression." + exit 0 + fi + + echo "::group::Merge-base fuzz test output" + set +e + cd Tools/Python + ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted 2>&1 | tee /tmp/fuzz_base.log + BASE_EXIT=${PIPESTATUS[0]} + echo "::endgroup::" + + if [ $BASE_EXIT -ne 0 ]; then + echo "result=pre-existing" >> $GITHUB_OUTPUT + echo "" + echo "⚠️ Merge base ALSO fails with the same seed." + echo "This is a pre-existing bug, not a regression from this PR." + else + echo "result=regression" >> $GITHUB_OUTPUT + echo "" + echo "❌ Merge base passes but PR fails." + echo "This PR introduced a regression." + fi + + - name: Create issue for pre-existing bug + if: steps.analyse.outputs.result == 'pre-existing' + uses: actions/github-script@v7 + with: + script: | + const seed = '${{ steps.seed.outputs.value }}'; + const title = `[fuzz] Pre-existing Python front-end bug (seed ${seed})`; + // Check for duplicate issues + const existing = await github.rest.issues.listForRepo({ + owner: context.repo.owner, + repo: context.repo.repo, + state: 'open', + labels: 'fuzz-bug', + per_page: 100, + }); + if (existing.data.some(i => i.title.includes(`seed ${seed}`))) { + console.log('Issue already exists for this seed, skipping.'); + return; + } + await github.rest.issues.create({ + owner: context.repo.owner, + repo: context.repo.repo, + title: title, + labels: ['fuzz-bug'], + body: [ + `A fuzz test found a pre-existing failure in the Python front-end.`, + ``, + `**Seed:** \`${seed}\``, + `**PR:** #${context.issue.number}`, + `**Merge base also fails:** yes`, + ``, + `### Reproduce`, + `\`\`\`bash`, + `cd Tools/Python`, + `./scripts/hypothesmith.sh 10 ${seed} both --unrestricted`, + `\`\`\``, + ``, + `This bug exists on \`main\` and was not introduced by the PR.`, + ].join('\n'), + }); + + - name: Fail if PR introduced a regression + if: steps.analyse.outputs.result == 'regression' + run: | + echo "::error::Fuzz test regression detected (seed=${{ steps.seed.outputs.value }}). The merge base passes but this PR fails." + echo "" + echo "Reproduce locally:" + echo " cd Tools/Python" + echo " ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted" + exit 1 + + - name: Fail if analysis was inconclusive + if: steps.analyse.outputs.result == 'inconclusive' + run: | + echo "::warning::Fuzz test failed (seed=${{ steps.seed.outputs.value }}) but could not build merge base to determine if this is a regression." + echo "" + echo "Reproduce locally:" + echo " cd Tools/Python" + echo " ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted" + exit 1 + + - name: Report seed on success + if: steps.fuzz_pr.outputs.exit_code == '0' + run: echo "✅ All fuzz tests passed (seed=${{ steps.seed.outputs.value }})" From 47a4eb0d74393bffd7d0d4ac9929d816ca5a7e86 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Apr 2026 18:58:25 +0000 Subject: [PATCH 04/13] Add extensive documentation to fuzz testing scripts and CI workflow All four files now include thorough documentation: - python-fuzz.yml: Header block explaining the trigger policy, test modes, failure analysis flow (with ASCII diagram), reproducibility, and file inventory. Each step has inline comments explaining its purpose. - hypothesmith.sh: Full header documenting background/motivation, both test modes, result classification (OK/SKIP/TIMEOUT/FAIL with subtypes), reproducibility, usage, prerequisites, and exit codes. Inline comments on each pipeline step. - gen_random_python.py: Module docstring covering both modes, generator categories (base vs unrestricted), reproducibility mechanism, usage examples, and all CLI options. Section headers and docstrings on all functions. - gen_unrestricted.py: Module docstring with categorised inventory of all ~60 generators, instructions for adding new generators, and section headers grouping generators by category. Co-authored-by: Kiro --- .github/workflows/python-fuzz.yml | 138 +++++++++++++- Tools/Python/scripts/gen_random_python.py | 209 ++++++++++++++++------ Tools/Python/scripts/gen_unrestricted.py | 104 ++++++++++- Tools/Python/scripts/hypothesmith.sh | 179 +++++++++++++++--- 4 files changed, 542 insertions(+), 88 deletions(-) diff --git a/.github/workflows/python-fuzz.yml b/.github/workflows/python-fuzz.yml index 56e395706e..84c909ac6b 100644 --- a/.github/workflows/python-fuzz.yml +++ b/.github/workflows/python-fuzz.yml @@ -1,3 +1,92 @@ +# Copyright Strata Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# ============================================================================= +# Python Front-End Fuzz Testing +# ============================================================================= +# +# This workflow fuzz-tests Strata's Python front-end by generating random +# Python programs and running them through the Strata pipeline. It is inspired +# by CBMC's use of CSmith (see .github/workflows/csmith.yaml in the CBMC +# repository) and by the hypothesmith project (https://github.com/Zac-HD/ +# hypothesmith), which generates syntactically valid Python programs using +# the Hypothesis property-based testing framework. +# +# ## Trigger +# +# Runs on pull_request only — not on merge_group or push to main. This is +# intentional: fuzz tests are non-deterministic and are meant to catch +# regressions in PRs, not to gate merges or post-merge builds. +# +# ## What it tests +# +# Two modes run in sequence: +# +# 1. **Syntax mode** — Uses hypothesmith to generate syntactically valid +# Python from the grammar. Each program is parsed into Strata's Ion +# format, round-tripped through `strata toIon`, and diffed. This tests +# that the parser pipeline doesn't crash on arbitrary valid Python. +# +# 2. **Semantic mode** — Uses a custom generator to produce typed Python +# programs with assertions whose expected values are computed by CPython +# at generation time (analogous to CSmith computing a checksum). Each +# program is first validated with CPython, then run through +# `pyAnalyzeLaurel`. If Strata reports a failing assertion on a program +# that CPython runs correctly, that's a semantic modelling bug. +# +# The `--unrestricted` flag is used, which includes generators for Python +# constructs beyond what Strata supports today (classes, generators, +# comprehensions, try/except, match, async, decorators, etc.). Programs +# that hit unsupported constructs are reported as SKIP, not failures. +# +# ## Failure analysis +# +# When fuzz tests fail on the PR, the workflow performs a bisection-style +# analysis by re-running the same tests (same seed) against the merge base: +# +# Pick random seed +# │ +# ▼ +# Run 10 fuzz tests on PR branch +# │ +# ┌───┴───┐ +# PASS FAIL +# │ │ +# ▼ ▼ +# Done Save fuzz scripts, checkout merge base, +# rebuild strata, re-run with same seed +# │ +# ┌───┴──────────┐ +# Base FAILS Base PASSES +# │ │ +# ▼ ▼ +# Create GitHub CI FAILS +# issue labeled (regression +# 'fuzz-bug' from PR) +# (pre-existing +# bug, PR not +# blocked) +# +# ## Reproducibility +# +# Every run uses a random seed derived from the current timestamp. The seed +# is reported in the step name, in the logs, and in all failure messages. +# To reproduce a failure locally: +# +# cd Tools/Python +# ./scripts/hypothesmith.sh 10 both --unrestricted +# +# The seed controls both the Hypothesis engine (syntax mode) and Python's +# random module (semantic mode), so identical seeds produce identical +# programs. +# +# ## Files +# +# - Tools/Python/scripts/hypothesmith.sh — Main driver script +# - Tools/Python/scripts/gen_random_python.py — Program generator +# - Tools/Python/scripts/gen_unrestricted.py — Extended generators +# ============================================================================= + name: Python Fuzz on: @@ -10,13 +99,18 @@ jobs: runs-on: ubuntu-latest permissions: contents: read + # Needed to create issues for pre-existing bugs. issues: write steps: - name: Checkout PR uses: actions/checkout@v6 with: + # Full history is needed to find the merge base for failure analysis. fetch-depth: 0 + # Generate a seed from the current nanosecond timestamp. This is + # reported in the step name and all log output so that any failure + # can be reproduced deterministically. - name: Pick random seed id: seed run: echo "value=$(date +%s%N | cut -c1-10)" >> $GITHUB_OUTPUT @@ -33,6 +127,7 @@ jobs: chmod +x cvc5-Linux-${ARCH_NAME}-static/bin/cvc5 echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> $GITHUB_PATH + # Try to restore a cached Lean build to avoid rebuilding from scratch. - name: Restore lake cache uses: actions/cache/restore@v5 with: @@ -43,6 +138,8 @@ jobs: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }} lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }} + # Build only the strata executable — skip proofs and other targets + # to keep the job fast. - name: Build Strata executables uses: leanprover/lean-action@v1 with: @@ -53,12 +150,17 @@ jobs: with: python-version: '3.14' + # Install the Strata Python bindings (for py_to_strata) and + # hypothesmith (for grammar-based program generation). - name: Install Python dependencies run: | python -m venv Tools/Python/.venv Tools/Python/.venv/bin/pip install --quiet -e Tools/Python Tools/Python/.venv/bin/pip install --quiet hypothesmith + # Run 10 fuzz tests in both syntax and semantic modes with + # --unrestricted. The seed is shown in the step name for easy + # identification in the GitHub Actions UI. - name: Run fuzz tests on PR (seed=${{ steps.seed.outputs.value }}) id: fuzz_pr working-directory: Tools/Python @@ -69,6 +171,14 @@ jobs: echo "exit_code=${PIPESTATUS[0]}" >> $GITHUB_OUTPUT echo "::endgroup::" + # --- Failure analysis --- + # If the PR fuzz tests failed, check whether the same failure exists + # at the merge base. This distinguishes regressions (PR broke it) + # from pre-existing bugs (already broken on main). + # + # The fuzz scripts are saved before checking out the merge base + # because they may not exist there (e.g., if this PR is the one + # that introduces the fuzz infrastructure). - name: Analyse failure against merge base id: analyse if: steps.fuzz_pr.outputs.exit_code != '0' @@ -76,28 +186,34 @@ jobs: echo "PR fuzz tests failed with seed ${{ steps.seed.outputs.value }}" echo "" - # Save the fuzz scripts from the PR branch — they may not exist at the merge base + # Save the fuzz scripts from the PR branch — they may not exist + # at the merge base. cp -r Tools/Python/scripts /tmp/fuzz_scripts - # Check out the merge base and re-run with the same seed + # Find and check out the merge base (the common ancestor of the + # PR branch and the target branch). MERGE_BASE=$(git merge-base HEAD origin/${{ github.base_ref }}) echo "Merge base: $MERGE_BASE" git checkout "$MERGE_BASE" - # Restore the fuzz scripts into the merge-base tree + # Restore the fuzz scripts into the merge-base working tree. cp /tmp/fuzz_scripts/gen_random_python.py Tools/Python/scripts/ cp /tmp/fuzz_scripts/gen_unrestricted.py Tools/Python/scripts/ cp /tmp/fuzz_scripts/hypothesmith.sh Tools/Python/scripts/ chmod +x Tools/Python/scripts/hypothesmith.sh - # Rebuild strata at merge base (only executables, skip proofs) - # This may fail if the toolchain changed significantly; treat that as inconclusive. + # Rebuild strata at the merge base. This may fail if the Lean + # toolchain or dependencies changed significantly between the + # merge base and the PR. In that case, we can't determine + # whether this is a regression, so we report "inconclusive". if ! lake build strata:exe strata 2>&1 | tail -10; then echo "result=inconclusive" >> $GITHUB_OUTPUT echo "⚠️ Could not build merge base. Cannot determine if this is a regression." exit 0 fi + # Re-run the exact same fuzz tests (same seed, same count, same + # modes) against the merge-base build. echo "::group::Merge-base fuzz test output" set +e cd Tools/Python @@ -117,6 +233,11 @@ jobs: echo "This PR introduced a regression." fi + # --- Pre-existing bug: file an issue --- + # If the merge base also fails, this is a bug that already exists on + # main. We create a GitHub issue (with deduplication by seed) so it + # gets tracked, but we do NOT fail the CI — the PR author shouldn't + # be blocked by a pre-existing bug. - name: Create issue for pre-existing bug if: steps.analyse.outputs.result == 'pre-existing' uses: actions/github-script@v7 @@ -124,7 +245,7 @@ jobs: script: | const seed = '${{ steps.seed.outputs.value }}'; const title = `[fuzz] Pre-existing Python front-end bug (seed ${seed})`; - // Check for duplicate issues + // Deduplicate: don't create a second issue for the same seed. const existing = await github.rest.issues.listForRepo({ owner: context.repo.owner, repo: context.repo.repo, @@ -158,6 +279,8 @@ jobs: ].join('\n'), }); + # --- Regression: fail CI --- + # The merge base passes but the PR fails — this PR broke something. - name: Fail if PR introduced a regression if: steps.analyse.outputs.result == 'regression' run: | @@ -168,6 +291,9 @@ jobs: echo " ./scripts/hypothesmith.sh 10 ${{ steps.seed.outputs.value }} both --unrestricted" exit 1 + # --- Inconclusive: fail CI conservatively --- + # We couldn't build the merge base, so we can't tell if this is a + # regression or pre-existing. Fail to be safe. - name: Fail if analysis was inconclusive if: steps.analyse.outputs.result == 'inconclusive' run: | diff --git a/Tools/Python/scripts/gen_random_python.py b/Tools/Python/scripts/gen_random_python.py index 7699e3d362..3d0217cc6e 100644 --- a/Tools/Python/scripts/gen_random_python.py +++ b/Tools/Python/scripts/gen_random_python.py @@ -4,23 +4,86 @@ """ Generate random Python programs for fuzz-testing Strata's Python front-end. -Two modes: - --mode syntax Use hypothesmith to generate syntactically valid Python. - Tests the parser pipeline (py_to_strata + Ion round-trip). - --mode semantic Use a custom generator to produce typed programs with - assertions that have known outcomes. Tests that - pyAnalyzeLaurel correctly models Python semantics. - -Size control: - --max-examples N Number of Hypothesis examples to try (default: 100). - --max-nodes N Filter: discard programs with more than N AST nodes (default: 50). - --seed S Fixed Hypothesis seed for reproducibility. - -Options: - --unrestricted Include generators for Python constructs that may be - beyond what Strata supports today (classes, generators, - comprehensions, try/except, match, async, decorators, - etc.). Useful for discovering gaps in Strata's coverage. +This script is the program generator used by hypothesmith.sh. It produces +Python source files that can be fed through Strata's pipeline to find bugs. + +## Modes + +### Syntax mode (--mode syntax) + +Uses the hypothesmith library (https://github.com/Zac-HD/hypothesmith) to +generate syntactically valid Python programs from the Python grammar. The +Hypothesis property-based testing framework drives generation, using its +grammar-inversion strategy to produce programs that pass CPython's +``compile()`` function. + +Generated programs are filtered by AST node count (--max-nodes) to keep +them small and debuggable. Programs with fewer than 2 AST nodes (empty +or trivial) are discarded. + +### Semantic mode (--mode semantic) + +Uses a custom generator to produce typed Python programs with assertions +whose expected values are computed by CPython at generation time. This is +analogous to CSmith computing a checksum: the generated program contains +its own expected output, so any disagreement between CPython and Strata +indicates a semantic modelling bug. + +Each program is structured as: + + def main(): + + + ... + main() + +where each block declares typed variables, performs operations, and asserts +the expected result. For example: + + def main(): + a: int = 89 + b: int = -30 + r: int = a + b + assert r == 59, "int add" + main() + +## Generators + +The **base generators** (always included) cover constructs known to work +in Strata today: + - Integer arithmetic (+, -, *) + - Integer comparisons (<, <=, >, >=, ==, !=) + - Boolean logic (and, or, not) + - String concatenation + - If/else branching + - Floor division (//) and modulo (%) + - Unary negation + +The **unrestricted generators** (--unrestricted flag) add ~60 generators +for constructs that may be beyond Strata's current support. See +gen_unrestricted.py for the full list. Programs using unsupported +constructs will be reported as SKIP by hypothesmith.sh, not as failures. + +## Reproducibility + +Both modes are fully deterministic given the same --seed value: + - Syntax mode: sets HYPOTHESIS_SEED and uses derandomize=True + - Semantic mode: seeds Python's random module + +## Usage + + python gen_random_python.py --mode syntax --output-dir /tmp/fuzz --seed 42 + python gen_random_python.py --mode semantic --output-dir /tmp/fuzz --seed 42 + python gen_random_python.py --mode semantic --output-dir /tmp/fuzz --seed 42 --unrestricted + +## Options + + --mode {syntax,semantic} Generation mode (required) + --output-dir DIR Directory for generated .py files (required) + --max-examples N Number of programs to generate (default: 100) + --max-nodes N Max AST nodes per program, syntax mode only (default: 50) + --seed S Random seed for reproducibility + --unrestricted Include generators beyond what Strata supports today """ import argparse @@ -31,27 +94,36 @@ from pathlib import Path +# ============================================================================= +# Syntax mode +# ============================================================================= + def gen_syntax(args): - """Generate syntactically valid Python via hypothesmith.""" + """Generate syntactically valid Python via hypothesmith. + + Uses hypothesmith's ``from_grammar()`` strategy, which inverts the Python + grammar to produce random valid source code. The ``auto_target=True`` + option enables Hypothesis's hill-climbing search to drive toward larger + and more complex programs over time. + + Programs are filtered to have between 2 and ``max_nodes`` AST nodes. + This keeps them small enough to debug while still being non-trivial. + """ import hypothesmith from hypothesis import given, settings, HealthCheck, Phase - phases = [Phase.generate] - if args.seed is not None: - phases = [Phase.generate] - out = Path(args.output_dir) out.mkdir(parents=True, exist_ok=True) count = [0] - health_checks = [HealthCheck.too_slow, HealthCheck.filter_too_much] - @settings( max_examples=args.max_examples, - suppress_health_check=health_checks, + suppress_health_check=[HealthCheck.too_slow, HealthCheck.filter_too_much], database=None, + # When a seed is provided, use derandomize mode so that the same + # seed always produces the same sequence of examples. derandomize=args.seed is not None, - phases=phases, + phases=[Phase.generate], ) @given(source_code=hypothesmith.from_grammar(auto_target=True)) def collect(source_code): @@ -60,8 +132,10 @@ def collect(source_code): nodes = len(list(ast.walk(tree))) except SyntaxError: return + # Skip trivial programs (empty files, bare comments). if nodes < 2: return + # Skip programs that are too large to debug easily. if nodes > args.max_nodes: return idx = count[0] @@ -75,22 +149,29 @@ def collect(source_code): print(f"Generated {count[0]} syntax-mode programs in {out}") -# --------------------------------------------------------------------------- -# Semantic mode: build programs with typed variables and checkable assertions -# --------------------------------------------------------------------------- +# ============================================================================= +# Semantic mode — base generators +# ============================================================================= +# Each generator function returns a string containing one or more indented +# Python statements (at 4-space indent) that declare variables, perform +# operations, and assert the expected result. The expected values are +# computed by CPython at generation time, so any disagreement with Strata +# indicates a bug in Strata's semantic model. def _rand_int(): + """Random integer in [-100, 100].""" return random.randint(-100, 100) def _rand_bool(): + """Random boolean.""" return random.choice([True, False]) def _rand_str(): - words = ["hello", "world", "foo", "bar", "", "abc", "x"] - return random.choice(words) + """Random short string from a fixed vocabulary.""" + return random.choice(["hello", "world", "foo", "bar", "", "abc", "x"]) def _gen_int_arithmetic(): - """Generate an int arithmetic block with a true assertion.""" + """Integer addition, subtraction, or multiplication.""" a, b = _rand_int(), _rand_int() op_name, op_sym, result_fn = random.choice([ ("add", "+", lambda a, b: a + b), @@ -106,7 +187,7 @@ def _gen_int_arithmetic(): ) def _gen_int_comparison(): - """Generate an int comparison with a true assertion.""" + """Integer comparison with all six operators.""" a, b = _rand_int(), _rand_int() op_sym, result = random.choice([ ("<", a < b), ("<=", a <= b), (">", a > b), @@ -119,7 +200,7 @@ def _gen_int_comparison(): ) def _gen_bool_logic(): - """Generate a boolean logic block with a true assertion.""" + """Boolean and/or.""" a, b = _rand_bool(), _rand_bool() op_name, op_sym, result_fn = random.choice([ ("and", "and", lambda a, b: a and b), @@ -134,7 +215,7 @@ def _gen_bool_logic(): ) def _gen_str_concat(): - """Generate a string concatenation with a true assertion.""" + """String concatenation.""" a, b = _rand_str(), _rand_str() result = a + b return ( @@ -145,7 +226,7 @@ def _gen_str_concat(): ) def _gen_if_else(): - """Generate an if/else with a true assertion about the result.""" + """If/else with a known branch outcome.""" cond_val = _rand_bool() a, b = _rand_int(), _rand_int() expected = a if cond_val else b @@ -159,7 +240,7 @@ def _gen_if_else(): ) def _gen_floor_div(): - """Generate floor division with a true assertion.""" + """Floor division (Python's // operator).""" a = _rand_int() b = random.choice([x for x in range(-10, 11) if x != 0]) result = a // b @@ -171,7 +252,7 @@ def _gen_floor_div(): ) def _gen_modulo(): - """Generate modulo with a true assertion.""" + """Modulo (Python's % operator, which uses floored division).""" a = _rand_int() b = random.choice([x for x in range(-10, 11) if x != 0]) result = a % b @@ -183,7 +264,7 @@ def _gen_modulo(): ) def _gen_negation(): - """Generate unary negation with a true assertion.""" + """Unary negation.""" a = _rand_int() return ( f" a: int = {a}\n" @@ -192,7 +273,7 @@ def _gen_negation(): ) def _gen_not(): - """Generate boolean not with a true assertion.""" + """Boolean not.""" a = _rand_bool() return ( f" a: bool = {a}\n" @@ -200,6 +281,7 @@ def _gen_not(): f' assert r == {not a}, "bool not"\n' ) +# The base generator list — only constructs known to work in Strata today. GENERATORS = [ _gen_int_arithmetic, _gen_int_comparison, @@ -214,9 +296,16 @@ def _gen_not(): def _get_generators(unrestricted): + """Return the list of generators to use. + + With --unrestricted, loads the extended generators from + gen_unrestricted.py (in the same directory) and appends them to the + base list. This produces programs using Python constructs that Strata + may not support yet, which is useful for discovering coverage gaps. + """ if not unrestricted: return GENERATORS - import importlib.util, os + import importlib.util spec = importlib.util.spec_from_file_location( "gen_unrestricted", os.path.join(os.path.dirname(__file__), "gen_unrestricted.py")) @@ -225,8 +314,18 @@ def _get_generators(unrestricted): return GENERATORS + mod.UNRESTRICTED_GENERATORS +# ============================================================================= +# Semantic mode — program assembly +# ============================================================================= + def gen_semantic(args): - """Generate typed Python programs with known-true assertions.""" + """Generate typed Python programs with known-true assertions. + + Each program contains 1–5 randomly chosen blocks, wrapped in a + ``def main(): ... main()`` structure to match Strata's test convention. + The blocks are independent — each declares its own variables and asserts + its own expected result. + """ out = Path(args.output_dir) out.mkdir(parents=True, exist_ok=True) @@ -236,11 +335,11 @@ def gen_semantic(args): generators = _get_generators(args.unrestricted) for i in range(args.max_examples): - # Pick 1-5 random blocks per program + # Pick 1–5 random blocks per program. n_blocks = random.randint(1, 5) blocks = [random.choice(generators)() for _ in range(n_blocks)] - # Wrap in a function and call it (matches Strata test convention) + # Wrap in a function and call it (matches Strata test convention). body = "\n".join(blocks) program = f"def main():\n{body}\nmain()\n" @@ -250,18 +349,28 @@ def gen_semantic(args): print(f"Generated {args.max_examples} semantic-mode programs in {out}") +# ============================================================================= +# CLI +# ============================================================================= + def main(): - parser = argparse.ArgumentParser(description=__doc__, + parser = argparse.ArgumentParser( + description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) - parser.add_argument("--mode", choices=["syntax", "semantic"], required=True) - parser.add_argument("--output-dir", required=True, help="Directory for generated .py files") - parser.add_argument("--max-examples", type=int, default=100) + parser.add_argument("--mode", choices=["syntax", "semantic"], required=True, + help="Generation mode: 'syntax' for grammar-based, " + "'semantic' for typed programs with assertions") + parser.add_argument("--output-dir", required=True, + help="Directory for generated .py files (created if needed)") + parser.add_argument("--max-examples", type=int, default=100, + help="Number of programs to generate (default: 100)") parser.add_argument("--max-nodes", type=int, default=50, - help="Max AST nodes per program (syntax mode)") + help="Max AST nodes per program, syntax mode only (default: 50)") parser.add_argument("--seed", type=int, default=None, help="Random seed for reproducibility") parser.add_argument("--unrestricted", action="store_true", - help="Include generators beyond what Strata supports today") + help="Include generators for Python constructs beyond " + "what Strata supports today") args = parser.parse_args() if args.mode == "syntax": diff --git a/Tools/Python/scripts/gen_unrestricted.py b/Tools/Python/scripts/gen_unrestricted.py index 115a217df4..f5b8d92c07 100644 --- a/Tools/Python/scripts/gen_unrestricted.py +++ b/Tools/Python/scripts/gen_unrestricted.py @@ -1,27 +1,115 @@ """Unrestricted Python program generators for fuzz testing. -These generators produce constructs that may be beyond what Strata supports -today. Used when --unrestricted is passed to gen_random_python.py. +This module contains ~60 generators that produce Python code blocks using +constructs that may be beyond what Strata supports today. It is loaded by +gen_random_python.py when the --unrestricted flag is passed. + +Each generator function returns a string of indented Python statements +(4-space indent) that can be placed inside a ``def main():`` body. Every +block includes at least one ``assert`` whose expected value is computed by +CPython at generation time. If Strata's verifier disagrees with CPython +on any of these assertions, that indicates a semantic modelling bug. + +## Categories of generators + +### Operators + - Bitwise: &, |, ^, ~ (gen_bitwise, gen_bitnot) + - Shifts: <<, >> (gen_shift) + - Power: ** (gen_power) + - Augmented assignment: +=, -=, *= (gen_augmented_assign) + +### Expressions + - Ternary: x if cond else y (gen_ternary) + - Chained comparisons: a <= b <= c (gen_chained_cmp) + - F-strings (gen_fstring) + - Lambda (gen_lambda) + - Walrus operator := (gen_walrus, gen_walrus_while) + +### Data structures + - Lists: create, index, slice, concat, in, append (gen_list_*) + - Dicts: create, access, in (gen_dict_*) + - Sets: union, intersection (gen_set_ops) + - Tuple unpacking, star unpacking (gen_tuple_unpack, gen_star_unpack) + - Multiple assignment / swap (gen_multi_assign) + +### Strings + - len, indexing, multiply, methods (upper/lower/strip), format + +### Control flow + - For loops over lists and range (gen_for_sum, gen_for_range) + - While loops (gen_while_countdown) + - Break (gen_break) + - Nested if, elif chains (gen_nested_if, gen_elif) + - Nested loops (gen_nested_loop) + +### Functions + - Nested calls (gen_nested_call) + - Default arguments (gen_default_args) + - *args, **kwargs (gen_varargs, gen_kwargs) + - Recursion (gen_recursion) + - Decorators (gen_decorator) + - Generators / yield (gen_generator) + +### Classes + - Basic class with __init__ (gen_class_basic) + - Class with methods (gen_class_method) + +### Exception handling + - try/except (gen_try_except) + - try/except/else (gen_try_except_else) + - try/finally (gen_try_finally) + - Multiple except clauses (gen_multi_except) + - raise (gen_raise) + +### Other + - None checks, Optional type (gen_none_check, gen_optional) + - isinstance (gen_isinstance) + - Type conversions: int(), str(), bool(), float(), list() (gen_type_conv) + - With statement / context managers (gen_with_stmt) + - Nonlocal (gen_nonlocal) + - Pass, del (gen_pass, gen_del) + - Async def / asyncio.run (gen_async_def) + - Match statement, Python 3.10+ (gen_match) + +## Adding new generators + +To add a new generator: +1. Write a function that returns a string of 4-space-indented Python + statements including at least one assert with a CPython-computed + expected value. +2. Test it: ``python3 -c "exec('def main():\\n' + gen_your_thing() + 'main()')"`` +3. Add it to the UNRESTRICTED_GENERATORS list at the bottom. """ import random +# --------------------------------------------------------------------------- +# Helpers — shared random value generators +# --------------------------------------------------------------------------- + def _rand_int(): + """Random integer in [-100, 100].""" return random.randint(-100, 100) def _rand_bool(): + """Random boolean.""" return random.choice([True, False]) def _rand_str(): + """Random short string from a fixed vocabulary.""" return random.choice(["hello", "world", "foo", "bar", "", "abc", "x"]) def _nonzero(): + """Random non-zero integer in [-10, 10].""" return random.choice([x for x in range(-10, 11) if x != 0]) def _rand_var(prefix="v"): + """Random variable name like v42.""" return f"{prefix}{random.randint(0, 99)}" -# --- Bitwise operations --- +# --------------------------------------------------------------------------- +# Operators +# --------------------------------------------------------------------------- def gen_bitwise(): a, b = _rand_int(), _rand_int() @@ -37,12 +125,15 @@ def gen_shift(): return f" assert ({a} {sym} {b}) == {r}, \"{op}\"\n" def gen_bitnot(): + """Bitwise NOT (~).""" a = _rand_int() return f" assert ~{a} == {~a}, \"bitnot\"\n" # --- Power --- def gen_power(): + """Exponentiation (**). Uses non-negative base to avoid precedence issues + with unary minus (``-2 ** 2`` is ``-(2**2)`` in Python).""" base = random.randint(0, 5) exp = random.randint(0, 4) r = base ** exp @@ -693,6 +784,13 @@ def gen_match(): ) +# --------------------------------------------------------------------------- +# Registry +# --------------------------------------------------------------------------- +# All unrestricted generators, imported by gen_random_python.py when +# --unrestricted is passed. The order doesn't matter — generators are +# chosen uniformly at random. + UNRESTRICTED_GENERATORS = [ gen_bitwise, gen_shift, gen_bitnot, gen_power, gen_augmented_assign, gen_ternary, gen_multi_assign, diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index 68343224a2..ab4756faa9 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -2,27 +2,103 @@ # Copyright Strata Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT # -# Fuzz-test Strata's Python front-end with randomly generated programs. +# ============================================================================= +# hypothesmith.sh — Fuzz-test Strata's Python front-end +# ============================================================================= +# +# This script generates random Python programs and runs them through Strata's +# Python front-end pipeline to find crashes, round-trip failures, and semantic +# modelling bugs. It is analogous to CBMC's scripts/csmith.sh, which uses +# CSmith to generate random C programs for testing CBMC. +# +# ## Background +# +# The approach is inspired by: +# - CSmith (https://embed.cs.utah.edu/csmith/) for random C program generation +# - hypothesmith (https://github.com/Zac-HD/hypothesmith) for random Python +# program generation using the Hypothesis property-based testing framework +# - The discussion at https://bugs.python.org/issue42109 about using Hypothesis +# and hypothesmith for testing CPython itself +# +# ## Modes +# +# **Syntax mode** — Uses hypothesmith's `from_grammar()` strategy to generate +# syntactically valid Python programs from the Python grammar. Each program is: +# 1. Parsed into Strata's Ion format via `python -m strata.gen py_to_strata` +# 2. Round-tripped through `strata toIon` +# 3. Diffed against the original Ion to check for round-trip fidelity +# +# This tests that the parser pipeline doesn't crash or lose information on +# arbitrary valid Python. Programs that fail to parse are SKIPped (hypothesmith +# may generate constructs the Strata parser doesn't support yet). +# +# **Semantic mode** — Uses a custom generator (gen_random_python.py) to produce +# typed Python programs with assertions whose expected values are computed by +# CPython at generation time. This is the CSmith checksum analogy: +# 1. CPython runs the program to confirm all assertions pass (reference) +# 2. The program is parsed into Ion format +# 3. `pyAnalyzeLaurel` verifies the program via the Laurel pipeline +# 4. If Strata reports a failing assertion on a program that CPython runs +# correctly, that indicates a semantic modelling bug in the +# Python → Laurel → Core translation pipeline +# +# ## Result classification +# +# Each test program gets one of these outcomes: +# OK — Pipeline completed successfully, all checks passed +# SKIP (parse) — Strata's parser couldn't handle the syntax (expected) +# SKIP (unsupported)— pyAnalyzeLaurel hit an unsupported construct (expected) +# TIMEOUT — Analysis exceeded the time limit (not counted as failure) +# FAIL (toIon) — Ion round-trip produced different output (bug) +# FAIL (diff) — Ion diff detected a mismatch (bug) +# FAIL (internal) — Strata panicked or leaked memory (bug) +# FAIL (verification)— Strata says assertion fails but CPython says it passes +# (semantic modelling bug) +# BUG (generator) — The generated program itself fails under CPython +# (bug in our generator, not in Strata) +# +# ## Reproducibility +# +# Every run uses a seed that controls both the Hypothesis engine (syntax mode) +# and Python's random module (semantic mode). Given the same seed, the same +# programs are generated. The seed is printed at the start and end of every +# run. To reproduce a failure: +# +# cd Tools/Python +# ./scripts/hypothesmith.sh 10 both --unrestricted +# +# ## Usage # -# Usage: # ./hypothesmith.sh [N [SEED [MODE [--unrestricted]]]] # -# N Number of programs to generate (default: 10) -# SEED Random seed for reproducibility (default: current timestamp) -# MODE "syntax" or "semantic" or "both" (default: both) -# --unrestricted Include Python constructs beyond what Strata supports today +# N Number of programs to generate per mode (default: 10) +# SEED Random seed for reproducibility (default: current timestamp) +# MODE "syntax", "semantic", or "both" (default: both) +# --unrestricted Include generators for Python constructs beyond what Strata +# supports today (classes, generators, comprehensions, +# try/except, match, async, decorators, etc.) +# +# ## Prerequisites # -# Requires: -# - The venv at Tools/Python/.venv with hypothesmith and strata installed -# - strata built (lake build strata) -# - The Python dialect file at Tools/Python/dialects/Python.dialect.st.ion +# - Python venv at Tools/Python/.venv with hypothesmith and strata installed: +# python3 -m venv Tools/Python/.venv +# Tools/Python/.venv/bin/pip install -e Tools/Python hypothesmith +# - Strata built: lake build strata +# - Python dialect file at Tools/Python/dialects/Python.dialect.st.ion # -# Exit codes: -# 0 All tests passed -# 1 At least one test failed (source code is printed for reproduction) +# ## Exit codes +# +# 0 All tests passed (or only SKIPs/TIMEOUTs) +# 1 At least one FAIL detected (source code is printed for reproduction) +# +# ============================================================================= set -euo pipefail +# --------------------------------------------------------------------------- +# Configuration +# --------------------------------------------------------------------------- + SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" TOOLS_PY="$REPO_ROOT/Tools/Python" @@ -30,6 +106,7 @@ PYTHON="$TOOLS_PY/.venv/bin/python3" STRATA="$REPO_ROOT/.lake/build/bin/strata" DIALECT="$TOOLS_PY/dialects/Python.dialect.st.ion" +# Command-line arguments with defaults. N="${1:-10}" SEED="${2:-$(date +%s)}" MODE="${3:-both}" @@ -38,13 +115,21 @@ if [ "${4:-}" = "--unrestricted" ]; then UNRESTRICTED="--unrestricted" fi -# Timeouts (seconds) +# Timeouts (seconds) for individual pipeline steps. +# Parse timeout covers py_to_strata and toIon; analyse timeout covers +# pyAnalyzeLaurel which invokes the SMT solver. PARSE_TIMEOUT=30 ANALYZE_TIMEOUT=90 +# --------------------------------------------------------------------------- +# Prerequisite checks +# --------------------------------------------------------------------------- + if [ ! -x "$PYTHON" ]; then echo "ERROR: Python venv not found at $TOOLS_PY/.venv" - echo "Run: python3 -m venv $TOOLS_PY/.venv && $TOOLS_PY/.venv/bin/pip install -e $TOOLS_PY -e ~/hypothesmith.git" + echo "Set up with:" + echo " python3 -m venv $TOOLS_PY/.venv" + echo " $TOOLS_PY/.venv/bin/pip install -e $TOOLS_PY hypothesmith" exit 1 fi @@ -58,11 +143,21 @@ if [ ! -f "$DIALECT" ]; then exit 1 fi +# --------------------------------------------------------------------------- +# Working directory (cleaned up on exit) +# --------------------------------------------------------------------------- + workdir=$(mktemp -d /tmp/strata-fuzz.XXX) trap 'rm -rf "$workdir"' EXIT failures=0 +# --------------------------------------------------------------------------- +# Syntax mode +# --------------------------------------------------------------------------- +# Generate random syntactically-valid Python via hypothesmith, then test +# the parse → Ion → round-trip pipeline. + run_syntax_tests() { local gen_dir="$workdir/syntax" echo "=== Syntax mode: generating $N programs (seed=$SEED) ===" @@ -79,16 +174,18 @@ run_syntax_tests() { local ion="$gen_dir/${base}.python.st.ion" local ion2="$gen_dir/${base}.python.st.ion2" - # Step 1: Parse Python -> Ion + # Step 1: Parse Python → Ion via the external Python tool. + # Parse failures are acceptable — hypothesmith may generate constructs + # that the Strata parser doesn't support yet. if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \ --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then - # Parse failure is acceptable — hypothesmith may generate constructs - # the Strata parser doesn't support yet. Just skip. echo " SKIP (parse): $base" continue fi - # Step 2: Ion round-trip + # Step 2: Round-trip the Ion through strata toIon. + # This re-serialises the Ion file; a failure here means the Lean-side + # reader or writer has a bug. if ! timeout "$PARSE_TIMEOUT" "$STRATA" toIon \ --include "$TOOLS_PY/dialects" "$ion" "$ion2" 2>/dev/null; then echo " FAIL (toIon): $base" @@ -99,7 +196,8 @@ run_syntax_tests() { continue fi - # Step 3: Diff + # Step 3: Diff the original and round-tripped Ion files. + # Any difference means information was lost or corrupted. if ! "$STRATA" diff --include "$TOOLS_PY/dialects" "$ion" "$ion2" 2>/dev/null; then echo " FAIL (diff): $base" echo "--- Source code ---" @@ -114,6 +212,13 @@ run_syntax_tests() { echo "Syntax tests: $count processed, $failures failures" } +# --------------------------------------------------------------------------- +# Semantic mode +# --------------------------------------------------------------------------- +# Generate typed Python programs with known-true assertions, validate them +# with CPython, then verify with pyAnalyzeLaurel. A verification failure +# on a CPython-passing program indicates a semantic modelling bug. + run_semantic_tests() { local gen_dir="$workdir/semantic" echo "=== Semantic mode: generating $N programs (seed=$SEED) ===" @@ -130,7 +235,10 @@ run_semantic_tests() { base=$(basename "$pyfile" .py) local ion="$gen_dir/${base}.python.st.ion" - # Step 1: Sanity check — run with CPython to confirm assertions pass + # Step 1: Sanity check — run with CPython to confirm assertions pass. + # This is the "reference execution" (analogous to CSmith's GCC run + # that computes the reference checksum). If CPython fails, the bug + # is in our generator, not in Strata. if ! timeout 10 python3 "$pyfile" 2>/dev/null; then echo " BUG (generator): $base fails under CPython!" cat "$pyfile" @@ -138,7 +246,7 @@ run_semantic_tests() { continue fi - # Step 2: Parse Python -> Ion + # Step 2: Parse Python → Ion. if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \ --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then echo " FAIL (parse): $base" @@ -149,19 +257,22 @@ run_semantic_tests() { continue fi - # Step 3: Run pyAnalyzeLaurel + # Step 3: Run pyAnalyzeLaurel — the full Python → Laurel → Core → SMT + # verification pipeline. local output local ec=0 output=$(timeout "$ANALYZE_TIMEOUT" "$STRATA" pyAnalyzeLaurel "$ion" 2>&1) || ec=$? + # Handle timeouts (exit 124 from timeout, 137 from SIGKILL). if [ $ec -eq 124 ] || [ $ec -eq 137 ]; then echo " TIMEOUT: $base" continue fi + # Non-zero exit from pyAnalyzeLaurel. Distinguish between: + # - Internal errors (panics, memory leaks) → real bugs, count as FAIL + # - Translation failures → unsupported constructs, count as SKIP if [ $ec -ne 0 ]; then - # Non-zero exit from pyAnalyzeLaurel — could be unsupported construct. - # Check if it's an internal error vs. expected limitation. if echo "$output" | grep -qi "panic\|LEAK"; then echo " FAIL (internal error): $base" echo "--- Source code ---" @@ -172,16 +283,22 @@ run_semantic_tests() { sem_failures=$((sem_failures + 1)) continue fi - # Translation failures and other non-zero exits are unsupported constructs + # Translation failures and other non-zero exits are unsupported + # constructs — expected when using --unrestricted. echo " SKIP (unsupported): $base" continue fi - # Step 4: Check that all assertions passed (no "failed" in DETAIL line) + # Step 4: Check verification results. If pyAnalyzeLaurel reports any + # failed assertions, but CPython ran the program successfully (Step 1), + # then Strata's semantic model disagrees with CPython. This is the + # most interesting kind of bug to find — analogous to CBMC finding a + # counterexample to the CSmith checksum assertion. if echo "$output" | grep -qE '[1-9][0-9]* failed'; then echo " FAIL (verification): $base" - echo " Strata reports a failing assertion on a program that CPython runs correctly." - echo " This indicates a semantic modelling bug in the Python-to-Core pipeline." + echo " Strata reports a failing assertion on a program that CPython" + echo " runs correctly. This indicates a semantic modelling bug in" + echo " the Python → Laurel → Core translation pipeline." echo "--- Source code ---" cat "$pyfile" echo "--- pyAnalyzeLaurel output ---" @@ -197,6 +314,10 @@ run_semantic_tests() { echo "Semantic tests: $count processed, $sem_failures failures" } +# --------------------------------------------------------------------------- +# Main +# --------------------------------------------------------------------------- + echo "Strata Python front-end fuzz test" echo "Seed: $SEED N: $N Mode: $MODE Unrestricted: ${UNRESTRICTED:-no}" echo "" From cee7768cb5277bf5719f7429e68ea8bcc090152c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Apr 2026 14:31:01 +0000 Subject: [PATCH 05/13] Address Copilot review feedback - Parse RESULT: line for non-zero pyAnalyzeLaurel exits to correctly classify verification failures and internal errors instead of blanket-skipping them - Use $PYTHON instead of python3 for CPython validation so generation/validation/parsing all use the same interpreter - Fix gen_fstring() to declare a variable and use single-brace interpolation (triple braces produced literal braces, mismatching the expected string) - Guard issue creation on fork PRs where GITHUB_TOKEN is read-only, and add continue-on-error as safety net - Add clarifying comment on gen_dict_create() f-string evaluation Co-authored-by: Kiro --- .github/workflows/python-fuzz.yml | 3 ++- Tools/Python/scripts/gen_random_python.py | 4 ++-- Tools/Python/scripts/gen_unrestricted.py | 9 ++++++++- Tools/Python/scripts/hypothesmith.sh | 22 +++++++++++++++++++++- 4 files changed, 33 insertions(+), 5 deletions(-) diff --git a/.github/workflows/python-fuzz.yml b/.github/workflows/python-fuzz.yml index 84c909ac6b..a1bbbf1d62 100644 --- a/.github/workflows/python-fuzz.yml +++ b/.github/workflows/python-fuzz.yml @@ -239,7 +239,8 @@ jobs: # gets tracked, but we do NOT fail the CI — the PR author shouldn't # be blocked by a pre-existing bug. - name: Create issue for pre-existing bug - if: steps.analyse.outputs.result == 'pre-existing' + if: steps.analyse.outputs.result == 'pre-existing' && github.event.pull_request.head.repo.full_name == github.repository + continue-on-error: true uses: actions/github-script@v7 with: script: | diff --git a/Tools/Python/scripts/gen_random_python.py b/Tools/Python/scripts/gen_random_python.py index 3d0217cc6e..54b990f84e 100644 --- a/Tools/Python/scripts/gen_random_python.py +++ b/Tools/Python/scripts/gen_random_python.py @@ -1,6 +1,6 @@ -#!/usr/bin/env python3 # Copyright Strata Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# SPDX-License-Identifier: Apache-2.0 OR MIT """ Generate random Python programs for fuzz-testing Strata's Python front-end. diff --git a/Tools/Python/scripts/gen_unrestricted.py b/Tools/Python/scripts/gen_unrestricted.py index f5b8d92c07..07e3cf984f 100644 --- a/Tools/Python/scripts/gen_unrestricted.py +++ b/Tools/Python/scripts/gen_unrestricted.py @@ -1,3 +1,6 @@ +# Copyright Strata Contributors +# +# SPDX-License-Identifier: Apache-2.0 OR MIT """Unrestricted Python program generators for fuzz testing. This module contains ~60 generators that produce Python code blocks using @@ -228,6 +231,7 @@ def gen_list_append(): def gen_dict_create(): keys = random.sample(["a", "b", "c", "d", "e"], random.randint(1, 4)) d = {k: _rand_int() for k in keys} + # {len(d)} is evaluated at generation time, producing e.g. "assert len(d) == 3" return ( f" d: dict = {d}\n" f' assert len(d) == {len(d)}, "dict len"\n' @@ -557,7 +561,10 @@ def gen_walrus(): def gen_fstring(): a = random.randint(0, 50) - return f' assert f"val={{{a}}}" == "val={a}", "fstring"\n' + return ( + f" a = {a}\n" + f' assert f"val={{a}}" == "val={a}", "fstring"\n' + ) # --- Star unpacking --- diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index ab4756faa9..9c7ac52623 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -239,7 +239,7 @@ run_semantic_tests() { # This is the "reference execution" (analogous to CSmith's GCC run # that computes the reference checksum). If CPython fails, the bug # is in our generator, not in Strata. - if ! timeout 10 python3 "$pyfile" 2>/dev/null; then + if ! timeout 10 "$PYTHON" "$pyfile" 2>/dev/null; then echo " BUG (generator): $base fails under CPython!" cat "$pyfile" sem_failures=$((sem_failures + 1)) @@ -283,6 +283,26 @@ run_semantic_tests() { sem_failures=$((sem_failures + 1)) continue fi + if echo "$output" | grep -q "RESULT: Failures found"; then + echo " FAIL (verification, exit $ec): $base" + echo "--- Source code ---" + cat "$pyfile" + echo "--- pyAnalyzeLaurel output ---" + echo "$output" + echo "---" + sem_failures=$((sem_failures + 1)) + continue + fi + if echo "$output" | grep -q "RESULT: Internal error"; then + echo " FAIL (internal error): $base" + echo "--- Source code ---" + cat "$pyfile" + echo "--- Output ---" + echo "$output" | head -20 + echo "---" + sem_failures=$((sem_failures + 1)) + continue + fi # Translation failures and other non-zero exits are unsupported # constructs — expected when using --unrestricted. echo " SKIP (unsupported): $base" From 6a3341219690ba0848373d361e845cf686ce01c7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Apr 2026 15:20:44 +0000 Subject: [PATCH 06/13] ci: disable lake test in fuzz workflow (only need executable) lean-action runs lake test by default when lake check-test succeeds. The fuzz workflow only needs the strata executable, not the full test suite. Running lake test fails because z3 is not installed in the fuzz runner (T19_InvokeOn requires z3). Co-authored-by: Kiro --- .github/workflows/python-fuzz.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/python-fuzz.yml b/.github/workflows/python-fuzz.yml index a1bbbf1d62..839857e397 100644 --- a/.github/workflows/python-fuzz.yml +++ b/.github/workflows/python-fuzz.yml @@ -145,6 +145,7 @@ jobs: with: use-github-cache: false build-args: 'strata:exe strata' + test: false - uses: actions/setup-python@v6 with: From 08609541a0ff8a51880d99db5ee8d9278846bf08 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 23 Apr 2026 10:20:38 +0000 Subject: [PATCH 07/13] Classify parse failures as SKIP in semantic mode Parse failures in semantic mode are now SKIP (parse), matching syntax mode behavior and the documented result classification. The generator may produce constructs the Strata parser doesn't support yet, which are expected limitations, not regressions. Co-authored-by: Kiro --- Tools/Python/scripts/hypothesmith.sh | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index 9c7ac52623..f1a7498b7f 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -247,13 +247,11 @@ run_semantic_tests() { fi # Step 2: Parse Python → Ion. + # Parse failures are acceptable — the generator may produce constructs + # that the Strata parser doesn't support yet (same as syntax mode). if ! timeout "$PARSE_TIMEOUT" "$PYTHON" -m strata.gen py_to_strata \ --dialect "$DIALECT" "$pyfile" "$ion" 2>/dev/null; then - echo " FAIL (parse): $base" - echo "--- Source code ---" - cat "$pyfile" - echo "---" - sem_failures=$((sem_failures + 1)) + echo " SKIP (parse): $base" continue fi From 7f9aaa50869389b1ff9f0e383ad01ad88f8153f3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 23 Apr 2026 10:59:24 +0000 Subject: [PATCH 08/13] Add lightweight fuzz test integration with lake test - hypothesmith.sh now respects PYTHON env var (falls back to .venv) - New StrataTest/Fuzz/HypotheSmith.lean runs 3 deterministic fuzz tests via withPython when Python + hypothesmith are available, skips gracefully otherwise - Uses the established findPython3/withPython/pythonCheckModule pattern from StrataTest/Util/Python.lean - Full random-seed fuzzing remains in the CI workflow Co-authored-by: Kiro --- StrataTest/Fuzz/HypotheSmith.lean | 36 ++++++++++++++++++++++++++++ Tools/Python/scripts/hypothesmith.sh | 2 +- 2 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 StrataTest/Fuzz/HypotheSmith.lean diff --git a/StrataTest/Fuzz/HypotheSmith.lean b/StrataTest/Fuzz/HypotheSmith.lean new file mode 100644 index 0000000000..a24d7a4ca5 --- /dev/null +++ b/StrataTest/Fuzz/HypotheSmith.lean @@ -0,0 +1,36 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Util.Python + +/-! +# Lightweight fuzz test via hypothesmith + +Runs a small deterministic batch of fuzz tests when the Python tooling +is available. Skips gracefully otherwise. The full random-seed fuzzing +lives in `.github/workflows/python-fuzz.yml`. +-/ + +open Strata.Python in +#guard_msgs in +#eval withPython (warnOnSkip := true) fun pythonCmd => do + -- Check that hypothesmith is installed + unless ← pythonCheckModule pythonCmd "hypothesmith" do + IO.eprintln "⚠ Fuzz test skipped: hypothesmith not installed" + return + + -- Run a small deterministic batch (3 tests, fixed seed, both modes) + let script := "Tools/Python/scripts/hypothesmith.sh" + let result ← IO.Process.output { + cmd := "bash" + args := #[script, "3", "20260423", "both"] + env := #[("PYTHON", pythonCmd.toString)] + inheritEnv := true + } + IO.print result.stdout + if result.exitCode != 0 then + IO.eprint result.stderr + throw <| .userError s!"Fuzz test failed (exit code {result.exitCode})" diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index f1a7498b7f..d6e9d90cf4 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -102,7 +102,7 @@ set -euo pipefail SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" REPO_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)" TOOLS_PY="$REPO_ROOT/Tools/Python" -PYTHON="$TOOLS_PY/.venv/bin/python3" +PYTHON="${PYTHON:-$TOOLS_PY/.venv/bin/python3}" STRATA="$REPO_ROOT/.lake/build/bin/strata" DIALECT="$TOOLS_PY/dialects/Python.dialect.st.ion" From cc70d5511cbbaa67df493517b36b8b1db0c564f7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 May 2026 11:21:23 +0000 Subject: [PATCH 09/13] Fix: remove warnOnSkip parameter, fix hypothesmith.sh python check - Remove warnOnSkip parameter from withPython call (parameter removed on main) - Fix hypothesmith.sh: use 'command -v' instead of '[ -x ]' to check PYTHON, so bare command names (e.g. 'python3') work alongside full paths Co-authored-by: Kiro --- StrataTest/Fuzz/HypotheSmith.lean | 2 +- Tools/Python/scripts/hypothesmith.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/StrataTest/Fuzz/HypotheSmith.lean b/StrataTest/Fuzz/HypotheSmith.lean index fd3504b274..4bcb2c3a08 100644 --- a/StrataTest/Fuzz/HypotheSmith.lean +++ b/StrataTest/Fuzz/HypotheSmith.lean @@ -15,7 +15,7 @@ lives in `.github/workflows/python-fuzz.yml`. -/ open Strata.Python in -#eval withPython (warnOnSkip := true) fun pythonCmd => do +#eval withPython fun pythonCmd => do -- Check that hypothesmith is installed unless ← pythonCheckModule pythonCmd "hypothesmith" do IO.eprintln "⚠ Fuzz test skipped: hypothesmith not installed" diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index d6e9d90cf4..911cad04cc 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -125,7 +125,7 @@ ANALYZE_TIMEOUT=90 # Prerequisite checks # --------------------------------------------------------------------------- -if [ ! -x "$PYTHON" ]; then +if ! command -v "$PYTHON" &>/dev/null; then echo "ERROR: Python venv not found at $TOOLS_PY/.venv" echo "Set up with:" echo " python3 -m venv $TOOLS_PY/.venv" From 0a39094ca5671f7490066253461854d1c284894b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 May 2026 19:08:43 +0000 Subject: [PATCH 10/13] Fix CI: skip fuzz test gracefully when Python/strata.gen is unavailable The HypotheSmith.lean test used withPython which throws when strata.gen is not installed. The 'Build and test Lean' CI job doesn't install Python Strata libraries, and --exclude Languages.Python doesn't cover StrataTest.Fuzz.*. Replace withPython with try/catch on findPython3 and explicit pythonCheckModule guards so the test skips with a warning. Co-authored-by: Kiro --- StrataTest/Fuzz/HypotheSmith.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/StrataTest/Fuzz/HypotheSmith.lean b/StrataTest/Fuzz/HypotheSmith.lean index 4bcb2c3a08..eb02ceaaf8 100644 --- a/StrataTest/Fuzz/HypotheSmith.lean +++ b/StrataTest/Fuzz/HypotheSmith.lean @@ -15,11 +15,15 @@ lives in `.github/workflows/python-fuzz.yml`. -/ open Strata.Python in -#eval withPython fun pythonCmd => do - -- Check that hypothesmith is installed +#eval do + -- Skip gracefully when Python or strata.gen is not available (e.g. in the + -- "Build and test Lean" CI job which doesn't install Python libraries). + let pythonCmd ← try findPython3 (minVersion := 11) (maxVersion := 14) + catch _ => IO.eprintln "⚠ Fuzz test skipped: Python 3 not found"; return + unless ← pythonCheckModule pythonCmd "strata.gen" do + IO.eprintln "⚠ Fuzz test skipped: strata.gen not installed"; return unless ← pythonCheckModule pythonCmd "hypothesmith" do - IO.eprintln "⚠ Fuzz test skipped: hypothesmith not installed" - return + IO.eprintln "⚠ Fuzz test skipped: hypothesmith not installed"; return -- Run a small deterministic batch (3 tests, fixed seed, both modes) let script := "Tools/Python/scripts/hypothesmith.sh" @@ -32,4 +36,4 @@ open Strata.Python in IO.print result.stdout if result.exitCode != 0 then IO.eprint result.stderr - throw <| .userError s!"Fuzz test failed (exit code {result.exitCode})" + throw <| IO.userError s!"Fuzz test failed (exit code {result.exitCode})" From 6c1b779118713bb63a0cf042b4b63ff0cf27e238 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 May 2026 19:08:50 +0000 Subject: [PATCH 11/13] Address review: include generated Python program in fuzz bug issues When filing GitHub issues for pre-existing fuzz bugs, extract the first failing program's source code from the fuzz log and include it in the issue body. This lets agents group issues by root cause without having to re-generate the code. Addresses feedback from olivier-aws in PR #984 thread 6. Co-authored-by: Kiro --- .github/workflows/python-fuzz.yml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/.github/workflows/python-fuzz.yml b/.github/workflows/python-fuzz.yml index 839857e397..0a363fe569 100644 --- a/.github/workflows/python-fuzz.yml +++ b/.github/workflows/python-fuzz.yml @@ -259,6 +259,19 @@ jobs: console.log('Issue already exists for this seed, skipping.'); return; } + // Extract failing source code from the fuzz log (between "--- Source code ---" markers) + const fs = require('fs'); + let sourceSnippet = ''; + try { + const log = fs.readFileSync('/tmp/fuzz_pr.log', 'utf8'); + const sourceMatch = log.match(/--- Source code ---\n([\s\S]*?)(?=\n---)/); + if (sourceMatch) { + sourceSnippet = sourceMatch[1].substring(0, 2000); + } + } catch (e) { /* log not available */ } + const sourceSection = sourceSnippet + ? [`### Generated program`, '```python', sourceSnippet, '```', ''] + : []; await github.rest.issues.create({ owner: context.repo.owner, repo: context.repo.repo, @@ -271,6 +284,7 @@ jobs: `**PR:** #${context.issue.number}`, `**Merge base also fails:** yes`, ``, + ...sourceSection, `### Reproduce`, `\`\`\`bash`, `cd Tools/Python`, From 30ef165d4a61d9a915788e0eef61d96cb57fcef1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 4 May 2026 19:09:00 +0000 Subject: [PATCH 12/13] Address review: generate compound boolean conditions in if-else tests Extend _gen_if_else() to randomly produce compound conditions using 'and', 'or', 'not', and None identity checks ('None is None', 'None is not None') in addition to simple boolean literals. This exercises more of the Python front-end's condition handling. Addresses feedback from olivier-aws in PR #984 thread 7. Co-authored-by: Kiro --- Tools/Python/scripts/gen_random_python.py | 31 ++++++++++++++++++++--- 1 file changed, 27 insertions(+), 4 deletions(-) diff --git a/Tools/Python/scripts/gen_random_python.py b/Tools/Python/scripts/gen_random_python.py index 54b990f84e..224b6999e5 100644 --- a/Tools/Python/scripts/gen_random_python.py +++ b/Tools/Python/scripts/gen_random_python.py @@ -226,13 +226,36 @@ def _gen_str_concat(): ) def _gen_if_else(): - """If/else with a known branch outcome.""" - cond_val = _rand_bool() + """If/else with a known branch outcome, using compound boolean conditions.""" a, b = _rand_int(), _rand_int() + # Pick a random condition style + style = random.choice(["simple", "and", "or", "not", "none_check"]) + if style == "simple": + cond_val = _rand_bool() + cond_expr = str(cond_val) + elif style == "and": + x, y = _rand_bool(), _rand_bool() + cond_val = x and y + cond_expr = f"{x} and {y}" + elif style == "or": + x, y = _rand_bool(), _rand_bool() + cond_val = x or y + cond_expr = f"{x} or {y}" + elif style == "not": + x = _rand_bool() + cond_val = not x + cond_expr = f"not {x}" + else: # none_check + use_none = _rand_bool() + if use_none: + cond_val = False + cond_expr = "None is not None" + else: + cond_val = True + cond_expr = "None is None" expected = a if cond_val else b return ( - f" cond: bool = {cond_val}\n" - f" if cond:\n" + f" if {cond_expr}:\n" f" r: int = {a}\n" f" else:\n" f" r: int = {b}\n" From 31b3687a2966af7dbf4c245c3a993b3161eb616f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 May 2026 11:15:38 +0000 Subject: [PATCH 13/13] Clarify 'failed' semantics in verification check comment 'N failed' in the DETAIL line means the solver proved the assertion does not hold (found a counterexample), not merely 'failed to prove'. Inconclusive results are handled separately. Also note pyInterpret (#869) as a future improvement for concrete comparison. Co-authored-by: Kiro --- Tools/Python/scripts/hypothesmith.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Tools/Python/scripts/hypothesmith.sh b/Tools/Python/scripts/hypothesmith.sh index 911cad04cc..ca41602c6a 100755 --- a/Tools/Python/scripts/hypothesmith.sh +++ b/Tools/Python/scripts/hypothesmith.sh @@ -312,6 +312,13 @@ run_semantic_tests() { # then Strata's semantic model disagrees with CPython. This is the # most interesting kind of bug to find — analogous to CBMC finding a # counterexample to the CSmith checksum assertion. + # + # The grep matches "N failed" in the DETAIL line, which means the solver + # *proved* the assertion does not hold (found a counterexample). This is + # distinct from "inconclusive" (solver couldn't determine either way), + # which is not treated as a failure here. + # TODO: Once pyInterpret (#869) is available, use it for concrete + # pass/fail comparison with CPython (no unknown middle ground). if echo "$output" | grep -qE '[1-9][0-9]* failed'; then echo " FAIL (verification): $base" echo " Strata reports a failing assertion on a program that CPython"