From df1751311e9fbd6cb58332c253df702caeffcd27 Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Tue, 30 Apr 2024 18:29:58 +0900
Subject: [PATCH 1/5] allow override of `:nonoverlayed`

---
 base/boot.jl                            |  3 +-
 base/compiler/abstractinterpretation.jl |  3 +-
 base/compiler/compiler.jl               | 11 ++++--
 base/compiler/effects.jl                |  4 +-
 base/compiler/typeinfer.jl              |  3 ++
 base/essentials.jl                      | 36 ++++++++++++------
 base/expr.jl                            | 18 ++++++---
 src/julia.h                             |  3 +-
 src/method.c                            |  1 +
 test/compiler/AbstractInterpreter.jl    | 50 ++++++++++++++++++-------
 10 files changed, 93 insertions(+), 39 deletions(-)

diff --git a/base/boot.jl b/base/boot.jl
index 0f9069190e526..5e7691c21b338 100644
--- a/base/boot.jl
+++ b/base/boot.jl
@@ -283,7 +283,8 @@ macro _foldable_meta()
         #=:notaskstate=#true,
         #=:inaccessiblememonly=#true,
         #=:noub=#true,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 
 macro inline()   Expr(:meta, :inline)   end
diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 6d22083cbbe8c..a384c120ac7ac 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -2820,7 +2820,8 @@ function override_effects(effects::Effects, override::EffectsOverride)
         inaccessiblememonly = override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
         noub = override.noub ? ALWAYS_TRUE :
                override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE ? NOUB_IF_NOINBOUNDS :
-               effects.noub)
+               effects.noub,
+        nonoverlayed = override.nonoverlayed ? true : effects.nonoverlayed)
 end
 
 isdefined_globalref(g::GlobalRef) = !iszero(ccall(:jl_globalref_boundp, Cint, (Any,), g))
diff --git a/base/compiler/compiler.jl b/base/compiler/compiler.jl
index fb59b9b63b02d..45e8b2edd14b4 100644
--- a/base/compiler/compiler.jl
+++ b/base/compiler/compiler.jl
@@ -48,10 +48,11 @@ struct EffectsOverride
     inaccessiblememonly::Bool
     noub::Bool
     noub_if_noinbounds::Bool
+    nonoverlayed::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,
@@ -60,7 +61,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,
+    nonoverlayed::Bool = override.nonoverlayed)
     return EffectsOverride(
         consistent,
         effect_free,
@@ -70,9 +72,10 @@ function EffectsOverride(
         notaskstate,
         inaccessiblememonly,
         noub,
-        noub_if_noinbounds)
+        noub_if_noinbounds,
+        nonoverlayed)
 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")
diff --git a/base/compiler/effects.jl b/base/compiler/effects.jl
index a3d30baef9efa..5bafd8a0bfad3 100644
--- a/base/compiler/effects.jl
+++ b/base/compiler/effects.jl
@@ -329,6 +329,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.nonoverlayed        && (e |= (0x0001 << 9))
     return e
 end
 
@@ -342,7 +343,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) =
diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl
index c8c624970aa26..8f2441a47cbaa 100644
--- a/base/compiler/typeinfer.jl
+++ b/base/compiler/typeinfer.jl
@@ -502,6 +502,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, :nonoverlayed)
+        ipo_effects = Effects(ipo_effects; nonoverlayed=true)
+    end
     return ipo_effects
 end
 
diff --git a/base/essentials.jl b/base/essentials.jl
index c907d95c47265..08b4ce12898c6 100644
--- a/base/essentials.jl
+++ b/base/essentials.jl
@@ -201,7 +201,8 @@ macro _total_meta()
         #=:notaskstate=#true,
         #=:inaccessiblememonly=#true,
         #=:noub=#true,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :foldable` (supposed to be used for bootstrapping)
 macro _foldable_meta()
@@ -214,7 +215,8 @@ macro _foldable_meta()
         #=:notaskstate=#true,
         #=:inaccessiblememonly=#true,
         #=:noub=#true,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :terminates_locally` (supposed to be used for bootstrapping)
 macro _terminates_locally_meta()
@@ -227,7 +229,8 @@ macro _terminates_locally_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :terminates_globally` (supposed to be used for bootstrapping)
 macro _terminates_globally_meta()
@@ -240,7 +243,8 @@ macro _terminates_globally_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :terminates_globally :notaskstate` (supposed to be used for bootstrapping)
 macro _terminates_globally_notaskstate_meta()
@@ -253,7 +257,8 @@ macro _terminates_globally_notaskstate_meta()
         #=:notaskstate=#true,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :terminates_globally :noub` (supposed to be used for bootstrapping)
 macro _terminates_globally_noub_meta()
@@ -266,7 +271,8 @@ macro _terminates_globally_noub_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#true,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#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()
@@ -279,7 +285,8 @@ macro _effect_free_terminates_locally_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :nothrow :noub` (supposed to be used for bootstrapping)
 macro _nothrow_noub_meta()
@@ -292,7 +299,8 @@ macro _nothrow_noub_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#true,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
 macro _nothrow_meta()
@@ -305,7 +313,8 @@ macro _nothrow_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
 macro _noub_meta()
@@ -318,7 +327,8 @@ macro _noub_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#true,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :notaskstate` (supposed to be used for bootstrapping)
 macro _notaskstate_meta()
@@ -331,7 +341,8 @@ macro _notaskstate_meta()
         #=:notaskstate=#true,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#false))
+        #=:noub_if_noinbounds=#false,
+        #=:nonoverlayed=#false))
 end
 # can be used in place of `@assume_effects :noub_if_noinbounds` (supposed to be used for bootstrapping)
 macro _noub_if_noinbounds_meta()
@@ -344,7 +355,8 @@ macro _noub_if_noinbounds_meta()
         #=:notaskstate=#false,
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
-        #=:noub_if_noinbounds=#true))
+        #=:noub_if_noinbounds=#true,
+        #=:nonoverlayed=#false))
 end
 
 # another version of inlining that propagates an inbounds context
diff --git a/base/expr.jl b/base/expr.jl
index cbeb16dd8d79b..cd66e5150b951 100644
--- a/base/expr.jl
+++ b/base/expr.jl
@@ -479,7 +479,7 @@ CodeInfo(
 !!! compat "Julia 1.10"
     The usage within a function body requires at least Julia 1.10.
 
-!!! compact "Julia 1.11"
+!!! compat "Julia 1.11"
     The code block annotation requires at least Julia 1.11.
 
 !!! warning
@@ -505,6 +505,7 @@ The following `setting`s are supported.
 - `:inaccessiblememonly`
 - `:noub`
 - `:noub_if_noinbounds`
+- `:nonoverlayed`
 - `:foldable`
 - `:removable`
 - `:total`
@@ -673,6 +674,10 @@ The `:noub` setting asserts that the method will not execute any undefined behav
 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`
+TODO.
+
 ---
 ## `:foldable`
 
@@ -793,6 +798,8 @@ function compute_assumed_setting(override::EffectsOverride, @nospecialize(settin
         return EffectsOverride(override; noub = val)
     elseif setting === :noub_if_noinbounds
         return EffectsOverride(override; noub_if_noinbounds = val)
+    elseif setting === :nonoverlayed
+        return EffectsOverride(override; nonoverlayed = val)
     elseif setting === :foldable
         consistent = effect_free = terminates_globally = noub = val
         return EffectsOverride(override; consistent, effect_free, terminates_globally, noub)
@@ -810,10 +817,11 @@ function compute_assumed_setting(override::EffectsOverride, @nospecialize(settin
 end
 
 function form_purity_expr(override::EffectsOverride)
-    return Expr(:purity,
-        override.consistent, override.effect_free, override.nothrow,
-        override.terminates_globally, override.terminates_locally, override.notaskstate,
-        override.inaccessiblememonly, override.noub, override.noub_if_noinbounds)
+    ex = Expr(:purity)
+    for i = 1:Core.Compiler.NUM_EFFECTS_OVERRIDES
+        push!(ex.args, getfield(override, i))
+    end
+    return ex
 end
 
 """
diff --git a/src/julia.h b/src/julia.h
index a7c26977aa20b..886421a738719 100644
--- a/src/julia.h
+++ b/src/julia.h
@@ -279,11 +279,12 @@ typedef union __jl_purity_overrides_t {
         uint16_t ipo_inaccessiblememonly : 1;
         uint16_t ipo_noub                : 1;
         uint16_t ipo_noub_if_noinbounds  : 1;
+        uint16_t ipo_nonoverlayed        : 1;
     } overrides;
     uint16_t bits;
 } _jl_purity_overrides_t;
 
-#define NUM_EFFECTS_OVERRIDES 9
+#define NUM_EFFECTS_OVERRIDES 10
 #define NUM_IR_FLAGS 13
 
 // This type describes a single function body
diff --git a/src/method.c b/src/method.c
index 531ad444b1640..3f54b57c3c3fb 100644
--- a/src/method.c
+++ b/src/method.c
@@ -479,6 +479,7 @@ jl_code_info_t *jl_new_code_info_from_ir(jl_expr_t *ir)
                         li->purity.overrides.ipo_inaccessiblememonly = jl_unbox_bool(jl_exprarg(ma, 6));
                         li->purity.overrides.ipo_noub = jl_unbox_bool(jl_exprarg(ma, 7));
                         li->purity.overrides.ipo_noub_if_noinbounds = jl_unbox_bool(jl_exprarg(ma, 8));
+                        li->purity.overrides.ipo_nonoverlayed = jl_unbox_bool(jl_exprarg(ma, 9));
                     }
                 }
                 else
diff --git a/test/compiler/AbstractInterpreter.jl b/test/compiler/AbstractInterpreter.jl
index 4c468d1504bef..3978050616a3e 100644
--- a/test/compiler/AbstractInterpreter.jl
+++ b/test/compiler/AbstractInterpreter.jl
@@ -31,8 +31,8 @@ using Base.Experimental: @MethodTable, @overlay
 end
 
 @newinterp MTOverlayInterp
-@MethodTable OverlayedMT
-CC.method_table(interp::MTOverlayInterp) = CC.OverlayMethodTable(CC.get_inference_world(interp), OverlayedMT)
+@MethodTable OVERLAY_MT
+CC.method_table(interp::MTOverlayInterp) = CC.OverlayMethodTable(CC.get_inference_world(interp), OVERLAY_MT)
 
 function CC.add_remark!(interp::MTOverlayInterp, ::CC.InferenceState, remark)
     if interp.meta !== nothing
@@ -44,7 +44,7 @@ end
 
 struct StrangeSinError end
 strangesin(x) = sin(x)
-@overlay OverlayedMT strangesin(x::Float64) =
+@overlay OVERLAY_MT strangesin(x::Float64) =
     iszero(x) ? throw(StrangeSinError()) : x < 0 ? nothing : cos(x)
 
 # inference should use the overlayed method table
@@ -102,7 +102,7 @@ end |> only === Float64
 
 # not fully covered overlay method match
 overlay_match(::Any) = nothing
-@overlay OverlayedMT overlay_match(::Int) = missing
+@overlay OVERLAY_MT overlay_match(::Int) = missing
 @test Base.return_types((Any,); interp=MTOverlayInterp()) do x
     overlay_match(x)
 end |> only === Union{Nothing,Missing}
@@ -134,11 +134,33 @@ Base.@assume_effects :total totalcall(f, args...) = f(args...)
     end
 end |> only === Nothing
 
+# override `:native_executable` to allow concrete-eval for overlay-ed methods
+Base.@assume_effects :foldable function gpucompiler384(x::Int)
+    1 < x < 20 || error("x is too big")
+    return factorial(x)
+end
+@overlay OVERLAY_MT Base.@assume_effects :foldable :nonoverlayed function gpucompiler384(x::Int)
+    1 < x < 20 || raise_on_gpu("x is too big")
+    return factorial(x)
+end
+@noinline raise_on_gpu(x) = #=do something with GPU=# error(x)
+call_gpucompiler384(x) = gpucompiler384(x)
+
+@test Base.infer_effects(gpucompiler384, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_nonoverlayed
+@test Base.infer_effects(call_gpucompiler384, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_nonoverlayed
+
+@test Base.infer_return_type(; interp=MTOverlayInterp()) do
+    Val(gpucompiler384(3))
+end == Val{6}
+@test Base.infer_return_type(; interp=MTOverlayInterp()) do
+    Val(call_gpucompiler384(3))
+end == Val{6}
+
 # GPUCompiler needs accurate inference through kwfunc with the overlay of `Core.throw_inexacterror`
 # https://github.com/JuliaLang/julia/issues/48097
 @newinterp Issue48097Interp
-@MethodTable Issue48097MT
-CC.method_table(interp::Issue48097Interp) = CC.OverlayMethodTable(CC.get_inference_world(interp), Issue48097MT)
+@MethodTable ISSUE_48097_MT
+CC.method_table(interp::Issue48097Interp) = CC.OverlayMethodTable(CC.get_inference_world(interp), ISSUE_48097_MT)
 CC.InferenceParams(::Issue48097Interp) = CC.InferenceParams(; unoptimize_throw_blocks=false)
 function CC.concrete_eval_eligible(interp::Issue48097Interp,
     @nospecialize(f), result::CC.MethodCallResult, arginfo::CC.ArgInfo, sv::CC.AbsIntState)
@@ -150,7 +172,7 @@ function CC.concrete_eval_eligible(interp::Issue48097Interp,
     end
     return ret
 end
-@overlay Issue48097MT @noinline Core.throw_inexacterror(f::Symbol, ::Type{T}, val) where {T} = return
+@overlay ISSUE_48097_MT @noinline Core.throw_inexacterror(f::Symbol, ::Type{T}, val) where {T} = return
 issue48097(; kwargs...) = return 42
 @test fully_eliminated(; interp=Issue48097Interp(), retval=42) do
     issue48097(; a=1f0, b=1.0)
@@ -166,11 +188,11 @@ outer52938(x) = @inline inner52938(x, Tuple{}; foo=Ref(42), bar=1)
 
 # Should not concrete-eval overlayed methods in semi-concrete interpretation
 @newinterp OverlaySinInterp
-@MethodTable OverlaySinMT
-CC.method_table(interp::OverlaySinInterp) = CC.OverlayMethodTable(CC.get_inference_world(interp), OverlaySinMT)
+@MethodTable OVERLAY_SIN_MT
+CC.method_table(interp::OverlaySinInterp) = CC.OverlayMethodTable(CC.get_inference_world(interp), OVERLAY_SIN_MT)
 overlay_sin1(x) = error("Not supposed to be called.")
-@overlay OverlaySinMT overlay_sin1(x) = cos(x)
-@overlay OverlaySinMT Base.sin(x::Union{Float32,Float64}) = overlay_sin1(x)
+@overlay OVERLAY_SIN_MT overlay_sin1(x) = cos(x)
+@overlay OVERLAY_SIN_MT Base.sin(x::Union{Float32,Float64}) = overlay_sin1(x)
 let ir = Base.code_ircode(; interp=OverlaySinInterp()) do
         sin(0.)
     end |> only |> first
@@ -178,7 +200,7 @@ let ir = Base.code_ircode(; interp=OverlaySinInterp()) do
     oc = Core.OpaqueClosure(ir)
     @test oc() == cos(0.)
 end
-@overlay OverlaySinMT Base.sin(x::Union{Float32,Float64}) = @noinline overlay_sin1(x)
+@overlay OVERLAY_SIN_MT Base.sin(x::Union{Float32,Float64}) = @noinline overlay_sin1(x)
 let ir = Base.code_ircode(; interp=OverlaySinInterp()) do
         sin(0.)
     end |> only |> first
@@ -187,9 +209,9 @@ let ir = Base.code_ircode(; interp=OverlaySinInterp()) do
     @test oc() == cos(0.)
 end
 _overlay_sin2(x) = error("Not supposed to be called.")
-@overlay OverlaySinMT _overlay_sin2(x) = cos(x)
+@overlay OVERLAY_SIN_MT _overlay_sin2(x) = cos(x)
 overlay_sin2(x) = _overlay_sin2(x)
-@overlay OverlaySinMT Base.sin(x::Union{Float32,Float64}) = @noinline overlay_sin2(x)
+@overlay OVERLAY_SIN_MT Base.sin(x::Union{Float32,Float64}) = @noinline overlay_sin2(x)
 let ir = Base.code_ircode(; interp=OverlaySinInterp()) do
         sin(0.)
     end |> only |> first

From 65bfc95db9d0644614c7d187782e5dd20fc71c9b Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Wed, 1 May 2024 00:56:09 +0900
Subject: [PATCH 2/5] extend `:nonoverlayed` effect bit and add new
 `:consistent_overlay` override

---
 base/boot.jl                            |  2 +-
 base/compiler/abstractinterpretation.jl | 17 +++++---
 base/compiler/compiler.jl               |  6 +--
 base/compiler/effects.jl                | 57 ++++++++++++++++---------
 base/compiler/inferencestate.jl         |  5 ++-
 base/compiler/ssair/show.jl             |  3 +-
 base/compiler/typeinfer.jl              |  4 +-
 base/essentials.jl                      | 24 +++++------
 base/expr.jl                            | 35 ++++++++++++---
 src/julia.h                             | 13 +++---
 src/method.c                            |  2 +-
 test/compiler/AbstractInterpreter.jl    | 37 ++++++++--------
 test/namedtuple.jl                      |  4 +-
 13 files changed, 130 insertions(+), 79 deletions(-)

diff --git a/base/boot.jl b/base/boot.jl
index 5e7691c21b338..3d19e46bf5d5d 100644
--- a/base/boot.jl
+++ b/base/boot.jl
@@ -284,7 +284,7 @@ macro _foldable_meta()
         #=:inaccessiblememonly=#true,
         #=:noub=#true,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#false))
+        #=:consistent_overlay=#false))
 end
 
 macro inline()   Expr(:meta, :inline)   end
diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index a384c120ac7ac..36303a8379515 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -501,7 +501,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
@@ -903,7 +903,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
@@ -2819,9 +2827,8 @@ 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 :
-               effects.noub,
-        nonoverlayed = override.nonoverlayed ? true : effects.nonoverlayed)
+               (override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE) ? NOUB_IF_NOINBOUNDS :
+               effects.noub)
 end
 
 isdefined_globalref(g::GlobalRef) = !iszero(ccall(:jl_globalref_boundp, Cint, (Any,), g))
diff --git a/base/compiler/compiler.jl b/base/compiler/compiler.jl
index 45e8b2edd14b4..05ecdb0846039 100644
--- a/base/compiler/compiler.jl
+++ b/base/compiler/compiler.jl
@@ -48,7 +48,7 @@ struct EffectsOverride
     inaccessiblememonly::Bool
     noub::Bool
     noub_if_noinbounds::Bool
-    nonoverlayed::Bool
+    consistent_overlay::Bool
 end
 function EffectsOverride(
     override::EffectsOverride =
@@ -62,7 +62,7 @@ function EffectsOverride(
     inaccessiblememonly::Bool = override.inaccessiblememonly,
     noub::Bool = override.noub,
     noub_if_noinbounds::Bool = override.noub_if_noinbounds,
-    nonoverlayed::Bool = override.nonoverlayed)
+    consistent_overlay::Bool = override.consistent_overlay)
     return EffectsOverride(
         consistent,
         effect_free,
@@ -73,7 +73,7 @@ function EffectsOverride(
         inaccessiblememonly,
         noub,
         noub_if_noinbounds,
-        nonoverlayed)
+        consistent_overlay)
 end
 const NUM_EFFECTS_OVERRIDES = 10 # sync with julia.h
 
diff --git a/base/compiler/effects.jl b/base/compiler/effects.jl
index 5bafd8a0bfad3..0375b8dba922c 100644
--- a/base/compiler/effects.jl
+++ b/base/compiler/effects.jl
@@ -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
@@ -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
@@ -105,7 +112,7 @@ struct Effects
     notaskstate::Bool
     inaccessiblememonly::UInt8
     noub::UInt8
-    nonoverlayed::Bool
+    nonoverlayed::UInt8
     function Effects(
         consistent::UInt8,
         effect_free::UInt8,
@@ -114,7 +121,7 @@ struct Effects
         notaskstate::Bool,
         inaccessiblememonly::UInt8,
         noub::UInt8,
-        nonoverlayed::Bool)
+        nonoverlayed::UInt8)
         return new(
             consistent,
             effect_free,
@@ -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,
@@ -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,
@@ -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
@@ -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) =
@@ -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)  |
@@ -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)
@@ -329,7 +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.nonoverlayed        && (e |= (0x0001 << 9))
+    eo.consistent_overlay  && (e |= (0x0001 << 9))
     return e
 end
 
diff --git a/base/compiler/inferencestate.jl b/base/compiler/inferencestate.jl
index a7f5302866e5c..a9a3b0ade8f12 100644
--- a/base/compiler/inferencestate.jl
+++ b/base/compiler/inferencestate.jl
@@ -336,7 +336,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)
diff --git a/base/compiler/ssair/show.jl b/base/compiler/ssair/show.jl
index 7f2854959ce5e..82ca6e364f2fa 100644
--- a/base/compiler/ssair/show.jl
+++ b/base/compiler/ssair/show.jl
@@ -1048,8 +1048,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
diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl
index 8f2441a47cbaa..804989d0c5295 100644
--- a/base/compiler/typeinfer.jl
+++ b/base/compiler/typeinfer.jl
@@ -502,8 +502,8 @@ 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, :nonoverlayed)
-        ipo_effects = Effects(ipo_effects; nonoverlayed=true)
+    if is_effect_overridden(override, :consistent_overlay)
+        ipo_effects = Effects(ipo_effects; nonoverlayed=CONSISTENT_OVERLAY)
     end
     return ipo_effects
 end
diff --git a/base/essentials.jl b/base/essentials.jl
index 08b4ce12898c6..00801a6a50194 100644
--- a/base/essentials.jl
+++ b/base/essentials.jl
@@ -202,7 +202,7 @@ macro _total_meta()
         #=:inaccessiblememonly=#true,
         #=:noub=#true,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#false))
+        #=:consistent_overlay=#false))
 end
 # can be used in place of `@assume_effects :foldable` (supposed to be used for bootstrapping)
 macro _foldable_meta()
@@ -216,7 +216,7 @@ macro _foldable_meta()
         #=:inaccessiblememonly=#true,
         #=:noub=#true,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -230,7 +230,7 @@ macro _terminates_locally_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -244,7 +244,7 @@ macro _terminates_globally_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -258,7 +258,7 @@ macro _terminates_globally_notaskstate_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -272,7 +272,7 @@ macro _terminates_globally_noub_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#true,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -286,7 +286,7 @@ macro _effect_free_terminates_locally_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -300,7 +300,7 @@ macro _nothrow_noub_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#true,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#false))
+        #=:consistent_overlay=#false))
 end
 # can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
 macro _nothrow_meta()
@@ -314,7 +314,7 @@ macro _nothrow_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#false))
+        #=:consistent_overlay=#false))
 end
 # can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
 macro _noub_meta()
@@ -328,7 +328,7 @@ macro _noub_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#true,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#false))
+        #=:consistent_overlay=#false))
 end
 # can be used in place of `@assume_effects :notaskstate` (supposed to be used for bootstrapping)
 macro _notaskstate_meta()
@@ -342,7 +342,7 @@ macro _notaskstate_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#false,
-        #=:nonoverlayed=#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()
@@ -356,7 +356,7 @@ macro _noub_if_noinbounds_meta()
         #=:inaccessiblememonly=#false,
         #=:noub=#false,
         #=:noub_if_noinbounds=#true,
-        #=:nonoverlayed=#false))
+        #=:consistent_overlay=#false))
 end
 
 # another version of inlining that propagates an inbounds context
diff --git a/base/expr.jl b/base/expr.jl
index cd66e5150b951..9173bf6f6e156 100644
--- a/base/expr.jl
+++ b/base/expr.jl
@@ -505,7 +505,7 @@ The following `setting`s are supported.
 - `:inaccessiblememonly`
 - `:noub`
 - `:noub_if_noinbounds`
-- `:nonoverlayed`
+- `:consistent_overlay`
 - `:foldable`
 - `:removable`
 - `:total`
@@ -526,7 +526,7 @@ The `:consistent` setting asserts that for egal (`===`) inputs:
 
 !!! note
     The `:consistent`-cy assertion is made world-age wise. More formally, write
-    ``fᵢ`` for the evaluation of ``f`` in world-age ``i``, then we require:
+    ``fᵢ`` for the evaluation of ``f`` in world-age ``i``, then this setting requires:
     ```math
     ∀ i, x, y: x ≡ y → fᵢ(x) ≡ fᵢ(y)
     ```
@@ -675,8 +675,27 @@ any other effect assertions (such as `:consistent` or `:effect_free`) as well, b
 not model this, and they assume the absence of undefined behavior.
 
 ---
-## `:nonoverlayed`
-TODO.
+## `:consistent_overlay`
+
+The `:consistent_overlay` setting asserts that any overlayed methods potentially called by
+the method are `:consistent` with their original, non-overlayed counterparts. For the exact
+definition of `:consistent`, refer to the earlier explanation.
+
+More formally, when evaluating a generic function call ``f(x)`` at a specific world-age ``i``,
+and the regular method call ``fᵢ(x)`` is redirected to an overlay method ``fᵢ′(x)``, this
+setting requires that ``fᵢ(x) ≡ fᵢ′(x)``.
+
+!!! note
+    Note that the requirements for `:consistent`-cy include not only that the return values
+    are egal, but also that the manner of termination is the same.
+    However, it's important to aware that when they throw exceptions, the exceptions
+    themselves don't necessarily have to be egal as explained in the note of `:consistent`.
+    In other words, if ``fᵢ(x)`` throws an exception, this settings requires ``fᵢ′(x)`` to
+    also raise one, but the exact exceptions may differ.
+
+!!! note
+    This setting isn't supported at the callsite; it has to be applied at the definition
+    site. Also, given its nature, it's expected to be used together with `Base.Experimental.@overlay`.
 
 ---
 ## `:foldable`
@@ -754,6 +773,8 @@ macro assume_effects(args...)
         return Expr(:meta, form_purity_expr(override′))
     else
         # call site annotation case
+        override.consistent_overlay &&
+            throw(ArgumentError("Callsite `@assume_effects :consistent_overlay` is not supported"))
         return Expr(:block,
                     form_purity_expr(override),
                     Expr(:local, Expr(:(=), :val, esc(lastex))),
@@ -767,7 +788,7 @@ function compute_assumed_settings(settings)
     for setting in settings
         override = compute_assumed_setting(override, setting)
         override === nothing &&
-            throw(ArgumentError("@assume_effects $setting not supported"))
+            throw(ArgumentError("`@assume_effects $setting` not supported"))
     end
     return override
 end
@@ -798,8 +819,8 @@ function compute_assumed_setting(override::EffectsOverride, @nospecialize(settin
         return EffectsOverride(override; noub = val)
     elseif setting === :noub_if_noinbounds
         return EffectsOverride(override; noub_if_noinbounds = val)
-    elseif setting === :nonoverlayed
-        return EffectsOverride(override; nonoverlayed = val)
+    elseif setting === :consistent_overlay
+        return EffectsOverride(override; consistent_overlay = val)
     elseif setting === :foldable
         consistent = effect_free = terminates_globally = noub = val
         return EffectsOverride(override; consistent, effect_free, terminates_globally, noub)
diff --git a/src/julia.h b/src/julia.h
index 886421a738719..5380128d06202 100644
--- a/src/julia.h
+++ b/src/julia.h
@@ -279,7 +279,7 @@ typedef union __jl_purity_overrides_t {
         uint16_t ipo_inaccessiblememonly : 1;
         uint16_t ipo_noub                : 1;
         uint16_t ipo_noub_if_noinbounds  : 1;
-        uint16_t ipo_nonoverlayed        : 1;
+        uint16_t ipo_consistent_overlay  : 1;
     } overrides;
     uint16_t bits;
 } _jl_purity_overrides_t;
@@ -460,13 +460,14 @@ typedef struct _jl_code_instance_t {
     // see also encode_effects() and decode_effects() in `base/compiler/effects.jl`,
     _Atomic(uint32_t) ipo_purity_bits;
     // purity_flags:
-    //     uint8_t consistent          : 2;
+    //     uint8_t consistent          : 3;
     //     uint8_t effect_free         : 2;
-    //     uint8_t nothrow             : 2;
-    //     uint8_t terminates          : 2;
-    //     uint8_t nonoverlayed        : 1;
-    //     uint8_t notaskstate         : 2;
+    //     uint8_t nothrow             : 1;
+    //     uint8_t terminates          : 1;
+    //     uint8_t notaskstate         : 1;
     //     uint8_t inaccessiblememonly : 2;
+    //     uint8_t noub                : 2;
+    //     uint8_t nonoverlayed        : 2;
     jl_value_t *analysis_results; // Analysis results about this code (IPO-safe)
 
     // compilation state cache
diff --git a/src/method.c b/src/method.c
index 3f54b57c3c3fb..3dd3f15bbb745 100644
--- a/src/method.c
+++ b/src/method.c
@@ -479,7 +479,7 @@ jl_code_info_t *jl_new_code_info_from_ir(jl_expr_t *ir)
                         li->purity.overrides.ipo_inaccessiblememonly = jl_unbox_bool(jl_exprarg(ma, 6));
                         li->purity.overrides.ipo_noub = jl_unbox_bool(jl_exprarg(ma, 7));
                         li->purity.overrides.ipo_noub_if_noinbounds = jl_unbox_bool(jl_exprarg(ma, 8));
-                        li->purity.overrides.ipo_nonoverlayed = jl_unbox_bool(jl_exprarg(ma, 9));
+                        li->purity.overrides.ipo_consistent_overlay = jl_unbox_bool(jl_exprarg(ma, 9));
                     }
                 }
                 else
diff --git a/test/compiler/AbstractInterpreter.jl b/test/compiler/AbstractInterpreter.jl
index 3978050616a3e..2ed5e254003fc 100644
--- a/test/compiler/AbstractInterpreter.jl
+++ b/test/compiler/AbstractInterpreter.jl
@@ -135,25 +135,28 @@ Base.@assume_effects :total totalcall(f, args...) = f(args...)
 end |> only === Nothing
 
 # override `:native_executable` to allow concrete-eval for overlay-ed methods
-Base.@assume_effects :foldable function gpucompiler384(x::Int)
-    1 < x < 20 || error("x is too big")
-    return factorial(x)
-end
-@overlay OVERLAY_MT Base.@assume_effects :foldable :nonoverlayed function gpucompiler384(x::Int)
-    1 < x < 20 || raise_on_gpu("x is too big")
-    return factorial(x)
+function myfactorial(x::Int, raise)
+    res = 1
+    0 ≤ x < 20 || raise("x is too big")
+    Base.@assume_effects :terminates_locally while x > 1
+        res *= x
+        x -= 1
+    end
+    return res
 end
-@noinline raise_on_gpu(x) = #=do something with GPU=# error(x)
-call_gpucompiler384(x) = gpucompiler384(x)
-
-@test Base.infer_effects(gpucompiler384, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_nonoverlayed
-@test Base.infer_effects(call_gpucompiler384, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_nonoverlayed
-
-@test Base.infer_return_type(; interp=MTOverlayInterp()) do
-    Val(gpucompiler384(3))
-end == Val{6}
+raise_on_gpu1(x) = error(x)
+@overlay OVERLAY_MT @noinline raise_on_gpu1(x) = #=do something with GPU=# error(x)
+raise_on_gpu2(x) = error(x)
+@overlay OVERLAY_MT @noinline Base.@assume_effects :consistent_overlay raise_on_gpu2(x) = #=do something with GPU=# error(x)
+cpu_factorial(x::Int) = myfactorial(x, error)
+gpu_factorial1(x::Int) = myfactorial(x, raise_on_gpu1)
+gpu_factorial2(x::Int) = myfactorial(x, raise_on_gpu2)
+
+@test Base.infer_effects(cpu_factorial, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_nonoverlayed
+@test Base.infer_effects(gpu_factorial1, (Int,); interp=MTOverlayInterp()) |> !Core.Compiler.is_nonoverlayed
+@test Base.infer_effects(gpu_factorial2, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_consistent_overlay
 @test Base.infer_return_type(; interp=MTOverlayInterp()) do
-    Val(call_gpucompiler384(3))
+    Val(gpu_factorial2(3))
 end == Val{6}
 
 # GPUCompiler needs accurate inference through kwfunc with the overlay of `Core.throw_inexacterror`
diff --git a/test/namedtuple.jl b/test/namedtuple.jl
index 2c9c1ef3cff53..0487f96496309 100644
--- a/test/namedtuple.jl
+++ b/test/namedtuple.jl
@@ -398,14 +398,14 @@ for f in (Base.merge, Base.structdiff)
         fallback_func(a::NamedTuple, b::NamedTuple) = @invoke f(a::NamedTuple, b::NamedTuple)
         @testset let eff = Base.infer_effects(fallback_func)
             @test Core.Compiler.is_foldable(eff)
-            @test eff.nonoverlayed
+            @test Core.Compiler.is_nonoverlayed(eff)
         end
         @test only(Base.return_types(fallback_func)) == NamedTuple
         # test if `max_methods = 4` setting works as expected
         general_func(a::NamedTuple, b::NamedTuple) = f(a, b)
         @testset let eff = Base.infer_effects(general_func)
             @test Core.Compiler.is_foldable(eff)
-            @test eff.nonoverlayed
+            @test Core.Compiler.is_nonoverlayed(eff)
         end
         @test only(Base.return_types(general_func)) == NamedTuple
     end

From 0ecb74777ff941e5ad6970e23e43c1239b5ea80c Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Wed, 8 May 2024 21:19:08 +0900
Subject: [PATCH 3/5] implement new macro `@consistent_overlay` instead of
 `@assume_effects`

---
 base/experimental.jl                 | 90 ++++++++++++++++++++++++++--
 base/expr.jl                         | 30 +---------
 src/method.c                         | 31 ++++++----
 test/compiler/AbstractInterpreter.jl | 16 ++++-
 4 files changed, 121 insertions(+), 46 deletions(-)

diff --git a/base/experimental.jl b/base/experimental.jl
index 8dbdcacd65376..a2228267a6a6b 100644
--- a/base/experimental.jl
+++ b/base/experimental.jl
@@ -318,7 +318,7 @@ function show_error_hints(io, ex, args...)
     isnothing(hinters) && return
     for handler in hinters
         try
-            Base.invokelatest(handler, io, ex, args...)
+            @invokelatest handler(io, ex, args...)
         catch err
             tn = typeof(handler).name
             @error "Hint-handler $handler for $(typeof(ex)) in $(tn.module) caused an error"
@@ -330,17 +330,97 @@ end
 include("opaque_closure.jl")
 
 """
-    Experimental.@overlay mt [function def]
+    Base.Experimental.@overlay mt [function def]
 
 Define a method and add it to the method table `mt` instead of to the global method table.
 This can be used to implement a method override mechanism. Regular compilation will not
 consider these methods, and you should customize the compilation flow to look in these
 method tables (e.g., using [`Core.Compiler.OverlayMethodTable`](@ref)).
+
+!!! note
+    Please be aware that when defining overlay methods using `@overlay`, it is not necessary
+    to have an original method that corresponds exactly in terms of how the method dispatches.
+    This means that the method overlay mechanism enabled by `@overlay` is not implemented by
+    replacing the methods themselves, but through an additional and prioritized method
+    lookup during the method dispatch.
+
+    Considering this, it is important to understand that in compilations using an overlay
+    method table like the following, the method dispatched by `callx(x)` is not the regular
+    method `callx(::Float64)`, but the overlay method `callx(x::Real)`:
+    ```julia
+    callx(::Real) = :real
+    @overlay SOME_OVERLAY_MT callx(::Real) = :overlay_real
+    callx(::Float64) = :float64
+
+    # some overlay callsite
+    let x::Float64
+        callx(x) #> :overlay_real
+    end
+    ```
 """
 macro overlay(mt, def)
-    def = macroexpand(__module__, def) # to expand @inline, @generated, etc
-    is_function_def(def) || error("@overlay requires a function definition")
-    return esc(overlay_def!(mt, def))
+    inner = Base.unwrap_macrocalls(def)
+    is_function_def(inner) || error("@overlay requires a function definition")
+    overlay_def!(mt, inner)
+    return esc(def)
+end
+
+"""
+    Base.Experimental.@consistent_overlay mt [function def]
+
+This macro operates almost identically to [`Base.Experimental.@overlay`](@ref), defining a
+new overlay method. The key difference with this macro is that it informs the compiler that
+the invocation of the overlay method it defines is `:consistent` with a regular,
+non-overlayed method call.
+
+More formally, when evaluating a generic function call ``f(x)`` at a specific world age
+``i``, if a regular method call ``fᵢ(x)`` is redirected to an overlay method call ``fᵢ′(x)``
+defined by this macro, it must be ensured that ``fᵢ(x) ≡ fᵢ′(x)``.
+
+For a detailed definition of `:consistent`-cy, consult the corresponding section in
+[`Base.@assume_effects`](@ref).
+
+!!! note
+    Note that the requirements for `:consistent`-cy include not only that the return values
+    are egal, but also that the manner of termination is the same.
+    However, it's important to aware that when they throw exceptions, the exceptions
+    themselves don't necessarily have to be egal as explained in the note of `:consistent`.
+    In other words, if ``fᵢ(x)`` throws an exception, ``fᵢ′(x)`` is required to also throw
+    one, but the exact exceptions may differ.
+
+!!! note
+    Please note that the `:consistent`-cy requirement applies not to method itself but to
+    _method invocation_. This means that for the use of `@consistent_overlay`, it is
+    necessary for method invocations with the native regular compilation and those with
+    a compilation with overlay method table to be `:consistent`.
+
+    For example, it is important to understand that, `@consistent_overlay` can be used like
+    the following:
+    ```julia
+    callsin(x::Real) = x < 0 ? error(x) : sin(x)
+    @consistent_overlay SOME_OVERLAY_MT callsin(x::Float64) =
+        x < 0 ? error_somehow(x) : sin(x)
+    ```
+    However, be aware that this `@consistent_overlay` will immediately become invalid if a
+    new method for `callsin` is defined subsequently, such as:
+    ```julia
+    callsin(x::Float64) = cos(x)
+    ```
+
+    This specifically implies that the use of `@consistent_overlay` should be restricted as
+    much as possible to cases where a regular method with a concrete signature is replaced
+    by an overlay method with the same concrete signature.
+
+    This constraint is closely related to the note in [`Base.Experimental.@overlay`](@ref);
+    you are advised to consult that as well.
+"""
+macro consistent_overlay(mt, def)
+    inner = Base.unwrap_macrocalls(def)
+    is_function_def(inner) || error("@consistent_overlay requires a function definition")
+    overlay_def!(mt, inner)
+    override = Core.Compiler.EffectsOverride(; consistent_overlay=true)
+    Base.pushmeta!(def::Expr, Base.form_purity_expr(override))
+    return esc(def)
 end
 
 function overlay_def!(mt, @nospecialize ex)
diff --git a/base/expr.jl b/base/expr.jl
index 9173bf6f6e156..b92332c7bbfd8 100644
--- a/base/expr.jl
+++ b/base/expr.jl
@@ -505,7 +505,6 @@ The following `setting`s are supported.
 - `:inaccessiblememonly`
 - `:noub`
 - `:noub_if_noinbounds`
-- `:consistent_overlay`
 - `:foldable`
 - `:removable`
 - `:total`
@@ -674,29 +673,6 @@ The `:noub` setting asserts that the method will not execute any undefined behav
 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.
 
----
-## `:consistent_overlay`
-
-The `:consistent_overlay` setting asserts that any overlayed methods potentially called by
-the method are `:consistent` with their original, non-overlayed counterparts. For the exact
-definition of `:consistent`, refer to the earlier explanation.
-
-More formally, when evaluating a generic function call ``f(x)`` at a specific world-age ``i``,
-and the regular method call ``fᵢ(x)`` is redirected to an overlay method ``fᵢ′(x)``, this
-setting requires that ``fᵢ(x) ≡ fᵢ′(x)``.
-
-!!! note
-    Note that the requirements for `:consistent`-cy include not only that the return values
-    are egal, but also that the manner of termination is the same.
-    However, it's important to aware that when they throw exceptions, the exceptions
-    themselves don't necessarily have to be egal as explained in the note of `:consistent`.
-    In other words, if ``fᵢ(x)`` throws an exception, this settings requires ``fᵢ′(x)`` to
-    also raise one, but the exact exceptions may differ.
-
-!!! note
-    This setting isn't supported at the callsite; it has to be applied at the definition
-    site. Also, given its nature, it's expected to be used together with `Base.Experimental.@overlay`.
-
 ---
 ## `:foldable`
 
@@ -761,7 +737,7 @@ macro assume_effects(args...)
     lastex = args[end]
     override = compute_assumed_settings(args[begin:end-1])
     if is_function_def(unwrap_macrocalls(lastex))
-        return esc(pushmeta!(lastex, form_purity_expr(override)))
+        return esc(pushmeta!(lastex::Expr, form_purity_expr(override)))
     elseif isexpr(lastex, :macrocall) && lastex.args[1] === Symbol("@ccall")
         lastex.args[1] = GlobalRef(Base, Symbol("@ccall_effects"))
         insert!(lastex.args, 3, Core.Compiler.encode_effects_override(override))
@@ -773,8 +749,6 @@ macro assume_effects(args...)
         return Expr(:meta, form_purity_expr(override′))
     else
         # call site annotation case
-        override.consistent_overlay &&
-            throw(ArgumentError("Callsite `@assume_effects :consistent_overlay` is not supported"))
         return Expr(:block,
                     form_purity_expr(override),
                     Expr(:local, Expr(:(=), :val, esc(lastex))),
@@ -819,8 +793,6 @@ function compute_assumed_setting(override::EffectsOverride, @nospecialize(settin
         return EffectsOverride(override; noub = val)
     elseif setting === :noub_if_noinbounds
         return EffectsOverride(override; noub_if_noinbounds = val)
-    elseif setting === :consistent_overlay
-        return EffectsOverride(override; consistent_overlay = val)
     elseif setting === :foldable
         consistent = effect_free = terminates_globally = noub = val
         return EffectsOverride(override; consistent, effect_free, terminates_globally, noub)
diff --git a/src/method.c b/src/method.c
index 3dd3f15bbb745..cb3d481cfc22c 100644
--- a/src/method.c
+++ b/src/method.c
@@ -470,16 +470,27 @@ jl_code_info_t *jl_new_code_info_from_ir(jl_expr_t *ir)
                     li->constprop = 2;
                 else if (jl_is_expr(ma) && ((jl_expr_t*)ma)->head == jl_purity_sym) {
                     if (jl_expr_nargs(ma) == NUM_EFFECTS_OVERRIDES) {
-                        li->purity.overrides.ipo_consistent = jl_unbox_bool(jl_exprarg(ma, 0));
-                        li->purity.overrides.ipo_effect_free = jl_unbox_bool(jl_exprarg(ma, 1));
-                        li->purity.overrides.ipo_nothrow = jl_unbox_bool(jl_exprarg(ma, 2));
-                        li->purity.overrides.ipo_terminates_globally = jl_unbox_bool(jl_exprarg(ma, 3));
-                        li->purity.overrides.ipo_terminates_locally = jl_unbox_bool(jl_exprarg(ma, 4));
-                        li->purity.overrides.ipo_notaskstate = jl_unbox_bool(jl_exprarg(ma, 5));
-                        li->purity.overrides.ipo_inaccessiblememonly = jl_unbox_bool(jl_exprarg(ma, 6));
-                        li->purity.overrides.ipo_noub = jl_unbox_bool(jl_exprarg(ma, 7));
-                        li->purity.overrides.ipo_noub_if_noinbounds = jl_unbox_bool(jl_exprarg(ma, 8));
-                        li->purity.overrides.ipo_consistent_overlay = jl_unbox_bool(jl_exprarg(ma, 9));
+                        // N.B. this code allows multiple :purity expressions to be present in a single `:meta` node
+                        int8_t consistent = jl_unbox_bool(jl_exprarg(ma, 0));
+                        if (consistent) li->purity.overrides.ipo_consistent = consistent;
+                        int8_t effect_free = jl_unbox_bool(jl_exprarg(ma, 1));
+                        if (effect_free) li->purity.overrides.ipo_effect_free = effect_free;
+                        int8_t nothrow = jl_unbox_bool(jl_exprarg(ma, 2));
+                        if (nothrow) li->purity.overrides.ipo_nothrow = nothrow;
+                        int8_t terminates_globally = jl_unbox_bool(jl_exprarg(ma, 3));
+                        if (terminates_globally) li->purity.overrides.ipo_terminates_globally = terminates_globally;
+                        int8_t terminates_locally = jl_unbox_bool(jl_exprarg(ma, 4));
+                        if (terminates_locally) li->purity.overrides.ipo_terminates_locally = terminates_locally;
+                        int8_t notaskstate = jl_unbox_bool(jl_exprarg(ma, 5));
+                        if (notaskstate) li->purity.overrides.ipo_notaskstate = notaskstate;
+                        int8_t inaccessiblememonly = jl_unbox_bool(jl_exprarg(ma, 6));
+                        if (inaccessiblememonly) li->purity.overrides.ipo_inaccessiblememonly = inaccessiblememonly;
+                        int8_t noub = jl_unbox_bool(jl_exprarg(ma, 7));
+                        if (noub) li->purity.overrides.ipo_noub = noub;
+                        int8_t noub_if_noinbounds = jl_unbox_bool(jl_exprarg(ma, 8));
+                        if (noub_if_noinbounds) li->purity.overrides.ipo_noub_if_noinbounds = noub_if_noinbounds;
+                        int8_t consistent_overlay = jl_unbox_bool(jl_exprarg(ma, 9));
+                        if (consistent_overlay) li->purity.overrides.ipo_consistent_overlay = consistent_overlay;
                     }
                 }
                 else
diff --git a/test/compiler/AbstractInterpreter.jl b/test/compiler/AbstractInterpreter.jl
index 2ed5e254003fc..d816c3aa4647b 100644
--- a/test/compiler/AbstractInterpreter.jl
+++ b/test/compiler/AbstractInterpreter.jl
@@ -21,7 +21,7 @@ CC.transform_result_for_cache(::AbsIntOnlyInterp2, ::Core.MethodInstance, ::CC.W
 # OverlayMethodTable
 # ==================
 
-using Base.Experimental: @MethodTable, @overlay
+using Base.Experimental: @MethodTable, @overlay, @consistent_overlay
 
 # @overlay method with return type annotation
 @MethodTable RT_METHOD_DEF
@@ -147,17 +147,29 @@ end
 raise_on_gpu1(x) = error(x)
 @overlay OVERLAY_MT @noinline raise_on_gpu1(x) = #=do something with GPU=# error(x)
 raise_on_gpu2(x) = error(x)
-@overlay OVERLAY_MT @noinline Base.@assume_effects :consistent_overlay raise_on_gpu2(x) = #=do something with GPU=# error(x)
+@consistent_overlay OVERLAY_MT @noinline raise_on_gpu2(x) = #=do something with GPU=# error(x)
+raise_on_gpu3(x) = error(x)
+@consistent_overlay OVERLAY_MT @noinline Base.@assume_effects :foldable raise_on_gpu3(x) = #=do something with GPU=# error_on_gpu(x)
 cpu_factorial(x::Int) = myfactorial(x, error)
 gpu_factorial1(x::Int) = myfactorial(x, raise_on_gpu1)
 gpu_factorial2(x::Int) = myfactorial(x, raise_on_gpu2)
+gpu_factorial3(x::Int) = myfactorial(x, raise_on_gpu3)
 
 @test Base.infer_effects(cpu_factorial, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_nonoverlayed
 @test Base.infer_effects(gpu_factorial1, (Int,); interp=MTOverlayInterp()) |> !Core.Compiler.is_nonoverlayed
 @test Base.infer_effects(gpu_factorial2, (Int,); interp=MTOverlayInterp()) |> Core.Compiler.is_consistent_overlay
+let effects = Base.infer_effects(gpu_factorial3, (Int,); interp=MTOverlayInterp())
+    # check if `@consistent_overlay` together works with `@assume_effects`
+    # N.B. the overlaid `raise_on_gpu3` is not :foldable otherwise since `error_on_gpu` is (intetionally) undefined.
+    @test Core.Compiler.is_consistent_overlay(effects)
+    @test Core.Compiler.is_foldable(effects)
+end
 @test Base.infer_return_type(; interp=MTOverlayInterp()) do
     Val(gpu_factorial2(3))
 end == Val{6}
+@test Base.infer_return_type(; interp=MTOverlayInterp()) do
+    Val(gpu_factorial3(3))
+end == Val{6}
 
 # GPUCompiler needs accurate inference through kwfunc with the overlay of `Core.throw_inexacterror`
 # https://github.com/JuliaLang/julia/issues/48097

From 3f6d21c21936961309f3bb4013aae804f6ff82ca Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Tue, 18 Jun 2024 16:14:56 +0900
Subject: [PATCH 4/5] add test cases from JuliaGPU/CUDA.jl#2241

---
 test/compiler/AbstractInterpreter.jl | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/test/compiler/AbstractInterpreter.jl b/test/compiler/AbstractInterpreter.jl
index d816c3aa4647b..0d475a8259000 100644
--- a/test/compiler/AbstractInterpreter.jl
+++ b/test/compiler/AbstractInterpreter.jl
@@ -201,6 +201,23 @@ inner52938(x, types::Type, args...; kwargs...) = x
 outer52938(x) = @inline inner52938(x, Tuple{}; foo=Ref(42), bar=1)
 @test fully_eliminated(outer52938, (Any,); interp=Issue52938Interp(), retval=Argument(2))
 
+# https://github.com/JuliaGPU/CUDA.jl/issues/2241
+@newinterp Cuda2241Interp
+@MethodTable CUDA_2241_MT
+CC.method_table(interp::Cuda2241Interp) = CC.OverlayMethodTable(CC.get_inference_world(interp), CUDA_2241_MT)
+inner2241(f, types::Type, args...; kwargs...) = nothing
+function outer2241(f)
+    @inline inner2241(f, Tuple{}; foo=Ref(42), bar=1)
+    return nothing
+end
+# NOTE CUDA.jl overlays `throw_boundserror` in a way that causes effects, but these effects
+#      are ignored for this call graph at the `@assume_effects` annotation on `typejoin`.
+#      Here it's important to use `@consistent_overlay` to avoid tainting the `:nonoverlayed` bit.
+const cuda_kernel_state = Ref{Any}()
+@consistent_overlay CUDA_2241_MT @inline Base.throw_boundserror(A, I) =
+    (cuda_kernel_state[] = (A, I); error())
+@test fully_eliminated(outer2241, (Nothing,); interp=Cuda2241Interp(), retval=nothing)
+
 # Should not concrete-eval overlayed methods in semi-concrete interpretation
 @newinterp OverlaySinInterp
 @MethodTable OVERLAY_SIN_MT

From b1e031e6b13734fc3cb0072cd21bda3e4d9e5eec Mon Sep 17 00:00:00 2001
From: Shuhei Kadowaki <aviatesk@gmail.com>
Date: Tue, 18 Jun 2024 17:09:44 +0900
Subject: [PATCH 5/5] refine the docstring a bit

---
 base/experimental.jl | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

diff --git a/base/experimental.jl b/base/experimental.jl
index a2228267a6a6b..58c7258120f3f 100644
--- a/base/experimental.jl
+++ b/base/experimental.jl
@@ -330,7 +330,7 @@ end
 include("opaque_closure.jl")
 
 """
-    Base.Experimental.@overlay mt [function def]
+    Base.Experimental.@overlay mt def
 
 Define a method and add it to the method table `mt` instead of to the global method table.
 This can be used to implement a method override mechanism. Regular compilation will not
@@ -366,7 +366,7 @@ macro overlay(mt, def)
 end
 
 """
-    Base.Experimental.@consistent_overlay mt [function def]
+    Base.Experimental.@consistent_overlay mt def
 
 This macro operates almost identically to [`Base.Experimental.@overlay`](@ref), defining a
 new overlay method. The key difference with this macro is that it informs the compiler that
@@ -375,18 +375,20 @@ non-overlayed method call.
 
 More formally, when evaluating a generic function call ``f(x)`` at a specific world age
 ``i``, if a regular method call ``fᵢ(x)`` is redirected to an overlay method call ``fᵢ′(x)``
-defined by this macro, it must be ensured that ``fᵢ(x) ≡ fᵢ′(x)``.
+defined by this macro, ``fᵢ(x)`` and ``fᵢ′(x)`` are considered `:consistent` if the following
+conditions are met:
+- If ``fᵢ(x)`` returns a value ``y``, then ``fᵢ′(x)`` also returns some value ``yᵢ``, and ``y ≡ yᵢ`` holds.
+- If ``fᵢ(x)`` throws an exception, then ``fᵢ′(x)`` also throws some exception.
 
 For a detailed definition of `:consistent`-cy, consult the corresponding section in
 [`Base.@assume_effects`](@ref).
 
 !!! note
     Note that the requirements for `:consistent`-cy include not only that the return values
-    are egal, but also that the manner of termination is the same.
-    However, it's important to aware that when they throw exceptions, the exceptions
-    themselves don't necessarily have to be egal as explained in the note of `:consistent`.
-    In other words, if ``fᵢ(x)`` throws an exception, ``fᵢ′(x)`` is required to also throw
-    one, but the exact exceptions may differ.
+    are egal, but also that the manner of termination is the same. However, it's important
+    to aware that when they throw exceptions, the exceptions themselves don't necessarily
+    have to be egal. In other words, if ``fᵢ(x)`` throws an exception, ``fᵢ′(x)`` is
+    required to also throw one, but the exact exceptions may differ.
 
 !!! note
     Please note that the `:consistent`-cy requirement applies not to method itself but to
@@ -447,11 +449,11 @@ let new_mt(name::Symbol, mod::Module) = begin
 end
 
 """
-    Experimental.@MethodTable(name)
+    Base.Experimental.@MethodTable name
 
 Create a new MethodTable in the current module, bound to `name`. This method table can be
-used with the [`Experimental.@overlay`](@ref) macro to define methods for a function without
-adding them to the global method table.
+used with the [`Base.Experimental.@overlay`](@ref) macro to define methods for a function
+without adding them to the global method table.
 """
 :@MethodTable