Skip to content

Commit

Permalink
effects: separate :noub effect bit from :consistent
Browse files Browse the repository at this point in the history
The current `:consistent` effect bit carries dual meanings:
1. "the return value is always consistent"
2. "this method does not cause any undefined behavior".

This design makes the effect bit unclear and hard to manage.
Specifically, the current design prevents a post-inference analysis
(as discussed in #50805) from safely refining
"consistent"-cy using post-optimization state IR. This is because it is
impossible to tell whether the `:consistent`-cy has been influenced by
the first or second meaning.

To address this, this commit splits them into two distinct effect bits:
`:consistent` for consistent return values and `:noub` for no undefined
behavior.
  • Loading branch information
aviatesk committed Aug 6, 2023
1 parent 3e04129 commit d1d8ae6
Show file tree
Hide file tree
Showing 15 changed files with 180 additions and 124 deletions.
3 changes: 2 additions & 1 deletion base/boot.jl
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,8 @@ macro _foldable_meta()
#=:terminates_globally=#true,
#=:terminates_locally=#false,
#=:notaskstate=#false,
#=:inaccessiblememonly=#false))
#=:inaccessiblememonly=#false,
#=:noub=#true))
end

const NTuple{N,T} = Tuple{Vararg{T,N}}
Expand Down
50 changes: 25 additions & 25 deletions base/compiler/abstractinterpretation.jl
Original file line number Diff line number Diff line change
Expand Up @@ -464,9 +464,9 @@ function add_call_backedges!(interp::AbstractInterpreter, @nospecialize(rettype)
if !isoverlayed(method_table(interp))
all_effects = Effects(all_effects; nonoverlayed=false)
end
if (# ignore the `:noinbounds` property if `:consistent`-cy is tainted already
(sv isa InferenceState && sv.ipo_effects.consistent === ALWAYS_FALSE) ||
all_effects.consistent === ALWAYS_FALSE ||
if (# ignore the `:noinbounds` property if `:noub` is tainted already
(sv isa InferenceState && !sv.ipo_effects.noub) ||
!all_effects.noub ||
# or this `:noinbounds` doesn't taint it
!stmt_taints_inbounds_consistency(sv))
all_effects = Effects(all_effects; noinbounds=false)
Expand Down Expand Up @@ -1999,7 +1999,7 @@ function abstract_call_known(interp::AbstractInterpreter, @nospecialize(f),
# N.B.: This isn't about the effects of the call itself, but a delayed contribution of the :boundscheck
# statement, so we need to merge this directly into sv, rather than modifying thte effects.
merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; noinbounds=false,
consistent = (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0 ? ALWAYS_FALSE : ALWAYS_TRUE))
noub = iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS)))
end
return CallMeta(rt, effects, NoCallInfo())
elseif isa(f, Core.OpaqueClosure)
Expand Down Expand Up @@ -2222,22 +2222,22 @@ function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::
f = abstract_eval_value(interp, stmt.args[1], vtypes, sv)
if f isa Const && f.val === getfield
# boundscheck of `getfield` call is analyzed by tfunc potentially without
# tainting :inbounds or :consistent when it's known to be nothrow
# tainting :noinbounds or :noub when it's known to be nothrow
@goto delay_effects_analysis
end
end
# If there is no particular `@inbounds` for this function, then we only taint `:noinbounds`,
# which will subsequently taint `:consistent`-cy if this function is called from another
# which will subsequently taint `:noub` if this function is called from another
# function that uses `@inbounds`. However, if this `:boundscheck` is itself within an
# `@inbounds` region, its value depends on `--check-bounds`, so we need to taint
# `:consistent`-cy here also.
merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; noinbounds=false,
consistent = (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0 ? ALWAYS_FALSE : ALWAYS_TRUE))
noub = iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS)))
end
@label delay_effects_analysis
rt = Bool
elseif head === :inbounds
@assert false && "Expected this to have been moved into flags"
@assert false "Expected `:inbounds` expression to have been moved into SSA flags"
elseif head === :the_exception
merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; consistent=ALWAYS_FALSE))
end
Expand Down Expand Up @@ -2355,22 +2355,23 @@ function abstract_eval_statement_expr(interp::AbstractInterpreter, e::Expr, vtyp
t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
ut = unwrap_unionall(t)
consistent = ALWAYS_FALSE
nothrow = false
nothrow = noub = false
if isa(ut, DataType) && !isabstracttype(ut)
ismutable = ismutabletype(ut)
fcount = datatype_fieldcount(ut)
nargs = length(e.args) - 1
if (fcount === nothing || (fcount > nargs && (let t = t
any(i::Int -> !is_undefref_fieldtype(fieldtype(t, i)), (nargs+1):fcount)
end)))
# allocation with undefined field leads to undefined behavior and should taint `:consistent`-cy
consistent = ALWAYS_FALSE
# allocation with undefined field leads to undefined behavior and should taint `:noub`
elseif ismutable
# mutable object isn't `:consistent`, but we can still give the return
# type information a chance to refine this `:consistent`-cy later
# mutable object isn't `:consistent`, but we still have a chance that
# return type information later refines the `:consistent`-cy of the method
consistent = CONSISTENT_IF_NOTRETURNED
noub = true
else
consistent = ALWAYS_TRUE
noub = true
end
if isconcretedispatch(t)
nothrow = true
Expand Down Expand Up @@ -2414,7 +2415,7 @@ function abstract_eval_statement_expr(interp::AbstractInterpreter, e::Expr, vtyp
t = refine_partial_type(t)
end
end
effects = Effects(EFFECTS_TOTAL; consistent, nothrow)
effects = Effects(EFFECTS_TOTAL; consistent, nothrow, noub)
elseif ehead === :splatnew
t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
nothrow = false # TODO: More precision
Expand Down Expand Up @@ -2557,15 +2558,14 @@ function abstract_eval_foreigncall(interp::AbstractInterpreter, e::Expr, vtypes:
cconv = e.args[5]
if isa(cconv, QuoteNode) && (v = cconv.value; isa(v, Tuple{Symbol, UInt8}))
override = decode_effects_override(v[2])
effects = Effects(
override.consistent ? ALWAYS_TRUE : effects.consistent,
override.effect_free ? ALWAYS_TRUE : effects.effect_free,
override.nothrow ? true : effects.nothrow,
override.terminates_globally ? true : effects.terminates,
override.notaskstate ? true : effects.notaskstate,
override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
effects.nonoverlayed,
effects.noinbounds)
effects = Effects(effects;
consistent = override.consistent ? ALWAYS_TRUE : effects.consistent,
effect_free = override.effect_free ? ALWAYS_TRUE : effects.effect_free,
nothrow = override.nothrow ? true : effects.nothrow,
terminates = override.terminates_globally ? true : effects.terminates,
notaskstate = override.notaskstate ? true : effects.notaskstate,
inaccessiblememonly = override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
noub = override.noub ? true : effects.noub)
end
return RTEffects(t, effects)
end
Expand Down Expand Up @@ -2600,8 +2600,8 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
# we ourselves don't read our parent's inbounds.
effects = Effects(effects; noinbounds=true)
end
if (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0
effects = Effects(effects; consistent=ALWAYS_FALSE)
if !iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS)
effects = Effects(effects; noub=false)
end
end
merge_effects!(interp, sv, effects)
Expand Down
71 changes: 46 additions & 25 deletions base/compiler/effects.jl
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Represents computational effects of a method call.
The effects are a composition of different effect bits that represent some program property
of the method being analyzed. They are represented as `Bool` or `UInt8` bits with the
following meanings:
- `effects.consistent::UInt8`:
- `consistent::UInt8`:
* `ALWAYS_TRUE`: this method is guaranteed to return or terminate consistently.
* `ALWAYS_FALSE`: this method may be not return or terminate consistently, and there is
no need for further analysis with respect to this effect property as this conclusion
Expand Down Expand Up @@ -38,6 +38,10 @@ following meanings:
except that it may access or modify mutable memory pointed to by its call arguments.
This may later be refined to `ALWAYS_TRUE` in a case when call arguments are known to be immutable.
This state corresponds to LLVM's `inaccessiblemem_or_argmemonly` function attribute.
- `noub::Bool`: indicates that the method will not execute any undefined behavior (for any input).
Note that undefined behavior may technically cause the method to violate any other effect
assertions (such as `:consistent` or `:effect_free`) as well, but we do not model this,
and they assume the absence of undefined behavior.
- `nonoverlayed::Bool`: indicates that any methods that may be called within this method
are not defined in an [overlayed method table](@ref OverlayMethodTable).
- `noinbounds::Bool`: If set, indicates that this method does not read the parent's `:inbounds`
Expand Down Expand Up @@ -80,7 +84,10 @@ The output represents the state of different effect properties in the following
- `+m` (green): `ALWAYS_TRUE`
- `-m` (red): `ALWAYS_FALSE`
- `?m` (yellow): `INACCESSIBLEMEM_OR_ARGMEMONLY`
7. `noinbounds` (`i`):
7. `noub` (`u`):
- `+u` (green): `true`
- `-u` (red): `false`
8. `noinbounds` (`i`):
- `+i` (green): `true`
- `-i` (red): `false`
Expand All @@ -93,6 +100,7 @@ struct Effects
terminates::Bool
notaskstate::Bool
inaccessiblememonly::UInt8
noub::Bool
nonoverlayed::Bool
noinbounds::Bool
function Effects(
Expand All @@ -102,6 +110,7 @@ struct Effects
terminates::Bool,
notaskstate::Bool,
inaccessiblememonly::UInt8,
noub::Bool,
nonoverlayed::Bool,
noinbounds::Bool)
return new(
Expand All @@ -111,6 +120,7 @@ struct Effects
terminates,
notaskstate,
inaccessiblememonly,
noub,
nonoverlayed,
noinbounds)
end
Expand All @@ -129,27 +139,29 @@ const EFFECT_FREE_IF_INACCESSIBLEMEMONLY = 0x01 << 1
# :inaccessiblememonly bits
const INACCESSIBLEMEM_OR_ARGMEMONLY = 0x01 << 1

const EFFECTS_TOTAL = Effects(ALWAYS_TRUE, ALWAYS_TRUE, true, true, true, ALWAYS_TRUE, true, true)
const EFFECTS_THROWS = Effects(ALWAYS_TRUE, ALWAYS_TRUE, false, true, true, ALWAYS_TRUE, true, true)
const EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, true, true) # unknown mostly, but it's not overlayed and noinbounds at least (e.g. it's not a call)
const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, false, false) # unknown really
const EFFECTS_TOTAL = Effects(ALWAYS_TRUE, ALWAYS_TRUE, true, true, true, ALWAYS_TRUE, true, true, true)
const EFFECTS_THROWS = Effects(ALWAYS_TRUE, ALWAYS_TRUE, false, true, true, ALWAYS_TRUE, true, true, true)
const EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, false, true, true) # unknown mostly, but it's not overlayed and noinbounds at least (e.g. it's not a call)
const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, false, false, false) # unknown really

function Effects(e::Effects = _EFFECTS_UNKNOWN;
consistent::UInt8 = e.consistent,
effect_free::UInt8 = e.effect_free,
nothrow::Bool = e.nothrow,
terminates::Bool = e.terminates,
notaskstate::Bool = e.notaskstate,
inaccessiblememonly::UInt8 = e.inaccessiblememonly,
nonoverlayed::Bool = e.nonoverlayed,
noinbounds::Bool = e.noinbounds)
function Effects(effects::Effects = _EFFECTS_UNKNOWN;
consistent::UInt8 = effects.consistent,
effect_free::UInt8 = effects.effect_free,
nothrow::Bool = effects.nothrow,
terminates::Bool = effects.terminates,
notaskstate::Bool = effects.notaskstate,
inaccessiblememonly::UInt8 = effects.inaccessiblememonly,
noub::Bool = effects.noub,
nonoverlayed::Bool = effects.nonoverlayed,
noinbounds::Bool = effects.noinbounds)
return Effects(
consistent,
effect_free,
nothrow,
terminates,
notaskstate,
inaccessiblememonly,
noub,
nonoverlayed,
noinbounds)
end
Expand All @@ -162,6 +174,7 @@ function merge_effects(old::Effects, new::Effects)
merge_effectbits(old.terminates, new.terminates),
merge_effectbits(old.notaskstate, new.notaskstate),
merge_effectbits(old.inaccessiblememonly, new.inaccessiblememonly),
merge_effectbits(old.noub, new.noub),
merge_effectbits(old.nonoverlayed, new.nonoverlayed),
merge_effectbits(old.noinbounds, new.noinbounds))
end
Expand All @@ -180,18 +193,21 @@ is_nothrow(effects::Effects) = effects.nothrow
is_terminates(effects::Effects) = effects.terminates
is_notaskstate(effects::Effects) = effects.notaskstate
is_inaccessiblememonly(effects::Effects) = effects.inaccessiblememonly === ALWAYS_TRUE
is_noub(effects::Effects) = effects.noub
is_nonoverlayed(effects::Effects) = effects.nonoverlayed

# implies `is_notaskstate` & `is_inaccessiblememonly`, but not explicitly checked here
is_foldable(effects::Effects) =
is_consistent(effects) &&
is_noub(effects) &&
is_effect_free(effects) &&
is_terminates(effects)

is_foldable_nothrow(effects::Effects) =
is_foldable(effects) &&
is_nothrow(effects)

# TODO add `is_noub` here?
is_removable_if_unused(effects::Effects) =
is_effect_free(effects) &&
is_terminates(effects) &&
Expand All @@ -209,14 +225,15 @@ is_effect_free_if_inaccessiblememonly(effects::Effects) = !iszero(effects.effect
is_inaccessiblemem_or_argmemonly(effects::Effects) = effects.inaccessiblememonly === INACCESSIBLEMEM_OR_ARGMEMONLY

function encode_effects(e::Effects)
return ((e.consistent % UInt32) << 0) |
((e.effect_free % UInt32) << 3) |
((e.nothrow % UInt32) << 5) |
((e.terminates % UInt32) << 6) |
((e.notaskstate % UInt32) << 7) |
((e.inaccessiblememonly % UInt32) << 8) |
((e.nonoverlayed % UInt32) << 10)|
((e.noinbounds % UInt32) << 11)
return ((e.consistent % UInt32) << 0) |
((e.effect_free % UInt32) << 3) |
((e.nothrow % UInt32) << 5) |
((e.terminates % UInt32) << 6) |
((e.notaskstate % UInt32) << 7) |
((e.inaccessiblememonly % UInt32) << 8) |
((e.noub % UInt32) << 10) |
((e.nonoverlayed % UInt32) << 11) |
((e.noinbounds % UInt32) << 12)
end

function decode_effects(e::UInt32)
Expand All @@ -228,7 +245,8 @@ function decode_effects(e::UInt32)
_Bool((e >> 7) & 0x01),
UInt8((e >> 8) & 0x03),
_Bool((e >> 10) & 0x01),
_Bool((e >> 11) & 0x01))
_Bool((e >> 11) & 0x01),
_Bool((e >> 12) & 0x01))
end

struct EffectsOverride
Expand All @@ -239,6 +257,7 @@ struct EffectsOverride
terminates_locally::Bool
notaskstate::Bool
inaccessiblememonly::Bool
noub::Bool
end

function encode_effects_override(eo::EffectsOverride)
Expand All @@ -250,6 +269,7 @@ function encode_effects_override(eo::EffectsOverride)
eo.terminates_locally && (e |= (0x01 << 4))
eo.notaskstate && (e |= (0x01 << 5))
eo.inaccessiblememonly && (e |= (0x01 << 6))
eo.noub && (e |= (0x01 << 7))
return e
end

Expand All @@ -261,5 +281,6 @@ function decode_effects_override(e::UInt8)
(e & (0x01 << 3)) != 0x00,
(e & (0x01 << 4)) != 0x00,
(e & (0x01 << 5)) != 0x00,
(e & (0x01 << 6)) != 0x00)
(e & (0x01 << 6)) != 0x00,
(e & (0x01 << 7)) != 0x00)
end
2 changes: 2 additions & 0 deletions base/compiler/ssair/show.jl
Original file line number Diff line number Diff line change
Expand Up @@ -1020,6 +1020,8 @@ function Base.show(io::IO, e::Effects)
print(io, ',')
printstyled(io, effectbits_letter(e, :inaccessiblememonly, 'm'); color=effectbits_color(e, :inaccessiblememonly))
print(io, ',')
printstyled(io, effectbits_letter(e, :noub, 'u'); color=effectbits_color(e, :noub))
print(io, ',')
printstyled(io, effectbits_letter(e, :noinbounds, 'i'); color=effectbits_color(e, :noinbounds))
print(io, ')')
e.nonoverlayed || printstyled(io, ''; color=:red)
Expand Down
Loading

0 comments on commit d1d8ae6

Please sign in to comment.