From f58960acfcec0e3a814293ce559e5c6b3810e43c Mon Sep 17 00:00:00 2001 From: Keno Fischer Date: Wed, 16 Apr 2025 22:07:09 -0400 Subject: [PATCH] Strengthen language around `@assume_effects` :consistent The current language of `:consistent` for assume_effects is problematic, because it explicitly promises something false: That you're allowed to mark a method as `:consistent` even in the face of redefinitions. To understand this problem a bit better, we need to think about the primary use case of the `:consistent` annotation: To perform constant propagation evaluation of fuctions with constant arguments. However, since constant evaluation only runs in a single world (unlike the abstract interpreter, which symbolically runs in multiple worlds and keeps track of which world range its result is valid for), we run into a bit of a problem. In principle, for full correctness and under the current definition of consistentcy, we can only claim that we know the result for a single world age (the one that we ran in). This is problematic, because it would force us to re-infer the function for every new world age. In practice however, ignoring `@assume_effects` for the moment, we have a stronger guarantee. When inference sets the :consistent effect bit, it guarantees consistentcy across the entire computed min_world:max_world range. If there is a redefinition, the world range will be terminated, even if it is `:consistent` both before and after and even if the redefinition would not otherwise affect inference's computed information. This is useful, because it lets us conclude that the information derived from concrete evluation is valid for the entire min_world:max_world range of the corresponding code instance. Coming back to `@assume_effects` we run into a problem however, because we have no way to provide the required edges to inference. In practice inference will probably be able to figure it out, but this is insufficient as a semantic guarantee. After some discussion within the compiler team, we came to the conclusion that the best resolution was to change the documented semantics of `@assume_effects :consistent` to require consistent-cy across the entire defined world range of the method, not just world-age-by-world-age. This is a significantly stronger guarantee, but appears necessary for semantic correctness. In the future we may want to consider `:consistent` annotations for particular if blocks, which would not require the same restrictions (because it would still rely on inference to add appropriate edges for redefinitions) --- Compiler/src/abstractinterpretation.jl | 14 +++++++++++++ Compiler/src/typeinfer.jl | 29 +++++++++++++++++++------- base/expr.jl | 14 ++++++++----- 3 files changed, 44 insertions(+), 13 deletions(-) diff --git a/Compiler/src/abstractinterpretation.jl b/Compiler/src/abstractinterpretation.jl index 3a2d04a127607..188085f52d091 100644 --- a/Compiler/src/abstractinterpretation.jl +++ b/Compiler/src/abstractinterpretation.jl @@ -3499,6 +3499,20 @@ function merge_override_effects!(interp::AbstractInterpreter, effects::Effects, # It is possible for arguments (GlobalRef/:static_parameter) to throw, # but these will be recomputed during SSA construction later. override = decode_statement_effects_override(sv) + if override.consistent + m = sv.linfo.def + if isa(m, Method) + # N.B.: We'd like deleted_world here, but we can't add an appropriate edge at this point. + # However, in order to reach here in the first place, ordinary method lookup would have + # had to add an edge and appropriate invalidation trigger. + valid_worlds = WorldRange(m.primary_world, typemax(Int)) + if sv.world.this in valid_worlds + update_valid_age!(sv, valid_worlds) + else + override = EffectsOverride(override, consistent=false) + end + end + end effects = override_effects(effects, override) set_curr_ssaflag!(sv, flags_for_effects(effects), IR_FLAGS_EFFECTS) merge_effects!(interp, sv, effects) diff --git a/Compiler/src/typeinfer.jl b/Compiler/src/typeinfer.jl index 2b4ada7805140..a5b87c86a3ac2 100644 --- a/Compiler/src/typeinfer.jl +++ b/Compiler/src/typeinfer.jl @@ -368,11 +368,17 @@ function cycle_fix_limited(@nospecialize(typ), sv::InferenceState, cycleid::Int) return typ end -function adjust_effects(ipo_effects::Effects, def::Method) +function adjust_effects(ipo_effects::Effects, def::Method, world::UInt) # override the analyzed effects using manually annotated effect settings override = decode_effects_override(def.purity) + valid_worlds = WorldRange(0, typemax(UInt)) if is_effect_overridden(override, :consistent) - ipo_effects = Effects(ipo_effects; consistent=ALWAYS_TRUE) + # See note on `typemax(Int)` instead of `deleted_world` in adjust_effects! + override_valid_worlds = WorldRange(def.primary_world, typemax(Int)) + if world in override_valid_worlds + ipo_effects = Effects(ipo_effects; consistent=ALWAYS_TRUE) + valid_worlds = override_valid_worlds + end end if is_effect_overridden(override, :effect_free) ipo_effects = Effects(ipo_effects; effect_free=ALWAYS_TRUE) @@ -400,7 +406,7 @@ function adjust_effects(ipo_effects::Effects, def::Method) if is_effect_overridden(override, :nortcall) ipo_effects = Effects(ipo_effects; nortcall=true) end - return ipo_effects + return (ipo_effects, valid_worlds) end function adjust_effects(sv::InferenceState) @@ -454,7 +460,8 @@ function adjust_effects(sv::InferenceState) # override the analyzed effects using manually annotated effect settings def = sv.linfo.def if isa(def, Method) - ipo_effects = adjust_effects(ipo_effects, def) + (ipo_effects, valid_worlds) = adjust_effects(ipo_effects, def, sv.world.this) + update_valid_age!(sv, valid_worlds) end return ipo_effects @@ -492,9 +499,9 @@ function finishinfer!(me::InferenceState, interp::AbstractInterpreter, cycleid:: end end result = me.result - result.valid_worlds = me.world.valid_worlds result.result = bestguess ipo_effects = result.ipo_effects = me.ipo_effects = adjust_effects(me) + result.valid_worlds = me.world.valid_worlds result.exc_result = me.exc_bestguess = refine_exception_type(me.exc_bestguess, ipo_effects) me.src.rettype = widenconst(ignorelimited(bestguess)) me.src.ssaflags = me.ssaflags @@ -957,8 +964,13 @@ function typeinf_edge(interp::AbstractInterpreter, method::Method, @nospecialize update_valid_age!(caller, frame.world.valid_worlds) local isinferred = is_inferred(frame) local edge = isinferred ? edge_ci : nothing - local effects = isinferred ? frame.result.ipo_effects : # effects are adjusted already within `finish` for ipo_effects - adjust_effects(effects_for_cycle(frame.ipo_effects), method) + local effects, valid_worlds + if isinferred + effects = frame.result.ipo_effects # effects are adjusted already within `finish` for ipo_effects + else + (effects, valid_worlds) = adjust_effects(effects_for_cycle(frame.ipo_effects), method, frame.world.this) + update_valid_age!(caller, valid_worlds) + end local bestguess = frame.bestguess local exc_bestguess = refine_exception_type(frame.exc_bestguess, effects) # propagate newly inferred source to the inliner, allowing efficient inlining w/o deserialization: @@ -981,7 +993,8 @@ function typeinf_edge(interp::AbstractInterpreter, method::Method, @nospecialize # return the current knowledge about this cycle frame = frame::InferenceState update_valid_age!(caller, frame.world.valid_worlds) - effects = adjust_effects(effects_for_cycle(frame.ipo_effects), method) + (effects, valid_worlds) = adjust_effects(effects_for_cycle(frame.ipo_effects), method, frame.world.this) + update_valid_age!(caller, valid_worlds) bestguess = frame.bestguess exc_bestguess = refine_exception_type(frame.exc_bestguess, effects) return Future(MethodCallResult(interp, caller, method, bestguess, exc_bestguess, effects, nothing, edgecycle, edgelimited)) diff --git a/base/expr.jl b/base/expr.jl index dd357736bc529..ca9c6b46b41b2 100644 --- a/base/expr.jl +++ b/base/expr.jl @@ -540,16 +540,20 @@ The `:consistent` setting asserts that for egal (`===`) inputs: contents) are not egal. !!! note - The `:consistent`-cy assertion is made world-age wise. More formally, write - ``fᵢ`` for the evaluation of ``f`` in world-age ``i``, then this setting requires: + The `:consistent`-cy assertion is made with respect to a particular world range `R`. + More formally, write ``fᵢ`` for the evaluation of ``f`` in world-age ``i``, then this setting requires: ```math - ∀ i, x, y: x ≡ y → fᵢ(x) ≡ fᵢ(y) + ∀ i ∈ R, j ∈ R, x, y: x ≡ y → fᵢ(x) ≡ fⱼ(y) ``` - However, for two world ages ``i``, ``j`` s.t. ``i ≠ j``, we may have ``fᵢ(x) ≢ fⱼ(y)``. + + For `@assume_effects`, the range `R` is `m.primary_world:m.deleted_world` of + the annotated or containing method. + + For ordinary code instances, `R` is `ci.min_world:ci.max_world`. A further implication is that `:consistent` functions may not make their return value dependent on the state of the heap or any other global state - that is not constant for a given world age. + that is not constant over the given world age range. !!! note The `:consistent`-cy includes all legal rewrites performed by the optimizer.