Skip to content

Commit dbe39aa

Browse files
committed
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 fc31b09 commit dbe39aa

14 files changed

+291
-91
lines changed

base/boot.jl

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

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

base/compiler/abstractinterpretation.jl

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -491,7 +491,7 @@ function add_call_backedges!(interp::AbstractInterpreter, @nospecialize(rettype)
491491
# ignore the `:nonoverlayed` property if `interp` doesn't use overlayed method table
492492
# since it will never be tainted anyway
493493
if !isoverlayed(method_table(interp))
494-
all_effects = Effects(all_effects; nonoverlayed=false)
494+
all_effects = Effects(all_effects; nonoverlayed=ALWAYS_FALSE)
495495
end
496496
all_effects === Effects() && return nothing
497497
end
@@ -889,7 +889,15 @@ function concrete_eval_eligible(interp::AbstractInterpreter,
889889
mi = result.edge
890890
if mi !== nothing && is_foldable(effects)
891891
if f !== nothing && is_all_const_arg(arginfo, #=start=#2)
892-
if is_nonoverlayed(interp) || is_nonoverlayed(effects)
892+
if (is_nonoverlayed(interp) || is_nonoverlayed(effects) ||
893+
# Even if overlay methods are involved, when `:consistent_overlay` is
894+
# explicitly applied, we can still perform concrete evaluation using the
895+
# original methods for executing them.
896+
# While there's a chance that the non-overlayed counterparts may raise
897+
# non-egal exceptions, it will not impact the compilation validity, since:
898+
# - the results of the concrete evaluation will not be inlined
899+
# - the exception types from the concrete evaluation will not be propagated
900+
is_consistent_overlay(effects))
893901
return :concrete_eval
894902
end
895903
# disable concrete-evaluation if this function call is tainted by some overlayed
@@ -2770,7 +2778,7 @@ function override_effects(effects::Effects, override::EffectsOverride)
27702778
notaskstate = override.notaskstate ? true : effects.notaskstate,
27712779
inaccessiblememonly = override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
27722780
noub = override.noub ? ALWAYS_TRUE :
2773-
override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE ? NOUB_IF_NOINBOUNDS :
2781+
(override.noub_if_noinbounds && effects.noub !== ALWAYS_TRUE) ? NOUB_IF_NOINBOUNDS :
27742782
effects.noub)
27752783
end
27762784

base/compiler/compiler.jl

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -47,10 +47,11 @@ struct EffectsOverride
4747
inaccessiblememonly::Bool
4848
noub::Bool
4949
noub_if_noinbounds::Bool
50+
consistent_overlay::Bool
5051
end
5152
function EffectsOverride(
5253
override::EffectsOverride =
53-
EffectsOverride(false, false, false, false, false, false, false, false, false);
54+
EffectsOverride(false, false, false, false, false, false, false, false, false, false);
5455
consistent::Bool = override.consistent,
5556
effect_free::Bool = override.effect_free,
5657
nothrow::Bool = override.nothrow,
@@ -59,7 +60,8 @@ function EffectsOverride(
5960
notaskstate::Bool = override.notaskstate,
6061
inaccessiblememonly::Bool = override.inaccessiblememonly,
6162
noub::Bool = override.noub,
62-
noub_if_noinbounds::Bool = override.noub_if_noinbounds)
63+
noub_if_noinbounds::Bool = override.noub_if_noinbounds,
64+
consistent_overlay::Bool = override.consistent_overlay)
6365
return EffectsOverride(
6466
consistent,
6567
effect_free,
@@ -69,9 +71,10 @@ function EffectsOverride(
6971
notaskstate,
7072
inaccessiblememonly,
7173
noub,
72-
noub_if_noinbounds)
74+
noub_if_noinbounds,
75+
consistent_overlay)
7376
end
74-
const NUM_EFFECTS_OVERRIDES = 9 # sync with julia.h
77+
const NUM_EFFECTS_OVERRIDES = 10 # sync with julia.h
7578

7679
# essential files and libraries
7780
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
@@ -329,7 +329,10 @@ mutable struct InferenceState
329329
end
330330

331331
if def isa Method
332-
ipo_effects = Effects(ipo_effects; nonoverlayed=is_nonoverlayed(def))
332+
nonoverlayed = is_nonoverlayed(def) ? ALWAYS_TRUE :
333+
is_effect_overridden(def, :consistent_overlay) ? CONSISTENT_OVERLAY :
334+
ALWAYS_FALSE
335+
ipo_effects = Effects(ipo_effects; nonoverlayed)
333336
end
334337

335338
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
@@ -1019,8 +1019,9 @@ function Base.show(io::IO, e::Effects)
10191019
printstyled(io, effectbits_letter(e, :inaccessiblememonly, 'm'); color=effectbits_color(e, :inaccessiblememonly))
10201020
print(io, ',')
10211021
printstyled(io, effectbits_letter(e, :noub, 'u'); color=effectbits_color(e, :noub))
1022+
print(io, ',')
1023+
printstyled(io, effectbits_letter(e, :nonoverlayed, 'o'); color=effectbits_color(e, :nonoverlayed))
10221024
print(io, ')')
1023-
e.nonoverlayed || printstyled(io, ''; color=:red)
10241025
end
10251026

10261027
@specialize

base/compiler/typeinfer.jl

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -492,6 +492,9 @@ function adjust_effects(ipo_effects::Effects, def::Method)
492492
elseif is_effect_overridden(override, :noub_if_noinbounds) && ipo_effects.noub !== ALWAYS_TRUE
493493
ipo_effects = Effects(ipo_effects; noub=NOUB_IF_NOINBOUNDS)
494494
end
495+
if is_effect_overridden(override, :consistent_overlay)
496+
ipo_effects = Effects(ipo_effects; nonoverlayed=CONSISTENT_OVERLAY)
497+
end
495498
return ipo_effects
496499
end
497500

base/essentials.jl

Lines changed: 24 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,8 @@ macro _total_meta()
212212
#=:notaskstate=#true,
213213
#=:inaccessiblememonly=#true,
214214
#=:noub=#true,
215-
#=:noub_if_noinbounds=#false))
215+
#=:noub_if_noinbounds=#false,
216+
#=:consistent_overlay=#false))
216217
end
217218
# can be used in place of `@assume_effects :foldable` (supposed to be used for bootstrapping)
218219
macro _foldable_meta()
@@ -225,7 +226,8 @@ macro _foldable_meta()
225226
#=:notaskstate=#true,
226227
#=:inaccessiblememonly=#true,
227228
#=:noub=#true,
228-
#=:noub_if_noinbounds=#false))
229+
#=:noub_if_noinbounds=#false,
230+
#=:consistent_overlay=#false))
229231
end
230232
# can be used in place of `@assume_effects :terminates_locally` (supposed to be used for bootstrapping)
231233
macro _terminates_locally_meta()
@@ -238,7 +240,8 @@ macro _terminates_locally_meta()
238240
#=:notaskstate=#false,
239241
#=:inaccessiblememonly=#false,
240242
#=:noub=#false,
241-
#=:noub_if_noinbounds=#false))
243+
#=:noub_if_noinbounds=#false,
244+
#=:consistent_overlay=#false))
242245
end
243246
# can be used in place of `@assume_effects :terminates_globally` (supposed to be used for bootstrapping)
244247
macro _terminates_globally_meta()
@@ -251,7 +254,8 @@ macro _terminates_globally_meta()
251254
#=:notaskstate=#false,
252255
#=:inaccessiblememonly=#false,
253256
#=:noub=#false,
254-
#=:noub_if_noinbounds=#false))
257+
#=:noub_if_noinbounds=#false,
258+
#=:consistent_overlay=#false))
255259
end
256260
# can be used in place of `@assume_effects :terminates_globally :notaskstate` (supposed to be used for bootstrapping)
257261
macro _terminates_globally_notaskstate_meta()
@@ -264,7 +268,8 @@ macro _terminates_globally_notaskstate_meta()
264268
#=:notaskstate=#true,
265269
#=:inaccessiblememonly=#false,
266270
#=:noub=#false,
267-
#=:noub_if_noinbounds=#false))
271+
#=:noub_if_noinbounds=#false,
272+
#=:consistent_overlay=#false))
268273
end
269274
# can be used in place of `@assume_effects :terminates_globally :noub` (supposed to be used for bootstrapping)
270275
macro _terminates_globally_noub_meta()
@@ -277,7 +282,8 @@ macro _terminates_globally_noub_meta()
277282
#=:notaskstate=#false,
278283
#=:inaccessiblememonly=#false,
279284
#=:noub=#true,
280-
#=:noub_if_noinbounds=#false))
285+
#=:noub_if_noinbounds=#false,
286+
#=:consistent_overlay=#false))
281287
end
282288
# can be used in place of `@assume_effects :effect_free :terminates_locally` (supposed to be used for bootstrapping)
283289
macro _effect_free_terminates_locally_meta()
@@ -290,7 +296,8 @@ macro _effect_free_terminates_locally_meta()
290296
#=:notaskstate=#false,
291297
#=:inaccessiblememonly=#false,
292298
#=:noub=#false,
293-
#=:noub_if_noinbounds=#false))
299+
#=:noub_if_noinbounds=#false,
300+
#=:consistent_overlay=#false))
294301
end
295302
# can be used in place of `@assume_effects :nothrow :noub` (supposed to be used for bootstrapping)
296303
macro _nothrow_noub_meta()
@@ -303,7 +310,8 @@ macro _nothrow_noub_meta()
303310
#=:notaskstate=#false,
304311
#=:inaccessiblememonly=#false,
305312
#=:noub=#true,
306-
#=:noub_if_noinbounds=#false))
313+
#=:noub_if_noinbounds=#false,
314+
#=:consistent_overlay=#false))
307315
end
308316
# can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
309317
macro _nothrow_meta()
@@ -316,7 +324,8 @@ macro _nothrow_meta()
316324
#=:notaskstate=#false,
317325
#=:inaccessiblememonly=#false,
318326
#=:noub=#false,
319-
#=:noub_if_noinbounds=#false))
327+
#=:noub_if_noinbounds=#false,
328+
#=:consistent_overlay=#false))
320329
end
321330
# can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping)
322331
macro _noub_meta()
@@ -329,7 +338,8 @@ macro _noub_meta()
329338
#=:notaskstate=#false,
330339
#=:inaccessiblememonly=#false,
331340
#=:noub=#true,
332-
#=:noub_if_noinbounds=#false))
341+
#=:noub_if_noinbounds=#false,
342+
#=:consistent_overlay=#false))
333343
end
334344
# can be used in place of `@assume_effects :notaskstate` (supposed to be used for bootstrapping)
335345
macro _notaskstate_meta()
@@ -342,7 +352,8 @@ macro _notaskstate_meta()
342352
#=:notaskstate=#true,
343353
#=:inaccessiblememonly=#false,
344354
#=:noub=#false,
345-
#=:noub_if_noinbounds=#false))
355+
#=:noub_if_noinbounds=#false,
356+
#=:consistent_overlay=#false))
346357
end
347358
# can be used in place of `@assume_effects :noub_if_noinbounds` (supposed to be used for bootstrapping)
348359
macro _noub_if_noinbounds_meta()
@@ -355,7 +366,8 @@ macro _noub_if_noinbounds_meta()
355366
#=:notaskstate=#false,
356367
#=:inaccessiblememonly=#false,
357368
#=:noub=#false,
358-
#=:noub_if_noinbounds=#true))
369+
#=:noub_if_noinbounds=#true,
370+
#=:consistent_overlay=#false))
359371
end
360372

361373
# another version of inlining that propagates an inbounds context

0 commit comments

Comments
 (0)