You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Windows CI: remaining follow-ups after enabling the Windows job
Windows CI is green as of #466 (first-ever passing Windows job). That PR
deliberately deferred a few things to keep the initial job green. This issue
tracks them.
Context: the suite is sound on Windows — no crashes, no correctness/soundness
bugs. The blocker was runtime (heavy z3 queries overrunning their soft
wall-clock timeout), addressed with an opt-in deterministic z3 work budget
(CROSSHAIR_SMT_RLIMIT, set to 200000000 for the Windows job only).
Deferred items
Un-skip fuzz_core_test on Windows and triage the real gaps.
Currently skipped via a module-level pytest.mark.skipif(sys.platform == "win32", ...) in crosshair/fuzz_core_test.py. A partial Windows run surfaced genuine failures in three buckets:
Windows-only ops not modeled/classified: msvcrt.open_osfhandle, msvcrt.SetErrorMode, ctypes.set_last_error (these don't exist on Linux, so CI never exercised them).
Platform-divergent ops: select.select, os.waitstatus_to_exitcode, turtle.back (needs a display).
Cross-platform, need verification (may also fail on Linux, or be timing-flaky): operator.pow, operator.ipow, statistics.linear_regression, bz2.decompress, ast.parse.
Fix path: classify the Windows-only/OS-handle ops into the appropriate override tables (SIDE_EFFECT_OVERRIDES / _OS_HANDLE_PARAMS / PROBE_HAZARD_OVERRIDES), and root-cause the cross-platform divergences.
Run the inputgen probe guard on Windows. inputgen_test.py::test_uncategorized_ops_probe_cleanly is skipped on Windows because probe_side_effect_isolated (crosshair/inputgen.py) uses multiprocessing.get_context("fork"), and fork is unavailable on Windows. Its docstring says this guard should run per-platform (it's what would force-classify the msvcrt/winreg/winsound ops above). A spawn fallback isn't a drop-in — the probed call holds live, often-unpicklable objects. Needs a fork-free probe design. (Bucket with the item above.)
Normalize --unblock matching across platforms.
Python's subprocess.Popen audit event has a different arg shape on Windows — (None, "<joined cmdline>", None, None) vs Linux (argv0, [argv], cwd, env). The auditwall matches positionally over map(str, args) (crosshair/auditwall.py), so --unblock=subprocess.Popen:echo doesn't match on Windows — a real (if minor) user-facing bug. Two tests are pinned-skipped on win32: auditwall_test.py::test_popen_allowed_if_prefix_allowed and watcher_test.py::test_auditwall_unblock[...echo...CONFIRMED]. Fix: canonicalize the subprocess.Popen args to a cross-platform shape before matching (design decision on the canonical form + a docs update), then un-skip.
Tune the rlimit budget. CROSSHAIR_SMT_RLIMIT=200000000 is validated but generous. Lower it for speed while watching for tests flipping pass → CANNOT_CONFIRM (that's the signal the budget is too tight). Also consider whether an rlimit belongs on more platforms as a general determinism win, and whether the underlying wall-clock-timeout overrun is worth addressing at the source.
Expand the Windows matrix.
The Windows job currently runs Python 3.13 only. Add more versions once it's proven stable.
Windows CI: remaining follow-ups after enabling the Windows job
Windows CI is green as of #466 (first-ever passing Windows job). That PR
deliberately deferred a few things to keep the initial job green. This issue
tracks them.
Context: the suite is sound on Windows — no crashes, no correctness/soundness
bugs. The blocker was runtime (heavy z3 queries overrunning their soft
wall-clock timeout), addressed with an opt-in deterministic z3 work budget
(
CROSSHAIR_SMT_RLIMIT, set to200000000for the Windows job only).Deferred items
Un-skip
fuzz_core_teston Windows and triage the real gaps.Currently skipped via a module-level
pytest.mark.skipif(sys.platform == "win32", ...)incrosshair/fuzz_core_test.py. A partial Windows run surfaced genuine failures in three buckets:msvcrt.open_osfhandle,msvcrt.SetErrorMode,ctypes.set_last_error(these don't exist on Linux, so CI never exercised them).select.select,os.waitstatus_to_exitcode,turtle.back(needs a display).operator.pow,operator.ipow,statistics.linear_regression,bz2.decompress,ast.parse.Fix path: classify the Windows-only/OS-handle ops into the appropriate override tables (
SIDE_EFFECT_OVERRIDES/_OS_HANDLE_PARAMS/PROBE_HAZARD_OVERRIDES), and root-cause the cross-platform divergences.Run the
inputgenprobe guard on Windows.inputgen_test.py::test_uncategorized_ops_probe_cleanlyis skipped on Windows becauseprobe_side_effect_isolated(crosshair/inputgen.py) usesmultiprocessing.get_context("fork"), and fork is unavailable on Windows. Its docstring says this guard should run per-platform (it's what would force-classify the msvcrt/winreg/winsound ops above). Aspawnfallback isn't a drop-in — the probedcallholds live, often-unpicklable objects. Needs a fork-free probe design. (Bucket with the item above.)Normalize
--unblockmatching across platforms.Python's
subprocess.Popenaudit event has a different arg shape on Windows —(None, "<joined cmdline>", None, None)vs Linux(argv0, [argv], cwd, env). The auditwall matches positionally overmap(str, args)(crosshair/auditwall.py), so--unblock=subprocess.Popen:echodoesn't match on Windows — a real (if minor) user-facing bug. Two tests are pinned-skipped on win32:auditwall_test.py::test_popen_allowed_if_prefix_allowedandwatcher_test.py::test_auditwall_unblock[...echo...CONFIRMED]. Fix: canonicalize thesubprocess.Popenargs to a cross-platform shape before matching (design decision on the canonical form + a docs update), then un-skip.One-time
git add --renormalize .commit.Enable Windows CI: bound z3 work with rlimit; fix test Unix-isms #466 adds
.gitattributes(* text=auto eol=lf). Do a dedicated renormalization commit so files currently committed with CRLF get normalized and future diffs stay clean.Tune the rlimit budget.
CROSSHAIR_SMT_RLIMIT=200000000is validated but generous. Lower it for speed while watching for tests flipping pass →CANNOT_CONFIRM(that's the signal the budget is too tight). Also consider whether an rlimit belongs on more platforms as a general determinism win, and whether the underlying wall-clock-timeoutoverrun is worth addressing at the source.Expand the Windows matrix.
The Windows job currently runs Python 3.13 only. Add more versions once it's proven stable.