effects: separate :noub effect bit from :consistent

The current `:consistent` effect bit carries dual meanings:
1. "the return value is always consistent"
2. "this method does not cause any undefined behavior".

This design makes the effect bit unclear and hard to manage.
Specifically, the current design prevents a post-inference analysis
(as discussed in #50805) from safely refining
"consistent"-cy using post-optimization state IR. This is because it is
impossible to tell whether the `:consistent`-cy has been influenced by
the first or second meaning.

To address this, this commit splits them into two distinct effect bits:
`:consistent` for consistent return values and `:noub` for no undefined
behavior.

This commit also introduces an override mechanism for `:noub` as it is
necessary for `@assume_effects` to concrete-evaluate the annotated
methods. While this might sound risky and not in line with the existing
designs of `:nonoverlayed` and `:noinbounds`, where their overrides are
prohibited, but we already have an override mechanism in place for
`:consistent`, which implicitly overrides `:noub`. Given this precedent,
the override for `:noub` should probably be justified.

base/boot.jl

@@ -463,7 +463,8 @@ macro _foldable_meta()
         #=:terminates_globally=#true,
         #=:terminates_locally=#false,
         #=:notaskstate=#false,
-        #=:inaccessiblememonly=#false))
+        #=:inaccessiblememonly=#false,
+        #=:noub=#true))
 end
 
 const NTuple{N,T} = Tuple{Vararg{T,N}}

base/compiler/abstractinterpretation.jl

@@ -464,9 +464,9 @@ function add_call_backedges!(interp::AbstractInterpreter, @nospecialize(rettype)
         if !isoverlayed(method_table(interp))
             all_effects = Effects(all_effects; nonoverlayed=false)
         end
-        if (# ignore the `:noinbounds` property if `:consistent`-cy is tainted already
-            (sv isa InferenceState && sv.ipo_effects.consistent === ALWAYS_FALSE) ||
-            all_effects.consistent === ALWAYS_FALSE ||
+        if (# ignore the `:noinbounds` property if `:noub` is tainted already
+            (sv isa InferenceState && !sv.ipo_effects.noub) ||
+            !all_effects.noub ||
             # or this `:noinbounds` doesn't taint it
             !stmt_taints_inbounds_consistency(sv))
             all_effects = Effects(all_effects; noinbounds=false)
@@ -848,7 +848,7 @@ function concrete_eval_eligible(interp::AbstractInterpreter,
         end
     end
     if !effects.noinbounds && stmt_taints_inbounds_consistency(sv)
-        # If the current statement is @inbounds or we propagate inbounds, the call's consistency
+        # If the current statement is @inbounds or we propagate inbounds, the call's :noub
         # is tainted and not consteval eligible.
         add_remark!(interp, sv, "[constprop] Concrete evel disabled for inbounds")
         return :none
@@ -1993,13 +1993,16 @@ function abstract_call_known(interp::AbstractInterpreter, @nospecialize(f),
         end
         rt = abstract_call_builtin(interp, f, arginfo, sv)
         effects = builtin_effects(𝕃ᵢ, f, arginfo, rt)
-        if f === getfield && (fargs !== nothing && isexpr(fargs[end], :boundscheck)) && !is_nothrow(effects) && isa(sv, InferenceState)
-            # As a special case, we delayed tainting `noinbounds` for getfield calls in case we can prove
-            # in-boundedness indepedently. Here we need to put that back in other cases.
-            # N.B.: This isn't about the effects of the call itself, but a delayed contribution of the :boundscheck
-            # statement, so we need to merge this directly into sv, rather than modifying thte effects.
+        if (isa(sv, InferenceState) && f === getfield && fargs !== nothing &&
+            isexpr(fargs[end], :boundscheck) && !is_nothrow(effects))
+            # As a special case, we delayed tainting `noinbounds` for `getfield` calls
+            # in case we can prove in-boundedness indepedently.
+            # Here we need to put that back in other cases.
+            # N.B. This isn't about the effects of the call itself,
+            # but a delayed contribution of the :boundscheck statement,
+            # so we need to merge this directly into sv, rather than modifying the effects.
             merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; noinbounds=false,
-                consistent = (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0 ? ALWAYS_FALSE : ALWAYS_TRUE))
+                noub = iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS)))
         end
         return CallMeta(rt, effects, NoCallInfo())
     elseif isa(f, Core.OpaqueClosure)
@@ -2222,22 +2225,22 @@ function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::
                 f = abstract_eval_value(interp, stmt.args[1], vtypes, sv)
                 if f isa Const && f.val === getfield
                     # boundscheck of `getfield` call is analyzed by tfunc potentially without
-                    # tainting :inbounds or :consistent when it's known to be nothrow
+                    # tainting :noinbounds or :noub when it's known to be nothrow
                     @goto delay_effects_analysis
                 end
             end
             # If there is no particular `@inbounds` for this function, then we only taint `:noinbounds`,
-            # which will subsequently taint `:consistent`-cy if this function is called from another
+            # which will subsequently taint `:noub` if this function is called from another
             # function that uses `@inbounds`. However, if this `:boundscheck` is itself within an
             # `@inbounds` region, its value depends on `--check-bounds`, so we need to taint
-            # `:consistent`-cy here also.
+            # `:noub`-cy here also.
             merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; noinbounds=false,
-                consistent = (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0 ? ALWAYS_FALSE : ALWAYS_TRUE))
+                noub = iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS)))
         end
         @label delay_effects_analysis
         rt = Bool
     elseif head === :inbounds
-        @assert false && "Expected this to have been moved into flags"
+        @assert false "Expected `:inbounds` expression to have been moved into SSA flags"
     elseif head === :the_exception
         merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; consistent=ALWAYS_FALSE))
     end
@@ -2355,22 +2358,23 @@ function abstract_eval_statement_expr(interp::AbstractInterpreter, e::Expr, vtyp
         t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
         ut = unwrap_unionall(t)
         consistent = ALWAYS_FALSE
-        nothrow = false
+        nothrow = noub = false
         if isa(ut, DataType) && !isabstracttype(ut)
             ismutable = ismutabletype(ut)
             fcount = datatype_fieldcount(ut)
             nargs = length(e.args) - 1
             if (fcount === nothing || (fcount > nargs && (let t = t
                     any(i::Int -> !is_undefref_fieldtype(fieldtype(t, i)), (nargs+1):fcount)
                 end)))
-                # allocation with undefined field leads to undefined behavior and should taint `:consistent`-cy
-                consistent = ALWAYS_FALSE
+                # allocation with undefined field leads to undefined behavior and should taint `:noub`
             elseif ismutable
-                # mutable object isn't `:consistent`, but we can still give the return
-                # type information a chance to refine this `:consistent`-cy later
+                # mutable object isn't `:consistent`, but we still have a chance that
+                # return type information later refines the `:consistent`-cy of the method
                 consistent = CONSISTENT_IF_NOTRETURNED
+                noub = true
             else
                 consistent = ALWAYS_TRUE
+                noub = true
             end
             if isconcretedispatch(t)
                 nothrow = true
@@ -2414,7 +2418,7 @@ function abstract_eval_statement_expr(interp::AbstractInterpreter, e::Expr, vtyp
                 t = refine_partial_type(t)
             end
         end
-        effects = Effects(EFFECTS_TOTAL; consistent, nothrow)
+        effects = Effects(EFFECTS_TOTAL; consistent, nothrow, noub)
     elseif ehead === :splatnew
         t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
         nothrow = false # TODO: More precision
@@ -2557,15 +2561,14 @@ function abstract_eval_foreigncall(interp::AbstractInterpreter, e::Expr, vtypes:
     cconv = e.args[5]
     if isa(cconv, QuoteNode) && (v = cconv.value; isa(v, Tuple{Symbol, UInt8}))
         override = decode_effects_override(v[2])
-        effects = Effects(
-            override.consistent          ? ALWAYS_TRUE : effects.consistent,
-            override.effect_free         ? ALWAYS_TRUE : effects.effect_free,
-            override.nothrow             ? true        : effects.nothrow,
-            override.terminates_globally ? true        : effects.terminates,
-            override.notaskstate         ? true        : effects.notaskstate,
-            override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
-            effects.nonoverlayed,
-            effects.noinbounds)
+        effects = Effects(effects;
+            consistent          = override.consistent ? ALWAYS_TRUE : effects.consistent,
+            effect_free         = override.effect_free ? ALWAYS_TRUE : effects.effect_free,
+            nothrow             = override.nothrow ? true : effects.nothrow,
+            terminates          = override.terminates_globally ? true : effects.terminates,
+            notaskstate         = override.notaskstate ? true : effects.notaskstate,
+            inaccessiblememonly = override.inaccessiblememonly ? ALWAYS_TRUE : effects.inaccessiblememonly,
+            noub                = override.noub ? true : effects.noub)
     end
     return RTEffects(t, effects)
 end
@@ -2600,8 +2603,8 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             # we ourselves don't read our parent's inbounds.
             effects = Effects(effects; noinbounds=true)
         end
-        if (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0
-            effects = Effects(effects; consistent=ALWAYS_FALSE)
+        if !iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS)
+            effects = Effects(effects; noub=false)
         end
     end
     merge_effects!(interp, sv, effects)

base/compiler/effects.jl

@@ -6,7 +6,7 @@ Represents computational effects of a method call.
 The effects are a composition of different effect bits that represent some program property
 of the method being analyzed. They are represented as `Bool` or `UInt8` bits with the
 following meanings:
-- `effects.consistent::UInt8`:
+- `consistent::UInt8`:
   * `ALWAYS_TRUE`: this method is guaranteed to return or terminate consistently.
   * `ALWAYS_FALSE`: this method may be not return or terminate consistently, and there is
     no need for further analysis with respect to this effect property as this conclusion
@@ -38,6 +38,10 @@ 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::Bool`: 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.
 - `nonoverlayed::Bool`: indicates that any methods that may be called within this method
   are not defined in an [overlayed method table](@ref OverlayMethodTable).
 - `noinbounds::Bool`: If set, indicates that this method does not read the parent's `:inbounds`
@@ -80,7 +84,10 @@ The output represents the state of different effect properties in the following
     - `+m` (green): `ALWAYS_TRUE`
     - `-m` (red): `ALWAYS_FALSE`
     - `?m` (yellow): `INACCESSIBLEMEM_OR_ARGMEMONLY`
-7. `noinbounds` (`i`):
+7. `noub` (`u`):
+    - `+u` (green): `true`
+    - `-u` (red): `false`
+8. `noinbounds` (`i`):
     - `+i` (green): `true`
     - `-i` (red): `false`
 
@@ -93,6 +100,7 @@ struct Effects
     terminates::Bool
     notaskstate::Bool
     inaccessiblememonly::UInt8
+    noub::Bool
     nonoverlayed::Bool
     noinbounds::Bool
     function Effects(
@@ -102,6 +110,7 @@ struct Effects
         terminates::Bool,
         notaskstate::Bool,
         inaccessiblememonly::UInt8,
+        noub::Bool,
         nonoverlayed::Bool,
         noinbounds::Bool)
         return new(
@@ -111,6 +120,7 @@ struct Effects
             terminates,
             notaskstate,
             inaccessiblememonly,
+            noub,
             nonoverlayed,
             noinbounds)
     end
@@ -129,27 +139,29 @@ const EFFECT_FREE_IF_INACCESSIBLEMEMONLY = 0x01 << 1
 # :inaccessiblememonly bits
 const INACCESSIBLEMEM_OR_ARGMEMONLY = 0x01 << 1
 
-const EFFECTS_TOTAL    = Effects(ALWAYS_TRUE,  ALWAYS_TRUE,  true,  true,  true,  ALWAYS_TRUE,  true,  true)
-const EFFECTS_THROWS   = Effects(ALWAYS_TRUE,  ALWAYS_TRUE,  false, true,  true,  ALWAYS_TRUE,  true,  true)
-const EFFECTS_UNKNOWN  = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, true,  true)  # unknown mostly, but it's not overlayed and noinbounds at least (e.g. it's not a call)
-const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, false, false) # unknown really
+const EFFECTS_TOTAL    = Effects(ALWAYS_TRUE,  ALWAYS_TRUE,  true,  true,  true,  ALWAYS_TRUE,  true,  true,  true)
+const EFFECTS_THROWS   = Effects(ALWAYS_TRUE,  ALWAYS_TRUE,  false, true,  true,  ALWAYS_TRUE,  true,  true,  true)
+const EFFECTS_UNKNOWN  = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, false, true,  true) # unknown mostly, but it's not overlayed and noinbounds at least (e.g. it's not a call)
+const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, false, false, false) # unknown really
 
-function Effects(e::Effects = _EFFECTS_UNKNOWN;
-    consistent::UInt8 = e.consistent,
-    effect_free::UInt8 = e.effect_free,
-    nothrow::Bool = e.nothrow,
-    terminates::Bool = e.terminates,
-    notaskstate::Bool = e.notaskstate,
-    inaccessiblememonly::UInt8 = e.inaccessiblememonly,
-    nonoverlayed::Bool = e.nonoverlayed,
-    noinbounds::Bool = e.noinbounds)
+function Effects(effects::Effects = _EFFECTS_UNKNOWN;
+    consistent::UInt8 = effects.consistent,
+    effect_free::UInt8 = effects.effect_free,
+    nothrow::Bool = effects.nothrow,
+    terminates::Bool = effects.terminates,
+    notaskstate::Bool = effects.notaskstate,
+    inaccessiblememonly::UInt8 = effects.inaccessiblememonly,
+    noub::Bool = effects.noub,
+    nonoverlayed::Bool = effects.nonoverlayed,
+    noinbounds::Bool = effects.noinbounds)
     return Effects(
         consistent,
         effect_free,
         nothrow,
         terminates,
         notaskstate,
         inaccessiblememonly,
+        noub,
         nonoverlayed,
         noinbounds)
 end
@@ -162,6 +174,7 @@ function merge_effects(old::Effects, new::Effects)
         merge_effectbits(old.terminates, new.terminates),
         merge_effectbits(old.notaskstate, new.notaskstate),
         merge_effectbits(old.inaccessiblememonly, new.inaccessiblememonly),
+        merge_effectbits(old.noub, new.noub),
         merge_effectbits(old.nonoverlayed, new.nonoverlayed),
         merge_effectbits(old.noinbounds, new.noinbounds))
 end
@@ -180,18 +193,21 @@ is_nothrow(effects::Effects)             = effects.nothrow
 is_terminates(effects::Effects)          = effects.terminates
 is_notaskstate(effects::Effects)         = effects.notaskstate
 is_inaccessiblememonly(effects::Effects) = effects.inaccessiblememonly === ALWAYS_TRUE
+is_noub(effects::Effects)                = effects.noub
 is_nonoverlayed(effects::Effects)        = effects.nonoverlayed
 
 # implies `is_notaskstate` & `is_inaccessiblememonly`, but not explicitly checked here
 is_foldable(effects::Effects) =
     is_consistent(effects) &&
+    is_noub(effects) &&
     is_effect_free(effects) &&
     is_terminates(effects)
 
 is_foldable_nothrow(effects::Effects) =
     is_foldable(effects) &&
     is_nothrow(effects)
 
+# TODO add `is_noub` here?
 is_removable_if_unused(effects::Effects) =
     is_effect_free(effects) &&
     is_terminates(effects) &&
@@ -209,14 +225,15 @@ is_effect_free_if_inaccessiblememonly(effects::Effects) = !iszero(effects.effect
 is_inaccessiblemem_or_argmemonly(effects::Effects) = effects.inaccessiblememonly === INACCESSIBLEMEM_OR_ARGMEMONLY
 
 function encode_effects(e::Effects)
-    return ((e.consistent          % UInt32) << 0) |
-           ((e.effect_free         % UInt32) << 3) |
-           ((e.nothrow             % UInt32) << 5) |
-           ((e.terminates          % UInt32) << 6) |
-           ((e.notaskstate         % UInt32) << 7) |
-           ((e.inaccessiblememonly % UInt32) << 8) |
-           ((e.nonoverlayed        % UInt32) << 10)|
-           ((e.noinbounds          % UInt32) << 11)
+    return ((e.consistent          % UInt32) << 0)  |
+           ((e.effect_free         % UInt32) << 3)  |
+           ((e.nothrow             % UInt32) << 5)  |
+           ((e.terminates          % UInt32) << 6)  |
+           ((e.notaskstate         % UInt32) << 7)  |
+           ((e.inaccessiblememonly % UInt32) << 8)  |
+           ((e.noub                % UInt32) << 10) |
+           ((e.nonoverlayed        % UInt32) << 11) |
+           ((e.noinbounds          % UInt32) << 12)
 end
 
 function decode_effects(e::UInt32)
@@ -228,7 +245,8 @@ function decode_effects(e::UInt32)
         _Bool((e >> 7) & 0x01),
         UInt8((e >> 8) & 0x03),
         _Bool((e >> 10) & 0x01),
-        _Bool((e >> 11) & 0x01))
+        _Bool((e >> 11) & 0x01),
+        _Bool((e >> 12) & 0x01))
 end
 
 struct EffectsOverride
@@ -239,6 +257,7 @@ struct EffectsOverride
     terminates_locally::Bool
     notaskstate::Bool
     inaccessiblememonly::Bool
+    noub::Bool
 end
 
 function encode_effects_override(eo::EffectsOverride)
@@ -250,6 +269,7 @@ function encode_effects_override(eo::EffectsOverride)
     eo.terminates_locally  && (e |= (0x01 << 4))
     eo.notaskstate         && (e |= (0x01 << 5))
     eo.inaccessiblememonly && (e |= (0x01 << 6))
+    eo.noub                && (e |= (0x01 << 7))
     return e
 end
 
@@ -261,5 +281,6 @@ function decode_effects_override(e::UInt8)
         (e & (0x01 << 3)) != 0x00,
         (e & (0x01 << 4)) != 0x00,
         (e & (0x01 << 5)) != 0x00,
-        (e & (0x01 << 6)) != 0x00)
+        (e & (0x01 << 6)) != 0x00,
+        (e & (0x01 << 7)) != 0x00)
 end

base/compiler/ssair/show.jl

@@ -1020,6 +1020,8 @@ function Base.show(io::IO, e::Effects)
     print(io, ',')
     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, :noinbounds, 'i'); color=effectbits_color(e, :noinbounds))
     print(io, ')')
     e.nonoverlayed || printstyled(io, '′'; color=:red)