From 7e69e7b23e5670d3b8df493adbbca5b6aaffa899 Mon Sep 17 00:00:00 2001 From: Pragyansh Chaturvedi Date: Tue, 27 Oct 2026 21:05:23 +0530 Subject: [PATCH 1/4] Tests: Let host_jit read a function's result as any ctypes type run_function took the return type from the IR and read only i32 and i64, as signed. It now takes an optional ctypes type, so a caller can read an unsigned or narrow result the way C would see it. Without one, it does what it did before. Co-Authored-By: Claude Opus 5.5 --- tests/framework/host_jit.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/tests/framework/host_jit.py b/tests/framework/host_jit.py index e865c1d..e193e0c 100644 --- a/tests/framework/host_jit.py +++ b/tests/framework/host_jit.py @@ -17,7 +17,9 @@ import llvmlite.binding as llvm -def run_function(ll_text: str, func_name: str) -> int: +def run_function(ll_text: str, func_name: str, restype=None) -> int: + """Call func_name(NULL) and return its result. restype is the ctypes type + to read the result as; by default the IR's i32 or i64, read as signed.""" ll_text = re.sub(r'^target (triple|datalayout) = ".*"$', "", ll_text, flags=re.M) llvm.initialize_native_target() llvm.initialize_native_asmprinter() @@ -27,12 +29,15 @@ def run_function(ll_text: str, func_name: str) -> int: engine = llvm.create_mcjit_compiler(mod, tm) engine.finalize_object() - ret = re.search(rf'define [^\n]*?\bi(\d+) @"?{re.escape(func_name)}"?\(', ll_text) - ret_ty = {64: ctypes.c_int64, 32: ctypes.c_int32}[int(ret.group(1))] - func = ctypes.CFUNCTYPE(ret_ty, ctypes.c_void_p)( + if restype is None: + ret = re.search( + rf'define [^\n]*?\bi(\d+) @"?{re.escape(func_name)}"?\(', ll_text + ) + restype = {64: ctypes.c_int64, 32: ctypes.c_int32}[int(ret.group(1))] + func = ctypes.CFUNCTYPE(restype, ctypes.c_void_p)( engine.get_function_address(func_name) ) - return func(None) + return int(func(None)) def run_in_subprocess(ll_path, func_name: str, timeout: float) -> int: From ed5bc467939304d9ffa7dd5e4f302277bb56a2e2 Mon Sep 17 00:00:00 2001 From: Pragyansh Chaturvedi Date: Tue, 27 Oct 2026 21:05:25 +0530 Subject: [PATCH 2/4] Tests: Add Hypothesis, with dev, ci and thorough profiles hypothesis joins the test extra. conftest.py registers three profiles, chosen with HYPOTHESIS_PROFILE: - dev (the default): 100 examples. - ci: 100 examples, derandomized, so a CI failure always reproduces. - thorough: 3000 examples, for bug hunting. None of them has a deadline: an example compiles a program twice. CI runs the suite with the ci profile. The example database (.hypothesis/) is ignored. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/test.yml | 3 +++ .gitignore | 1 + pyproject.toml | 1 + tests/conftest.py | 19 +++++++++++++++++++ 4 files changed, 24 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index f510c69..3ab5ec3 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -72,6 +72,9 @@ jobs: run: uv pip install --system -e ".[test]" - name: Run test suite + env: + # tests/property: derandomized, so a failure always reproduces + HYPOTHESIS_PROFILE: ci run: make test - name: Check whether sudo is usable diff --git a/.gitignore b/.gitignore index bb41570..d232ae6 100644 --- a/.gitignore +++ b/.gitignore @@ -14,3 +14,4 @@ vmlinux.h # Documentation build artifacts docs/_build/ docs/_templates/ +.hypothesis/ diff --git a/pyproject.toml b/pyproject.toml index 40c07e7..e18f4fd 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -42,6 +42,7 @@ docs = [ test = [ "pytest>=8.0", "pytest-cov>=5.0", + "hypothesis>=6.100", "ctypeslib2", # Pinned rather than left to ctypeslib2's own (unpinned) dependency: pip # installs the latest release by default, and its libclang API surface diff --git a/tests/conftest.py b/tests/conftest.py index f70dee2..0a6665d 100644 --- a/tests/conftest.py +++ b/tests/conftest.py @@ -116,3 +116,22 @@ def pytest_collection_modifyitems(items): def set_log_level(caplog): with caplog.at_level(logging.ERROR, logger="pythonbpf"): yield + + +# ── Hypothesis profiles (tests/property) ──────────────────────────────────── +# dev (default) for local runs, ci for GitHub Actions (derandomized, so a PR +# never fails on an example nobody can reproduce), thorough for bug hunting: +# HYPOTHESIS_PROFILE=thorough pytest tests/property + +try: + import os + + from hypothesis import HealthCheck, settings + + _common = dict(deadline=None, suppress_health_check=[HealthCheck.too_slow]) + settings.register_profile("dev", max_examples=100, **_common) + settings.register_profile("ci", max_examples=100, derandomize=True, **_common) + settings.register_profile("thorough", max_examples=3000, **_common) + settings.load_profile(os.environ.get("HYPOTHESIS_PROFILE", "dev")) +except ImportError: + pass From 7b328fb9b748f0a91e5e64e2cc77689d2e4292c2 Mon Sep 17 00:00:00 2001 From: Pragyansh Chaturvedi Date: Tue, 27 Oct 2026 21:05:37 +0530 Subject: [PATCH 3/4] Tests: Property-test integer arithmetic and conversions against clang tests/property generates integer programs, prints each as PythonBPF and as C, and runs both on the host. clang's result is the specification: - clang compiles the C (-O0 -fwrapv) to a native object. - PythonBPF's IR is retargeted to the host. - Both are JIT-run in a worker process, so a miscompile that traps cannot end the pytest run. cints.py models C's promotions, usual arithmetic conversions and operators. It discards programs that would be undefined in C, and it is checked against clang on every example, so a model bug is never blamed on the compiler. Three properties: - test_int_expressions: random nested expressions over every ctypes integer type and c_bool, with typed and untyped temporaries. The worked examples of integers.md are pinned. - test_int_operators: every binary operator on every pair of types. - test_int_conversions: every (source type, destination type, site) triple. The sites are constructor, declaration, reassignment, untyped local, global store, return, global initialiser and each augmented assignment. Deliberately breaking >>, %, /, the usual arithmetic conversions, promotion, sign extension or c_bool conversion fails a property each time, shrunk to a program of two or three lines. Divergences found and not yet fixed are in known_gaps.py, each pinned as a strict xfail in test_known_gaps.py: - negated-literal-rank: -2147483648 is ranked int, not long long. - untyped-local-unary-or-compare: `t = -x`, `t = not x` and `t = a < b` give "Undefined variable". - shift-result-type: a shift is typed by both operands, not by its promoted left operand. This includes <<= and >>=. - untyped-copy-keeps-narrow-type: `t = a` keeps a's narrow type, where integers.md says an undeclared local is 64 bits. - The global_init site: a negative @bpfglobal initialiser becomes 0, and c_bool(2) becomes 0. tests/README.md documents the suite and the plan for what comes next. Co-Authored-By: Claude Opus 5.5 --- tests/README.md | 69 +++++ tests/property/__init__.py | 0 tests/property/cints.py | 182 +++++++++++++ tests/property/harness.py | 188 +++++++++++++ tests/property/known_gaps.py | 129 +++++++++ tests/property/programs.py | 358 +++++++++++++++++++++++++ tests/property/test_int_conversions.py | 145 ++++++++++ tests/property/test_int_expressions.py | 93 +++++++ tests/property/test_int_operators.py | 52 ++++ tests/property/test_known_gaps.py | 46 ++++ 10 files changed, 1262 insertions(+) create mode 100644 tests/property/__init__.py create mode 100644 tests/property/cints.py create mode 100644 tests/property/harness.py create mode 100644 tests/property/known_gaps.py create mode 100644 tests/property/programs.py create mode 100644 tests/property/test_int_conversions.py create mode 100644 tests/property/test_int_expressions.py create mode 100644 tests/property/test_int_operators.py create mode 100644 tests/property/test_known_gaps.py diff --git a/tests/README.md b/tests/README.md index d972939..a5f5a5d 100644 --- a/tests/README.md +++ b/tests/README.md @@ -133,6 +133,69 @@ Anything importing from `vmlinux` belongs in `vmlinux/`, which is registered in `VMLINUX_TEST_DIRS_PASSING` so it is skipped rather than failed where no `vmlinux.py` has been generated. +## Property-based tests (`tests/property/`) + +The integer rules in `docs/user-guide/integers.md` are tested with +[Hypothesis](https://hypothesis.readthedocs.io): instead of hand-picked cases, +programs are generated, and each one is compiled two ways and run. + +* **The oracle is clang.** Every generated program is printed twice, as + PythonBPF and as the equivalent C. clang compiles the C (`-O0 -fwrapv`) to a + native object; PythonBPF's IR is retargeted to the host. Both are JIT-run + in a worker process (a miscompile can trap or abort inside LLVM, which must + not take pytest down with it) and must return the same value. +* **A model keeps undefined behaviour out.** `cints.py` implements C's + promotions, usual arithmetic conversions and operators. Programs where C + would be undefined (division by zero, `MIN / -1`, shift counts out of + range) are discarded before anything runs. The model is also checked + against clang on every example, so a disagreement is reported as a model + bug, never blamed on PythonBPF. + +| File | Property | +|---|---| +| `test_int_expressions.py` | Random straight-line programs over every ctypes integer type and `c_bool`: `+ - * / // % << >> & \| ^`, comparisons as values, unary `-`, `not`, constructor casts, typed and untyped temporaries, nested. The worked examples of `integers.md` are pinned with `@example`. | +| `test_int_operators.py` | Every binary operator on every pair of operand types, values drawn edge-first. Random trees rarely reach a negative dividend under a signed `%` and return it undisturbed; this property always does. | +| `test_int_conversions.py` | Every (source type, destination type, site) triple, where a site is each place a conversion happens: constructor call, declaration, reassignment, untyped local, global store, `return`, global initialiser, and each augmented assignment. | +| `test_known_gaps.py` | Each known divergence's smallest program, as a strict xfail. | + +### Known gaps + +`known_gaps.py` lists the divergences from C the suite has found and not yet +had fixed. Each has a predicate, so the properties step around it and keep +finding *new* bugs, and a pinned program that `test_known_gaps.py` runs as a +strict xfail. A fix makes that test XPASS, failing the run until the gap is +deleted, at which point the properties cover that ground again. A failing +conversion site is a strict xfail on its parameter instead. + +### Running + +```bash +pytest tests/property # dev profile: 100 examples +HYPOTHESIS_PROFILE=thorough pytest tests/property # 3000 examples, for bug hunting +``` + +CI uses the `ci` profile (100 examples, derandomized, so a failure always +reproduces), about 90 seconds. The operator and conversion properties run a +quarter of the profile's count per parameter. Profiles are registered in +`conftest.py`. A failure prints both programs and the model's value; +Hypothesis shrinks it to the smallest program that still fails. + +### Plan + +1. **Integers and conversions** (done): the three properties above. A + mutation check (deliberately breaking `>>`, `%`, `/`, the usual arithmetic + conversions, integer promotion, sign extension and `c_bool` conversion in + the compiler) is caught every time, each shrunk to a program of two or + three lines. +2. **Fix the known gaps**, each on its own branch; its strict xfail flips to + XPASS and the gap is deleted. +3. **Widen the sites**: struct field stores and vmlinux field reads; map keys + and values, which needs helper calls stubbed with host functions in the + JIT; `range()` loops with random bounds, steps and types against CPython. +4. **Robustness**: every generated program in the supported subset must + also pass `llc` for BPF, and a program outside the subset must be rejected + with a deliberate error, never an internal `KeyError` or `TypeError`. + ## Directory structure ``` @@ -147,7 +210,13 @@ tests/ │ ├── bpf_test_case.py ← BpfTestCase dataclass │ ├── collector.py ← discovers test files, reads test_config.toml │ ├── compiler.py ← wrappers around compile_to_ir() + _run_llc() +│ ├── host_jit.py ← run a helper-free program's IR on the host │ └── verifier.py ← bpftool subprocess wrapper +├── property/ ← Hypothesis property tests (integers, conversions) +│ ├── cints.py ← reference model of C's integer rules +│ ├── programs.py ← generated programs, printed as PythonBPF and C +│ ├── harness.py ← compile both, JIT-run in a worker, compare +│ └── known_gaps.py ← divergences found and not yet fixed ├── passing_tests/ ← programs that should compile and verify cleanly ├── failing_tests/ ← programs with known issues (declared in test_config.toml) └── kernel_selftest_equivalent/ ← ports of kernel selftests + feature roadmap tests diff --git a/tests/property/__init__.py b/tests/property/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/tests/property/cints.py b/tests/property/cints.py new file mode 100644 index 0000000..993beb8 --- /dev/null +++ b/tests/property/cints.py @@ -0,0 +1,182 @@ +""" +A reference model of C's integer rules, as docs/user-guide/integers.md states +them for PythonBPF. + +clang is the specification; this model is not. It exists for two reasons: + +* To keep undefined behaviour out of the generated programs. Division by zero, + INT_MIN / -1 and out-of-range shift counts are undefined in C (and the first + two trap on the host), so a program that would hit them is discarded before + anything is compiled. Signed overflow is left in: the C reference is built + with -fwrapv, which defines it as wrapping, as BPF does. +* To give a third opinion when PythonBPF and clang disagree. If the model + disagrees with clang, the model is wrong; the property tests report that + separately from a compiler bug. + +Values are plain Python ints holding the value as the type reads it (so a +c_int8 holding 0xff is -1), and every operation returns (value, type). +""" + +from dataclasses import dataclass + + +class UndefinedBehaviour(Exception): + """The C program would be undefined here, so the example is discarded.""" + + +@dataclass(frozen=True) +class IntType: + name: str # the ctypes name, as written in PythonBPF source + c_name: str # the C type, as written in the reference program + bits: int + signed: bool + + @property + def is_bool(self) -> bool: + return self.name == "c_bool" + + @property + def min(self) -> int: + return -(1 << (self.bits - 1)) if self.signed else 0 + + @property + def max(self) -> int: + if self.is_bool: + return 1 + return (1 << (self.bits - 1)) - 1 if self.signed else (1 << self.bits) - 1 + + def __repr__(self) -> str: + return self.name + + +C_INT8 = IntType("c_int8", "signed char", 8, True) +C_INT16 = IntType("c_int16", "short", 16, True) +C_INT32 = IntType("c_int32", "int", 32, True) +C_INT64 = IntType("c_int64", "long long", 64, True) +C_UINT8 = IntType("c_uint8", "unsigned char", 8, False) +C_UINT16 = IntType("c_uint16", "unsigned short", 16, False) +C_UINT32 = IntType("c_uint32", "unsigned int", 32, False) +C_UINT64 = IntType("c_uint64", "unsigned long long", 64, False) +C_BOOL = IntType("c_bool", "_Bool", 8, False) + +INTEGER_TYPES = [ + C_INT8, + C_INT16, + C_INT32, + C_INT64, + C_UINT8, + C_UINT16, + C_UINT32, + C_UINT64, +] +ALL_TYPES = INTEGER_TYPES + [C_BOOL] + + +def convert(value: int, ty: IntType) -> int: + """C's conversion of `value` to `ty`: _Bool is `value != 0`; otherwise the + low `bits` bits, read with ty's sign (truncation, or reinterpretation at + the same width; widening is the identity on the value).""" + if ty.is_bool: + return int(value != 0) + value &= (1 << ty.bits) - 1 + if ty.signed and value >> (ty.bits - 1): + value -= 1 << ty.bits + return value + + +def literal_type(value: int) -> IntType: + """A non-negative decimal literal is an `int` if it fits, else 64-bit + signed (C's `long`/`long long`, the same on BPF and LP64 hosts).""" + assert 0 <= value <= C_INT64.max, value + return C_INT32 if value <= C_INT32.max else C_INT64 + + +def promote(ty: IntType) -> IntType: + """Integer promotion: anything narrower than int (and _Bool) becomes int.""" + return C_INT32 if ty.bits < 32 else ty + + +def common_type(a: IntType, b: IntType) -> IntType: + """C's usual arithmetic conversions, as integers.md lists them.""" + a, b = promote(a), promote(b) + if a.signed == b.signed: + return a if a.bits >= b.bits else b + unsigned, signed = (a, b) if not a.signed else (b, a) + return unsigned if unsigned.bits >= signed.bits else signed + + +def untyped_local_type(ty: IntType) -> IntType: + """An undeclared local is a 64-bit slot with the sign of its expression.""" + return C_INT64 if ty.signed else C_UINT64 + + +ARITH_OPS = ["+", "-", "*", "&", "|", "^"] +DIV_OPS = ["/", "//", "%"] +SHIFT_OPS = ["<<", ">>"] +COMPARE_OPS = ["<", "<=", ">", ">=", "==", "!="] + + +def binary_type(op: str, a: IntType, b: IntType) -> IntType: + if op in SHIFT_OPS: + return promote(a) # a shift has the type of its promoted left operand + if op in COMPARE_OPS: + return C_INT32 + return common_type(a, b) + + +def _trunc_div(a: int, b: int) -> int: + q = abs(a) // abs(b) + return q if (a < 0) == (b < 0) else -q + + +def binary(op: str, a: int, a_ty: IntType, b: int, b_ty: IntType) -> int: + """Value of `a op b` in C, given each operand's value and type.""" + if op in SHIFT_OPS: + ty = promote(a_ty) + if not 0 <= b < ty.bits: + raise UndefinedBehaviour(f"shift count {b} for a {ty.bits}-bit value") + a = convert(a, ty) + # Python's >> on a negative int is arithmetic, as C's is on a signed + # type; an unsigned value is never negative, so it shifts in zeros. + return convert(a << b if op == "<<" else a >> b, ty) + + ty = common_type(a_ty, b_ty) + a, b = convert(a, ty), convert(b, ty) + if op in COMPARE_OPS: + return int( + { + "<": a < b, + "<=": a <= b, + ">": a > b, + ">=": a >= b, + "==": a == b, + "!=": a != b, + }[op] + ) + if op in DIV_OPS: + if b == 0: + raise UndefinedBehaviour("division by zero") + if ty.signed and a == ty.min and b == -1: + raise UndefinedBehaviour(f"{ty.name} minimum divided by -1") + q = _trunc_div(a, b) + return convert(q if op != "%" else a - q * b, ty) + return convert( + { + "+": a + b, + "-": a - b, + "*": a * b, + "&": a & b, + "|": a | b, + "^": a ^ b, + }[op], + ty, + ) + + +def negate(a: int, a_ty: IntType) -> int: + ty = promote(a_ty) + return convert(-convert(a, ty), ty) + + +def logical_not(a: int) -> int: + return int(a == 0) diff --git a/tests/property/harness.py b/tests/property/harness.py new file mode 100644 index 0000000..9864824 --- /dev/null +++ b/tests/property/harness.py @@ -0,0 +1,188 @@ +""" +Compile a generated Program both ways, run both on the host, and compare. + +PythonBPF's IR is JIT compiled on the host (tests/framework/host_jit.py); the +C reference is compiled by clang, with -fwrapv, to a native object file that +the same JIT loads and links. Native code rather than `-target bpf` IR: the +IR a newer clang emits need not parse with llvmlite's LLVM, while an ELF +object always loads, and a fixed-width integer computation means the same on +BPF and on an LP64 host. (An object, not a shared library: linking was 60 of +the 90 ms an example took.) + +Both run in a worker process. The model only rules out undefined behaviour +for the *correct* types, so a miscompile can still trap (SIGFPE on a signed +division PythonBPF should not have emitted) or abort inside LLVM; in the +pytest process that would end the whole run. +""" + +import atexit +import ctypes +import itertools +import logging +import multiprocessing +import shutil +import subprocess +import tempfile +from concurrent.futures import ProcessPoolExecutor +from concurrent.futures.process import BrokenProcessPool +from pathlib import Path + +import llvmlite.binding as llvm +from hypothesis import assume, note +from hypothesis.control import currently_in_test_context + +from pythonbpf.codegen import compile_to_ir +from tests.framework.host_jit import run_function +from tests.property.cints import IntType, UndefinedBehaviour +from tests.property.programs import Program + +CLANG = shutil.which("clang") +WORKDIR = Path(tempfile.mkdtemp(prefix="pythonbpf-pbt-")) +atexit.register(shutil.rmtree, WORKDIR, ignore_errors=True) +_names = itertools.count() + + +class PythonBPFCompileError(Exception): + pass + + +class WorkerCrashed(Exception): + pass + + +# ── worker side ───────────────────────────────────────────────────────────── + + +def _run_ir(ll_text: str, restype_name: str) -> int: + return run_function(ll_text, "prog", getattr(ctypes, restype_name)) + + +def _run_object(path: str, restype_name: str) -> int: + llvm.initialize_native_target() + llvm.initialize_native_asmprinter() + tm = llvm.Target.from_default_triple().create_target_machine() + engine = llvm.create_mcjit_compiler(llvm.parse_assembly(""), tm) + engine.add_object_file(path) + engine.finalize_object() + func = ctypes.CFUNCTYPE(getattr(ctypes, restype_name), ctypes.c_void_p)( + engine.get_function_address("prog") + ) + return int(func(None)) + + +_pool = None + + +def _in_worker(fn, *args): + global _pool + if _pool is None: + _pool = ProcessPoolExecutor( + max_workers=1, mp_context=multiprocessing.get_context("forkserver") + ) + try: + return _pool.submit(fn, *args).result(timeout=60) + except BrokenProcessPool: + _pool = None + raise WorkerCrashed from None + + +@atexit.register +def _shutdown(): + if _pool is not None: + _pool.shutdown(cancel_futures=True) + + +# ── compile ───────────────────────────────────────────────────────────────── + + +class _Errors(logging.Handler): + """compile_to_ir can log an ERROR and carry on; that is a failure too.""" + + def __init__(self): + super().__init__(logging.ERROR) + self.messages = [] + + def emit(self, record): + self.messages.append(record.getMessage()) + + +def compile_pythonbpf(source: str) -> str: + stem = WORKDIR / f"p{next(_names)}" + py, ll = stem.with_suffix(".py"), stem.with_suffix(".ll") + py.write_text(source) + errors = _Errors() + logger = logging.getLogger("pythonbpf") + logger.addHandler(errors) + try: + compile_to_ir(str(py), str(ll), loglevel=logging.WARNING) + except Exception as e: + raise PythonBPFCompileError(f"{type(e).__name__}: {e}") from e + finally: + logger.removeHandler(errors) + if errors.messages: + raise PythonBPFCompileError("; ".join(errors.messages)) + return ll.read_text() + + +def compile_c(source: str) -> Path: + stem = WORKDIR / f"c{next(_names)}" + c, obj = stem.with_suffix(".c"), stem.with_suffix(".o") + c.write_text(source) + subprocess.run( + [CLANG, "-O0", "-fwrapv", "-w", "-c", "-fPIC", str(c), "-o", str(obj)], + check=True, + capture_output=True, + text=True, + ) + return obj + + +# ── the property ──────────────────────────────────────────────────────────── + + +def check_against_clang(program: Program, expected) -> None: + """Assert PythonBPF computes what clang computes for `program`. + + `expected` is a zero-argument callable returning the model's value; if it + raises UndefinedBehaviour the example is discarded before anything runs. + """ + in_hypothesis = currently_in_test_context() + try: + model = expected() + except UndefinedBehaviour: + if not in_hypothesis: + raise + assume(False) + py_source, c_source = program.py_source(), program.c_source() + # Shown with every failure: by note() under Hypothesis (which prints the + # shrunk example's notes), and in the message for a plain test. + shown = ( + f"\n\nPythonBPF source:\n{py_source}\nC reference:\n{c_source}\nmodel: {model}" + ) + if in_hypothesis: + note(shown) + shown = "" + ret: IntType = program.ret + + reference = _in_worker(_run_object, str(compile_c(c_source)), ret.name) + assert reference == model, ( + f"the model in tests/property/cints.py says {model}, clang says " + f"{reference}: the model is wrong, not PythonBPF{shown}" + ) + + try: + ll_text = compile_pythonbpf(py_source) + except PythonBPFCompileError as e: + raise AssertionError( + f"PythonBPF failed to compile the program: {e}{shown}" + ) from None + try: + got = _in_worker(_run_ir, ll_text, ret.name) + except WorkerCrashed: + raise AssertionError( + "PythonBPF's code crashed the host JIT (a trap or an LLVM abort); " + f"clang returns {reference}{shown}" + ) from None + assert got == reference, ( + f"PythonBPF returns {got}, clang returns {reference}{shown}" + ) diff --git a/tests/property/known_gaps.py b/tests/property/known_gaps.py new file mode 100644 index 0000000..0ca4aad --- /dev/null +++ b/tests/property/known_gaps.py @@ -0,0 +1,129 @@ +""" +Known divergences from C that the property tests step around. + +Each gap has a predicate that recognises a generated program hitting it, so +the properties keep looking for *new* bugs instead of re-finding this one, and +a pinned program that test_known_gaps.py runs as a strict xfail. When a fix +lands, that test XPASSes and fails the run: delete the gap here then, and the +properties start generating those programs again. +""" + +from dataclasses import dataclass +from typing import Callable + +from tests.property.cints import ( + C_INT8, + C_INT32, + C_INT64, + C_UINT8, + C_UINT32, + C_UINT64, + COMPARE_OPS, + SHIFT_OPS, + common_type, + promote, + untyped_local_type, +) +from tests.property.programs import Bin, ExpressionProgram, Lit, Neg, Not, Var + + +def walk(expr): + yield expr + for child in ("operand", "left", "right"): + if hasattr(expr, child): + yield from walk(getattr(expr, child)) + + +def nodes(program: ExpressionProgram): + for _, _, expr in program.temps: + yield from walk(expr) + yield from walk(program.result) + + +@dataclass(frozen=True) +class Gap: + name: str + reason: str + hits: Callable[[ExpressionProgram], bool] + # The smallest program showing it, run by test_known_gaps.py as a strict xfail + example: ExpressionProgram + + +GAPS: list[Gap] = [ + Gap( + "negated-literal-rank", + "`-2147483648` folds to a literal ranked by its negated value (int); " + "C ranks -x by x, and 2147483648 is a long long " + "(pythonbpf/expr/expr_pass.py, the USub constant fold)", + lambda p: any( + isinstance(n, Neg) + and isinstance(n.operand, Lit) + and n.operand.value == 2**31 + for n in nodes(p) + ), + # C: a 64-bit signed compare, 1. PythonBPF: an unsigned 32-bit one, 0. + ExpressionProgram( + [("a0", C_UINT32, 1)], [], Bin("<", Neg(Lit(2**31)), Var("a0", C_UINT32)) + ), + ), + Gap( + "untyped-local-unary-or-compare", + '`t = -x`, `t = not x` and `t = a < b` fail with "Undefined variable ' + 't": the allocation pass has no case for a UnaryOp or Compare ' + "right-hand side, so the local never gets a slot " + "(pythonbpf/allocation_pass.py, _allocate_for_value)", + lambda p: any( + isinstance(e, (Neg, Not)) or (isinstance(e, Bin) and e.op in COMPARE_OPS) + for _, _, e in p.temps + ), + ExpressionProgram( + [("a0", C_INT32, 3)], + [("t0", C_INT64, Neg(Var("a0", C_INT32)))], + Var("t0", C_INT64), + ), + ), + Gap( + "shift-result-type", + "a shift is typed by the usual arithmetic conversions of both operands; " + "C types it by the promoted left operand alone, so `int << s64` must " + "wrap at 32 bits and `s64 >> u64` must be arithmetic " + "(pythonbpf/expr/expr_pass.py _handle_binary_op_impl, " + "type_inference.py infer_int_type, and for `<<=`/`>>=` " + "functions/functions_pass.py's augmented assignment)", + lambda p: any( + isinstance(n, Bin) + and n.op in SHIFT_OPS + and promote(n.left.ty) != common_type(n.left.ty, n.right.ty) + for n in nodes(p) + ), + # C: -8 >> 1 in s64, -4. PythonBPF: a logical shift in u64. + ExpressionProgram( + [("a0", C_INT64, -8), ("a1", C_UINT64, 1)], + [], + Bin(">>", Var("a0", C_INT64), Var("a1", C_UINT64)), + ), + ), + Gap( + "untyped-copy-keeps-narrow-type", + "`t = a` gives t a's own type, so a c_bool/c_uint8/c_uint16 copy stays " + "narrow and promotes to int; integers.md says an undeclared local is " + "always 64 bits with the expression's sign (unsigned here). Code or " + "doc: a decision (pythonbpf/allocation_pass.py, _allocate_for_name)", + lambda p: any(isinstance(e, Var) and e.ty.bits < 32 for _, _, e in p.temps), + # C, by integers.md: -128 + (u64)1 is a u64, so 0 < it holds. PythonBPF: + # t1 stays a u8, the sum is the int -127, and the compare is false. + ExpressionProgram( + [("a0", C_INT8, -128), ("a1", C_UINT8, 1)], + [("t1", untyped_local_type(C_UINT8), Var("a1", C_UINT8))], + Bin( + "<", + Lit(0), + Bin("+", Var("a0", C_INT8), Var("t1", untyped_local_type(C_UINT8))), + ), + ), + ), +] + + +def gap_of(program: ExpressionProgram) -> "Gap | None": + return next((g for g in GAPS if g.hits(program)), None) diff --git a/tests/property/programs.py b/tests/property/programs.py new file mode 100644 index 0000000..e44f686 --- /dev/null +++ b/tests/property/programs.py @@ -0,0 +1,358 @@ +""" +Generated integer programs, printed twice: as PythonBPF source and as the C +program clang compiles for the same computation. + +A program is straight-line: input locals declared with a constructor and a +literal, optional temporaries, and a returned expression. Inputs are locals, +not literals, so neither compiler sees a constant expression; clang at -O0 +and PythonBPF both load them from the stack. + +What is not generated, and why (bugs PythonBPF has are generated, and stepped +around by tests/property/known_gaps.py instead): + * `~x`: PythonBPF does not support unary invert (a clean error). + * `and` / `or`: not C's integer operators, and not an integer question. + * Literal initialisers of @bpfglobal variables other than 0, outside + test_int_conversions' strict-xfail site: a negative one is silently + emitted as 0 (pythonbpf/globals_pass.py). +""" + +from dataclasses import dataclass, field + +from hypothesis import strategies as st + +from tests.property.cints import ( + ALL_TYPES, + ARITH_OPS, + C_INT32, + C_INT64, + COMPARE_OPS, + DIV_OPS, + SHIFT_OPS, + IntType, + binary, + binary_type, + convert, + literal_type, + logical_not, + negate, + promote, + untyped_local_type, +) + +INT64_MIN = -(1 << 63) +INT64_MAX = (1 << 63) - 1 + + +def literal_source(value: int) -> str: + """A decimal literal for `value` in [INT64_MIN, INT64_MAX], valid in both + languages and of a 64-bit-or-narrower signed type in C. Hex is never + used: C gives a hex literal that does not fit `int` an unsigned type.""" + if value >= 0: + return str(value) + if value == INT64_MIN: + return "(-9223372036854775807 - 1)" + return f"(-{-value})" + + +def as_literal(value: int, ty: IntType) -> int: + """A literal that converts to `value` in `ty` (a u64 above INT64_MAX is + written as the negative number with the same bits).""" + return value - (1 << 64) if value > INT64_MAX else value + + +# ── expressions ───────────────────────────────────────────────────────────── + + +@dataclass(frozen=True) +class Var: + name: str + ty: IntType + + def py(self) -> str: + return self.name + + def c(self) -> str: + return self.name + + def eval(self, env: dict) -> int: + return env[self.name] + + +@dataclass(frozen=True) +class Lit: + value: int # non-negative; a negative constant is Neg(Lit(n)), as in both languages + + @property + def ty(self) -> IntType: + return literal_type(self.value) + + def py(self) -> str: + return str(self.value) + + def c(self) -> str: + return str(self.value) + + def eval(self, env: dict) -> int: + return self.value + + +@dataclass(frozen=True) +class Neg: + operand: object + + @property + def ty(self) -> IntType: + return promote(self.operand.ty) + + def py(self) -> str: + return f"(-{self.operand.py()})" + + def c(self) -> str: + return f"(-{self.operand.c()})" + + def eval(self, env: dict) -> int: + return negate(self.operand.eval(env), self.operand.ty) + + +@dataclass(frozen=True) +class Not: + operand: object + + @property + def ty(self) -> IntType: + return C_INT32 # C's `!` is an int + + def py(self) -> str: + return f"(not {self.operand.py()})" + + def c(self) -> str: + return f"(!{self.operand.c()})" + + def eval(self, env: dict) -> int: + return logical_not(self.operand.eval(env)) + + +@dataclass(frozen=True) +class Cast: + ty: IntType + operand: object + + def py(self) -> str: + return f"{self.ty.name}({self.operand.py()})" + + def c(self) -> str: + return f"(({self.ty.c_name})({self.operand.c()}))" + + def eval(self, env: dict) -> int: + return convert(self.operand.eval(env), self.ty) + + +@dataclass(frozen=True) +class Bin: + op: str + left: object + right: object + + @property + def ty(self) -> IntType: + return binary_type(self.op, self.left.ty, self.right.ty) + + def py(self) -> str: + return f"({self.left.py()} {self.op} {self.right.py()})" + + def c(self) -> str: + op = "/" if self.op == "//" else self.op # both are C's truncating `/` + return f"({self.left.c()} {op} {self.right.c()})" + + def eval(self, env: dict) -> int: + return binary( + self.op, + self.left.eval(env), + self.left.ty, + self.right.eval(env), + self.right.ty, + ) + + +# ── programs ──────────────────────────────────────────────────────────────── + +PY_HEADER = """\ +from pythonbpf import bpf, section, bpfglobal, compile +from ctypes import ( + c_void_p, + c_bool, + c_int8, + c_int16, + c_int32, + c_int64, + c_uint8, + c_uint16, + c_uint32, + c_uint64, +) +""" + +PY_FOOTER = """ + +@bpf +@bpfglobal +def LICENSE() -> str: + return "GPL" + + +compile() +""" + + +@dataclass +class Program: + """One program in both languages. `globals` are (name, type, initial + literal); `py_body` and `c_body` are the statements of `prog`, in order.""" + + py_body: list[str] + c_body: list[str] + ret: IntType = C_INT64 + globals: list[tuple[str, IntType, int]] = field(default_factory=list) + + def py_source(self) -> str: + parts = [PY_HEADER] + for name, ty, init in self.globals: + parts.append( + f"\n@bpf\n@bpfglobal\ndef {name}() -> {ty.name}:\n" + f" return {ty.name}({literal_source(init)})\n" + ) + body = "".join(f" {line}\n" for line in self.py_body) + parts.append( + '\n@bpf\n@section("tracepoint/syscalls/sys_enter_getpid")\n' + f"def prog(ctx: c_void_p) -> {self.ret.name}:\n{body}" + ) + parts.append(PY_FOOTER) + return "".join(parts) + + def c_source(self) -> str: + lines = [ + f"{ty.c_name} {name} = {literal_source(init)};" + for name, ty, init in self.globals + ] + lines.append(f"{self.ret.c_name} prog(void *ctx)\n{{") + lines += [f" {line}" for line in self.c_body] + lines.append("}") + return "\n".join(lines) + "\n" + + +def input_decl(name: str, ty: IntType, value: int) -> tuple[str, str]: + """`name = c_T(lit)` and `T name = lit;` for an input holding `value`.""" + lit = literal_source(as_literal(value, ty)) + return f"{name} = {ty.name}({lit})", f"{ty.c_name} {name} = {lit};" + + +@dataclass +class ExpressionProgram: + """Inputs, temporaries and a returned expression; `program()` prints it + and `expected()` is the model's value (raising UndefinedBehaviour).""" + + inputs: list[tuple[str, IntType, int]] + temps: list[tuple[str, IntType, object]] # name, declared type, expression + result: object + + def program(self) -> Program: + py, c = [], [] + for name, ty, value in self.inputs: + p, q = input_decl(name, ty, value) + py.append(p) + c.append(q) + for name, ty, expr in self.temps: + py.append(f"{name} = {expr.py()}") + c.append(f"{ty.c_name} {name} = {expr.c()};") + py.append(f"return {self.result.py()}") + c.append(f"return {self.result.c()};") + return Program(py, c) + + def expected(self) -> int: + env = {name: value for name, _, value in self.inputs} + for name, ty, expr in self.temps: + env[name] = convert(expr.eval(env), ty) + return convert(self.result.eval(env), C_INT64) + + +# ── strategies ────────────────────────────────────────────────────────────── + + +def edge_values(ty: IntType) -> list[int]: + """The values where integer bugs live: zero, ±1, the type's limits, and + the limits of every narrower type.""" + candidates = {0, 1, -1, 2, ty.min, ty.max, ty.min + 1, ty.max - 1} + for k in (7, 8, 15, 16, 31, 32, 63): + candidates |= {1 << k, (1 << k) - 1, -(1 << k), -(1 << k) + 1} + return sorted(v for v in candidates if ty.min <= v <= ty.max) + + +def values_of(ty: IntType) -> st.SearchStrategy[int]: + return st.one_of(st.sampled_from(edge_values(ty)), st.integers(ty.min, ty.max)) + + +LITERALS = st.one_of( + st.sampled_from( + [0, 1, 2, 3, 7, 8, 31, 32, 63, 64, 127, 128, 255, 256, 32767, 32768, 65535] + + [65536, 2**31 - 1, 2**31, 2**32 - 1, 2**32, 2**63 - 1] + ), + st.integers(0, INT64_MAX), +) + + +@st.composite +def expressions(draw, leaves: list[Var], depth: int): + if depth == 0 or draw(st.integers(0, 3)) == 0: + # Mostly inputs: a literal is non-negative and often small, so a + # tree of literals rarely reaches a sign-sensitive case. + if leaves and draw(st.integers(0, 3)) > 0: + return draw(st.sampled_from(leaves)) + return Lit(draw(LITERALS)) + + sub = expressions(leaves, depth - 1) + kind = draw( + st.sampled_from( + ["arith", "arith", "div", "shift", "compare", "neg", "not", "cast"] + ) + ) + if kind == "neg": + return Neg(draw(sub)) + if kind == "not": + return Not(draw(sub)) + if kind == "cast": + return Cast(draw(st.sampled_from(ALL_TYPES)), draw(sub)) + if kind == "shift": + left, right = draw(sub), draw(sub) + # Mask the count into range so the shift is defined; the mask is a + # literal, so `right & mask` is never negative. + mask = Lit(promote(left.ty).bits - 1) + return Bin(draw(st.sampled_from(SHIFT_OPS)), left, Bin("&", right, mask)) + op = draw( + st.sampled_from( + {"arith": ARITH_OPS, "div": DIV_OPS, "compare": COMPARE_OPS}[kind] + ) + ) + return Bin(op, draw(sub), draw(sub)) + + +@st.composite +def expression_programs( + draw, max_inputs: int = 4, max_temps: int = 2, max_depth: int = 4 +): + inputs = [] + for i in range(draw(st.integers(1, max_inputs))): + ty = draw(st.sampled_from(ALL_TYPES)) + inputs.append((f"a{i}", ty, draw(values_of(ty)))) + leaves = [Var(name, ty) for name, ty, _ in inputs] + + temps = [] + for i in range(draw(st.integers(0, max_temps))): + expr = draw(expressions(leaves, draw(st.integers(1, 3)))) + # A constructor call declares the local with that type; anything else + # is an undeclared local: 64 bits, with the expression's sign. + ty = expr.ty if isinstance(expr, Cast) else untyped_local_type(expr.ty) + temps.append((f"t{i}", ty, expr)) + leaves.append(Var(f"t{i}", ty)) + + result = draw(expressions(leaves, draw(st.integers(0, max_depth)))) + return ExpressionProgram(inputs, temps, result) diff --git a/tests/property/test_int_conversions.py b/tests/property/test_int_conversions.py new file mode 100644 index 0000000..4689ec1 --- /dev/null +++ b/tests/property/test_int_conversions.py @@ -0,0 +1,145 @@ +""" +Integer conversions at every place PythonBPF converts: PythonBPF computes what +clang computes. + +A value of one type is converted to another at each site where integers.md +says a conversion happens (constructor calls, typed and untyped locals, +globals, `return`, augmented assignment). Random expressions reach these sites +only by accident; here every (source type, destination type, site) triple is +tested, with Hypothesis choosing the values, the edge values of each type +first. +""" + +import pytest +from hypothesis import assume, given, settings +from hypothesis import strategies as st + +from tests.property.cints import ( + ALL_TYPES, + ARITH_OPS, + C_INT64, + DIV_OPS, + SHIFT_OPS, + binary, + common_type, + convert, + promote, + untyped_local_type, +) +from tests.property.harness import CLANG, check_against_clang +from tests.property.programs import ( + INT64_MAX, + INT64_MIN, + Program, + as_literal, + input_decl, + literal_source, + values_of, +) + +pytestmark = pytest.mark.skipif(CLANG is None, reason="clang is not installed") + +TYPES = st.sampled_from(ALL_TYPES) + + +def _site_program(site, src, dst, value, other): + """(Program, model) for converting `a0`, a `src` holding `value`, to `dst` + at `site`. `other` is a second value, used where a site needs one.""" + decl_py, decl_c = input_decl("a0", src, value) + as_i64 = lambda v: convert(v, C_INT64) # noqa: E731 (prog returns c_int64) + + if site == "constructor": + return Program( + [decl_py, f"return {dst.name}(a0)"], + [decl_c, f"return ({dst.c_name})a0;"], + ), lambda: as_i64(convert(value, dst)) + if site == "declare": + return Program( + [decl_py, f"x = {dst.name}(a0)", "return x"], + [decl_c, f"{dst.c_name} x = a0;", "return x;"], + ), lambda: as_i64(convert(value, dst)) + if site == "reassign": + return Program( + [decl_py, f"x = {dst.name}(0)", "x = a0", "return x"], + [decl_c, f"{dst.c_name} x = 0;", "x = a0;", "return x;"], + ), lambda: as_i64(convert(value, dst)) + if site == "untyped_local": + # dst plays no part: an undeclared local is 64 bits with a0's sign + local = untyped_local_type(src) + return Program( + [decl_py, "x = a0", "return x"], + [decl_c, f"{local.c_name} x = a0;", "return x;"], + ), lambda: as_i64(convert(value, local)) + if site == "global_store": + return Program( + [decl_py, "global out", "out = a0", "return out"], + [decl_c, "out = a0;", "return out;"], + globals=[("out", dst, 0)], + ), lambda: as_i64(convert(value, dst)) + if site == "return": + return Program([decl_py, "return a0"], [decl_c, "return a0;"], ret=dst), ( + lambda: convert(value, dst) + ) + if site == "global_init": + # `value` is used as the initialiser literal itself + lit = as_literal(value, src) + return Program( + ["return g"], ["return g;"], globals=[("g", dst, lit)] + ), lambda: as_i64(convert(lit, dst)) + if site.startswith("augassign"): + op = site.split(" ")[1] + init = as_literal(other, dst) + return Program( + [ + decl_py, + f"x = {dst.name}({literal_source(init)})", + f"x {op}= a0", + "return x", + ], + [ + decl_c, + f"{dst.c_name} x = {literal_source(init)};", + f"x {'/' if op == '//' else op}= a0;", + "return x;", + ], + ), lambda: as_i64(convert(binary(op, convert(init, dst), dst, value, src), dst)) + raise ValueError(site) + + +SITES = [ + "constructor", + "declare", + "reassign", + "untyped_local", + "global_store", + "return", + pytest.param( + "global_init", + marks=pytest.mark.xfail( + strict=True, + raises=AssertionError, + reason="a @bpfglobal initialiser that is not a bare constant (as " + "c_int64(-5) is not: -5 is a UnaryOp) is emitted as 0, and a " + "constant is not converted to the type (c_bool(2) keeps the low " + "bit, 0, where C gives 1) (pythonbpf/globals_pass.py, _emit_global)", + ), + ), +] + [f"augassign {op}" for op in ARITH_OPS + DIV_OPS + SHIFT_OPS] + + +# A quarter of the profile's examples per site: there are 18 sites, and each +# example is cheap to state but costs a clang run (~40 ms). +@pytest.mark.parametrize("site", SITES) +@settings(max_examples=max(10, settings.default.max_examples // 4)) +@given(src=TYPES, dst=TYPES, data=st.data()) +def test_conversion_matches_clang(site, src, dst, data): + value = data.draw(values_of(src), label="value") + other = data.draw(values_of(dst), label="other") + if site == "global_init": + value = data.draw(st.integers(INT64_MIN, INT64_MAX), label="initialiser") + if site in ("augassign <<", "augassign >>"): + # known gap shift-result-type: `x >>= a` is typed by both operands + # (test_known_gaps.py pins this case) + assume(promote(dst) == common_type(dst, src)) + program, expected = _site_program(site, src, dst, value, other) + check_against_clang(program, expected) diff --git a/tests/property/test_int_expressions.py b/tests/property/test_int_expressions.py new file mode 100644 index 0000000..34620f8 --- /dev/null +++ b/tests/property/test_int_expressions.py @@ -0,0 +1,93 @@ +""" +Integer expressions: PythonBPF computes what clang computes. + +Random straight-line programs over every ctypes integer type (and c_bool): +arithmetic, division and remainder, shifts, comparisons used as values, unary +minus, `not`, constructor casts and untyped temporaries, nested. Each one is +printed as PythonBPF and as C, both are run on the host, and the results must +be equal. The rules being exercised are docs/user-guide/integers.md; clang is +their specification. +""" + +import pytest +from hypothesis import assume, example, given + +from tests.property.cints import ( + C_INT8, + C_INT32, + C_INT64, + C_UINT8, + C_UINT16, + C_UINT32, + C_UINT64, +) +from tests.property.harness import CLANG, check_against_clang +from tests.property.known_gaps import gap_of +from tests.property.programs import ( + Bin, + Cast, + ExpressionProgram, + Lit, + Neg, + Var, + expression_programs, +) + +pytestmark = pytest.mark.skipif(CLANG is None, reason="clang is not installed") + + +def _p(inputs, result, temps=()): + return ExpressionProgram(list(inputs), list(temps), result) + + +def _v(name, ty): + return Var(name, ty) + + +# The worked examples in integers.md, pinned so they always run. +DOC_EXAMPLES = [ + # u32 * u32 wraps at 32 bits before any widening + _p( + [("a0", C_UINT32, 0x80000000), ("a1", C_UINT32, 2)], + Bin("*", _v("a0", C_UINT32), _v("a1", C_UINT32)), + ), + # mixed signs go unsigned: 10u / -2 is 10 / 0xfffffffe + _p( + [("a0", C_UINT32, 10), ("a1", C_INT32, -2)], + Bin("/", _v("a0", C_UINT32), _v("a1", C_INT32)), + ), + # c_uint64(10) > c_int64(-1) is an unsigned compare: false + _p( + [("a0", C_UINT64, 10), ("a1", C_INT64, -1)], + Bin(">", _v("a0", C_UINT64), _v("a1", C_INT64)), + ), + # the literal -2 is an int, so count / -2 is a u32 division + _p([("a0", C_UINT32, 10)], Bin("/", _v("a0", C_UINT32), Neg(Lit(2)))), + # narrow operands promote to int: s8 * u16 is a signed 32-bit product + _p( + [("a0", C_INT8, -3), ("a1", C_UINT16, 65535)], + Bin("*", _v("a0", C_INT8), _v("a1", C_UINT16)), + ), + # a constructor-typed temporary keeps its width: c_uint8(300) is 44 + _p( + [("a0", C_INT32, 300)], + Bin("+", _v("t0", C_UINT8), Lit(0)), + temps=[("t0", C_UINT8, Cast(C_UINT8, _v("a0", C_INT32)))], + ), +] + + +def _pin(*programs): + def wrap(fn): + for program in reversed(programs): + fn = example(program)(fn) + return fn + + return wrap + + +@_pin(*DOC_EXAMPLES) +@given(expression_programs()) +def test_integer_expression_matches_clang(program): + assume(gap_of(program) is None) + check_against_clang(program.program(), program.expected) diff --git a/tests/property/test_int_operators.py b/tests/property/test_int_operators.py new file mode 100644 index 0000000..a3a65f8 --- /dev/null +++ b/tests/property/test_int_operators.py @@ -0,0 +1,52 @@ +""" +Every binary operator on every pair of operand types: PythonBPF computes what +clang computes. + +test_int_expressions finds bugs in how operations combine, but random trees +rarely put, say, a negative dividend under a signed `%` and then return the +result undisturbed (about 3 programs in 600 did). This property is the +enumerated complement: `a0 op a1` for each operator, left type and right type, +with Hypothesis choosing the operand values, the edge values of each type +first. Shift counts are drawn in range, since an out-of-range count is +undefined in C. +""" + +import pytest +from hypothesis import assume, given, settings +from hypothesis import strategies as st + +from tests.property.cints import ( + ALL_TYPES, + ARITH_OPS, + COMPARE_OPS, + DIV_OPS, + SHIFT_OPS, + promote, +) +from tests.property.harness import CLANG, check_against_clang +from tests.property.known_gaps import gap_of +from tests.property.programs import Bin, ExpressionProgram, Var, values_of + +pytestmark = pytest.mark.skipif(CLANG is None, reason="clang is not installed") + +TYPES = st.sampled_from(ALL_TYPES) + + +# A quarter of the profile's examples per operator, as there are 17 of them. +@pytest.mark.parametrize("op", ARITH_OPS + DIV_OPS + SHIFT_OPS + COMPARE_OPS) +@settings(max_examples=max(10, settings.default.max_examples // 4)) +@given(left_ty=TYPES, right_ty=TYPES, data=st.data()) +def test_binary_operator_matches_clang(op, left_ty, right_ty, data): + left = data.draw(values_of(left_ty), label="left") + if op in SHIFT_OPS: + count = st.integers(0, min(promote(left_ty).bits - 1, right_ty.max)) + right = data.draw(count, label="right") + else: + right = data.draw(values_of(right_ty), label="right") + program = ExpressionProgram( + [("a0", left_ty, left), ("a1", right_ty, right)], + [], + Bin(op, Var("a0", left_ty), Var("a1", right_ty)), + ) + assume(gap_of(program) is None) + check_against_clang(program.program(), program.expected) diff --git a/tests/property/test_known_gaps.py b/tests/property/test_known_gaps.py new file mode 100644 index 0000000..ab9fc3e --- /dev/null +++ b/tests/property/test_known_gaps.py @@ -0,0 +1,46 @@ +""" +Each known gap's smallest program, as a strict xfail: when a fix lands it +XPASSes and fails the run, as a reminder to delete the gap from +tests/property/known_gaps.py so the properties cover that ground again. +""" + +import pytest + +from tests.property.cints import C_INT64, convert +from tests.property.harness import CLANG, check_against_clang +from tests.property.known_gaps import GAPS +from tests.property.programs import Program + +pytestmark = pytest.mark.skipif(CLANG is None, reason="clang is not installed") + + +@pytest.mark.parametrize( + "gap", + [ + pytest.param( + g, + id=g.name, + marks=pytest.mark.xfail( + strict=True, raises=AssertionError, reason=g.reason + ), + ) + for g in GAPS + ], +) +def test_known_gap_still_diverges(gap): + assert gap.hits(gap.example), "the pinned program must hit its own gap" + check_against_clang(gap.example.program(), gap.example.expected) + + +@pytest.mark.xfail( + strict=True, + raises=AssertionError, + reason="shift-result-type, in augmented assignment: `x >>= a` with x a " + "c_int32 and a a c_uint32 shifts logically in u32; C shifts x's own int", +) +def test_known_gap_augassign_shift(): + program = Program( + ["a0 = c_uint32(1)", "x = c_int32(-2147483648)", "x >>= a0", "return x"], + ["unsigned int a0 = 1;", "int x = -2147483648;", "x >>= a0;", "return x;"], + ) + check_against_clang(program, lambda: convert(-(2**31) >> 1, C_INT64)) From 32c1afff3691f742a77b67b992cb03bfaa0ac8e1 Mon Sep 17 00:00:00 2001 From: Pragyansh Chaturvedi Date: Tue, 27 Oct 2026 21:55:59 +0530 Subject: [PATCH 4/4] Tests: Make the integer properties cover every type on every run Review of the first version of the suite found four holes. - The conversion sites returned the converted value, which shows its bits but not the type it was stored as. The untyped_local site passed over a real bug that way. Each site now reads the value back through an expression whose result depends on its sign and width. - With the type drawn at random, 25 examples per site left a single type with about 3. A deliberately broken c_bool conversion went undetected under some seeds. The conversion property is now parametrized by destination type and the operator property by left operand type, a sixteenth of the profile's examples each. - The global_init site was a strict xfail. Hypothesis shrank its expected failures, which took 115 of the property's 187 seconds. Its two bugs are now pinned in test_known_gaps.py, and the site steps around them. - Gaps are now stepped around by drawing only inputs that avoid them, not by assume(). Filtering tripped Hypothesis's filter_too_much health check. untyped-copy-keeps-narrow-type is renamed untyped-copy-keeps-source-type. `t = a` keeps a's type for any source that is not 64-bit, c_uint32 and c_int32 included, not only narrow ones. Under the ci profile, each of these deliberate compiler bugs fails a property: - >> always logical - % always unsigned - / always unsigned - equal-width mixed signs going signed - promotion keeping an unsigned sign - widening always by zero-extension - c_bool conversion by truncation Co-Authored-By: Claude Opus 5.5 --- tests/README.md | 17 ++- tests/property/known_gaps.py | 16 ++- tests/property/test_int_conversions.py | 170 ++++++++++++++++--------- tests/property/test_int_operators.py | 9 +- tests/property/test_known_gaps.py | 20 ++- 5 files changed, 154 insertions(+), 78 deletions(-) diff --git a/tests/README.md b/tests/README.md index a5f5a5d..0d94052 100644 --- a/tests/README.md +++ b/tests/README.md @@ -154,8 +154,8 @@ programs are generated, and each one is compiled two ways and run. | File | Property | |---|---| | `test_int_expressions.py` | Random straight-line programs over every ctypes integer type and `c_bool`: `+ - * / // % << >> & \| ^`, comparisons as values, unary `-`, `not`, constructor casts, typed and untyped temporaries, nested. The worked examples of `integers.md` are pinned with `@example`. | -| `test_int_operators.py` | Every binary operator on every pair of operand types, values drawn edge-first. Random trees rarely reach a negative dividend under a signed `%` and return it undisturbed; this property always does. | -| `test_int_conversions.py` | Every (source type, destination type, site) triple, where a site is each place a conversion happens: constructor call, declaration, reassignment, untyped local, global store, `return`, global initialiser, and each augmented assignment. | +| `test_int_operators.py` | Every binary operator, parametrized by the left operand's type, with the right type and both values drawn (edge values first). Random trees rarely reach a negative dividend under a signed `%` and return it undisturbed; this property always does. | +| `test_int_conversions.py` | Every conversion site, parametrized by the destination type: constructor call, declaration, reassignment, untyped local, global store, `return`, global initialiser, and each augmented assignment. The converted value is read back through an expression whose result depends on its sign and width, not just returned, so a value stored with the right bits but the wrong type is caught too. | | `test_known_gaps.py` | Each known divergence's smallest program, as a strict xfail. | ### Known gaps @@ -164,8 +164,10 @@ programs are generated, and each one is compiled two ways and run. had fixed. Each has a predicate, so the properties step around it and keep finding *new* bugs, and a pinned program that `test_known_gaps.py` runs as a strict xfail. A fix makes that test XPASS, failing the run until the gap is -deleted, at which point the properties cover that ground again. A failing -conversion site is a strict xfail on its parameter instead. +deleted, at which point the properties cover that ground again. The +operator and conversion properties step around a gap by drawing only what +avoids it (not by filtering, which Hypothesis rightly complains about), with +a comment naming the gap. ### Running @@ -175,9 +177,10 @@ HYPOTHESIS_PROFILE=thorough pytest tests/property # 3000 examples, for bug hunt ``` CI uses the `ci` profile (100 examples, derandomized, so a failure always -reproduces), about 90 seconds. The operator and conversion properties run a -quarter of the profile's count per parameter. Profiles are registered in -`conftest.py`. A failure prints both programs and the model's value; +reproduces): about two and a half minutes on a 16-core machine. The +operator and conversion properties are parametrized by type, so every type +is tested on every run, and run a sixteenth of the profile's count per +parameter. Profiles are registered in `conftest.py`. A failure prints both programs and the model's value; Hypothesis shrinks it to the smallest program that still fails. ### Plan diff --git a/tests/property/known_gaps.py b/tests/property/known_gaps.py index 0ca4aad..7fd4bc5 100644 --- a/tests/property/known_gaps.py +++ b/tests/property/known_gaps.py @@ -104,12 +104,16 @@ class Gap: ), ), Gap( - "untyped-copy-keeps-narrow-type", - "`t = a` gives t a's own type, so a c_bool/c_uint8/c_uint16 copy stays " - "narrow and promotes to int; integers.md says an undeclared local is " - "always 64 bits with the expression's sign (unsigned here). Code or " - "doc: a decision (pythonbpf/allocation_pass.py, _allocate_for_name)", - lambda p: any(isinstance(e, Var) and e.ty.bits < 32 for _, _, e in p.temps), + "untyped-copy-keeps-source-type", + "`t = a` gives t a's own type, whatever it is: a c_uint32 copy stays " + "u32 and a c_int8 copy stays narrow and promotes to int, while " + "integers.md says an undeclared local is always 64 bits with the " + "expression's sign. Only a 64-bit source is unaffected. Code or doc: " + "a decision (pythonbpf/allocation_pass.py, _allocate_for_name)", + lambda p: any( + isinstance(e, Var) and e.ty != untyped_local_type(e.ty) + for _, _, e in p.temps + ), # C, by integers.md: -128 + (u64)1 is a u64, so 0 < it holds. PythonBPF: # t1 stays a u8, the sum is the int -127, and the compare is false. ExpressionProgram( diff --git a/tests/property/test_int_conversions.py b/tests/property/test_int_conversions.py index 4689ec1..9b18812 100644 --- a/tests/property/test_int_conversions.py +++ b/tests/property/test_int_conversions.py @@ -11,7 +11,7 @@ """ import pytest -from hypothesis import assume, given, settings +from hypothesis import given, settings from hypothesis import strategies as st from tests.property.cints import ( @@ -29,8 +29,11 @@ from tests.property.harness import CLANG, check_against_clang from tests.property.programs import ( INT64_MAX, - INT64_MIN, + Bin, + Cast, + Lit, Program, + Var, as_literal, input_decl, literal_source, @@ -39,70 +42,100 @@ pytestmark = pytest.mark.skipif(CLANG is None, reason="clang is not installed") -TYPES = st.sampled_from(ALL_TYPES) + +# How the converted value is read back. `return x` alone shows the value but +# not the type it was stored as, and a later use depends on that type: these +# read it through an operation whose result changes with its sign and width. +PROBES = { + "value": lambda x: x, + # -1 in x's type (promoted), halved: 0 if signed, and u32 and u64 differ + "sign_and_width": lambda x: Bin("/", Bin("-", Bin("*", x, Lit(0)), Lit(1)), Lit(2)), + # INT_MAX + 1 wraps if x's type promotes to a 32-bit int, not if 64-bit + "int_overflow": lambda x: Bin( + "+", Bin("+", Bin("*", x, Lit(0)), Lit(2**31 - 1)), Lit(1) + ), +} -def _site_program(site, src, dst, value, other): +def _site_program(site, src, dst, value, other, probe): """(Program, model) for converting `a0`, a `src` holding `value`, to `dst` - at `site`. `other` is a second value, used where a site needs one.""" + at `site`, then returning probe(the converted value). `other` is a second + value, used where a site needs one.""" decl_py, decl_c = input_decl("a0", src, value) - as_i64 = lambda v: convert(v, C_INT64) # noqa: E731 (prog returns c_int64) + + def read_back(name, ty, stored, py, c, globals=()): + """Finish a program whose statements stored `stored` into `name`.""" + expr = probe(Var(name, ty)) + program = Program( + py + [f"return {expr.py()}"], + c + [f"return {expr.c()};"], + globals=list(globals), + ) + return program, lambda: convert(expr.eval({name: stored()}), C_INT64) if site == "constructor": + expr = probe(Cast(dst, Var("a0", src))) return Program( - [decl_py, f"return {dst.name}(a0)"], - [decl_c, f"return ({dst.c_name})a0;"], - ), lambda: as_i64(convert(value, dst)) + [decl_py, f"return {expr.py()}"], [decl_c, f"return {expr.c()};"] + ), lambda: convert(expr.eval({"a0": value}), C_INT64) if site == "declare": - return Program( - [decl_py, f"x = {dst.name}(a0)", "return x"], - [decl_c, f"{dst.c_name} x = a0;", "return x;"], - ), lambda: as_i64(convert(value, dst)) + return read_back( + "x", + dst, + lambda: convert(value, dst), + [decl_py, f"x = {dst.name}(a0)"], + [decl_c, f"{dst.c_name} x = a0;"], + ) if site == "reassign": - return Program( - [decl_py, f"x = {dst.name}(0)", "x = a0", "return x"], - [decl_c, f"{dst.c_name} x = 0;", "x = a0;", "return x;"], - ), lambda: as_i64(convert(value, dst)) + return read_back( + "x", + dst, + lambda: convert(value, dst), + [decl_py, f"x = {dst.name}(0)", "x = a0"], + [decl_c, f"{dst.c_name} x = 0;", "x = a0;"], + ) if site == "untyped_local": # dst plays no part: an undeclared local is 64 bits with a0's sign local = untyped_local_type(src) - return Program( - [decl_py, "x = a0", "return x"], - [decl_c, f"{local.c_name} x = a0;", "return x;"], - ), lambda: as_i64(convert(value, local)) + return read_back( + "x", + local, + lambda: convert(value, local), + [decl_py, "x = a0"], + [decl_c, f"{local.c_name} x = a0;"], + ) if site == "global_store": - return Program( - [decl_py, "global out", "out = a0", "return out"], - [decl_c, "out = a0;", "return out;"], + return read_back( + "out", + dst, + lambda: convert(value, dst), + [decl_py, "global out", "out = a0"], + [decl_c, "out = a0;"], globals=[("out", dst, 0)], - ), lambda: as_i64(convert(value, dst)) + ) if site == "return": + # Read through the function's own return type, so no probe. return Program([decl_py, "return a0"], [decl_c, "return a0;"], ret=dst), ( lambda: convert(value, dst) ) if site == "global_init": # `value` is used as the initialiser literal itself lit = as_literal(value, src) - return Program( - ["return g"], ["return g;"], globals=[("g", dst, lit)] - ), lambda: as_i64(convert(lit, dst)) + return read_back("g", dst, lambda: convert(lit, dst), [], [], [("g", dst, lit)]) if site.startswith("augassign"): op = site.split(" ")[1] init = as_literal(other, dst) - return Program( - [ - decl_py, - f"x = {dst.name}({literal_source(init)})", - f"x {op}= a0", - "return x", - ], + return read_back( + "x", + dst, + lambda: convert(binary(op, convert(init, dst), dst, value, src), dst), + [decl_py, f"x = {dst.name}({literal_source(init)})", f"x {op}= a0"], [ decl_c, f"{dst.c_name} x = {literal_source(init)};", f"x {'/' if op == '//' else op}= a0;", - "return x;", ], - ), lambda: as_i64(convert(binary(op, convert(init, dst), dst, value, src), dst)) + ) raise ValueError(site) @@ -113,33 +146,48 @@ def _site_program(site, src, dst, value, other): "untyped_local", "global_store", "return", - pytest.param( - "global_init", - marks=pytest.mark.xfail( - strict=True, - raises=AssertionError, - reason="a @bpfglobal initialiser that is not a bare constant (as " - "c_int64(-5) is not: -5 is a UnaryOp) is emitted as 0, and a " - "constant is not converted to the type (c_bool(2) keeps the low " - "bit, 0, where C gives 1) (pythonbpf/globals_pass.py, _emit_global)", - ), - ), + "global_init", ] + [f"augassign {op}" for op in ARITH_OPS + DIV_OPS + SHIFT_OPS] -# A quarter of the profile's examples per site: there are 18 sites, and each -# example is cheap to state but costs a clang run (~40 ms). +# Parametrized over the destination type as well as the site, so every type +# gets examples on every run: drawn at random, a type-specific rule (such as +# c_bool's `!= 0`) went untested in some runs. 162 parameters, so a +# sixteenth of the profile's examples each. +@pytest.mark.parametrize("dst", ALL_TYPES, ids=lambda t: t.name) @pytest.mark.parametrize("site", SITES) -@settings(max_examples=max(10, settings.default.max_examples // 4)) -@given(src=TYPES, dst=TYPES, data=st.data()) -def test_conversion_matches_clang(site, src, dst, data): - value = data.draw(values_of(src), label="value") - other = data.draw(values_of(dst), label="other") - if site == "global_init": - value = data.draw(st.integers(INT64_MIN, INT64_MAX), label="initialiser") +@settings(max_examples=max(5, settings.default.max_examples // 16)) +@given(data=st.data()) +def test_conversion_matches_clang(site, dst, data): + # Known gaps are stepped around by drawing only what avoids them, not by + # filtering (test_known_gaps.py pins each one): + sources = ALL_TYPES + if site in ("augassign <<", "augassign >>"): + # shift-result-type: `x >>= a` is typed by both operands, so only a + # source that leaves the type at x's own promoted type + sources = [t for t in ALL_TYPES if common_type(dst, t) == promote(dst)] + if site == "untyped_local": + # untyped-copy-keeps-source-type: `x = a0` keeps a0's type, which is + # right only for a 64-bit a0 (and dst plays no part here) + sources = [t for t in ALL_TYPES if untyped_local_type(t) == t] + if site == "global_init" and dst.is_bool: + pytest.skip("known gap global-initialiser: c_bool(2) keeps its low bit") + src = data.draw(st.sampled_from(sources), label="src") + if site in ("augassign <<", "augassign >>"): - # known gap shift-result-type: `x >>= a` is typed by both operands - # (test_known_gaps.py pins this case) - assume(promote(dst) == common_type(dst, src)) - program, expected = _site_program(site, src, dst, value, other) + # a count out of range is undefined in C + top = min(promote(dst).bits - 1, src.max) + value = data.draw(st.integers(0, top), label="count") + elif site == "global_init": + # global-initialiser: a negative initialiser is emitted as 0. `value` + # is the initialiser literal itself, out-of-range ones included. + value = data.draw(st.integers(0, INT64_MAX), label="initialiser") + else: + value = data.draw(values_of(src), label="value") + other = data.draw(values_of(dst), label="other") + # global_init's gap is the value itself, which the type probes multiply + # away (global_store reads a global's type through them) + probes = ["value"] if site == "global_init" else sorted(PROBES) + probe = data.draw(st.sampled_from(probes), label="probe") + program, expected = _site_program(site, src, dst, value, other, PROBES[probe]) check_against_clang(program, expected) diff --git a/tests/property/test_int_operators.py b/tests/property/test_int_operators.py index a3a65f8..377a71b 100644 --- a/tests/property/test_int_operators.py +++ b/tests/property/test_int_operators.py @@ -32,10 +32,13 @@ TYPES = st.sampled_from(ALL_TYPES) -# A quarter of the profile's examples per operator, as there are 17 of them. +# Parametrized over the left operand's type as well as the operator, so every +# type gets examples on every run (153 parameters, a sixteenth of the +# profile's examples each). +@pytest.mark.parametrize("left_ty", ALL_TYPES, ids=lambda t: t.name) @pytest.mark.parametrize("op", ARITH_OPS + DIV_OPS + SHIFT_OPS + COMPARE_OPS) -@settings(max_examples=max(10, settings.default.max_examples // 4)) -@given(left_ty=TYPES, right_ty=TYPES, data=st.data()) +@settings(max_examples=max(5, settings.default.max_examples // 16)) +@given(right_ty=TYPES, data=st.data()) def test_binary_operator_matches_clang(op, left_ty, right_ty, data): left = data.draw(values_of(left_ty), label="left") if op in SHIFT_OPS: diff --git a/tests/property/test_known_gaps.py b/tests/property/test_known_gaps.py index ab9fc3e..7857076 100644 --- a/tests/property/test_known_gaps.py +++ b/tests/property/test_known_gaps.py @@ -6,7 +6,7 @@ import pytest -from tests.property.cints import C_INT64, convert +from tests.property.cints import C_BOOL, C_INT64, convert from tests.property.harness import CLANG, check_against_clang from tests.property.known_gaps import GAPS from tests.property.programs import Program @@ -44,3 +44,21 @@ def test_known_gap_augassign_shift(): ["unsigned int a0 = 1;", "int x = -2147483648;", "x >>= a0;", "return x;"], ) check_against_clang(program, lambda: convert(-(2**31) >> 1, C_INT64)) + + +GLOBAL_INIT_REASON = ( + "global-initialiser: a @bpfglobal initialiser that is not a bare constant " + "(c_int64(-5) is not: -5 is a UnaryOp) is emitted as 0, and a constant is " + "not converted to the type, so c_bool(2) keeps the low bit, 0, where C " + "gives 1 (pythonbpf/globals_pass.py, _emit_global). " + "test_int_conversions' global_init site steps around both." +) + + +@pytest.mark.xfail(strict=True, raises=AssertionError, reason=GLOBAL_INIT_REASON) +@pytest.mark.parametrize( + "ty, literal", [(C_INT64, -5), (C_BOOL, 2)], ids=["negative", "c_bool"] +) +def test_known_gap_global_initialiser(ty, literal): + program = Program(["return g"], ["return g;"], globals=[("g", ty, literal)]) + check_against_clang(program, lambda: convert(convert(literal, ty), C_INT64))