[mark14wu]

Summary

Triton's signed integer // and % round toward zero, as in C: -63 // 64 == 0 and -63 % 64 == -63. The interpreter computes these values, on the GPU and under TRITON_INTERPRET=1. BinarySymbolicExpr._op_idiv and _op_mod, however, lowered them to Z3's integer / and %, which are Euclidean and give -1 and 1. Whenever the dividend can be negative, the model and the program disagree:

• False positive. A sliding-window start lo = (pid * B - (B - 1)) // B * B is 0 for pid == 0 in Triton. The model gave -B, so the load x + lo + tl.arange(0, B) was reported. A branch such as if lo < 0: does not help, because it is evaluated on the concrete, truncated value.
• Missed access. (pid - 1) % N is -1 for pid == 0 in Triton, so tl.load(x + (pid - 1) % N) reads x[-1]. The model gave N - 1 and reported nothing.

This PR lowers signed // to the truncating quotient If(a >= 0, a / b, -((-a) / b)), and signed % to a - b * trunc(a / b). Unsigned operations keep Z3's semantics, which agree for non-negative values. The NumPy fallback in BinarySymbolicExpr.concretize for an idiv without a frontend concrete function used np.floor_divide; it truncates now as well, so that both paths agree.

Tests

• New in tests/unit/test_symbolic_client.py:
  • test_signed_idiv_and_mod_round_toward_zero: every sign combination. The cases with a negative dividend fail on main.
  • test_signed_idiv_of_symbolic_dividend_rounds_toward_zero: (pid - 63) // 64 is 0 for pid == 0. It fails on main.
  • test_unsigned_idiv_and_mod_eval
  • test_idiv_concretize_without_frontend_fn_rounds_toward_zero: the NumPy fallback. It fails on main.
• New in tests/end_to_end/test_sanitizer.py:
  • test_signed_division_rounds_toward_zero: the sliding window above, in bounds. Main reports it.
  • test_signed_modulo_keeps_the_sign_of_the_dividend: the x[-1] load above. Main misses it.
• pytest tests/: 366 passed, 6 skipped on main; 378 passed, 6 skipped with this PR (Python 3.12, Triton 3.8.0).
• ruff check and ruff format --check (v0.1.9) pass on the changed files. mypy (v1.8.0) reports no new errors.
• CI: the build job installs Triton 3.9.0 and then Triton main. With those, about 96 tests of the existing suite fail whatever the change (the run on [FIX] Stop the sanitizer from skipping repeated launches #518 also has 96 failures), mostly with 'SymbolicScalarDType' object has no attribute 'scalar' or 'SymbolicExprDataWrapper' object has no attribute 'astype'. The new end-to-end tests fail there with the same errors as the existing sanitizer tests; the new unit tests pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_016HMpCLXdUVNfMbJTj8aHE2

[github-actions]

Performance Benchmark

Benchmark	main (min)	PR (min)	Change	Samples
gemm	N/A	N/A	N/A	0 / 0
gemm_oob	N/A	N/A	N/A	0 / 0
indirect_load	N/A	N/A	N/A	0 / 0
nested_loop	N/A	N/A	N/A	0 / 0
block_pointer_loop_advance	N/A	N/A	N/A	0 / 0
liger_jsd	N/A	N/A	N/A	0 / 0
flaggems_layernorm	N/A	N/A	N/A	0 / 0
swiglu	0.086s	0.087s	+0.2%	20 / 20
cross_entropy	N/A	N/A	N/A	0 / 0
fused_linear_jsd	N/A	N/A	N/A	0 / 0
Total	N/A	N/A	N/A	N/A

Iterations: 1 warmup + 20 measured
Samples are shown as main / PR; long pytest benchmarks may use fewer samples.