diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 2a91bad7acbb2..a5f23697706f6 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -386,6 +386,11 @@ function collect_limitations!(@nospecialize(typ), sv::InferenceState)
     return typ
 end
 
+function collect_limitations!(@nospecialize(typ), ::IRCode)
+    @assert !isa(typ, LimitedAccuracy) "semi-concrete eval on recursive call graph"
+    return typ
+end
+
 function from_interconditional(@nospecialize(typ), sv::InferenceState, (; fargs, argtypes)::ArgInfo, @nospecialize(maybecondinfo))
     fargs === nothing && return widenconditional(typ)
     slot = 0
@@ -772,18 +777,33 @@ function _pure_eval_call(@nospecialize(f), arginfo::ArgInfo)
     return Const(value)
 end
 
+# - true: eligible for concrete evaluation
+# - false: eligible for semi-concrete evaluation
+# - nothing: not eligible for either of it
 function concrete_eval_eligible(interp::AbstractInterpreter,
     @nospecialize(f), result::MethodCallResult, arginfo::ArgInfo, sv::InferenceState)
-    # disable concrete-evaluation if this function call is tainted by some overlayed
+    # disable all concrete-evaluation if this function call is tainted by some overlayed
     # method since currently there is no direct way to execute overlayed methods
-    isoverlayed(method_table(interp)) && !is_nonoverlayed(result.effects) && return false
-    return f !== nothing &&
-           result.edge !== nothing &&
-           is_foldable(result.effects) &&
-           is_all_const_arg(arginfo)
+    isoverlayed(method_table(interp)) && !is_nonoverlayed(result.effects) && return nothing
+    if f !== nothing && result.edge !== nothing && is_foldable(result.effects)
+        if is_all_const_arg(arginfo)
+            return true
+        else
+            # TODO: is_nothrow is not an actual requirement here, this is just a hack
+            # to avoid entering semi concrete eval while it doesn't properly propagate no_throw
+            return is_nothrow(result.effects) ? false : nothing
+        end
+    else
+        return nothing
+    end
+    # if f !== nothing && result.edge !== nothing && is_foldable(result.effects)
+    #   return is_all_const_arg(arginfo)
+    # else
+    #   return nothing
+    # end
 end
 
-is_all_const_arg(arginfo::ArgInfo) = is_all_const_arg(arginfo.argtypes)
+is_all_const_arg((; argtypes)::ArgInfo) = is_all_const_arg(argtypes)
 function is_all_const_arg(argtypes::Vector{Any})
     for i = 2:length(argtypes)
         a = widenconditional(argtypes[i])
@@ -792,8 +812,8 @@ function is_all_const_arg(argtypes::Vector{Any})
     return true
 end
 
-collect_const_args(arginfo::ArgInfo) = collect_const_args(arginfo.argtypes)
-function collect_const_args(argtypes::Vector{Any})
+collect_const_args(arginfo::ArgInfo, start::Int=2) = collect_const_args(arginfo.argtypes, start)
+function collect_const_args(argtypes::Vector{Any}, start::Int=2)
     return Any[ let a = widenconditional(argtypes[i])
                     isa(a, Const) ? a.val :
                     isconstType(a) ? (a::DataType).parameters[1] :
@@ -801,6 +821,16 @@ function collect_const_args(argtypes::Vector{Any})
                 end for i = 2:length(argtypes) ]
 end
 
+function collect_semi_const_args(argtypes::Vector{Any}, start::Int=2)
+    return Any[ let a = widenconditional(argtypes[i])
+                    isa(a, Const) ? a.val :
+                    isconstType(a) ? (a::DataType).parameters[1] :
+                    isdefined(a, :instance) ? (a::DataType).instance :
+                    nothing
+                end for i in start:length(argtypes) ]
+end
+
+
 function invoke_signature(invokesig::Vector{Any})
     ft, argtyps = widenconst(invokesig[2]), instanceof_tfunc(widenconst(invokesig[3]))[1]
     return rewrap_unionall(Tuple{ft, unwrap_unionall(argtyps).parameters...}, argtyps)
@@ -808,24 +838,32 @@ end
 
 function concrete_eval_call(interp::AbstractInterpreter,
     @nospecialize(f), result::MethodCallResult, arginfo::ArgInfo, sv::InferenceState)
-    concrete_eval_eligible(interp, f, result, arginfo, sv) || return nothing
-    args = collect_const_args(arginfo)
-    world = get_world_counter(interp)
-    value = try
-        Core._call_in_world_total(world, f, args...)
-    catch
-        # The evaulation threw. By :consistent-cy, we're guaranteed this would have happened at runtime
-        return ConstCallResults(Union{}, ConcreteResult(result.edge::MethodInstance, result.effects), result.effects)
-    end
-    if is_inlineable_constant(value) || call_result_unused(sv)
-        # If the constant is not inlineable, still do the const-prop, since the
-        # code that led to the creation of the Const may be inlineable in the same
-        # circumstance and may be optimizable.
-        return ConstCallResults(Const(value), ConcreteResult(result.edge::MethodInstance, EFFECTS_TOTAL, value), EFFECTS_TOTAL)
+    eligible = concrete_eval_eligible(interp, f, result, arginfo, sv)
+    eligible === nothing && return false
+    if eligible
+        args = collect_const_args(arginfo)
+        world = get_world_counter(interp)
+        value = try
+            Core._call_in_world_total(world, f, args...)
+        catch
+            # The evaulation threw. By :consistent-cy, we're guaranteed this would have happened at runtime
+            return ConstCallResults(Union{}, ConcreteResult(result.edge::MethodInstance, result.effects), result.effects)
+        end
+        if is_inlineable_constant(value) || call_result_unused(sv)
+            # If the constant is not inlineable, still do the const-prop, since the
+            # code that led to the creation of the Const may be inlineable in the same
+            # circumstance and may be optimizable.
+            return ConstCallResults(Const(value), ConcreteResult(result.edge::MethodInstance, EFFECTS_TOTAL, value), EFFECTS_TOTAL)
+        end
+        return false
+    else # eligible for semi-concrete evaluation
+        return true
     end
-    return nothing
 end
 
+has_conditional(argtypes::Vector{Any}) = _any(@nospecialize(x)->isa(x, Conditional), argtypes)
+has_conditional((; argtypes)::ArgInfo) = has_conditional(argtypes)
+
 function const_prop_enabled(interp::AbstractInterpreter, sv::InferenceState, match::MethodMatch)
     if !InferenceParams(interp).ipo_constant_propagation
         add_remark!(interp, sv, "[constprop] Disabled by parameter")
@@ -854,13 +892,27 @@ function abstract_call_method_with_const_args(interp::AbstractInterpreter, resul
     if !const_prop_enabled(interp, sv, match)
         return nothing
     end
-    val = concrete_eval_call(interp, f, result, arginfo, sv)
-    if val !== nothing
-        add_backedge!(val.const_result.mi, sv)
-        return val
+    res = concrete_eval_call(interp, f, result, arginfo, sv)
+    if isa(res, ConstCallResults)
+        add_backedge!(res.const_result.mi, sv)
+        return res
     end
     mi = maybe_get_const_prop_profitable(interp, result, f, arginfo, match, sv)
     mi === nothing && return nothing
+    # try semi-concrete evaluation
+    if res::Bool && !has_conditional(arginfo)
+        mi_cache = WorldView(code_cache(interp), sv.world)
+        code = get(mi_cache, mi, nothing)
+        if code !== nothing
+            ir = codeinst_to_ir(interp, code)
+            if isa(ir, IRCode)
+                T = ir_abstract_constant_propagation(interp, mi_cache, sv, mi, ir, arginfo.argtypes)
+                if !isa(T, Type) || typeintersect(T, Bool) === Union{}
+                    return ConstCallResults(T, SemiConcreteResult(mi, ir, result.effects), result.effects)
+                end
+            end
+        end
+    end
     # try constant prop'
     inf_cache = get_inference_cache(interp)
     inf_result = cache_lookup(mi, arginfo.argtypes, inf_cache)
@@ -1129,6 +1181,7 @@ end
 
 # This is only for use with `Conditional`.
 # In general, usage of this is wrong.
+ssa_def_slot(@nospecialize(arg), sv::IRCode) = nothing
 function ssa_def_slot(@nospecialize(arg), sv::InferenceState)
     code = sv.src.code
     init = sv.currpc
@@ -1183,7 +1236,8 @@ end
 # refine its type to an array of element types.
 # Union of Tuples of the same length is converted to Tuple of Unions.
 # returns an array of types
-function precise_container_type(interp::AbstractInterpreter, @nospecialize(itft), @nospecialize(typ), sv::InferenceState)
+function precise_container_type(interp::AbstractInterpreter, @nospecialize(itft), @nospecialize(typ),
+                                sv::Union{InferenceState, IRCode})
     if isa(typ, PartialStruct) && typ.typ.name === Tuple.name
         return typ.fields, nothing
     end
@@ -1248,7 +1302,7 @@ function precise_container_type(interp::AbstractInterpreter, @nospecialize(itft)
 end
 
 # simulate iteration protocol on container type up to fixpoint
-function abstract_iteration(interp::AbstractInterpreter, @nospecialize(itft), @nospecialize(itertype), sv::InferenceState)
+function abstract_iteration(interp::AbstractInterpreter, @nospecialize(itft), @nospecialize(itertype), sv::Union{InferenceState, IRCode})
     if isa(itft, Const)
         iteratef = itft.val
     else
@@ -1334,7 +1388,7 @@ function abstract_iteration(interp::AbstractInterpreter, @nospecialize(itft), @n
 end
 
 # do apply(af, fargs...), where af is a function value
-function abstract_apply(interp::AbstractInterpreter, argtypes::Vector{Any}, sv::InferenceState,
+function abstract_apply(interp::AbstractInterpreter, argtypes::Vector{Any}, sv::Union{InferenceState, IRCode},
                         max_methods::Int = get_max_methods(sv.mod, interp))
     itft = argtype_by_index(argtypes, 2)
     aft = argtype_by_index(argtypes, 3)
@@ -1450,7 +1504,7 @@ function argtype_tail(argtypes::Vector{Any}, i::Int)
 end
 
 function abstract_call_builtin(interp::AbstractInterpreter, f::Builtin, (; fargs, argtypes)::ArgInfo,
-                               sv::InferenceState, max_methods::Int)
+                               sv::Union{InferenceState, IRCode}, max_methods::Int)
     @nospecialize f
     la = length(argtypes)
     if f === Core.ifelse && fargs isa Vector{Any} && la == 4
@@ -1678,8 +1732,8 @@ end
 
 # call where the function is known exactly
 function abstract_call_known(interp::AbstractInterpreter, @nospecialize(f),
-        arginfo::ArgInfo, sv::InferenceState,
-        max_methods::Int = get_max_methods(f, sv.mod, interp))
+        arginfo::ArgInfo, sv::Union{InferenceState, IRCode},
+        max_methods::Int = isa(sv, InferenceState) ? get_max_methods(f, sv.mod, interp) : 0)
     (; fargs, argtypes) = arginfo
     la = length(argtypes)
 
@@ -1829,7 +1883,7 @@ end
 
 # call where the function is any lattice element
 function abstract_call(interp::AbstractInterpreter, arginfo::ArgInfo,
-                       sv::InferenceState, max_methods::Union{Int, Nothing} = nothing)
+                       sv::Union{InferenceState, IRCode}, max_methods::Union{Int, Nothing} = isa(sv, IRCode) ? 0 : nothing)
     argtypes = arginfo.argtypes
     ft = argtypes[1]
     f = singleton_type(ft)
@@ -1902,7 +1956,7 @@ function abstract_eval_cfunction(interp::AbstractInterpreter, e::Expr, vtypes::V
     nothing
 end
 
-function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::VarTable, sv::InferenceState)
+function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, sv::Union{InferenceState, IRCode})
     head = e.head
     if head === :static_parameter
         n = e.args[1]::Int
@@ -1920,13 +1974,20 @@ function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::
     return Any
 end
 
-function abstract_eval_special_value(interp::AbstractInterpreter, @nospecialize(e), vtypes::VarTable, sv::InferenceState)
+function abstract_eval_special_value(interp::AbstractInterpreter, @nospecialize(e), vtypes::Union{VarTable, Nothing}, sv::Union{InferenceState, IRCode})
     if isa(e, QuoteNode)
         return Const(e.value)
     elseif isa(e, SSAValue)
         return abstract_eval_ssavalue(e, sv)
-    elseif isa(e, SlotNumber) || isa(e, Argument)
+    elseif isa(e, SlotNumber)
         return vtypes[slot_id(e)].typ
+    elseif isa(e, Argument)
+        if !isa(vtypes, Nothing)
+            return vtypes[slot_id(e)].typ
+        else
+            @assert isa(sv, IRCode)
+            return sv.argtypes[e.n]
+        end
     elseif isa(e, GlobalRef)
         return abstract_eval_global(interp, e.mod, e.name, sv)
     end
@@ -1934,16 +1995,16 @@ function abstract_eval_special_value(interp::AbstractInterpreter, @nospecialize(
     return Const(e)
 end
 
-function abstract_eval_value(interp::AbstractInterpreter, @nospecialize(e), vtypes::VarTable, sv::InferenceState)
+function abstract_eval_value(interp::AbstractInterpreter, @nospecialize(e), vtypes::Union{VarTable, Nothing}, sv::Union{InferenceState, IRCode})
     if isa(e, Expr)
-        return abstract_eval_value_expr(interp, e, vtypes, sv)
+        return abstract_eval_value_expr(interp, e, sv)
     else
         typ = abstract_eval_special_value(interp, e, vtypes, sv)
         return collect_limitations!(typ, sv)
     end
 end
 
-function collect_argtypes(interp::AbstractInterpreter, ea::Vector{Any}, vtypes::VarTable, sv::InferenceState)
+function collect_argtypes(interp::AbstractInterpreter, ea::Vector{Any}, vtypes::Union{VarTable, Nothing}, sv::Union{InferenceState, IRCode})
     n = length(ea)
     argtypes = Vector{Any}(undef, n)
     @inbounds for i = 1:n
@@ -1956,30 +2017,30 @@ function collect_argtypes(interp::AbstractInterpreter, ea::Vector{Any}, vtypes::
     return argtypes
 end
 
-function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e), vtypes::VarTable, sv::InferenceState)
-    if !isa(e, Expr)
-        if isa(e, PhiNode)
-            rt = Union{}
-            for val in e.values
-                rt = tmerge(rt, abstract_eval_special_value(interp, val, vtypes, sv))
-            end
-            return rt
-        end
-        return abstract_eval_special_value(interp, e, vtypes, sv)
-    end
-    e = e::Expr
+struct RTEffects
+    rt
+    effects::Effects
+    RTEffects(@nospecialize(rt), effects::Effects) = new(rt, effects)
+end
+
+function abstract_eval_statement_expr(interp::AbstractInterpreter, e::Expr, vtypes::Union{VarTable, Nothing},
+                                      sv::Union{InferenceState, IRCode}, mi::Union{MethodInstance, Nothing})::RTEffects
+    effects = EFFECTS_UNKNOWN
     ehead = e.head
     if ehead === :call
         ea = e.args
         argtypes = collect_argtypes(interp, ea, vtypes, sv)
         if argtypes === nothing
-            t = Bottom
+            rt = Bottom
+            effects = Effects()
         else
-            callinfo = abstract_call(interp, ArgInfo(ea, argtypes), sv)
-            merge_effects!(interp, sv, callinfo.effects)
-            sv.stmt_info[sv.currpc] = callinfo.info
-            t = callinfo.rt
+            (; rt, effects, info) = abstract_call(interp, ArgInfo(ea, argtypes), sv)
+            merge_effects!(interp, sv, effects)
+            if isa(sv, InferenceState)
+                sv.stmt_info[sv.currpc] = info
+            end
         end
+        t = rt
     elseif ehead === :new
         t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
         nothrow = true
@@ -2037,7 +2098,8 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             consistent = ALWAYS_FALSE
             nothrow = false
         end
-        merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; consistent, nothrow))
+        effects = Effects(EFFECTS_TOTAL; consistent, nothrow)
+        merge_effects!(interp, sv, effects)
     elseif ehead === :splatnew
         t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
         nothrow = false # TODO: More precision
@@ -2055,19 +2117,22 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             end
         end
         consistent = !ismutabletype(t) ? ALWAYS_TRUE : CONSISTENT_IF_NOTRETURNED
-        merge_effects!(interp, sv, Effects(EFFECTS_TOTAL; consistent, nothrow))
+        effects = Effects(EFFECTS_TOTAL; consistent, nothrow)
+        merge_effects!(interp, sv, effects)
     elseif ehead === :new_opaque_closure
-        merge_effects!(interp, sv, Effects()) # TODO
         t = Union{}
+        effects = Effects() # TODO
+        merge_effects!(interp, sv, effects)
         if length(e.args) >= 4
             ea = e.args
             argtypes = collect_argtypes(interp, ea, vtypes, sv)
             if argtypes === nothing
                 t = Bottom
             else
+                mi′ = isa(sv, InferenceState) ? sv.linfo : mi
                 t = _opaque_closure_tfunc(argtypes[1], argtypes[2], argtypes[3],
-                    argtypes[4], argtypes[5:end], sv.linfo)
-                if isa(t, PartialOpaque)
+                    argtypes[4], argtypes[5:end], mi′)
+                if isa(t, PartialOpaque) && isa(sv, InferenceState)
                     # Infer this now so that the specialization is available to
                     # optimization.
                     argtypes = most_general_argtypes(t)
@@ -2079,39 +2144,22 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             end
         end
     elseif ehead === :foreigncall
-        abstract_eval_value(interp, e.args[1], vtypes, sv)
-        t = sp_type_rewrap(e.args[2], sv.linfo, true)
-        for i = 3:length(e.args)
-            if abstract_eval_value(interp, e.args[i], vtypes, sv) === Bottom
-                @goto always_throw
-            end
-        end
-        effects = foreigncall_effects(e) do @nospecialize x
-            abstract_eval_value(interp, x, vtypes, sv)
-        end
-        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)
-        end
+        (;rt, effects) = abstract_eval_foreigncall(interp, e, vtypes, sv, mi)
+        t = rt
         merge_effects!(interp, sv, effects)
     elseif ehead === :cfunction
-        merge_effects!(interp, sv, EFFECTS_UNKNOWN)
+        effects = EFFECTS_UNKNOWN
+        merge_effects!(interp, sv, effects)
         t = e.args[1]
         isa(t, Type) || (t = Any)
         abstract_eval_cfunction(interp, e, vtypes, sv)
     elseif ehead === :method
-        merge_effects!(interp, sv, EFFECTS_UNKNOWN)
         t = (length(e.args) == 1) ? Any : Nothing
+        effects = EFFECTS_UNKNOWN
+        merge_effects!(interp, sv, effects)
     elseif ehead === :copyast
-        merge_effects!(interp, sv, EFFECTS_UNKNOWN)
+        effects = EFFECTS_UNKNOWN
+        merge_effects!(interp, sv, effects)
         t = abstract_eval_value(interp, e.args[1], vtypes, sv)
         if t isa Const && t.val isa Expr
             # `copyast` makes copies of Exprs
@@ -2149,24 +2197,69 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
     elseif false
         @label always_throw
         t = Bottom
-        merge_effects!(interp, sv, EFFECTS_THROWS)
+        effects = EFFECTS_THROWS
+        merge_effects!(interp, sv, effects)
     else
-        t = abstract_eval_value_expr(interp, e, vtypes, sv)
+        t = abstract_eval_value_expr(interp, e, sv)
     end
-    @assert !isa(t, TypeVar) "unhandled TypeVar"
-    if isa(t, DataType) && isdefined(t, :instance)
-        # replace singleton types with their equivalent Const object
-        t = Const(t.instance)
+    return RTEffects(t, effects)
+end
+
+function abstract_eval_foreigncall(interp::AbstractInterpreter, e::Expr, vtypes::Union{VarTable, Nothing}, sv::Union{InferenceState, IRCode}, mi::Union{MethodInstance, Nothing}=nothing)
+    abstract_eval_value(interp, e.args[1], vtypes, sv)
+    mi′ = isa(sv, InferenceState) ? sv.linfo : mi
+    t = sp_type_rewrap(e.args[2], mi′, true)
+    for i = 3:length(e.args)
+        if abstract_eval_value(interp, e.args[i], vtypes, sv) === Bottom
+            return RTEffects(Bottom, EFFECTS_THROWS)
+        end
+    end
+    effects = foreigncall_effects(e) do @nospecialize x
+        abstract_eval_value(interp, x, vtypes, sv)
+    end
+    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)
+    end
+    return RTEffects(t, effects)
+end
+
+function abstract_eval_phi(interp::AbstractInterpreter, phi::PhiNode, vtypes::Union{VarTable, Nothing}, sv::Union{InferenceState, IRCode})
+    rt = Union{}
+    for val in phi.values
+        rt = tmerge(rt, abstract_eval_special_value(interp, val, vtypes, sv))
+    end
+    return rt
+end
+
+function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e), vtypes::VarTable, sv::InferenceState)
+    if !isa(e, Expr)
+        if isa(e, PhiNode)
+            return abstract_eval_phi(interp, e, vtypes, sv)
+        end
+        return abstract_eval_special_value(interp, e, vtypes, sv)
     end
+    (;rt, effects) = abstract_eval_statement_expr(interp, e, vtypes, sv, nothing)
+    e = e::Expr
+    @assert !isa(rt, TypeVar) "unhandled TypeVar"
+    rt = maybe_singleton_const(rt)
     if !isempty(sv.pclimitations)
-        if t isa Const || t === Bottom
+        if rt isa Const || rt === Union{}
             empty!(sv.pclimitations)
         else
-            t = LimitedAccuracy(t, sv.pclimitations)
+            rt = LimitedAccuracy(rt, sv.pclimitations)
             sv.pclimitations = IdSet{InferenceState}()
         end
     end
-    return t
+    return rt
 end
 
 function abstract_eval_global(M::Module, s::Symbol)
@@ -2178,7 +2271,7 @@ function abstract_eval_global(M::Module, s::Symbol)
     return ty
 end
 
-function abstract_eval_global(interp::AbstractInterpreter, M::Module, s::Symbol, frame::InferenceState)
+function abstract_eval_global(interp::AbstractInterpreter, M::Module, s::Symbol, frame::Union{InferenceState, IRCode})
     rt = abstract_eval_global(M, s)
     consistent = inaccessiblememonly = ALWAYS_FALSE
     nothrow = false
diff --git a/base/compiler/compiler.jl b/base/compiler/compiler.jl
index 5b3a83c325499..fd85266823ea2 100644
--- a/base/compiler/compiler.jl
+++ b/base/compiler/compiler.jl
@@ -164,7 +164,7 @@ include("compiler/stmtinfo.jl")
 
 include("compiler/abstractinterpretation.jl")
 include("compiler/typeinfer.jl")
-include("compiler/optimize.jl") # TODO: break this up further + extract utilities
+include("compiler/optimize.jl")
 
 # required for bootstrap because sort.jl uses extrema
 # to decide whether to dispatch to counting sort.
diff --git a/base/compiler/inferenceresult.jl b/base/compiler/inferenceresult.jl
index 1e570b943d968..615d42e7fadb9 100644
--- a/base/compiler/inferenceresult.jl
+++ b/base/compiler/inferenceresult.jl
@@ -16,6 +16,36 @@ function is_forwardable_argtype(@nospecialize x)
            isa(x, PartialOpaque)
 end
 
+function va_process_argtypes(given_argtypes::Vector{Any}, mi::MethodInstance,
+                             condargs::Union{Vector{Tuple{Int,Int}}, Nothing}=nothing)
+    isva = mi.def.isva
+    nargs = Int(mi.def.nargs)
+    if isva || isvarargtype(given_argtypes[end])
+        isva_given_argtypes = Vector{Any}(undef, nargs)
+        for i = 1:(nargs - isva)
+            isva_given_argtypes[i] = argtype_by_index(given_argtypes, i)
+        end
+        if isva
+            if length(given_argtypes) < nargs && isvarargtype(given_argtypes[end])
+                last = length(given_argtypes)
+            else
+                last = nargs
+            end
+            isva_given_argtypes[nargs] = tuple_tfunc(given_argtypes[last:end])
+            # invalidate `Conditional` imposed on varargs
+            if condargs !== nothing
+                for (slotid, i) in condargs
+                    if slotid ≥ last
+                        isva_given_argtypes[i] = widenconditional(isva_given_argtypes[i])
+                    end
+                end
+            end
+        end
+        return isva_given_argtypes
+    end
+    return given_argtypes
+end
+
 # In theory, there could be a `cache` containing a matching `InferenceResult`
 # for the provided `linfo` and `given_argtypes`. The purpose of this function is
 # to return a valid value for `cache_lookup(linfo, argtypes, cache).argtypes`,
@@ -56,30 +86,7 @@ function matching_cache_argtypes(
         end
         given_argtypes[i] = widenconditional(argtype)
     end
-    isva = def.isva
-    if isva || isvarargtype(given_argtypes[end])
-        isva_given_argtypes = Vector{Any}(undef, nargs)
-        for i = 1:(nargs - isva)
-            isva_given_argtypes[i] = argtype_by_index(given_argtypes, i)
-        end
-        if isva
-            if length(given_argtypes) < nargs && isvarargtype(given_argtypes[end])
-                last = length(given_argtypes)
-            else
-                last = nargs
-            end
-            isva_given_argtypes[nargs] = tuple_tfunc(given_argtypes[last:end])
-            # invalidate `Conditional` imposed on varargs
-            if condargs !== nothing
-                for (slotid, i) in condargs
-                    if slotid ≥ last
-                        isva_given_argtypes[i] = widenconditional(isva_given_argtypes[i])
-                    end
-                end
-            end
-        end
-        given_argtypes = isva_given_argtypes
-    end
+    given_argtypes = va_process_argtypes(given_argtypes, linfo, condargs)
     @assert length(given_argtypes) == nargs
     for i in 1:nargs
         given_argtype = given_argtypes[i]
diff --git a/base/compiler/inferencestate.jl b/base/compiler/inferencestate.jl
index b96854ca03ed6..11443cc6fde78 100644
--- a/base/compiler/inferencestate.jl
+++ b/base/compiler/inferencestate.jl
@@ -80,6 +80,12 @@ function in(idx::Int, bsbmp::BitSetBoundedMinPrioritySet)
     return idx in bsbmp.elems
 end
 
+function append!(bsbmp::BitSetBoundedMinPrioritySet, itr)
+    for val in itr
+        push!(bsbmp, val)
+    end
+end
+
 mutable struct InferenceState
     #= information about this method instance =#
     linfo::MethodInstance
@@ -209,8 +215,10 @@ Effects(state::InferenceState) = state.ipo_effects
 function merge_effects!(::AbstractInterpreter, caller::InferenceState, effects::Effects)
     caller.ipo_effects = merge_effects(caller.ipo_effects, effects)
 end
+
 merge_effects!(interp::AbstractInterpreter, caller::InferenceState, callee::InferenceState) =
     merge_effects!(interp, caller, Effects(callee))
+merge_effects!(interp::AbstractInterpreter, caller::IRCode, effects::Effects) = nothing
 
 is_effect_overridden(sv::InferenceState, effect::Symbol) = is_effect_overridden(sv.linfo, effect)
 function is_effect_overridden(linfo::MethodInstance, effect::Symbol)
@@ -226,15 +234,15 @@ function InferenceResult(
     return _InferenceResult(linfo, arginfo)
 end
 
-add_remark!(::AbstractInterpreter, sv::InferenceState, remark) = return
+add_remark!(::AbstractInterpreter, sv::Union{InferenceState, IRCode}, remark) = return
 
-function bail_out_toplevel_call(::AbstractInterpreter, @nospecialize(callsig), sv::InferenceState)
-    return sv.restrict_abstract_call_sites && !isdispatchtuple(callsig)
+function bail_out_toplevel_call(::AbstractInterpreter, @nospecialize(callsig), sv::Union{InferenceState, IRCode})
+    return isa(sv, InferenceState) && sv.restrict_abstract_call_sites && !isdispatchtuple(callsig)
 end
-function bail_out_call(::AbstractInterpreter, @nospecialize(rt), sv::InferenceState)
+function bail_out_call(::AbstractInterpreter, @nospecialize(rt), sv::Union{InferenceState, IRCode})
     return rt === Any
 end
-function bail_out_apply(::AbstractInterpreter, @nospecialize(rt), sv::InferenceState)
+function bail_out_apply(::AbstractInterpreter, @nospecialize(rt), sv::Union{InferenceState, IRCode})
     return rt === Any
 end
 
diff --git a/base/compiler/ssair/EscapeAnalysis/EscapeAnalysis.jl b/base/compiler/ssair/EscapeAnalysis/EscapeAnalysis.jl
index 272ea0e8edbbc..7785e61f31e09 100644
--- a/base/compiler/ssair/EscapeAnalysis/EscapeAnalysis.jl
+++ b/base/compiler/ssair/EscapeAnalysis/EscapeAnalysis.jl
@@ -31,7 +31,8 @@ import Core.Compiler: # Core.Compiler specific definitions
     isbitstype, isexpr, is_meta_expr_head, println, widenconst, argextype, singleton_type,
     fieldcount_noerror, try_compute_field, try_compute_fieldidx, hasintersect, ⊑,
     intrinsic_nothrow, array_builtin_common_typecheck, arrayset_typecheck,
-    setfield!_nothrow, alloc_array_ndims, check_effect_free!
+    setfield!_nothrow, alloc_array_ndims, stmt_effect_free, check_effect_free!,
+    SemiConcreteResult
 
 include(x) = _TOP_MOD.include(@__MODULE__, x)
 if _TOP_MOD === Core.Compiler
diff --git a/base/compiler/ssair/EscapeAnalysis/interprocedural.jl b/base/compiler/ssair/EscapeAnalysis/interprocedural.jl
index 5d75db990e6f4..5b5110fdaec08 100644
--- a/base/compiler/ssair/EscapeAnalysis/interprocedural.jl
+++ b/base/compiler/ssair/EscapeAnalysis/interprocedural.jl
@@ -6,7 +6,7 @@ import Core.Compiler:
     call_sig, argtypes_to_type, is_builtin, is_return_type, istopfunction, validate_sparams,
     specialize_method, invoke_rewrite
 
-const Linfo = Union{MethodInstance,InferenceResult}
+const Linfo = Union{MethodInstance,InferenceResult,SemiConcreteResult}
 struct CallInfo
     linfos::Vector{Linfo}
     nothrow::Bool
diff --git a/base/compiler/ssair/driver.jl b/base/compiler/ssair/driver.jl
index 1b6d0a0dfce4c..d9d32e66466c4 100644
--- a/base/compiler/ssair/driver.jl
+++ b/base/compiler/ssair/driver.jl
@@ -20,3 +20,4 @@ include("compiler/ssair/verify.jl")
 include("compiler/ssair/legacy.jl")
 include("compiler/ssair/EscapeAnalysis/EscapeAnalysis.jl")
 include("compiler/ssair/passes.jl")
+include("compiler/ssair/irinterp.jl")
diff --git a/base/compiler/ssair/inlining.jl b/base/compiler/ssair/inlining.jl
index 84864404f008e..c611a0ab5535a 100644
--- a/base/compiler/ssair/inlining.jl
+++ b/base/compiler/ssair/inlining.jl
@@ -1371,6 +1371,8 @@ function compute_inlining_cases(info::ConstCallInfo,
                 push!(cases, InliningCase(result.mi.specTypes, case))
             elseif isa(result, ConstPropResult)
                 handled_all_cases &= handle_const_prop_result!(result, argtypes, flag, state, cases, #=allow_abstract=#true)
+            elseif isa(result, SemiConcreteResult)
+                handled_all_cases &= handle_semi_concrete_result!(result, cases, #=allow_abstract=#true)
             else
                 @assert result === nothing
                 handled_all_cases &= handle_match!(match, argtypes, flag, state, cases, #=allow_abstract=#true, #=allow_typevars=#false)
@@ -1434,6 +1436,15 @@ function handle_const_prop_result!(
     return true
 end
 
+function handle_semi_concrete_result!(result::SemiConcreteResult, cases::Vector{InliningCase}, allow_abstract::Bool = false)
+    mi = result.mi
+    spec_types = mi.specTypes
+    allow_abstract || isdispatchtuple(spec_types) || return false
+    validate_sparams(mi.sparam_vals) || return false
+    push!(cases, InliningCase(spec_types, InliningTodo(mi, result.ir, result.effects)))
+    return true
+end
+
 function concrete_result_item(result::ConcreteResult, state::InliningState)
     if !isdefined(result, :result) || !is_inlineable_constant(result.result)
         case = compileable_specialization(state.et, result.mi, result.effects)
diff --git a/base/compiler/ssair/ir.jl b/base/compiler/ssair/ir.jl
index aee3f8f1ff6fe..d422aca269ae2 100644
--- a/base/compiler/ssair/ir.jl
+++ b/base/compiler/ssair/ir.jl
@@ -1050,15 +1050,22 @@ function renumber_ssa2!(@nospecialize(stmt), ssanums::Vector{Any}, used_ssas::Ve
 end
 
 # Used in inlining before we start compacting - Only works at the CFG level
-function kill_edge!(bbs::Vector{BasicBlock}, from::Int, to::Int)
+function kill_edge!(bbs::Vector{BasicBlock}, from::Int, to::Int, callback=nothing)
     preds, succs = bbs[to].preds, bbs[from].succs
     deleteat!(preds, findfirst(x->x === from, preds)::Int)
     deleteat!(succs, findfirst(x->x === to, succs)::Int)
     if length(preds) == 0
         for succ in copy(bbs[to].succs)
-            kill_edge!(bbs, to, succ)
+            kill_edge!(bbs, to, succ, callback)
         end
     end
+    if callback !== nothing
+        callback(from, to)
+    end
+end
+
+function kill_edge!(ir::IRCode, from::Int, to::Int, callback=nothing)
+    kill_edge!(ir.cfg.blocks, from, to, callback)
 end
 
 # N.B.: from and to are non-renamed indices
diff --git a/base/compiler/ssair/irinterp.jl b/base/compiler/ssair/irinterp.jl
new file mode 100644
index 0000000000000..08754900eddb1
--- /dev/null
+++ b/base/compiler/ssair/irinterp.jl
@@ -0,0 +1,401 @@
+
+function codeinst_to_ir(interp::AbstractInterpreter, code::CodeInstance)
+    src = code.inferred
+    mi = code.def
+
+    if isa(src, Vector{UInt8})
+        src = ccall(:jl_uncompress_ir, Any, (Any, Ptr{Cvoid}, Any), mi.def, C_NULL, src)::CodeInfo
+    end
+
+    isa(src, CodeInfo) || return src
+
+    return inflate_ir(src, mi)
+end
+
+function abstract_call_gf_by_type(interp::AbstractInterpreter, @nospecialize(f),
+                                  arginfo::ArgInfo, @nospecialize(atype),
+                                  sv::IRCode, max_methods::Int)
+    return CallMeta(Any, Effects(), false)
+end
+
+mutable struct TwoPhaseVectorView <: AbstractVector{Int}
+    const data::Vector{Int}
+    count::Int
+    const range::UnitRange{Int}
+end
+size(tpvv::TwoPhaseVectorView) = (tpvv.count,)
+function getindex(tpvv::TwoPhaseVectorView, i::Int)
+    checkbounds(tpvv, i)
+    @inbounds tpvv.data[first(tpvv.range) + i - 1]
+end
+function push!(tpvv::TwoPhaseVectorView, v::Int)
+    tpvv.count += 1
+    tpvv.data[first(tpvv.range) + tpvv.count - 1] = v
+    return nothing
+end
+
+"""
+    mutable struct TwoPhaseDefUseMap
+
+This struct is intended as a memory- and GC-pressure-efficient mechanism
+for incrementally computing def-use maps. The idea is that the def-use map
+is constructed into two passes over the IR. In the first, we simply count the
+the number of uses, computing the number of uses for each def as well as the
+total number of uses. In the second pass, we actually fill in the def-use
+information.
+
+The idea is that either of these two phases can be combined with other useful
+work that needs to scan the instruction stream anyway, while avoiding the
+significant allocation pressure of e.g. allocating an array for every SSA value
+or attempting to dynamically move things around as new uses are discovered.
+
+The def-use map is presented as a vector of vectors. For every def, indexing
+into the map will return a vector of uses.
+"""
+mutable struct TwoPhaseDefUseMap <: AbstractVector{TwoPhaseVectorView}
+    ssa_uses::Vector{Int}
+    data::Vector{Int}
+    complete::Bool
+end
+
+function complete!(tpdum::TwoPhaseDefUseMap)
+    cumsum = 0
+    for i = 1:length(tpdum.ssa_uses)
+        this_val = cumsum + 1
+        cumsum += tpdum.ssa_uses[i]
+        tpdum.ssa_uses[i] = this_val
+    end
+    resize!(tpdum.data, cumsum)
+    fill!(tpdum.data, 0)
+    tpdum.complete = true
+end
+
+function TwoPhaseDefUseMap(nssas::Int)
+    ssa_uses = zeros(Int, nssas)
+    data = Int[]
+    complete = false
+    return TwoPhaseDefUseMap(ssa_uses, data, complete)
+end
+
+function count!(tpdum::TwoPhaseDefUseMap, arg::SSAValue)
+    @assert !tpdum.complete
+    tpdum.ssa_uses[arg.id] += 1
+end
+
+function kill_def_use!(tpdum::TwoPhaseDefUseMap, def::Int, use::Int)
+    if !tpdum.complete
+        tpdum.ssa_uses[def] -= 1
+    else
+        @assert false && "TODO"
+    end
+end
+kill_def_use!(tpdum::TwoPhaseDefUseMap, def::SSAValue, use::Int) =
+    kill_def_use!(tpdum, def.id, use)
+
+function getindex(tpdum::TwoPhaseDefUseMap, idx::Int)
+    @assert tpdum.complete
+    range = tpdum.ssa_uses[idx]:(idx == length(tpdum.ssa_uses) ? length(tpdum.data) : (tpdum.ssa_uses[idx + 1] - 1))
+    # TODO: Make logarithmic
+    nelems = 0
+    for i in range
+        tpdum.data[i] == 0 && break
+        nelems += 1
+    end
+    return TwoPhaseVectorView(tpdum.data, nelems, range)
+end
+
+function concrete_eval_invoke(interp::AbstractInterpreter, ir::IRCode, mi_cache,
+    sv::InferenceState, inst::Expr, mi::MethodInstance)
+    code = get(mi_cache, mi, nothing)
+    code === nothing && return nothing
+    argtypes = collect_argtypes(interp, inst.args[2:end], nothing, ir)
+    effects = decode_effects(code.ipo_purity_bits)
+    if is_foldable(effects) && is_all_const_arg(argtypes)
+        args = collect_semi_const_args(argtypes, 1)
+        world = get_world_counter(interp)
+        value = try
+            Core._call_in_world_total(world, args...)
+        catch
+            return Union{}
+        end
+        if is_inlineable_constant(value) || call_result_unused(sv)
+            # If the constant is not inlineable, still do the const-prop, since the
+            # code that led to the creation of the Const may be inlineable in the same
+            # circumstance and may be optimizable.
+            return Const(value)
+        end
+    else
+        ir′ = codeinst_to_ir(interp, code)
+        if ir′ !== nothing
+            return ir_abstract_constant_propagation(interp, mi_cache, sv, mi, ir′, argtypes)
+        end
+    end
+    return nothing
+end
+
+function reprocess_instruction!(interp::AbstractInterpreter, ir::IRCode, mi::MethodInstance,
+                                mi_cache, sv::InferenceState,
+                                tpdum::TwoPhaseDefUseMap, idx::Int, bb::Union{Int, Nothing},
+                                @nospecialize(inst), @nospecialize(typ),
+                                phi_revisit::BitSet)
+    function update_phi!(from::Int, to::Int)
+        if length(ir.cfg.blocks[to].preds) == 0
+            return
+        end
+        for idx in ir.cfg.blocks[to].stmts
+            stmt = ir.stmts[idx][:inst]
+            isa(stmt, Nothing) && continue
+            isa(stmt, PhiNode) || break
+            for (i, edge) in enumerate(stmt.edges)
+                if edge == from
+                    deleteat!(stmt.edges, i)
+                    deleteat!(stmt.values, i)
+                    push!(phi_revisit, idx)
+                    break
+                end
+            end
+        end
+    end
+
+    if isa(inst, GotoIfNot)
+        cond = argextype(inst.cond, ir)
+        if isa(cond, Const)
+            if isa(inst.cond, SSAValue)
+                kill_def_use!(tpdum, inst.cond, idx)
+            end
+            if bb === nothing
+                bb = block_for_inst(ir, idx)
+            end
+            if (cond.val)::Bool
+                ir.stmts[idx][:inst] = nothing
+                kill_edge!(ir, bb, inst.dest, update_phi!)
+            else
+                ir.stmts[idx][:inst] = GotoNode(inst.dest)
+                kill_edge!(ir, bb, bb+1, update_phi!)
+            end
+            return true
+        end
+        return false
+    else
+        if isa(inst, Expr) || isa(inst, PhiNode)
+            if isa(inst, PhiNode) || inst.head === :call || inst.head === :foreigncall || inst.head === :new
+                if isa(inst, PhiNode)
+                    rt = abstract_eval_phi(interp, inst, nothing, ir)
+                else
+                    (;rt, effects) = abstract_eval_statement_expr(interp, inst, nothing, ir, mi)
+                    # All other effects already guaranteed effect free by construction
+                    if is_nothrow(effects)
+                        ir.stmts[idx][:flag] |= IR_FLAG_EFFECT_FREE
+                    end
+                end
+                if !(typ ⊑ rt)
+                    ir.stmts[idx][:type] = rt
+                    return true
+                end
+            elseif inst.head === :invoke
+                mi′ = inst.args[1]::MethodInstance
+                if mi′ !== mi # prevent infinite loop
+                    rr = concrete_eval_invoke(interp, ir, mi_cache, sv, inst, mi′)
+                    if rr !== nothing
+                        if !(typ ⊑ rr)
+                            ir.stmts[idx][:type] = rr
+                            return true
+                        end
+                    end
+                end
+            else
+                ccall(:jl_, Cvoid, (Any,), inst)
+                error()
+            end
+        elseif isa(inst, ReturnNode)
+            # Handled at the very end
+            return false
+        elseif isa(inst, PiNode)
+            rr = tmeet(argextype(inst.val, ir), inst.typ)
+            if !(typ ⊑ rr)
+                ir.stmts[idx][:type] = rr
+                return true
+            end
+        else
+            ccall(:jl_, Cvoid, (Any,), inst)
+            error()
+        end
+    end
+    return false
+end
+
+function _ir_abstract_constant_propagation(interp::AbstractInterpreter, mi_cache,
+    frame::InferenceState, mi::MethodInstance, ir::IRCode, argtypes::Vector{Any})
+    argtypes = va_process_argtypes(argtypes, mi)
+    argtypes_refined = Bool[!(ir.argtypes[i] ⊑ argtypes[i]) for i = 1:length(argtypes)]
+    empty!(ir.argtypes)
+    append!(ir.argtypes, argtypes)
+    ssa_refined = BitSet()
+
+    bbs = ir.cfg.blocks
+    ip = BitSetBoundedMinPrioritySet(length(bbs))
+    push!(ip, 1)
+    all_rets = Int[]
+
+    tpdum = TwoPhaseDefUseMap(length(ir.stmts))
+
+    """
+        process_terminator!
+
+    Process the terminator and add the successor to `ip`. Returns whether a
+    backedge was seen.
+    """
+    function process_terminator!(ip::BitSetBoundedMinPrioritySet, bb::Int, idx::Int)
+        inst = ir.stmts[idx][:inst]
+        if isa(inst, ReturnNode)
+            if isdefined(inst, :val)
+                push!(all_rets, idx)
+            end
+            return false
+        elseif isa(inst, GotoNode)
+            backedge = inst.label < bb
+            !backedge && push!(ip, inst.label)
+            return backedge
+        elseif isa(inst, GotoIfNot)
+            backedge = inst.dest < bb
+            !backedge && push!(ip, inst.dest)
+            push!(ip, bb + 1)
+            return backedge
+        elseif isexpr(inst, :enter)
+            dest = inst.args[1]::Int
+            @assert dest > bb
+            push!(ip, dest)
+            push!(ip, bb + 1)
+            return false
+        else
+            push!(ip, bb + 1)
+            return false
+        end
+    end
+
+    # Fast path: Scan both use counts and refinement in one single pass of
+    #            of the instructions. In the absence of backedges, this will
+    #            converge.
+    while !isempty(ip)
+        bb = popfirst!(ip)
+        stmts = bbs[bb].stmts
+        lstmt = last(stmts)
+        for idx = stmts
+            inst = ir.stmts[idx][:inst]
+            typ = ir.stmts[idx][:type]
+            any_refined = false
+            for ur in userefs(inst)
+                val = ur[]
+                if isa(val, Argument)
+                    any_refined |= argtypes_refined[val.n]
+                elseif isa(val, SSAValue)
+                    any_refined |= val.id in ssa_refined
+                    count!(tpdum, val)
+                end
+            end
+            if isa(inst, PhiNode) && idx in ssa_refined
+                any_refined = true
+                delete!(ssa_refined, idx)
+            end
+            if any_refined && reprocess_instruction!(interp, ir, mi, mi_cache,
+                    frame, tpdum, idx, bb, inst, typ, ssa_refined)
+                push!(ssa_refined, idx)
+            end
+            if idx == lstmt && process_terminator!(ip, bb, idx)
+                @goto residual_scan
+            end
+            if typ === Bottom && !isa(inst, PhiNode)
+                break
+            end
+        end
+    end
+    @goto compute_rt
+
+@label residual_scan
+    stmt_ip = BitSetBoundedMinPrioritySet(length(ir.stmts))
+    # Slow Path Phase 1.A: Complete use scanning
+    while !isempty(ip)
+        bb = popfirst!(ip)
+        stmts = bbs[bb].stmts
+        lstmt = last(stmts)
+        for idx = stmts
+            inst = ir.stmts[idx][:inst]
+            for ur in userefs(inst)
+                val = ur[]
+                if isa(val, Argument)
+                    if argtypes_refined[val.n]
+                        push!(stmt_ip, idx)
+                    end
+                elseif isa(val, SSAValue)
+                    count!(tpdum, val)
+                end
+            end
+            idx == lstmt && process_terminator!(ip, bb, idx)
+        end
+    end
+
+    # Slow Path Phase 1.B: Assemble def-use map
+    complete!(tpdum)
+    push!(ip, 1)
+    while !isempty(ip)
+        bb = popfirst!(ip)
+        stmts = bbs[bb].stmts
+        lstmt = last(stmts)
+        for idx = stmts
+            inst = ir.stmts[idx][:inst]
+            for ur in userefs(inst)
+                val = ur[]
+                if isa(val, SSAValue)
+                    push!(tpdum[val.id], idx)
+                end
+            end
+            idx == lstmt && process_terminator!(ip, bb, idx)
+        end
+    end
+
+    # Slow Path Phase 2: Use def-use map to converge cycles.
+    # TODO: It would be possible to return to the fast path after converging
+    #       each cycle, but that's somewhat complicated.
+    for val in ssa_refined
+        append!(stmt_ip, tpdum[val])
+    end
+
+    while !isempty(stmt_ip)
+        idx = popfirst!(stmt_ip)
+        inst = ir.stmts[idx][:inst]
+        typ = ir.stmts[idx][:type]
+        if reprocess_instruction!(interp, ir, mi, mi_cache, frame,
+                tpdum, idx, nothing, inst, typ, ssa_refined)
+            append!(stmt_ip, tpdum[idx])
+        end
+    end
+
+@label compute_rt
+    ultimate_rt = Union{}
+    for idx in all_rets
+        bb = block_for_inst(ir.cfg, idx)
+        if bb != 1 && length(ir.cfg.blocks[bb].preds) == 0
+            # Could have discovered this block is dead after the initial scan
+            continue
+        end
+        inst = ir.stmts[idx][:inst]::ReturnNode
+        rt = argextype(inst.val, ir)
+        ultimate_rt = tmerge(ultimate_rt, rt)
+    end
+    return ultimate_rt
+end
+
+function ir_abstract_constant_propagation(interp::AbstractInterpreter, mi_cache,
+    frame::InferenceState, mi::MethodInstance, ir::IRCode, argtypes::Vector{Any})
+    if __measure_typeinf__[]
+        inf_frame = Timings.InferenceFrameInfo(mi, frame.world, Any[], Any[], length(ir.argtypes))
+        Timings.enter_new_timer(inf_frame)
+        v = _ir_abstract_constant_propagation(interp, mi_cache, frame, mi, ir, argtypes)
+        append!(inf_frame.slottypes, ir.argtypes)
+        Timings.exit_current_timer(inf_frame)
+        return v
+    else
+        T = _ir_abstract_constant_propagation(interp, mi_cache, frame, mi, ir, argtypes)
+        return T
+    end
+end
diff --git a/base/compiler/ssair/passes.jl b/base/compiler/ssair/passes.jl
index 27b145d82c210..be2886fe1c437 100644
--- a/base/compiler/ssair/passes.jl
+++ b/base/compiler/ssair/passes.jl
@@ -75,7 +75,7 @@ end
 function find_curblock(domtree::DomTree, allblocks::Vector{Int}, curblock::Int)
     # TODO: This can be much faster by looking at current level and only
     # searching for those blocks in a sorted order
-    while !(curblock in allblocks)
+    while !(curblock in allblocks) && curblock !== 0
         curblock = domtree.idoms_bb[curblock]
     end
     return curblock
diff --git a/base/compiler/stmtinfo.jl b/base/compiler/stmtinfo.jl
index 72b4c8b829c06..966ee32338b48 100644
--- a/base/compiler/stmtinfo.jl
+++ b/base/compiler/stmtinfo.jl
@@ -60,7 +60,13 @@ struct ConcreteResult
     ConcreteResult(mi::MethodInstance, effects::Effects, @nospecialize val) = new(mi, effects, val)
 end
 
-const ConstResult = Union{ConstPropResult,ConcreteResult}
+struct SemiConcreteResult
+    mi::MethodInstance
+    ir::IRCode
+    effects::Effects
+end
+
+const ConstResult = Union{ConstPropResult,ConcreteResult, SemiConcreteResult}
 
 """
     info::ConstCallInfo
diff --git a/base/compiler/tfuncs.jl b/base/compiler/tfuncs.jl
index ca2f09103c425..713b579ac5a16 100644
--- a/base/compiler/tfuncs.jl
+++ b/base/compiler/tfuncs.jl
@@ -2010,7 +2010,7 @@ function builtin_nothrow(@nospecialize(f), argtypes::Vector{Any}, @nospecialize(
 end
 
 function builtin_tfunction(interp::AbstractInterpreter, @nospecialize(f), argtypes::Vector{Any},
-                           sv::Union{InferenceState,Nothing})
+                           sv::Union{InferenceState,IRCode,Nothing})
     if f === tuple
         return tuple_tfunc(argtypes)
     end
@@ -2176,7 +2176,7 @@ end
 # TODO: this function is a very buggy and poor model of the return_type function
 # since abstract_call_gf_by_type is a very inaccurate model of _method and of typeinf_type,
 # while this assumes that it is an absolutely precise and accurate and exact model of both
-function return_type_tfunc(interp::AbstractInterpreter, argtypes::Vector{Any}, sv::InferenceState)
+function return_type_tfunc(interp::AbstractInterpreter, argtypes::Vector{Any}, sv::Union{InferenceState, IRCode})
     if length(argtypes) == 3
         tt = argtypes[3]
         if isa(tt, Const) || (isType(tt) && !has_free_typevars(tt))
@@ -2192,10 +2192,14 @@ function return_type_tfunc(interp::AbstractInterpreter, argtypes::Vector{Any}, s
                     # Run the abstract_call without restricting abstract call
                     # sites. Otherwise, our behavior model of abstract_call
                     # below will be wrong.
-                    old_restrict = sv.restrict_abstract_call_sites
-                    sv.restrict_abstract_call_sites = false
-                    call = abstract_call(interp, ArgInfo(nothing, argtypes_vec), sv, -1)
-                    sv.restrict_abstract_call_sites = old_restrict
+                    if isa(sv, InferenceState)
+                        old_restrict = sv.restrict_abstract_call_sites
+                        sv.restrict_abstract_call_sites = false
+                        call = abstract_call(interp, ArgInfo(nothing, argtypes_vec), sv, -1)
+                        sv.restrict_abstract_call_sites = old_restrict
+                    else
+                        call = abstract_call(interp, ArgInfo(nothing, argtypes_vec), sv, -1)
+                    end
                     info = verbose_stmt_info(interp) ? MethodResultPure(ReturnTypeCallInfo(call.info)) : MethodResultPure()
                     rt = widenconditional(call.rt)
                     if isa(rt, Const)
@@ -2206,7 +2210,7 @@ function return_type_tfunc(interp::AbstractInterpreter, argtypes::Vector{Any}, s
                     if rt === Bottom || (isconcretetype(rt) && !iskindtype(rt))
                         # output cannot be improved so it is known for certain
                         return CallMeta(Const(rt), EFFECTS_TOTAL, info)
-                    elseif !isempty(sv.pclimitations)
+                    elseif isa(sv, InferenceState) && !isempty(sv.pclimitations)
                         # conservatively express uncertainty of this result
                         # in two ways: both as being a subtype of this, and
                         # because of LimitedAccuracy causes
diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl
index 228ca6d868b91..064dfb6776acb 100644
--- a/base/compiler/typeinfer.jl
+++ b/base/compiler/typeinfer.jl
@@ -45,6 +45,8 @@ function _typeinf_identifier(frame::Core.Compiler.InferenceState)
     return mi_info
 end
 
+_typeinf_identifier(frame::InferenceFrameInfo) = frame
+
 """
     Core.Compiler.Timing(mi_info, start_time, ...)
 
diff --git a/base/compiler/utilities.jl b/base/compiler/utilities.jl
index 0844550f97aef..564d52e61b392 100644
--- a/base/compiler/utilities.jl
+++ b/base/compiler/utilities.jl
@@ -293,6 +293,17 @@ function singleton_type(@nospecialize(ft))
     return nothing
 end
 
+function maybe_singleton_const(@nospecialize(t))
+    if isa(t, DataType)
+        if isdefined(t, :instance)
+            return Const(t.instance)
+        elseif isconstType(t)
+            return Const(t.parameters[1])
+        end
+    end
+    return t
+end
+
 ###################
 # SSAValues/Slots #
 ###################
diff --git a/base/essentials.jl b/base/essentials.jl
index d1313b0740995..f9a7abb774625 100644
--- a/base/essentials.jl
+++ b/base/essentials.jl
@@ -763,6 +763,7 @@ struct Colon <: Function
 end
 const (:) = Colon()
 
+
 """
     Val(c)
 
diff --git a/test/compiler/EscapeAnalysis/EAUtils.jl b/test/compiler/EscapeAnalysis/EAUtils.jl
index f8db1cb62f460..17a70faeb91b5 100644
--- a/test/compiler/EscapeAnalysis/EAUtils.jl
+++ b/test/compiler/EscapeAnalysis/EAUtils.jl
@@ -70,7 +70,8 @@ import Core:
 import .CC:
     InferenceResult, OptimizationState, IRCode, copy as cccopy,
     @timeit, convert_to_ircode, slot2reg, compact!, ssa_inlining_pass!, sroa_pass!,
-    adce_pass!, type_lift_pass!, JLOptions, verify_ir, verify_linetable
+    adce_pass!, type_lift_pass!, JLOptions, verify_ir, verify_linetable,
+    SemiConcreteResult
 import .EA: analyze_escapes, ArgEscapeCache, EscapeInfo, EscapeState, is_ipo_profitable
 
 # when working outside of Core.Compiler,
@@ -176,9 +177,11 @@ function cache_escapes!(interp::EscapeAnalyzer,
 end
 
 function get_escape_cache(interp::EscapeAnalyzer)
-    return function (linfo::Union{InferenceResult,MethodInstance})
+    return function (linfo::Union{InferenceResult,MethodInstance,SemiConcreteResult})
         if isa(linfo, InferenceResult)
             ecache = get(interp.cache, linfo, nothing)
+        elseif isa(linfo, SemiConcreteResult)
+            ecache = get(interp.cache, linfo, nothing)
         else
             ecache = get(GLOBAL_ESCAPE_CACHE, linfo, nothing)
         end
diff --git a/test/compiler/inference.jl b/test/compiler/inference.jl
index 8dbb4b4359b65..34547f97575a7 100644
--- a/test/compiler/inference.jl
+++ b/test/compiler/inference.jl
@@ -4191,3 +4191,13 @@ end
 
 # Test that Const ⊑ PartialStruct respects vararg
 @test Const((1,2)) ⊑ PartialStruct(Tuple{Vararg{Int}}, [Const(1), Vararg{Int}])
+
+# Test that semi-concrete interpretation doesn't break on functions with while loops in them.
+@Base.assume_effects :consistent :effect_free :terminates_globally function pure_annotated_loop(x::Int, y::Int)
+    for i = 1:2
+        x += y
+    end
+    return y
+end
+call_pure_annotated_loop(x) = Val{pure_annotated_loop(x, 1)}()
+@test only(Base.return_types(call_pure_annotated_loop, Tuple{Int})) === Val{1}