diff --git a/src/compiler/analysis/bounds.jl b/src/compiler/analysis/bounds.jl index 18f73863..2d0eca34 100644 --- a/src/compiler/analysis/bounds.jl +++ b/src/compiler/analysis/bounds.jl @@ -81,22 +81,29 @@ end =============================================================================# function transfer(a::BoundsAnalysis, r::DataflowResult, @nospecialize(func), - ops, block::Block, ::Any) + ops, block::Block, @nospecialize(inst)) + # Arithmetic transfers compute the exact mathematical interval, but + # the hardware op wraps modulo the result's element width — clamp + # each result through `clamp_to_width` so a range the runtime value + # can escape never reaches downstream consumers. if func === Intrinsics.addi length(ops) >= 2 || return TOP_RANGE - return range_add(operand_value(a, r, ops[1]), operand_value(a, r, ops[2])) + return clamp_to_width( + range_add(operand_value(a, r, ops[1]), operand_value(a, r, ops[2])), inst) end if func === Intrinsics.subi length(ops) >= 2 || return TOP_RANGE - return range_sub(operand_value(a, r, ops[1]), operand_value(a, r, ops[2])) + return clamp_to_width( + range_sub(operand_value(a, r, ops[1]), operand_value(a, r, ops[2])), inst) end if func === Intrinsics.muli length(ops) >= 2 || return TOP_RANGE - return range_mul(operand_value(a, r, ops[1]), operand_value(a, r, ops[2])) + return clamp_to_width( + range_mul(operand_value(a, r, ops[1]), operand_value(a, r, ops[2])), inst) end if func === Intrinsics.negi length(ops) >= 1 || return TOP_RANGE - return range_neg(operand_value(a, r, ops[1])) + return clamp_to_width(range_neg(operand_value(a, r, ops[1])), inst) end if func === Intrinsics.constant @@ -114,11 +121,14 @@ function transfer(a::BoundsAnalysis, r::DataflowResult, @nospecialize(func), end # `Intrinsics.assume(x, predicate)` — refines via `Bounded` (interval - # intersection), passes through for any other predicate kind. + # intersection), passes through for any other predicate kind. The + # predicate is resolved through `constant_operand`: pass-constructed + # assumes embed it raw, user-written ones arrive as a `QuoteNode` or + # const-inferred SSAValue. if func === Intrinsics.assume length(ops) >= 2 || return TOP_RANGE x_range = operand_value(a, r, ops[1]) - pred = ops[2] + pred = constant_operand(block, ops[2]) if pred isa Bounded return range_intersect(x_range, IntRange(pred.lb === nothing ? nothing : Int(pred.lb), @@ -127,14 +137,23 @@ function transfer(a::BoundsAnalysis, r::DataflowResult, @nospecialize(func), return x_range end - # Casts: `bitcast`/`exti` preserve the integer value (exti is sign- - # or zero-extend; both widen the type without changing the - # mathematical value). `trunci` clamps to the destination width's + # Casts: `bitcast` preserves the integer value. `exti` preserves it + # for sign-extension; zero-extension reinterprets the source bits as + # unsigned, so it is value-preserving only when the source provably + # can't be negative. `trunci` clamps to the destination width's # signed range — conservatively bail to top when truncating. - if func === Intrinsics.bitcast || func === Intrinsics.exti + if func === Intrinsics.bitcast length(ops) >= 1 || return TOP_RANGE return operand_value(a, r, ops[1]) end + if func === Intrinsics.exti + length(ops) >= 3 || return TOP_RANGE + v = operand_value(a, r, ops[1]) + s = constant_operand(block, ops[3]) + s === Signedness.Signed && return v + (v isa IntRange && v.lo !== nothing && v.lo >= 0) && return v + return TOP_RANGE + end if func === Intrinsics.trunci return TOP_RANGE end @@ -152,13 +171,10 @@ function transfer(a::BoundsAnalysis, r::DataflowResult, @nospecialize(func), end # Override the framework's default ForOp transfer to seed the IV with -# its static bounds. ForOp iterates `iv ∈ [lower, upper)` with stride -# `step`; when `lower`/`upper`/`step` are literal-resolvable, the IV -# range is exactly `[lower, last_iv]` where `last_iv = upper - step` -# (assuming `step > 0`). Without literal bounds, the IV defaults to -# top (the framework's default). +# its static bounds (see `compute_iv_range`). Back-edges are collected +# via `reachable_terminators`, mirroring the framework's ForOp handler. function transfer_cf!(analysis::BoundsAnalysis, result::DataflowResult, - op::ForOp, ::SSAValue, ::Block, tracker::ChangeTracker) + op::ForOp, ssa::SSAValue, ::Block, tracker::ChangeTracker) iv = compute_iv_range(analysis, result, op) record!(analysis, result, op.iv_arg, iv, tracker) @@ -166,25 +182,34 @@ function transfer_cf!(analysis::BoundsAnalysis, result::DataflowResult, record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end walk!(analysis, result, op.body, tracker) - term = op.body.terminator - if term isa ContinueOp - for (arg, v) in zip(op.body.args, term.values) + for t in reachable_terminators(op.body) + t isa ContinueOp || continue + for (arg, v) in zip(op.body.args, t.values) record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end end + record!(analysis, result, ssa, top(analysis), tracker) end +# ForOp iterates `iv ∈ [lower, upper)` with stride `step > 0`, so +# `upper.hi - 1` is always a sound upper bound on the IV. The sharper +# `upper - step` (the last IV taken) requires the trip length to divide +# the step — slt/sle-promoted while loops with `step > 1` overshoot it +# otherwise (0:4:10 visits 8, not 10 - 4 = 6) — so it is used only when +# `lower`, `upper`, and `step` are exact and the divisibility holds. function compute_iv_range(a::BoundsAnalysis, r::DataflowResult, op::ForOp) lower = operand_value(a, r, op.lower) upper = operand_value(a, r, op.upper) step = operand_value(a, r, op.step) iv_lo = (lower === nothing) ? nothing : lower.lo - # Last IV is `upper - step` (loop iterates while iv < upper). Need - # both an upper bound on `upper` and a lower bound on `step` to - # compute it. - iv_hi = (upper === nothing || step === nothing || - upper.hi === nothing || step.lo === nothing || step.lo < 1) ? - nothing : upper.hi - step.lo + iv_hi = (upper === nothing || upper.hi === nothing) ? nothing : + sub_or_nothing(upper.hi, 1) + if iv_hi !== nothing && + step !== nothing && step.lo !== nothing && step.lo == step.hi && step.lo > 1 && + lower !== nothing && lower.lo !== nothing && lower.lo == lower.hi && + upper.lo == upper.hi && mod(upper.hi - lower.lo, step.lo) == 0 + iv_hi = sub_or_nothing(upper.hi, step.lo) + end return IntRange(iv_lo, iv_hi) end @@ -252,6 +277,37 @@ function range_mul(a::Union{Nothing,IntRange}, b::Union{Nothing,IntRange}) return TOP_RANGE end +# Clamp an arithmetic transfer's result to what the destination element +# width can represent. The interval arithmetic above is exact over ℤ +# (saturating to open endpoints at the lattice level), but the hardware +# op wraps modulo the element width — once a computed range can escape +# `[typemin(T), typemax(T)]` (any open endpoint counts), the wrapped +# runtime value can land anywhere, so the result degrades to top rather +# than feeding a false range to downstream consumers (`Bounded` assume +# predicates, `nsw`/`nuw` flags). +function clamp_to_width(rng::Union{Nothing, IntRange}, @nospecialize(inst)) + rng === nothing && return rng # ⊥ stays ⊥ + T = result_int_eltype(inst) + T === nothing && return rng + sizeof(T) <= 8 || return TOP_RANGE + (rng.lo === nothing || rng.hi === nothing) && return TOP_RANGE + tmin = T <: Unsigned ? Int128(0) : Int128(typemin(T)) + return (tmin <= rng.lo && rng.hi <= Int128(typemax(T))) ? rng : TOP_RANGE +end + +# Integer element type of an instruction's inferred result type (peeling +# `Tile{T}` to `T`), or `nothing` when the result isn't a bit-integer. +function result_int_eltype(@nospecialize(inst)) + inst isa Instruction || return nothing + T = inst[:type] + T === nothing && return nothing + T = CC.widenconst(T) + T isa DataType || return nothing + T <: Tile && (T = eltype(T)) + (T isa DataType && T <: Base.BitInteger) || return nothing + return T +end + function range_intersect(a::Union{Nothing,IntRange}, b::Union{Nothing,IntRange}) a === nothing && return b b === nothing && return a diff --git a/src/compiler/analysis/dataflow.jl b/src/compiler/analysis/dataflow.jl index ef26dacf..7401c78c 100644 --- a/src/compiler/analysis/dataflow.jl +++ b/src/compiler/analysis/dataflow.jl @@ -143,13 +143,37 @@ Base.values(r::DataflowResult) = values(r.values) Lattice value for an operand as used *inside a transfer function*. The default handles `LatticeAnchor`s (via dict lookup) and treats everything -else (integer/float literals, QuoteNodes, GlobalRefs, …) as `bottom`. -Analyses override this to recognise raw literals when those are -meaningful lattice inputs — e.g. a constant analysis returns -the integer itself for a raw `Int` operand. +else (integer/float literals, QuoteNodes, GlobalRefs, …) as `top` — an +unrecognised literal is "no information", never ⊥. Bottom is the merge +identity, so returning it for a live operand would let the other side of +a join keep facts this operand doesn't share. Analyses override this to +recognise raw literals when those are meaningful lattice inputs — e.g. a +constant analysis returns the integer itself for a raw `Int` operand. """ operand_value(a::ForwardAnalysis, r::DataflowResult, @nospecialize(op)) = - op isa LatticeAnchor ? r[op] : bottom(a) + op isa LatticeAnchor ? r[op] : top(a) + +""" + constant_operand(block::Block, op) -> value or nothing + +Resolve an operand to its compile-time constant value, mirroring what +codegen's `get_constant` sees: raw embedded values are returned as-is, +`QuoteNode`s are unwrapped, and anchors (SSAValues etc.) are chased +through their inferred type via `singleton_type`. Returns `nothing` for +operands with no known constant. Used by transfer rules that key on a +constant operand — e.g. the `Intrinsics.assume` predicate, which is +embedded directly when a pass constructs the call but arrives as a +`QuoteNode` (or const-inferred SSAValue) from user-written kernels. +""" +function constant_operand(block::Block, @nospecialize(op)) + op isa QuoteNode && return op.value + if op isa LatticeAnchor + T = value_type(block, op) + T === nothing && return nothing + return CC.singleton_type(T) + end + return op +end """ lookup_def_call(block::Block, val::SSAValue) -> Union{Tuple, Nothing} @@ -234,6 +258,18 @@ function walk!(analysis::ForwardAnalysis, result::DataflowResult, block::Block, transfer_cf!(analysis, result, s, SSAValue(inst.ssa_idx), block, tracker) elseif s isa Expr transfer_call!(analysis, result, block, inst, tracker) + elseif s isa PiNode + # Type-narrowing assertion on the same runtime value — + # pass the operand's lattice element through. + record!(analysis, result, SSAValue(inst.ssa_idx), + operand_value(analysis, result, s.val), tracker) + else + # Statement kinds no transfer rule models (GlobalRefs, raw + # literals, …). Record ⊤ so the SSA never lingers at ⊥: + # bottom is the merge identity, and a ⊥ operand at a join + # would let the other side's facts survive unrefuted. + record!(analysis, result, SSAValue(inst.ssa_idx), + top(analysis), tracker) end end end @@ -241,7 +277,12 @@ end function transfer_call!(analysis::ForwardAnalysis, result::DataflowResult, block::Block, inst::Instruction, tracker::ChangeTracker) call = resolve_call(block, inst) - call === nothing && return + if call === nothing + # Unresolvable callee — same ⊥-lingering hazard as unmodeled + # statement kinds above. + record!(analysis, result, SSAValue(inst.ssa_idx), top(analysis), tracker) + return + end func, ops = call new_val = transfer(analysis, result, func, ops, block, inst) record!(analysis, result, SSAValue(inst.ssa_idx), new_val, tracker) @@ -309,8 +350,12 @@ function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult, tt = op.then_region.terminator et = op.else_region.terminator - (tt isa YieldOp && et isa YieldOp) || return - (isempty(tt.values) || isempty(et.values)) && return + if !(tt isa YieldOp && et isa YieldOp) || isempty(tt.values) || isempty(et.values) + # Shape we don't model (loop-exiting branch, no yields) — the + # IfOp's SSA must still leave ⊥. + record!(analysis, result, ssa, top(analysis), tracker) + return + end merged = bottom(analysis) n = min(length(tt.values), length(et.values)) @@ -324,25 +369,29 @@ end # ForOp — body.args receives loop-carried values: join(init_values, ContinueOp # yields). The IV lives in `op.iv_arg` (not in `body.args`), so init/continue # values line up positionally with `body.args` without skipping slot 1. -# The IV is seeded to `top` (unknown at compile time). +# The IV is seeded to `top` (unknown at compile time). Back-edges are +# collected via `reachable_terminators` — a ContinueOp may sit behind a +# nested IfOp branch, not only as the direct body terminator (same +# scoping rule as the LoopOp handler below). function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult, - op::ForOp, ::SSAValue, ::Block, tracker::ChangeTracker) + op::ForOp, ssa::SSAValue, ::Block, tracker::ChangeTracker) record!(analysis, result, op.iv_arg, top(analysis), tracker) for (arg, v) in zip(op.body.args, op.init_values) record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end walk!(analysis, result, op.body, tracker) - term = op.body.terminator - if term isa ContinueOp - for (arg, v) in zip(op.body.args, term.values) + for t in reachable_terminators(op.body) + t isa ContinueOp || continue + for (arg, v) in zip(op.body.args, t.values) record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end end + record!(analysis, result, ssa, top(analysis), tracker) end # WhileOp — before.args ← init ⊔ after yields; after.args ← before's ConditionOp args. function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult, - op::WhileOp, ::SSAValue, ::Block, tracker::ChangeTracker) + op::WhileOp, ssa::SSAValue, ::Block, tracker::ChangeTracker) for (arg, v) in zip(op.before.args, op.init_values) record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end @@ -360,6 +409,7 @@ function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult, record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end end + record!(analysis, result, ssa, top(analysis), tracker) end # LoopOp — body.args ← init ⊔ ContinueOp values ⊔ BreakOp values. ContinueOp / @@ -368,7 +418,7 @@ end # own scope and their terminators target *themselves*, not this outer LoopOp. # `reachable_terminators` encodes that scoping rule. function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult, - op::LoopOp, ::SSAValue, ::Block, tracker::ChangeTracker) + op::LoopOp, ssa::SSAValue, ::Block, tracker::ChangeTracker) for (arg, v) in zip(op.body.args, op.init_values) record!(analysis, result, arg, operand_value(analysis, result, v), tracker) end @@ -380,4 +430,5 @@ function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult, end end end + record!(analysis, result, ssa, top(analysis), tracker) end diff --git a/src/compiler/analysis/divisibility.jl b/src/compiler/analysis/divisibility.jl index 9786adc5..2c9185d6 100644 --- a/src/compiler/analysis/divisibility.jl +++ b/src/compiler/analysis/divisibility.jl @@ -131,13 +131,14 @@ function transfer(a::DivByAnalysis, r::DataflowResult, @nospecialize(func), end # `Intrinsics.assume(x, predicate)` — refines when the predicate is - # `DivBy`, otherwise passes through. The predicate is an embedded - # `AssumePredicate` value (constructed at pass time), so it lives in - # the operand list directly rather than being wrapped in a QuoteNode. + # `DivBy`, otherwise passes through. The predicate is resolved + # through `constant_operand`: pass-constructed assumes embed the + # `AssumePredicate` value directly in the operand list, user-written + # ones arrive as a `QuoteNode` or const-inferred SSAValue. if func === Intrinsics.assume length(ops) >= 2 || return 1 x_div = operand_value(a, r, ops[1]) - pred = ops[2] + pred = constant_operand(block, ops[2]) if pred isa DivBy d = pred.divisor return d > 0 ? lcm(max(x_div, 1), d) : x_div @@ -151,13 +152,28 @@ function transfer(a::DivByAnalysis, r::DataflowResult, @nospecialize(func), return operand_value(a, r, ops[1]) end - # Integer casts: `bitcast`/`exti` preserve the value (and so the - # divisor); `trunci` reduces to mod 2^bitwidth (matches Python's - # `TileAsType` rule on integer→integer). - if func === Intrinsics.bitcast || func === Intrinsics.exti + # Integer casts: `bitcast` preserves the value (and so the divisor); + # `trunci` reduces to mod 2^bitwidth (matches Python's `TileAsType` + # rule on integer→integer). + if func === Intrinsics.bitcast length(ops) >= 1 || return 1 return operand_value(a, r, ops[1]) end + # `exti` preserves the value for sign-extension. Zero-extension of a + # negative adds 2^src_bits (`zext(x) = x mod 2^w`), so only divisors + # of both `x` and `2^w` survive: reduce to `gcd(x_div, 2^w)`. + if func === Intrinsics.exti + length(ops) >= 3 || return 1 + x_div = operand_value(a, r, ops[1]) + s = constant_operand(block, ops[3]) + s === Signedness.Signed && return x_div + src_T = value_type(block, ops[1]) + src_T = src_T === nothing ? Any : CC.widenconst(src_T) + src_T <: Tile && (src_T = eltype(src_T)) + src_T isa DataType && src_T <: Base.BitInteger && sizeof(src_T) < 8 || + return 1 + return gcd(x_div, 1 << (sizeof(src_T) * 8)) + end if func === Intrinsics.trunci length(ops) >= 2 || return 1 x_div = operand_value(a, r, ops[1]) diff --git a/test/analysis/dataflow.jl b/test/analysis/dataflow.jl index db84bfae..0d225de6 100644 --- a/test/analysis/dataflow.jl +++ b/test/analysis/dataflow.jl @@ -6,11 +6,11 @@ # intrinsic IR exercises `IfOp` / `ForOp` / `WhileOp` paths with shape # that we can assert against. -using Core: SSAValue, Argument, ReturnNode +using Core: SSAValue, Argument, ReturnNode, PiNode, GlobalRef using IRStructurizer using IRStructurizer: code_structured, Block, BlockArgument, ForOp, LoopOp, - ContinueOp, ControlFlowOp, StructuredIRCode, blocks, - instructions + IfOp, YieldOp, ContinueOp, ControlFlowOp, + StructuredIRCode, blocks, instructions using cuTile: ForwardAnalysis, DataflowResult, analyze, record!, has_value, LatticeAnchor import cuTile: bottom, top, tmerge, transfer, max_iters, operand_value @@ -153,6 +153,109 @@ end end +# ── soundness: ⊥ must never act as best-info at a join ────────────────── + +@testset "PiNode passes through; unmodeled statements record ⊤" begin + entry = Block() + push!(entry, 1, Expr(:call, Core.Intrinsics.add_int, 2, 3), Int) + push!(entry, 2, PiNode(SSAValue(1), Int), Int) + push!(entry, 3, GlobalRef(Base, :pi), Any) + entry.terminator = ReturnNode(SSAValue(2)) + sci = StructuredIRCode(Any[Any], Any[], entry, 3) + r = analyze(ConstInt(), sci) + + @test r[SSAValue(2)] === 5 # PiNode forwards its operand's fact + @test r[SSAValue(3)] === CTOP # no transfer rule — never lingers at ⊥ +end + +@testset "PiNode-fed loop carry does not keep the init value's fact" begin + # Loop carry: init 16, ContinueOp yields a PiNode of an unanalysed + # argument. The PiNode's SSA used to linger at ⊥ (walk! skipped + # non-Expr statements), and ⊥ is the merge identity — so the carry + # incorrectly kept "divisible by 16" across iterations that replace + # it with an arbitrary value. + carry = BlockArgument(1, Int) + body = Block() + push!(body.args, carry) + push!(body, 1, PiNode(Argument(2), Int), Int) + body.terminator = ContinueOp(Any[SSAValue(1)]) + loop = LoopOp(body, Any[16]) + entry = Block() + push!(entry, 2, loop, Nothing) + entry.terminator = ReturnNode(nothing) + sci = StructuredIRCode(Any[Any, Int], Any[], entry, 2) + + r = cuTile.analyze_divisibility(sci) + @test cuTile.div_by(r, carry) == 1 +end + +@testset "ForOp merges continues nested behind IfOp branches" begin + # A ContinueOp may sit inside a nested IfOp branch rather than as + # the direct body terminator. Its values must be merged into the + # loop carries like the direct back-edge's. + iv = BlockArgument(1, Int) + carry = BlockArgument(2, Int) + then_r = Block() + then_r.terminator = ContinueOp(Any[999]) + else_r = Block() + else_r.terminator = YieldOp(Any[]) + body = Block() + push!(body.args, carry) + push!(body, 1, IfOp(true, then_r, else_r), Nothing) + body.terminator = ContinueOp(Any[carry]) + fop = ForOp(0, 10, 1, iv, body, Any[100]) + entry = Block() + push!(entry, 2, fop, Nothing) + entry.terminator = ReturnNode(nothing) + sci = StructuredIRCode(Any[Any], Any[], entry, 2) + + r = analyze(ConstInt(), sci) + @test r[carry] === CTOP # 100 ⊔ 999 → ⊤, not 100 +end + + +# ── user-written Intrinsics.assume ─────────────────────────────────────── + +@testset "assume(DivBy) refines through a QuoteNode predicate" begin + # Pass-constructed assumes embed the predicate value directly; user- + # written kernels arrive with it const-folded into a QuoteNode. Both + # must refine. + entry = Block() + push!(entry, 1, Expr(:call, cuTile.Intrinsics.assume, Argument(2), + QuoteNode(cuTile.DivBy(16))), Int) + entry.terminator = ReturnNode(SSAValue(1)) + sci = StructuredIRCode(Any[Any, Int], Any[], entry, 1) + + r = cuTile.analyze_divisibility(sci) + @test cuTile.div_by(r, SSAValue(1)) == 16 +end + + +# ── exti signedness (divisibility) ─────────────────────────────────────── + +@testset "zero-extension reduces divisibility mod 2^srcbits" begin + mk_exti(s) = begin + entry = Block() + push!(entry, 1, Expr(:call, cuTile.Intrinsics.constant, + QuoteNode(()), -6, Int8), Int8) + push!(entry, 2, Expr(:call, cuTile.Intrinsics.exti, + SSAValue(1), Int32, QuoteNode(s)), Int32) + entry.terminator = ReturnNode(SSAValue(2)) + sci = StructuredIRCode(Any[Any], Any[], entry, 2) + cuTile.analyze_divisibility(sci) + end + + # Sign-extension preserves the value, and so the divisor. + r = mk_exti(cuTile.Signedness.Signed) + @test cuTile.div_by(r, SSAValue(2)) == 6 + + # Zero-extension of Int8(-6) yields 250 = -6 + 2^8, which is not a + # multiple of 6; only divisors of gcd(6, 2^8) = 2 survive. + r = mk_exti(cuTile.Signedness.Unsigned) + @test cuTile.div_by(r, SSAValue(2)) == 2 +end + + # ── convergence cap ────────────────────────────────────────────────────── # A deliberately non-monotone analysis: its `tmerge` never stabilises, so the diff --git a/test/codegen/bounds.jl b/test/codegen/bounds.jl index f2197822..121bdae5 100644 --- a/test/codegen/bounds.jl +++ b/test/codegen/bounds.jl @@ -100,6 +100,100 @@ end cuTile.TOP_RANGE end +using Core: SSAValue, Argument, ReturnNode +using IRStructurizer: StructuredIRCode, Block, BlockArgument, ForOp, ContinueOp + +@testset "bounds — ForOp IV upper bound is sound for step > 1" begin + mk_for(lower, upper, step) = begin + iv = BlockArgument(1, Int) + body = Block() + body.terminator = ContinueOp(Any[]) + fop = ForOp(lower, upper, step, iv, body, Any[]) + entry = Block() + push!(entry, 1, fop, Nothing) + entry.terminator = ReturnNode(nothing) + sci = StructuredIRCode(Any[Any, Int], Any[], entry, 1) + (cuTile.analyze_bounds(sci), iv) + end + + # 0:4:<10 visits 0, 4, 8 — the last IV overshoots `upper - step` + # (= 6), so only the exclusive bound `upper - 1` is sound. + r, iv = mk_for(0, 10, 4) + @test r[iv] == cuTile.IntRange(0, 9) + + # Trip length divides the step: the sharp `upper - step` applies. + r, iv = mk_for(0, 12, 4) + @test r[iv] == cuTile.IntRange(0, 8) + + # Step 1: exclusive upper bound minus one, as before. + r, iv = mk_for(0, 10, 1) + @test r[iv] == cuTile.IntRange(0, 9) + + # Unknown step: `iv < upper` alone still bounds the IV. + r, iv = mk_for(0, 10, Argument(2)) + @test r[iv] == cuTile.IntRange(0, 9) +end + +@testset "bounds — exti consults signedness" begin + mk_exti(scalar, s) = begin + entry = Block() + push!(entry, 1, Expr(:call, cuTile.Intrinsics.constant, + QuoteNode(()), scalar, Int32), Int32) + push!(entry, 2, Expr(:call, cuTile.Intrinsics.exti, + SSAValue(1), Int64, QuoteNode(s)), Int64) + entry.terminator = ReturnNode(SSAValue(2)) + sci = StructuredIRCode(Any[Any], Any[], entry, 2) + cuTile.analyze_bounds(sci) + end + + # Sign-extension preserves the mathematical value. + r = mk_exti(-5, cuTile.Signedness.Signed) + @test cuTile.bounds(r, SSAValue(2)) == cuTile.IntRange(-5, -5) + + # Zero-extension of a possibly-negative value reinterprets the bits + # (Int32(-5) zexts to 2^32 - 5) — the range must not pass through. + r = mk_exti(-5, cuTile.Signedness.Unsigned) + @test cuTile.bounds(r, SSAValue(2)) == cuTile.TOP_RANGE + + # Zero-extension of a provably non-negative value stays exact. + r = mk_exti(5, cuTile.Signedness.Unsigned) + @test cuTile.bounds(r, SSAValue(2)) == cuTile.IntRange(5, 5) +end + +@testset "bounds — arithmetic clamps to the result element width" begin + mk_add(T) = begin + entry = Block() + push!(entry, 1, Expr(:call, cuTile.Intrinsics.constant, + QuoteNode(()), typemax(Int32), Int32), Int32) + push!(entry, 2, Expr(:call, cuTile.Intrinsics.addi, + SSAValue(1), SSAValue(1)), T) + entry.terminator = ReturnNode(SSAValue(2)) + sci = StructuredIRCode(Any[Any], Any[], entry, 2) + cuTile.analyze_bounds(sci) + end + + # i32 + i32 wraps at runtime: the exact sum 2^32 - 2 escapes Int32, + # so the wrapped value can land anywhere. + r = mk_add(Int32) + @test cuTile.bounds(r, SSAValue(2)) == cuTile.TOP_RANGE + + # The same sum fits an Int64 destination and is kept exact. + r = mk_add(Int64) + @test cuTile.bounds(r, SSAValue(2)) == + cuTile.IntRange(2 * Int(typemax(Int32)), 2 * Int(typemax(Int32))) +end + +@testset "bounds — assume(Bounded) refines through a QuoteNode predicate" begin + entry = Block() + push!(entry, 1, Expr(:call, cuTile.Intrinsics.assume, Argument(2), + QuoteNode(cuTile.Bounded(0, 63))), Int) + entry.terminator = ReturnNode(SSAValue(1)) + sci = StructuredIRCode(Any[Any, Int], Any[], entry, 1) + + r = cuTile.analyze_bounds(sci) + @test cuTile.bounds(r, SSAValue(1)) == cuTile.IntRange(0, 63) +end + @testset "bounds — combine narrows structural with dataflow" begin a = cuTile.BoundsAnalysis() nonneg = cuTile.IntRange(0, nothing)