effects: separate :noub effect bit from :consistent (#50808)

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

@nanosoldier `runbenchmarks("inference", vs=":master")`

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

@@ -854,8 +854,8 @@ 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
- # is tainted and not consteval eligible.
+ # If the current statement is @inbounds or we propagate inbounds,
+ # the call's :consistent-cy is tainted and not consteval eligible.
  add_remark!(interp, sv, "[constprop] Concrete evel disabled for inbounds")
  return :none
  end
@@ -1999,13 +1999,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))
+ consistent = iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) ? ALWAYS_TRUE : ALWAYS_FALSE))
  end
  return CallMeta(rt, effects, NoCallInfo())
  elseif isa(f, Core.OpaqueClosure)
@@ -2209,7 +2212,6 @@ function abstract_eval_cfunction(interp::AbstractInterpreter, e::Expr, vtypes::U
 end
 
 function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::Union{VarTable,Nothing}, sv::AbsIntState)
- rt = Any
  head = e.head
  if head === :static_parameter
  n = e.args[1]::Int
@@ -2218,6 +2220,8 @@ function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::
  sp = sv.sptypes[n]
  rt = sp.typ
  nothrow = !sp.undef
+ else
+ rt = Any
  end
  merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; nothrow))
  return rt
@@ -2228,26 +2232,26 @@ 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
- @goto delay_effects_analysis
+ # tainting :noinbounds or :noub when it's known to be nothrow
+ return Bool
  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 `:consistent` 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.
  merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; noinbounds=false,
- consistent = (get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) != 0 ? ALWAYS_FALSE : ALWAYS_TRUE))
+ consistent = iszero(get_curr_ssaflag(sv) & IR_FLAG_INBOUNDS) ? ALWAYS_TRUE : ALWAYS_FALSE))
  end
- @label delay_effects_analysis
- rt = Bool
+ return 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))
+ return Any
  end
- return rt
+ return Any
 end
 
 function abstract_eval_special_value(interp::AbstractInterpreter, @nospecialize(e), vtypes::Union{VarTable,Nothing}, sv::AbsIntState)
@@ -2361,22 +2365,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
@@ -2420,7 +2425,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
@@ -2563,15 +2568,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
@@ -2606,8 +2610,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; consistent=ALWAYS_FALSE, 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)