Skip to content

Commit

Permalink
irverify: Enforce invariant that PhiNodes are at the beginning of a BB
Browse files Browse the repository at this point in the history 
We have an invariant that all PhiNodes are at the beginning of a BasicBlock
(only possible interrupted by a `nothing`) and we rely on this in various
places for correctness. However, we did not actually verify this invariant.
  • Loading branch information
@Keno
Keno committed Jun 14, 2023
1 parent 8a1b642 commit 01fd53f
Showing 1 changed file with 70 additions and 56 deletions.
126 changes: 70 additions & 56 deletions base/compiler/ssair/verify.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -187,13 +187,22 @@ function verify_ir(ir::IRCode, print::Bool=true,
end
end
end
lastbb = 0
is_phinode_block = false
for (bb, idx) in bbidxiter(ir)
(bb != lastbb) && (is_phinode_block = true)
lastbb = bb
# We allow invalid IR in dead code to avoid passes having to detect when
# they're generating dead code.
bb_unreachable(domtree, bb) && continue
stmt = ir.stmts[idx][:inst]
stmt === nothing && continue
if isa(stmt, PhiNode)
if !is_phinode_block
# TODO: Move `unique` to Core.Compiler. For now we assume the predecessor list is
@verify_error "φ node $idx is not at the beginning of the basic block $bb"
error("")
end
@assert length(stmt.edges) == length(stmt.values)
for i = 1:length(stmt.edges)
edge = stmt.edges[i]
Expand Down Expand Up @@ -233,71 +242,76 @@ function verify_ir(ir::IRCode, print::Bool=true,
end
check_op(ir, domtree, val, Int(edge), last(ir.cfg.blocks[stmt.edges[i]].stmts)+1, idx, print, false, i, allow_frontend_forms)
end
elseif isa(stmt, PhiCNode)
for i = 1:length(stmt.values)
val = stmt.values[i]
if !isa(val, SSAValue)
@verify_error "Operand $i of PhiC node $idx must be an SSA Value."
error("")
end
if !isa(ir[val][:inst], UpsilonNode)
@verify_error "Operand $i of PhiC node $idx must reference an Upsilon node."
error("")
end
end
elseif (isa(stmt, GotoNode) || isa(stmt, GotoIfNot) || isexpr(stmt, :enter)) && idx != last(ir.cfg.blocks[bb].stmts)
@verify_error "Terminator $idx in bb $bb is not the last statement in the block"
error("")
elseif stmt === nothing
# Nothing to do
else
if isa(stmt, Expr) || isa(stmt, ReturnNode) # TODO: make sure everything has line info
if (stmt isa ReturnNode)
if isdefined(stmt, :val)
# TODO: Disallow unreachable returns?
# bb_unreachable(domtree, Int64(edge))
else
#@verify_error "Missing line number information for statement $idx of $ir"
is_phinode_block = false
if isa(stmt, PhiCNode)
for i = 1:length(stmt.values)
val = stmt.values[i]
if !isa(val, SSAValue)
@verify_error "Operand $i of PhiC node $idx must be an SSA Value."
error("")
end
end
if !(stmt isa ReturnNode && !isdefined(stmt, :val)) # not actually a return node, but an unreachable marker
if ir.stmts[idx][:line] <= 0
if !isa(ir[val][:inst], UpsilonNode)
@verify_error "Operand $i of PhiC node $idx must reference an Upsilon node."
error("")
end
end
end
isforeigncall = false
if isa(stmt, Expr)
if stmt.head === :(=)
if stmt.args[1] isa SSAValue
@verify_error "SSAValue as assignment LHS"
error("")
elseif (isa(stmt, GotoNode) || isa(stmt, GotoIfNot) || isexpr(stmt, :enter)) && idx != last(ir.cfg.blocks[bb].stmts)
@verify_error "Terminator $idx in bb $bb is not the last statement in the block"
error("")
else
if isa(stmt, Expr) || isa(stmt, ReturnNode) # TODO: make sure everything has line info
if (stmt isa ReturnNode)
if isdefined(stmt, :val)
# TODO: Disallow unreachable returns?
# bb_unreachable(domtree, Int64(edge))
else
#@verify_error "Missing line number information for statement $idx of $ir"
end
end
if stmt.args[2] isa GlobalRef
# undefined GlobalRef as assignment RHS is OK
continue
if !(stmt isa ReturnNode && !isdefined(stmt, :val)) # not actually a return node, but an unreachable marker
if ir.stmts[idx][:line] <= 0
end
end
elseif stmt.head === :gc_preserve_end
# We allow gc_preserve_end tokens to span across try/catch
# blocks, which isn't allowed for regular SSA values, so
# we skip the validation below.
continue
elseif stmt.head === :foreigncall
isforeigncall = true
elseif stmt.head === :isdefined && length(stmt.args) == 1 &&
(stmt.args[1] isa GlobalRef || isexpr(stmt.args[1], :static_parameter))
# a GlobalRef or static_parameter isdefined check does not evaluate its argument
continue
elseif stmt.head === :call
f = stmt.args[1]
if f isa GlobalRef && f.name === :cglobal
# TODO: these are not yet linearized
end
isforeigncall = false
if isa(stmt, Expr)
if stmt.head === :(=)
if stmt.args[1] isa SSAValue
@verify_error "SSAValue as assignment LHS"
error("")
end
if stmt.args[2] isa GlobalRef
# undefined GlobalRef as assignment RHS is OK
continue
end
elseif stmt.head === :gc_preserve_end
# We allow gc_preserve_end tokens to span across try/catch
# blocks, which isn't allowed for regular SSA values, so
# we skip the validation below.
continue
elseif stmt.head === :foreigncall
isforeigncall = true
elseif stmt.head === :isdefined && length(stmt.args) == 1 &&
(stmt.args[1] isa GlobalRef || isexpr(stmt.args[1], :static_parameter))
# a GlobalRef or static_parameter isdefined check does not evaluate its argument
continue
elseif stmt.head === :call
f = stmt.args[1]
if f isa GlobalRef && f.name === :cglobal
# TODO: these are not yet linearized
continue
end
end
end
end
n = 1
for op in userefs(stmt)
op = op[]
check_op(ir, domtree, op, bb, idx, idx, print, isforeigncall, n, allow_frontend_forms)
n += 1
n = 1
for op in userefs(stmt)
op = op[]
check_op(ir, domtree, op, bb, idx, idx, print, isforeigncall, n, allow_frontend_forms)
n += 1
end
end
end
end
Expand Down

0 comments on commit 01fd53f

Please sign in to comment.