Skip to content

Fix soundness holes in the bounds/divisibility dataflow analyses #265

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
AntonOresten wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Fix soundness holes in the bounds/divisibility dataflow analyses #265

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
108 changes: 82 additions & 26 deletions src/compiler/analysis/bounds.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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),
Expand All @@ -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
Expand All @@ -152,39 +171,45 @@ 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)

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

# 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

Expand Down Expand Up @@ -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
Expand Down
81 changes: 66 additions & 15 deletions src/compiler/analysis/dataflow.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down Expand Up @@ -234,14 +258,31 @@ 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

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)
Expand Down Expand Up @@ -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))
Expand All @@ -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
Expand All @@ -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 /
Expand All @@ -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
Expand All @@ -380,4 +430,5 @@ function transfer_cf!(analysis::ForwardAnalysis, result::DataflowResult,
end
end
end
record!(analysis, result, ssa, top(analysis), tracker)
end
32 changes: 24 additions & 8 deletions src/compiler/analysis/divisibility.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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])
Expand Down
Loading