Skip to content

Commit

Permalink
effects: add new @consistent_overlay macro (#54322)
Browse files Browse the repository at this point in the history
This PR serves to replace #51080 and close #52940.
It extends the `:nonoverlayed` to `UInt8` and introduces the
`CONSISTENT_OVERLAY` effect bit, allowing for concrete evaluation of
overlay methods using the original non-overlayed counterparts when
applied. This newly added `:nonoverlayed`-bit is enabled through the
newly added `Base.Experimental.@consistent_overlay mt def` macro.
`@consistent_overlay` is similar to `@overlay`, but it sets the
`:nonoverlayed`-bit to `CONSISTENT_OVERLAY` for the target method
definition, allowing the method to be concrete-evaluated.
To use this feature safely, I have also added quite precise
documentation to `@consistent_overlay`.
  • Loading branch information
aviatesk authored and KristofferC committed Jun 18, 2024
1 parent f41f896 commit 8bdf1fa
Show file tree
Hide file tree
Showing 14 changed files with 291 additions and 91 deletions.
3 changes: 2 additions & 1 deletion base/boot.jl
Original file line number Diff line number Diff line change
Expand Up @@ -282,7 +282,8 @@ macro _foldable_meta()
#=:notaskstate=#true,
#=:inaccessiblememonly=#true,
#=:noub=#true,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end

macro inline() Expr(:meta, :inline) end
Expand Down
14 changes: 11 additions & 3 deletions base/compiler/abstractinterpretation.jl
Original file line number Diff line number Diff line change
Expand Up @@ -491,7 +491,7 @@ function add_call_backedges!(interp::AbstractInterpreter, @nospecialize(rettype)
# ignore the `:nonoverlayed` property if `interp` doesn't use overlayed method table
# since it will never be tainted anyway
if !isoverlayed(method_table(interp))
all_effects = Effects(all_effects; nonoverlayed=false)
all_effects = Effects(all_effects; nonoverlayed=ALWAYS_FALSE)
end
all_effects === Effects() && return nothing
end
Expand Down Expand Up @@ -889,7 +889,15 @@ function concrete_eval_eligible(interp::AbstractInterpreter,
mi = result.edge
if mi !== nothing && is_foldable(effects)
if f !== nothing && is_all_const_arg(arginfo, #=start=#2)
if is_nonoverlayed(interp) || is_nonoverlayed(effects)
if (is_nonoverlayed(interp) || is_nonoverlayed(effects) ||
# Even if overlay methods are involved, when `:consistent_overlay` is
# explicitly applied, we can still perform concrete evaluation using the
# original methods for executing them.
# While there's a chance that the non-overlayed counterparts may raise
# non-egal exceptions, it will not impact the compilation validity, since:
# - the results of the concrete evaluation will not be inlined
# - the exception types from the concrete evaluation will not be propagated
is_consistent_overlay(effects))
return :concrete_eval
end
# disable concrete-evaluation if this function call is tainted by some overlayed
Expand Down Expand Up @@ -2770,7 +2778,7 @@ function override_effects(effects::Effects, override::EffectsOverride)
notaskstate = override.notaskstate ? true : effects.notaskstate,
inaccessiblememonly = override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
noub = override.noub ? ALWAYS_TRUE :
override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE ? NOUB_IF_NOINBOUNDS :
(override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE) ? NOUB_IF_NOINBOUNDS :
effects.noub)
end

Expand Down
11 changes: 7 additions & 4 deletions base/compiler/compiler.jl
Original file line number Diff line number Diff line change
Expand Up @@ -47,10 +47,11 @@ struct EffectsOverride
inaccessiblememonly::Bool
noub::Bool
noub_if_noinbounds::Bool
consistent_overlay::Bool
end
function EffectsOverride(
override::EffectsOverride =
EffectsOverride(false, false, false, false, false, false, false, false, false);
EffectsOverride(false, false, false, false, false, false, false, false, false, false);
consistent::Bool = override.consistent,
effect_free::Bool = override.effect_free,
nothrow::Bool = override.nothrow,
Expand All @@ -59,7 +60,8 @@ function EffectsOverride(
notaskstate::Bool = override.notaskstate,
inaccessiblememonly::Bool = override.inaccessiblememonly,
noub::Bool = override.noub,
noub_if_noinbounds::Bool = override.noub_if_noinbounds)
noub_if_noinbounds::Bool = override.noub_if_noinbounds,
consistent_overlay::Bool = override.consistent_overlay)
return EffectsOverride(
consistent,
effect_free,
Expand All @@ -69,9 +71,10 @@ function EffectsOverride(
notaskstate,
inaccessiblememonly,
noub,
noub_if_noinbounds)
noub_if_noinbounds,
consistent_overlay)
end
const NUM_EFFECTS_OVERRIDES = 9 # sync with julia.h
const NUM_EFFECTS_OVERRIDES = 10 # sync with julia.h

# essential files and libraries
include("essentials.jl")
Expand Down
59 changes: 38 additions & 21 deletions base/compiler/effects.jl
Original file line number Diff line number Diff line change
Expand Up @@ -43,16 +43,21 @@ 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::UInt8`: 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.
* `ALWAYS_TRUE`: this method is guaranteed to not execute any undefined behavior.
- `noub::UInt8`:
* `ALWAYS_TRUE`: this method is guaranteed to not execute any undefined behavior (for any input).
* `ALWAYS_FALSE`: this method may execute undefined behavior.
* `NOUB_IF_NOINBOUNDS`: this method is guaranteed to not execute any undefined behavior
if the caller does not set nor propagate the `@inbounds` context.
- `nonoverlayed::Bool`: indicates that any methods that may be called within this method
are not defined in an [overlayed method table](@ref OverlayMethodTable).
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::UInt8`:
* `ALWAYS_TRUE`: this method is guaranteed to not invoke any methods that defined in an
[overlayed method table](@ref OverlayMethodTable).
* `CONSISTENT_OVERLAY`: this method may invoke overlayed methods, but all such overlayed
methods are `:consistent` with their non-overlayed original counterparts
(see [`Base.@assume_effects`](@ref) for the exact definition of `:consistenct`-cy).
* `ALWAYS_FALSE`: this method may invoke overlayed methods.
Note that the representations above are just internal implementation details and thus likely
to change in the future. See [`Base.@assume_effects`](@ref) for more detailed explanation
Expand Down Expand Up @@ -94,8 +99,10 @@ The output represents the state of different effect properties in the following
- `+u` (green): `true`
- `-u` (red): `false`
- `?u` (yellow): `NOUB_IF_NOINBOUNDS`
Additionally, if the `nonoverlayed` property is false, a red prime symbol (′) is displayed after the tuple.
8. `:nonoverlayed` (`o`):
- `+o` (green): `ALWAYS_TRUE`
- `-o` (red): `ALWAYS_FALSE`
- `?o` (yellow): `CONSISTENT_OVERLAY`
"""
struct Effects
consistent::UInt8
Expand All @@ -105,7 +112,7 @@ struct Effects
notaskstate::Bool
inaccessiblememonly::UInt8
noub::UInt8
nonoverlayed::Bool
nonoverlayed::UInt8
function Effects(
consistent::UInt8,
effect_free::UInt8,
Expand All @@ -114,7 +121,7 @@ struct Effects
notaskstate::Bool,
inaccessiblememonly::UInt8,
noub::UInt8,
nonoverlayed::Bool)
nonoverlayed::UInt8)
return new(
consistent,
effect_free,
Expand Down Expand Up @@ -150,10 +157,13 @@ const INACCESSIBLEMEM_OR_ARGMEMONLY = 0x01 << 1
# :noub bits
const NOUB_IF_NOINBOUNDS = 0x01 << 1

const EFFECTS_TOTAL = Effects(ALWAYS_TRUE, ALWAYS_TRUE, true, true, true, ALWAYS_TRUE, ALWAYS_TRUE, true)
const EFFECTS_THROWS = Effects(ALWAYS_TRUE, ALWAYS_TRUE, false, true, true, ALWAYS_TRUE, ALWAYS_TRUE, true)
const EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, ALWAYS_FALSE, true) # unknown mostly, but it's not overlayed at least (e.g. it's not a call)
const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, ALWAYS_FALSE, false) # unknown really
# :nonoverlayed bits
const CONSISTENT_OVERLAY = 0x01 << 1

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

function Effects(effects::Effects = _EFFECTS_UNKNOWN;
consistent::UInt8 = effects.consistent,
Expand All @@ -163,7 +173,7 @@ function Effects(effects::Effects = _EFFECTS_UNKNOWN;
notaskstate::Bool = effects.notaskstate,
inaccessiblememonly::UInt8 = effects.inaccessiblememonly,
noub::UInt8 = effects.noub,
nonoverlayed::Bool = effects.nonoverlayed)
nonoverlayed::UInt8 = effects.nonoverlayed)
return Effects(
consistent,
effect_free,
Expand Down Expand Up @@ -229,8 +239,11 @@ function is_better_effects(new::Effects, old::Effects)
elseif new.noub != old.noub
return false
end
if new.nonoverlayed
any_improved |= !old.nonoverlayed
if new.nonoverlayed == ALWAYS_TRUE
any_improved |= old.nonoverlayed != ALWAYS_TRUE
elseif new.nonoverlayed == CONSISTENT_OVERLAY
old.nonoverlayed == ALWAYS_TRUE && return false
any_improved |= old.nonoverlayed != CONSISTENT_OVERLAY
elseif new.nonoverlayed != old.nonoverlayed
return false
end
Expand Down Expand Up @@ -265,7 +278,7 @@ is_notaskstate(effects::Effects) = effects.notaskstate
is_inaccessiblememonly(effects::Effects) = effects.inaccessiblememonly === ALWAYS_TRUE
is_noub(effects::Effects) = effects.noub === ALWAYS_TRUE
is_noub_if_noinbounds(effects::Effects) = effects.noub === NOUB_IF_NOINBOUNDS
is_nonoverlayed(effects::Effects) = effects.nonoverlayed
is_nonoverlayed(effects::Effects) = effects.nonoverlayed === ALWAYS_TRUE

# implies `is_notaskstate` & `is_inaccessiblememonly`, but not explicitly checked here
is_foldable(effects::Effects) =
Expand Down Expand Up @@ -295,6 +308,8 @@ is_effect_free_if_inaccessiblememonly(effects::Effects) = !iszero(effects.effect

is_inaccessiblemem_or_argmemonly(effects::Effects) = effects.inaccessiblememonly === INACCESSIBLEMEM_OR_ARGMEMONLY

is_consistent_overlay(effects::Effects) = effects.nonoverlayed === CONSISTENT_OVERLAY

function encode_effects(e::Effects)
return ((e.consistent % UInt32) << 0) |
((e.effect_free % UInt32) << 3) |
Expand All @@ -315,7 +330,7 @@ function decode_effects(e::UInt32)
_Bool((e >> 7) & 0x01),
UInt8((e >> 8) & 0x03),
UInt8((e >> 10) & 0x03),
_Bool((e >> 12) & 0x01))
UInt8((e >> 12) & 0x03))
end

function encode_effects_override(eo::EffectsOverride)
Expand All @@ -329,6 +344,7 @@ function encode_effects_override(eo::EffectsOverride)
eo.inaccessiblememonly && (e |= (0x0001 << 6))
eo.noub && (e |= (0x0001 << 7))
eo.noub_if_noinbounds && (e |= (0x0001 << 8))
eo.consistent_overlay && (e |= (0x0001 << 9))
return e
end

Expand All @@ -342,7 +358,8 @@ function decode_effects_override(e::UInt16)
!iszero(e & (0x0001 << 5)),
!iszero(e & (0x0001 << 6)),
!iszero(e & (0x0001 << 7)),
!iszero(e & (0x0001 << 8)))
!iszero(e & (0x0001 << 8)),
!iszero(e & (0x0001 << 9)))
end

decode_statement_effects_override(ssaflag::UInt32) =
Expand Down
5 changes: 4 additions & 1 deletion base/compiler/inferencestate.jl
Original file line number Diff line number Diff line change
Expand Up @@ -329,7 +329,10 @@ mutable struct InferenceState
end

if def isa Method
ipo_effects = Effects(ipo_effects; nonoverlayed=is_nonoverlayed(def))
nonoverlayed = is_nonoverlayed(def) ? ALWAYS_TRUE :
is_effect_overridden(def, :consistent_overlay) ? CONSISTENT_OVERLAY :
ALWAYS_FALSE
ipo_effects = Effects(ipo_effects; nonoverlayed)
end

restrict_abstract_call_sites = isa(def, Module)
Expand Down
3 changes: 2 additions & 1 deletion base/compiler/ssair/show.jl
Original file line number Diff line number Diff line change
Expand Up @@ -1019,8 +1019,9 @@ function Base.show(io::IO, e::Effects)
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, :nonoverlayed, 'o'); color=effectbits_color(e, :nonoverlayed))
print(io, ')')
e.nonoverlayed || printstyled(io, ''; color=:red)
end

@specialize
3 changes: 3 additions & 0 deletions base/compiler/typeinfer.jl
Original file line number Diff line number Diff line change
Expand Up @@ -492,6 +492,9 @@ function adjust_effects(ipo_effects::Effects, def::Method)
elseif is_effect_overridden(override, :noub_if_noinbounds) && ipo_effects.noub !== ALWAYS_TRUE
ipo_effects = Effects(ipo_effects; noub=NOUB_IF_NOINBOUNDS)
end
if is_effect_overridden(override, :consistent_overlay)
ipo_effects = Effects(ipo_effects; nonoverlayed=CONSISTENT_OVERLAY)
end
return ipo_effects
end

Expand Down
36 changes: 24 additions & 12 deletions base/essentials.jl
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,8 @@ macro _total_meta()
#=:notaskstate=#true,
#=:inaccessiblememonly=#true,
#=:noub=#true,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :foldable` (supposed to be used for bootstrapping)
macro _foldable_meta()
Expand All @@ -225,7 +226,8 @@ macro _foldable_meta()
#=:notaskstate=#true,
#=:inaccessiblememonly=#true,
#=:noub=#true,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :terminates_locally` (supposed to be used for bootstrapping)
macro _terminates_locally_meta()
Expand All @@ -238,7 +240,8 @@ macro _terminates_locally_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :terminates_globally` (supposed to be used for bootstrapping)
macro _terminates_globally_meta()
Expand All @@ -251,7 +254,8 @@ macro _terminates_globally_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :terminates_globally :notaskstate` (supposed to be used for bootstrapping)
macro _terminates_globally_notaskstate_meta()
Expand All @@ -264,7 +268,8 @@ macro _terminates_globally_notaskstate_meta()
#=:notaskstate=#true,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :terminates_globally :noub` (supposed to be used for bootstrapping)
macro _terminates_globally_noub_meta()
Expand All @@ -277,7 +282,8 @@ macro _terminates_globally_noub_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#true,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :effect_free :terminates_locally` (supposed to be used for bootstrapping)
macro _effect_free_terminates_locally_meta()
Expand All @@ -290,7 +296,8 @@ macro _effect_free_terminates_locally_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :nothrow :noub` (supposed to be used for bootstrapping)
macro _nothrow_noub_meta()
Expand All @@ -303,7 +310,8 @@ macro _nothrow_noub_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#true,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
macro _nothrow_meta()
Expand All @@ -316,7 +324,8 @@ macro _nothrow_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
macro _noub_meta()
Expand All @@ -329,7 +338,8 @@ macro _noub_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#true,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :notaskstate` (supposed to be used for bootstrapping)
macro _notaskstate_meta()
Expand All @@ -342,7 +352,8 @@ macro _notaskstate_meta()
#=:notaskstate=#true,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#false))
#=:noub_if_noinbounds=#false,
#=:consistent_overlay=#false))
end
# can be used in place of `@assume_effects :noub_if_noinbounds` (supposed to be used for bootstrapping)
macro _noub_if_noinbounds_meta()
Expand All @@ -355,7 +366,8 @@ macro _noub_if_noinbounds_meta()
#=:notaskstate=#false,
#=:inaccessiblememonly=#false,
#=:noub=#false,
#=:noub_if_noinbounds=#true))
#=:noub_if_noinbounds=#true,
#=:consistent_overlay=#false))
end

# another version of inlining that propagates an inbounds context
Expand Down
Loading

0 comments on commit 8bdf1fa

Please sign in to comment.