From 19a82ef69b60135f57e1e0de4b38251132666dc2 Mon Sep 17 00:00:00 2001 From: Shuhei Kadowaki Date: Wed, 2 Aug 2023 17:04:29 -0400 Subject: [PATCH] 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 JuliaLang/julia#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. --- base/boot.jl | 3 +- base/compiler/abstractinterpretation.jl | 72 +++++++++++++------------ base/compiler/effects.jl | 71 +++++++++++++++--------- base/compiler/ssair/show.jl | 2 + base/compiler/tfuncs.jl | 50 ++++++++++------- base/compiler/typeinfer.jl | 3 ++ base/essentials.jl | 15 ++++-- base/expr.jl | 35 ++++++------ base/special/log.jl | 8 +-- base/special/rem_pio2.jl | 4 +- src/julia.h | 1 + src/method.c | 3 +- test/compiler/effects.jl | 12 ++--- test/compiler/inference.jl | 8 ++- test/math.jl | 39 ++++++++------ 15 files changed, 194 insertions(+), 132 deletions(-) diff --git a/base/boot.jl b/base/boot.jl index 78b7daaf47d64b..e24a6f4ffc0e0b 100644 --- a/base/boot.jl +++ b/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}} diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl index aa2bb35117c86c..39fea90cbe9936 100644 --- a/base/compiler/abstractinterpretation.jl +++ b/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,7 +2365,7 @@ 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) @@ -2369,14 +2373,15 @@ function abstract_eval_statement_expr(interp::AbstractInterpreter, e::Expr, vtyp 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) diff --git a/base/compiler/effects.jl b/base/compiler/effects.jl index 7d09769e5b31bd..a8f5596a0af9e2 100644 --- a/base/compiler/effects.jl +++ b/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,20 +139,21 @@ 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, @@ -150,6 +161,7 @@ function Effects(e::Effects = _EFFECTS_UNKNOWN; 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,11 +193,13 @@ 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) @@ -192,6 +207,7 @@ 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 diff --git a/base/compiler/ssair/show.jl b/base/compiler/ssair/show.jl index 0f460c5676df9c..4553553829d0b2 100644 --- a/base/compiler/ssair/show.jl +++ b/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) diff --git a/base/compiler/tfuncs.jl b/base/compiler/tfuncs.jl index 55b231e004e3ed..8eb3a5f1b0a462 100644 --- a/base/compiler/tfuncs.jl +++ b/base/compiler/tfuncs.jl @@ -2303,33 +2303,37 @@ end function getfield_effects(๐•ƒ::AbstractLattice, arginfo::ArgInfo, @nospecialize(rt)) (;argtypes) = arginfo - # consistent if the argtype is immutable length(argtypes) < 3 && return EFFECTS_THROWS obj = argtypes[2] - isvarargtype(obj) && return Effects(EFFECTS_THROWS; consistent=ALWAYS_FALSE) + if isvarargtype(obj) + return Effects(EFFECTS_THROWS; + consistent=CONSISTENT_IF_INACCESSIBLEMEMONLY, + nothrow=false, + inaccessiblememonly=ALWAYS_FALSE, + noub=false) + end + # :consistent if the argtype is immutable consistent = (is_immutable_argtype(obj) || is_mutation_free_argtype(obj)) ? ALWAYS_TRUE : CONSISTENT_IF_INACCESSIBLEMEMONLY - # access to `isbitstype`-field initialized with undefined value leads to undefined behavior - # so should taint `:consistent`-cy while access to uninitialized non-`isbitstype` field - # throws `UndefRefError` so doesn't need to taint it + # taint `:noub` if accessing `isbitstype`-type object field that may be initialized + # with undefined value: note that we don't need to taint `:noub` if accessing + # uninitialized non-`isbitstype` field since it will simply throw `UndefRefError` # NOTE `getfield_notundefined` conservatively checks if this field is never initialized - # with undefined value so that we don't taint `:consistent`-cy too aggressively here - if !(length(argtypes) โ‰ฅ 3 && getfield_notundefined(obj, argtypes[3])) - consistent = ALWAYS_FALSE - end + # with undefined value to avoid tainting `:noub` too aggressively + noub = length(argtypes) โ‰ฅ 3 && getfield_notundefined(obj, argtypes[3]) bcheck = getfield_boundscheck(arginfo) nothrow = getfield_nothrow(๐•ƒ, arginfo, bcheck) if !nothrow if !(bcheck === :on || bcheck === :boundscheck) - # If we cannot independently prove inboundsness, taint consistency. - # The inbounds-ness assertion requires dynamic reachability, while - # :consistent needs to be true for all input values. + # If we cannot independently prove inboundsness, taint `:noub`. + # The inbounds-ness assertion requires dynamic reachability, + # while `:noub` needs to be true for all input values. # However, as a special exception, we do allow literal `:boundscheck`. - # `:consistent`-cy will be tainted in any caller using `@inbounds` based - # on the `:noinbounds` effect. - # N.B. We do not taint for `--check-bounds=no` here. That is handled - # in concrete evaluation. - consistent = ALWAYS_FALSE + # `:noub` will be tainted in any caller using `@inbounds` + # based on the `:noinbounds` effect. + # N.B. We do not taint for `--check-bounds=no` here. + # That is handled in concrete evaluation. + noub = false end end if hasintersect(widenconst(obj), Module) @@ -2339,7 +2343,7 @@ function getfield_effects(๐•ƒ::AbstractLattice, arginfo::ArgInfo, @nospecialize else inaccessiblememonly = INACCESSIBLEMEM_OR_ARGMEMONLY end - return Effects(EFFECTS_TOTAL; consistent, nothrow, inaccessiblememonly) + return Effects(EFFECTS_TOTAL; consistent, nothrow, inaccessiblememonly, noub) end function getglobal_effects(argtypes::Vector{Any}, @nospecialize(rt)) @@ -2371,8 +2375,15 @@ function builtin_effects(๐•ƒ::AbstractLattice, @nospecialize(f::Builtin), argin if f === getfield return getfield_effects(๐•ƒ, arginfo, rt) end - argtypes = arginfo.argtypes[2:end] + # TODO taint `:noub` for `arrayref` and `arrayset` here + + # if this builtin call deterministically throws, + # don't bother to taint the other effects other than :nothrow: + # note this is safe only if we accounted for :noub already + rt === Bottom && return EFFECTS_THROWS + + argtypes = arginfo.argtypes[2:end] if f === isdefined return isdefined_effects(๐•ƒ, argtypes) elseif f === getglobal @@ -2759,7 +2770,6 @@ function _hasmethod_tfunc(interp::AbstractInterpreter, argtypes::Vector{Any}, sv return CallMeta(rt, EFFECTS_TOTAL, NoCallInfo()) end - # N.B.: typename maps type equivalence classes to a single value function typename_static(@nospecialize(t)) t isa Const && return _typename(t.val) diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl index e867f5e9ad9dcd..43f0816048706f 100644 --- a/base/compiler/typeinfer.jl +++ b/base/compiler/typeinfer.jl @@ -497,6 +497,9 @@ function adjust_effects(sv::InferenceState) if is_effect_overridden(override, :inaccessiblememonly) ipo_effects = Effects(ipo_effects; inaccessiblememonly=ALWAYS_TRUE) end + if is_effect_overridden(override, :noub) + ipo_effects = Effects(ipo_effects; noub=true) + end end return ipo_effects diff --git a/base/essentials.jl b/base/essentials.jl index b652d626283360..f0dd92553a5d6b 100644 --- a/base/essentials.jl +++ b/base/essentials.jl @@ -208,7 +208,8 @@ macro _total_meta() #=:terminates_globally=#true, #=:terminates_locally=#false, #=:notaskstate=#true, - #=:inaccessiblememonly=#true)) + #=:inaccessiblememonly=#true, + #=:noub=#true)) end # can be used in place of `@assume_effects :foldable` (supposed to be used for bootstrapping) macro _foldable_meta() @@ -219,7 +220,8 @@ macro _foldable_meta() #=:terminates_globally=#true, #=:terminates_locally=#false, #=:notaskstate=#false, - #=:inaccessiblememonly=#true)) + #=:inaccessiblememonly=#true, + #=:noub=#true)) end # can be used in place of `@assume_effects :nothrow` (supposed to be used for bootstrapping) macro _nothrow_meta() @@ -230,7 +232,8 @@ macro _nothrow_meta() #=:terminates_globally=#false, #=:terminates_locally=#false, #=:notaskstate=#false, - #=:inaccessiblememonly=#false)) + #=:inaccessiblememonly=#false, + #=:noub=#false)) end # can be used in place of `@assume_effects :terminates_locally` (supposed to be used for bootstrapping) macro _terminates_locally_meta() @@ -241,7 +244,8 @@ macro _terminates_locally_meta() #=:terminates_globally=#false, #=:terminates_locally=#true, #=:notaskstate=#false, - #=:inaccessiblememonly=#false)) + #=:inaccessiblememonly=#false, + #=:noub=#false)) end # can be used in place of `@assume_effects :effect_free :terminates_locally` (supposed to be used for bootstrapping) macro _effect_free_terminates_locally_meta() @@ -252,7 +256,8 @@ macro _effect_free_terminates_locally_meta() #=:terminates_globally=#false, #=:terminates_locally=#true, #=:notaskstate=#false, - #=:inaccessiblememonly=#false)) + #=:inaccessiblememonly=#false, + #=:noub=#false)) end # another version of inlining that propagates an inbounds context diff --git a/base/expr.jl b/base/expr.jl index b1bf938ec7fac5..82e88f4ba97497 100644 --- a/base/expr.jl +++ b/base/expr.jl @@ -478,6 +478,7 @@ The following `setting`s are supported. - `:terminates_locally` - `:notaskstate` - `:inaccessiblememonly` +- `:noub` - `:foldable` - `:removable` - `:total` @@ -515,13 +516,6 @@ The `:consistent` setting asserts that for egal (`===`) inputs: even for the same world age (e.g. because one ran in the interpreter, while the other was optimized). -!!! note - The `:consistent`-cy assertion currently includes the assertion that the function - will not execute any undefined behavior (for any input). Note that undefined behavior - may technically cause the function to violate other effect assertions (such as - `:nothrow` or `:effect_free`) as well, but we do not model this, and all effects - except `:consistent` assume the absence of undefined behavior. - !!! note If `:consistent` functions terminate by throwing an exception, that exception itself is not required to meet the egality requirement specified above. @@ -641,6 +635,14 @@ global state or mutable memory pointed to by its arguments. !!! note This `:inaccessiblememonly` assertion covers any other methods called by the annotated method. +--- +## `:noub` + +The `:noub` setting asserts 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. + --- ## `:foldable` @@ -650,6 +652,7 @@ currently equivalent to the following `setting`s: - `:consistent` - `:effect_free` - `:terminates_globally` +- `:noub` !!! note This list in particular does not include `:nothrow`. The compiler will still @@ -682,6 +685,7 @@ the following other `setting`s: - `:terminates_globally` - `:notaskstate` - `:inaccessiblememonly` +- `:noub` !!! warning `:total` is a very strong assertion and will likely gain additional semantics @@ -712,8 +716,8 @@ macro assume_effects(args...) ex = nothing idx = length(args) end - (consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly) = - (false, false, false, false, false, false, false, false) + (consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly, noub) = + (false, false, false, false, false, false, false, false, false) for org_setting in args[1:idx] (setting, val) = compute_assumed_setting(org_setting) if setting === :consistent @@ -730,28 +734,29 @@ macro assume_effects(args...) notaskstate = val elseif setting === :inaccessiblememonly inaccessiblememonly = val + elseif setting === :noub + noub = val elseif setting === :foldable - consistent = effect_free = terminates_globally = val + consistent = effect_free = terminates_globally = noub = val elseif setting === :removable effect_free = nothrow = terminates_globally = val elseif setting === :total - consistent = effect_free = nothrow = terminates_globally = notaskstate = inaccessiblememonly = val + consistent = effect_free = nothrow = terminates_globally = notaskstate = inaccessiblememonly = noub = val else throw(ArgumentError("@assume_effects $org_setting not supported")) end end if is_function_def(inner) return esc(pushmeta!(ex, :purity, - consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly)) + consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly, noub)) elseif isexpr(ex, :macrocall) && ex.args[1] === Symbol("@ccall") ex.args[1] = GlobalRef(Base, Symbol("@ccall_effects")) insert!(ex.args, 3, Core.Compiler.encode_effects_override(Core.Compiler.EffectsOverride( - consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly, - ))) + consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly, noub))) return esc(ex) else # anonymous function case return Expr(:meta, Expr(:purity, - consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly)) + consistent, effect_free, nothrow, terminates_globally, terminates_locally, notaskstate, inaccessiblememonly, noub)) end end diff --git a/base/special/log.jl b/base/special/log.jl index 5d7f1c8118724d..e2db746caecee0 100644 --- a/base/special/log.jl +++ b/base/special/log.jl @@ -155,10 +155,10 @@ logbU(::Type{Float64},::Val{10}) = 0.4342944819032518 logbL(::Type{Float64},::Val{10}) = 1.098319650216765e-17 # Procedure 1 -# XXX we want to mark :consistent-cy here so that this function can be concrete-folded, +# XXX we want to mark :noub here so that this function can be concrete-folded, # because the effect analysis currently can't prove it in the presence of `@inbounds` or # `:boundscheck`, but still the access to `t_log_Float64` is really safe here -Base.@assume_effects :consistent @inline function log_proc1(y::Float64,mf::Float64,F::Float64,f::Float64,base=Val(:โ„ฏ)) +Base.@assume_effects :consistent :noub @inline function log_proc1(y::Float64,mf::Float64,F::Float64,f::Float64,base=Val(:โ„ฏ)) jp = unsafe_trunc(Int,128.0*F)-127 ## Steps 1 and 2 @@ -216,10 +216,10 @@ end end # Procedure 1 -# XXX we want to mark :consistent-cy here so that this function can be concrete-folded, +# XXX we want to mark :noub here so that this function can be concrete-folded, # because the effect analysis currently can't prove it in the presence of `@inbounds` or # `:boundscheck`, but still the access to `t_log_Float32` is really safe here -Base.@assume_effects :consistent @inline function log_proc1(y::Float32,mf::Float32,F::Float32,f::Float32,base=Val(:โ„ฏ)) +Base.@assume_effects :consistent :noub @inline function log_proc1(y::Float32,mf::Float32,F::Float32,f::Float32,base=Val(:โ„ฏ)) jp = unsafe_trunc(Int,128.0f0*F)-127 ## Steps 1 and 2 diff --git a/base/special/rem_pio2.jl b/base/special/rem_pio2.jl index de5c4151df2d01..3086f3ebc02c95 100644 --- a/base/special/rem_pio2.jl +++ b/base/special/rem_pio2.jl @@ -126,10 +126,10 @@ function fromfraction(f::Int128) return (z1,z2) end -# XXX we want to mark :consistent-cy here so that this function can be concrete-folded, +# XXX we want to mark :noub here so that this function can be concrete-folded, # because the effect analysis currently can't prove it in the presence of `@inbounds` or # `:boundscheck`, but still the accesses to `INV_2PI` are really safe here -Base.@assume_effects :consistent function paynehanek(x::Float64) +Base.@assume_effects :consistent :noub function paynehanek(x::Float64) # 1. Convert to form # # x = X * 2^k, diff --git a/src/julia.h b/src/julia.h index a4b61a4ebd9136..a96b4a1f5e5628 100644 --- a/src/julia.h +++ b/src/julia.h @@ -268,6 +268,7 @@ typedef union __jl_purity_overrides_t { uint8_t ipo_terminates_locally : 1; uint8_t ipo_notaskstate : 1; uint8_t ipo_inaccessiblememonly : 1; + uint8_t ipo_noub : 1; } overrides; uint8_t bits; } _jl_purity_overrides_t; diff --git a/src/method.c b/src/method.c index 06a05361a927d5..00eae940f9f882 100644 --- a/src/method.c +++ b/src/method.c @@ -328,7 +328,7 @@ static void jl_code_info_set_ir(jl_code_info_t *li, jl_expr_t *ir) else if (ma == (jl_value_t*)jl_no_constprop_sym) li->constprop = 2; else if (jl_is_expr(ma) && ((jl_expr_t*)ma)->head == jl_purity_sym) { - if (jl_expr_nargs(ma) == 7) { + if (jl_expr_nargs(ma) == 8) { li->purity.overrides.ipo_consistent = jl_unbox_bool(jl_exprarg(ma, 0)); li->purity.overrides.ipo_effect_free = jl_unbox_bool(jl_exprarg(ma, 1)); li->purity.overrides.ipo_nothrow = jl_unbox_bool(jl_exprarg(ma, 2)); @@ -336,6 +336,7 @@ static void jl_code_info_set_ir(jl_code_info_t *li, jl_expr_t *ir) li->purity.overrides.ipo_terminates_locally = jl_unbox_bool(jl_exprarg(ma, 4)); li->purity.overrides.ipo_notaskstate = jl_unbox_bool(jl_exprarg(ma, 5)); li->purity.overrides.ipo_inaccessiblememonly = jl_unbox_bool(jl_exprarg(ma, 6)); + li->purity.overrides.ipo_noub = jl_unbox_bool(jl_exprarg(ma, 7)); } } else diff --git a/test/compiler/effects.jl b/test/compiler/effects.jl index 60acac844cd7ce..2cdd10e7014044 100644 --- a/test/compiler/effects.jl +++ b/test/compiler/effects.jl @@ -337,7 +337,7 @@ invoke44763(x) = @invoke increase_x44763!(x) end |> only === Int @test x44763 == 0 -# `@inbounds`/`@boundscheck` expression should taint :consistent-cy correctly +# `@inbounds`/`@boundscheck` expression should taint :noub correctly # https://github.com/JuliaLang/julia/issues/48099 function A1_inbounds() r = 0 @@ -356,7 +356,7 @@ function f_boundscheck_elim(n) # to run the `@inbounds getfield(sin, 1)` that `ntuple` generates. ntuple(x->(@inbounds ()[x]), n) end -@test_broken !Core.Compiler.is_consistent(Base.infer_effects(f_boundscheck_elim, (Int,))) +@test !Core.Compiler.is_noub(Base.infer_effects(f_boundscheck_elim, (Int,))) @test Tuple{} <: only(Base.return_types(f_boundscheck_elim, (Int,))) # Test that purity modeling doesn't accidentally introduce new world age issues @@ -445,10 +445,8 @@ mutable struct SetfieldNothrow end f_setfield_nothrow() = SetfieldNothrow(0).x = 1 let effects = Base.infer_effects(f_setfield_nothrow, ()) - # Technically effect free even though we use the heap, since the - # object doesn't escape, but the compiler doesn't know that. - #@test Core.Compiler.is_effect_free(effects) @test Core.Compiler.is_nothrow(effects) + @test Core.Compiler.is_effect_free(effects) # see EFFECT_FREE_IF_INACCESSIBLEMEMONLY end # even if 2-arg `getfield` may throw, it should be still `:consistent` @@ -460,7 +458,7 @@ end Core.svec(nothing, 1, "foo") end |> Core.Compiler.is_consistent -# fastmath operations are inconsistent +# fastmath operations are in-`:consistent` @test !Core.Compiler.is_consistent(Base.infer_effects((a,b)->@fastmath(a+b), (Float64,Float64))) # issue 46122: @assume_effects for @ccall @@ -894,7 +892,7 @@ end |> Core.Compiler.is_foldable_nothrow @test Base.infer_effects(Tuple{Int64}) do i @inbounds (1,2,3)[i] -end |> !Core.Compiler.is_consistent +end |> !Core.Compiler.is_noub @test Base.infer_effects(Tuple{Tuple{Int64}}) do x @inbounds x[1] diff --git a/test/compiler/inference.jl b/test/compiler/inference.jl index 31a70929c7705e..06e8baa5a4d539 100644 --- a/test/compiler/inference.jl +++ b/test/compiler/inference.jl @@ -3450,8 +3450,12 @@ end @test Base.return_types(h33768, ()) == Any[Union{}] # constant prop of `Symbol("")` -f_getf_computed_symbol(p) = getfield(p, Symbol("first")) -@test Base.return_types(f_getf_computed_symbol, Tuple{Pair{Int8,String}}) == [Int8] +@test Base.return_types() do + Val(Symbol("julia")) +end |> only == Val{:julia} +@test Base.return_types() do p::Pair{Int8,String} + getfield(p, Symbol("first")) +end |> only == Int8 # issue #33954 struct X33954 diff --git a/test/math.jl b/test/math.jl index 8e6afba0acfceb..c6600f79b424c0 100644 --- a/test/math.jl +++ b/test/math.jl @@ -1540,24 +1540,31 @@ end @test (@allocated f44336()) == 0 end -# test constant-foldability -for fn in (:sin, :cos, :tan, :log, :log2, :log10, :log1p, :exponent, :sqrt, :cbrt, :fourthroot, - :asin, :atan, :acos, :sinh, :cosh, :tanh, :asinh, :acosh, :atanh, - :exp, :exp2, :exp10, :expm1 - ) - for T in (Float16, Float32, Float64) - f = getfield(@__MODULE__, fn) - eff = Base.infer_effects(f, (T,)) - @test Core.Compiler.is_foldable(eff) +@testset "constant-foldability of core math functions" begin + for fn in (:sin, :cos, :tan, :log, :log2, :log10, :log1p, :exponent, :sqrt, :cbrt, :fourthroot, + :asin, :atan, :acos, :sinh, :cosh, :tanh, :asinh, :acosh, :atanh, + :exp, :exp2, :exp10, :expm1 + ) + for T in (Float16, Float32, Float64) + @testset let f = getfield(@__MODULE__, fn), T = T + @test Core.Compiler.is_foldable(Base.infer_effects(f, (T,))) + end + end end -end -for T in (Float16, Float32, Float64) - for f in (exp, exp2, exp10) - @test Core.Compiler.is_removable_if_unused(Base.infer_effects(f, (T,))) +end; +@testset "removability of core math functions" begin + for T in (Float16, Float32, Float64) + @testset let T = T + for f in (exp, exp2, exp10) + @testset let f = f + @test Core.Compiler.is_removable_if_unused(Base.infer_effects(f, (T,))) + end + end + @test Core.Compiler.is_foldable(Base.infer_effects(^, (T,Int))) + @test Core.Compiler.is_foldable(Base.infer_effects(^, (T,T))) + end end - @test Core.Compiler.is_foldable(Base.infer_effects(^, (T,Int))) - @test Core.Compiler.is_foldable(Base.infer_effects(^, (T,T))) -end +end; @testset "BigInt Rationals with special funcs" begin @test sinpi(big(1//1)) == big(0.0)