Strengthen language around @assume_effects :consistent (#58254)

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).

Closes #46156

Author: Keno

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)

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))

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.