Skip to content

Commit c5994e4

Browse files
authored
effects: add new @consistent_overlay macro (#54322)
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`.
1 parent ded0b28 commit c5994e4

File tree

14 files changed

+290
-91
lines changed

14 files changed

+290
-91
lines changed

base/boot.jl

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -283,7 +283,8 @@ macro _foldable_meta()
283283
#=:notaskstate=#true,
284284
#=:inaccessiblememonly=#true,
285285
#=:noub=#true,
286-
#=:noub_if_noinbounds=#false))
286+
#=:noub_if_noinbounds=#false,
287+
#=:consistent_overlay=#false))
287288
end
288289

289290
macro inline() Expr(:meta, :inline) end

base/compiler/abstractinterpretation.jl

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -501,7 +501,7 @@ function add_call_backedges!(interp::AbstractInterpreter, @nospecialize(rettype)
501501
# ignore the `:nonoverlayed` property if `interp` doesn't use overlayed method table
502502
# since it will never be tainted anyway
503503
if !isoverlayed(method_table(interp))
504-
all_effects = Effects(all_effects; nonoverlayed=false)
504+
all_effects = Effects(all_effects; nonoverlayed=ALWAYS_FALSE)
505505
end
506506
all_effects === Effects() && return nothing
507507
end
@@ -903,7 +903,15 @@ function concrete_eval_eligible(interp::AbstractInterpreter,
903903
mi = result.edge
904904
if mi !== nothing && is_foldable(effects)
905905
if f !== nothing && is_all_const_arg(arginfo, #=start=#2)
906-
if is_nonoverlayed(interp) || is_nonoverlayed(effects)
906+
if (is_nonoverlayed(interp) || is_nonoverlayed(effects) ||
907+
# Even if overlay methods are involved, when `:consistent_overlay` is
908+
# explicitly applied, we can still perform concrete evaluation using the
909+
# original methods for executing them.
910+
# While there's a chance that the non-overlayed counterparts may raise
911+
# non-egal exceptions, it will not impact the compilation validity, since:
912+
# - the results of the concrete evaluation will not be inlined
913+
# - the exception types from the concrete evaluation will not be propagated
914+
is_consistent_overlay(effects))
907915
return :concrete_eval
908916
end
909917
# disable concrete-evaluation if this function call is tainted by some overlayed
@@ -2819,7 +2827,7 @@ function override_effects(effects::Effects, override::EffectsOverride)
28192827
notaskstate = override.notaskstate ? true : effects.notaskstate,
28202828
inaccessiblememonly = override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
28212829
noub = override.noub ? ALWAYS_TRUE :
2822-
override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE ? NOUB_IF_NOINBOUNDS :
2830+
(override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE) ? NOUB_IF_NOINBOUNDS :
28232831
effects.noub)
28242832
end
28252833

base/compiler/compiler.jl

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -48,10 +48,11 @@ struct EffectsOverride
4848
inaccessiblememonly::Bool
4949
noub::Bool
5050
noub_if_noinbounds::Bool
51+
consistent_overlay::Bool
5152
end
5253
function EffectsOverride(
5354
override::EffectsOverride =
54-
EffectsOverride(false, false, false, false, false, false, false, false, false);
55+
EffectsOverride(false, false, false, false, false, false, false, false, false, false);
5556
consistent::Bool = override.consistent,
5657
effect_free::Bool = override.effect_free,
5758
nothrow::Bool = override.nothrow,
@@ -60,7 +61,8 @@ function EffectsOverride(
6061
notaskstate::Bool = override.notaskstate,
6162
inaccessiblememonly::Bool = override.inaccessiblememonly,
6263
noub::Bool = override.noub,
63-
noub_if_noinbounds::Bool = override.noub_if_noinbounds)
64+
noub_if_noinbounds::Bool = override.noub_if_noinbounds,
65+
consistent_overlay::Bool = override.consistent_overlay)
6466
return EffectsOverride(
6567
consistent,
6668
effect_free,
@@ -70,9 +72,10 @@ function EffectsOverride(
7072
notaskstate,
7173
inaccessiblememonly,
7274
noub,
73-
noub_if_noinbounds)
75+
noub_if_noinbounds,
76+
consistent_overlay)
7477
end
75-
const NUM_EFFECTS_OVERRIDES = 9 # sync with julia.h
78+
const NUM_EFFECTS_OVERRIDES = 10 # sync with julia.h
7679

7780
# essential files and libraries
7881
include("essentials.jl")

base/compiler/effects.jl

Lines changed: 38 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -43,16 +43,21 @@ following meanings:
4343
except that it may access or modify mutable memory pointed to by its call arguments.
4444
This may later be refined to `ALWAYS_TRUE` in a case when call arguments are known to be immutable.
4545
This state corresponds to LLVM's `inaccessiblemem_or_argmemonly` function attribute.
46-
- `noub::UInt8`: indicates that the method will not execute any undefined behavior (for any input).
47-
Note that undefined behavior may technically cause the method to violate any other effect
48-
assertions (such as `:consistent` or `:effect_free`) as well, but we do not model this,
49-
and they assume the absence of undefined behavior.
50-
* `ALWAYS_TRUE`: this method is guaranteed to not execute any undefined behavior.
46+
- `noub::UInt8`:
47+
* `ALWAYS_TRUE`: this method is guaranteed to not execute any undefined behavior (for any input).
5148
* `ALWAYS_FALSE`: this method may execute undefined behavior.
5249
* `NOUB_IF_NOINBOUNDS`: this method is guaranteed to not execute any undefined behavior
5350
if the caller does not set nor propagate the `@inbounds` context.
54-
- `nonoverlayed::Bool`: indicates that any methods that may be called within this method
55-
are not defined in an [overlayed method table](@ref OverlayMethodTable).
51+
Note that undefined behavior may technically cause the method to violate any other effect
52+
assertions (such as `:consistent` or `:effect_free`) as well, but we do not model this,
53+
and they assume the absence of undefined behavior.
54+
- `nonoverlayed::UInt8`:
55+
* `ALWAYS_TRUE`: this method is guaranteed to not invoke any methods that defined in an
56+
[overlayed method table](@ref OverlayMethodTable).
57+
* `CONSISTENT_OVERLAY`: this method may invoke overlayed methods, but all such overlayed
58+
methods are `:consistent` with their non-overlayed original counterparts
59+
(see [`Base.@assume_effects`](@ref) for the exact definition of `:consistenct`-cy).
60+
* `ALWAYS_FALSE`: this method may invoke overlayed methods.
5661
5762
Note that the representations above are just internal implementation details and thus likely
5863
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
9499
- `+u` (green): `true`
95100
- `-u` (red): `false`
96101
- `?u` (yellow): `NOUB_IF_NOINBOUNDS`
97-
98-
Additionally, if the `nonoverlayed` property is false, a red prime symbol (′) is displayed after the tuple.
102+
8. `:nonoverlayed` (`o`):
103+
- `+o` (green): `ALWAYS_TRUE`
104+
- `-o` (red): `ALWAYS_FALSE`
105+
- `?o` (yellow): `CONSISTENT_OVERLAY`
99106
"""
100107
struct Effects
101108
consistent::UInt8
@@ -105,7 +112,7 @@ struct Effects
105112
notaskstate::Bool
106113
inaccessiblememonly::UInt8
107114
noub::UInt8
108-
nonoverlayed::Bool
115+
nonoverlayed::UInt8
109116
function Effects(
110117
consistent::UInt8,
111118
effect_free::UInt8,
@@ -114,7 +121,7 @@ struct Effects
114121
notaskstate::Bool,
115122
inaccessiblememonly::UInt8,
116123
noub::UInt8,
117-
nonoverlayed::Bool)
124+
nonoverlayed::UInt8)
118125
return new(
119126
consistent,
120127
effect_free,
@@ -150,10 +157,13 @@ const INACCESSIBLEMEM_OR_ARGMEMONLY = 0x01 << 1
150157
# :noub bits
151158
const NOUB_IF_NOINBOUNDS = 0x01 << 1
152159

153-
const EFFECTS_TOTAL = Effects(ALWAYS_TRUE, ALWAYS_TRUE, true, true, true, ALWAYS_TRUE, ALWAYS_TRUE, true)
154-
const EFFECTS_THROWS = Effects(ALWAYS_TRUE, ALWAYS_TRUE, false, true, true, ALWAYS_TRUE, ALWAYS_TRUE, true)
155-
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)
156-
const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, ALWAYS_FALSE, false) # unknown really
160+
# :nonoverlayed bits
161+
const CONSISTENT_OVERLAY = 0x01 << 1
162+
163+
const EFFECTS_TOTAL = Effects(ALWAYS_TRUE, ALWAYS_TRUE, true, true, true, ALWAYS_TRUE, ALWAYS_TRUE, ALWAYS_TRUE)
164+
const EFFECTS_THROWS = Effects(ALWAYS_TRUE, ALWAYS_TRUE, false, true, true, ALWAYS_TRUE, ALWAYS_TRUE, ALWAYS_TRUE)
165+
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)
166+
const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, ALWAYS_FALSE, ALWAYS_FALSE) # unknown really
157167

158168
function Effects(effects::Effects = _EFFECTS_UNKNOWN;
159169
consistent::UInt8 = effects.consistent,
@@ -163,7 +173,7 @@ function Effects(effects::Effects = _EFFECTS_UNKNOWN;
163173
notaskstate::Bool = effects.notaskstate,
164174
inaccessiblememonly::UInt8 = effects.inaccessiblememonly,
165175
noub::UInt8 = effects.noub,
166-
nonoverlayed::Bool = effects.nonoverlayed)
176+
nonoverlayed::UInt8 = effects.nonoverlayed)
167177
return Effects(
168178
consistent,
169179
effect_free,
@@ -229,8 +239,11 @@ function is_better_effects(new::Effects, old::Effects)
229239
elseif new.noub != old.noub
230240
return false
231241
end
232-
if new.nonoverlayed
233-
any_improved |= !old.nonoverlayed
242+
if new.nonoverlayed == ALWAYS_TRUE
243+
any_improved |= old.nonoverlayed != ALWAYS_TRUE
244+
elseif new.nonoverlayed == CONSISTENT_OVERLAY
245+
old.nonoverlayed == ALWAYS_TRUE && return false
246+
any_improved |= old.nonoverlayed != CONSISTENT_OVERLAY
234247
elseif new.nonoverlayed != old.nonoverlayed
235248
return false
236249
end
@@ -265,7 +278,7 @@ is_notaskstate(effects::Effects) = effects.notaskstate
265278
is_inaccessiblememonly(effects::Effects) = effects.inaccessiblememonly === ALWAYS_TRUE
266279
is_noub(effects::Effects) = effects.noub === ALWAYS_TRUE
267280
is_noub_if_noinbounds(effects::Effects) = effects.noub === NOUB_IF_NOINBOUNDS
268-
is_nonoverlayed(effects::Effects) = effects.nonoverlayed
281+
is_nonoverlayed(effects::Effects) = effects.nonoverlayed === ALWAYS_TRUE
269282

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

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

311+
is_consistent_overlay(effects::Effects) = effects.nonoverlayed === CONSISTENT_OVERLAY
312+
298313
function encode_effects(e::Effects)
299314
return ((e.consistent % UInt32) << 0) |
300315
((e.effect_free % UInt32) << 3) |
@@ -315,7 +330,7 @@ function decode_effects(e::UInt32)
315330
_Bool((e >> 7) & 0x01),
316331
UInt8((e >> 8) & 0x03),
317332
UInt8((e >> 10) & 0x03),
318-
_Bool((e >> 12) & 0x01))
333+
UInt8((e >> 12) & 0x03))
319334
end
320335

321336
function encode_effects_override(eo::EffectsOverride)
@@ -329,6 +344,7 @@ function encode_effects_override(eo::EffectsOverride)
329344
eo.inaccessiblememonly && (e |= (0x0001 << 6))
330345
eo.noub && (e |= (0x0001 << 7))
331346
eo.noub_if_noinbounds && (e |= (0x0001 << 8))
347+
eo.consistent_overlay && (e |= (0x0001 << 9))
332348
return e
333349
end
334350

@@ -342,7 +358,8 @@ function decode_effects_override(e::UInt16)
342358
!iszero(e & (0x0001 << 5)),
343359
!iszero(e & (0x0001 << 6)),
344360
!iszero(e & (0x0001 << 7)),
345-
!iszero(e & (0x0001 << 8)))
361+
!iszero(e & (0x0001 << 8)),
362+
!iszero(e & (0x0001 << 9)))
346363
end
347364

348365
decode_statement_effects_override(ssaflag::UInt32) =

base/compiler/inferencestate.jl

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -336,7 +336,10 @@ mutable struct InferenceState
336336
end
337337

338338
if def isa Method
339-
ipo_effects = Effects(ipo_effects; nonoverlayed=is_nonoverlayed(def))
339+
nonoverlayed = is_nonoverlayed(def) ? ALWAYS_TRUE :
340+
is_effect_overridden(def, :consistent_overlay) ? CONSISTENT_OVERLAY :
341+
ALWAYS_FALSE
342+
ipo_effects = Effects(ipo_effects; nonoverlayed)
340343
end
341344

342345
restrict_abstract_call_sites = isa(def, Module)

base/compiler/ssair/show.jl

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1048,8 +1048,9 @@ function Base.show(io::IO, e::Effects)
10481048
printstyled(io, effectbits_letter(e, :inaccessiblememonly, 'm'); color=effectbits_color(e, :inaccessiblememonly))
10491049
print(io, ',')
10501050
printstyled(io, effectbits_letter(e, :noub, 'u'); color=effectbits_color(e, :noub))
1051+
print(io, ',')
1052+
printstyled(io, effectbits_letter(e, :nonoverlayed, 'o'); color=effectbits_color(e, :nonoverlayed))
10511053
print(io, ')')
1052-
e.nonoverlayed || printstyled(io, ''; color=:red)
10531054
end
10541055

10551056
@specialize

base/compiler/typeinfer.jl

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -502,6 +502,9 @@ function adjust_effects(ipo_effects::Effects, def::Method)
502502
elseif is_effect_overridden(override, :noub_if_noinbounds) && ipo_effects.noub !== ALWAYS_TRUE
503503
ipo_effects = Effects(ipo_effects; noub=NOUB_IF_NOINBOUNDS)
504504
end
505+
if is_effect_overridden(override, :consistent_overlay)
506+
ipo_effects = Effects(ipo_effects; nonoverlayed=CONSISTENT_OVERLAY)
507+
end
505508
return ipo_effects
506509
end
507510

base/essentials.jl

Lines changed: 24 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -201,7 +201,8 @@ macro _total_meta()
201201
#=:notaskstate=#true,
202202
#=:inaccessiblememonly=#true,
203203
#=:noub=#true,
204-
#=:noub_if_noinbounds=#false))
204+
#=:noub_if_noinbounds=#false,
205+
#=:consistent_overlay=#false))
205206
end
206207
# can be used in place of `@assume_effects :foldable` (supposed to be used for bootstrapping)
207208
macro _foldable_meta()
@@ -214,7 +215,8 @@ macro _foldable_meta()
214215
#=:notaskstate=#true,
215216
#=:inaccessiblememonly=#true,
216217
#=:noub=#true,
217-
#=:noub_if_noinbounds=#false))
218+
#=:noub_if_noinbounds=#false,
219+
#=:consistent_overlay=#false))
218220
end
219221
# can be used in place of `@assume_effects :terminates_locally` (supposed to be used for bootstrapping)
220222
macro _terminates_locally_meta()
@@ -227,7 +229,8 @@ macro _terminates_locally_meta()
227229
#=:notaskstate=#false,
228230
#=:inaccessiblememonly=#false,
229231
#=:noub=#false,
230-
#=:noub_if_noinbounds=#false))
232+
#=:noub_if_noinbounds=#false,
233+
#=:consistent_overlay=#false))
231234
end
232235
# can be used in place of `@assume_effects :terminates_globally` (supposed to be used for bootstrapping)
233236
macro _terminates_globally_meta()
@@ -240,7 +243,8 @@ macro _terminates_globally_meta()
240243
#=:notaskstate=#false,
241244
#=:inaccessiblememonly=#false,
242245
#=:noub=#false,
243-
#=:noub_if_noinbounds=#false))
246+
#=:noub_if_noinbounds=#false,
247+
#=:consistent_overlay=#false))
244248
end
245249
# can be used in place of `@assume_effects :terminates_globally :notaskstate` (supposed to be used for bootstrapping)
246250
macro _terminates_globally_notaskstate_meta()
@@ -253,7 +257,8 @@ macro _terminates_globally_notaskstate_meta()
253257
#=:notaskstate=#true,
254258
#=:inaccessiblememonly=#false,
255259
#=:noub=#false,
256-
#=:noub_if_noinbounds=#false))
260+
#=:noub_if_noinbounds=#false,
261+
#=:consistent_overlay=#false))
257262
end
258263
# can be used in place of `@assume_effects :terminates_globally :noub` (supposed to be used for bootstrapping)
259264
macro _terminates_globally_noub_meta()
@@ -266,7 +271,8 @@ macro _terminates_globally_noub_meta()
266271
#=:notaskstate=#false,
267272
#=:inaccessiblememonly=#false,
268273
#=:noub=#true,
269-
#=:noub_if_noinbounds=#false))
274+
#=:noub_if_noinbounds=#false,
275+
#=:consistent_overlay=#false))
270276
end
271277
# can be used in place of `@assume_effects :effect_free :terminates_locally` (supposed to be used for bootstrapping)
272278
macro _effect_free_terminates_locally_meta()
@@ -279,7 +285,8 @@ macro _effect_free_terminates_locally_meta()
279285
#=:notaskstate=#false,
280286
#=:inaccessiblememonly=#false,
281287
#=:noub=#false,
282-
#=:noub_if_noinbounds=#false))
288+
#=:noub_if_noinbounds=#false,
289+
#=:consistent_overlay=#false))
283290
end
284291
# can be used in place of `@assume_effects :nothrow :noub` (supposed to be used for bootstrapping)
285292
macro _nothrow_noub_meta()
@@ -292,7 +299,8 @@ macro _nothrow_noub_meta()
292299
#=:notaskstate=#false,
293300
#=:inaccessiblememonly=#false,
294301
#=:noub=#true,
295-
#=:noub_if_noinbounds=#false))
302+
#=:noub_if_noinbounds=#false,
303+
#=:consistent_overlay=#false))
296304
end
297305
# can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
298306
macro _nothrow_meta()
@@ -305,7 +313,8 @@ macro _nothrow_meta()
305313
#=:notaskstate=#false,
306314
#=:inaccessiblememonly=#false,
307315
#=:noub=#false,
308-
#=:noub_if_noinbounds=#false))
316+
#=:noub_if_noinbounds=#false,
317+
#=:consistent_overlay=#false))
309318
end
310319
# can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
311320
macro _noub_meta()
@@ -318,7 +327,8 @@ macro _noub_meta()
318327
#=:notaskstate=#false,
319328
#=:inaccessiblememonly=#false,
320329
#=:noub=#true,
321-
#=:noub_if_noinbounds=#false))
330+
#=:noub_if_noinbounds=#false,
331+
#=:consistent_overlay=#false))
322332
end
323333
# can be used in place of `@assume_effects :notaskstate` (supposed to be used for bootstrapping)
324334
macro _notaskstate_meta()
@@ -331,7 +341,8 @@ macro _notaskstate_meta()
331341
#=:notaskstate=#true,
332342
#=:inaccessiblememonly=#false,
333343
#=:noub=#false,
334-
#=:noub_if_noinbounds=#false))
344+
#=:noub_if_noinbounds=#false,
345+
#=:consistent_overlay=#false))
335346
end
336347
# can be used in place of `@assume_effects :noub_if_noinbounds` (supposed to be used for bootstrapping)
337348
macro _noub_if_noinbounds_meta()
@@ -344,7 +355,8 @@ macro _noub_if_noinbounds_meta()
344355
#=:notaskstate=#false,
345356
#=:inaccessiblememonly=#false,
346357
#=:noub=#false,
347-
#=:noub_if_noinbounds=#true))
358+
#=:noub_if_noinbounds=#true,
359+
#=:consistent_overlay=#false))
348360
end
349361

350362
# another version of inlining that propagates an inbounds context

0 commit comments

Comments
 (0)