Add hypothesis PBTs to make the type conversion logic more robust

.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

.gitignore

@@ -14,3 +14,4 @@ vmlinux.h
 # Documentation build artifacts
 docs/_build/
 docs/_templates/
+.hypothesis/

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

tests/README.md

@@ -133,6 +133,72 @@ 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, 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
+
+`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. 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
+
+```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 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
+
+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 +213,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

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

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:

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)