diff --git a/base/compiler/abstractinterpretation.jl b/base/compiler/abstractinterpretation.jl
index 20524b58b61f9..b32f21541a946 100644
--- a/base/compiler/abstractinterpretation.jl
+++ b/base/compiler/abstractinterpretation.jl
@@ -133,8 +133,9 @@ function abstract_call_gf_by_type(interp::AbstractInterpreter, @nospecialize(f),
                     f, this_arginfo, match, sv)
                 const_result = nothing
                 if const_call_result !== nothing
-                    if const_call_result.rt ⊑ rt
-                        rt = const_call_result.rt
+                    const_rt = const_call_result.rt
+                    if const_rt ⊑ rt
+                        rt = const_rt
                         (; effects, const_result) = const_call_result
                     end
                 end
@@ -387,6 +388,11 @@ function collect_limitations!(@nospecialize(typ), sv::InferenceState)
     return typ
 end
 
+function collect_limitations!(@nospecialize(typ), ::IRCode)
+    @assert !isa(typ, LimitedAccuracy)
+    return typ
+end
+
 function from_interconditional(@nospecialize(typ), sv::InferenceState, (; fargs, argtypes)::ArgInfo, @nospecialize(maybecondinfo))
     fargs === nothing && return widenconditional(typ)
     slot = 0
@@ -773,15 +779,19 @@ 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
     # 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)
+        return is_all_const_arg(arginfo)
+    else
+        return nothing
+    end
 end
 
 is_all_const_arg(arginfo::ArgInfo) = is_all_const_arg(arginfo.argtypes)
@@ -792,6 +802,7 @@ function is_all_const_arg(argtypes::Vector{Any})
     end
     return true
 end
+is_all_const_arg((; argtypes)::ArgInfo) = is_all_const_arg(argtypes)
 
 collect_const_args(arginfo::ArgInfo) = collect_const_args(arginfo.argtypes)
 function collect_const_args(argtypes::Vector{Any})
@@ -804,7 +815,9 @@ 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
+    eligibility = concrete_eval_eligible(interp, f, result, arginfo, sv)
+    eligibility === nothing && return false
+    eligibility || return true # eligible for semi-concrete evaluation
     args = collect_const_args(arginfo)
     world = get_world_counter(interp)
     value = try
@@ -819,9 +832,12 @@ function concrete_eval_call(interp::AbstractInterpreter,
         # circumstance and may be optimizable.
         return ConstCallResults(Const(value), ConcreteResult(result.edge::MethodInstance, EFFECTS_TOTAL, value), EFFECTS_TOTAL)
     end
-    return nothing
+    return false
 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")
@@ -850,13 +866,28 @@ 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)
+        # test
+        add_backedge!(result.edge, 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)
@@ -1119,6 +1150,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
@@ -1173,7 +1205,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
@@ -1238,7 +1271,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
@@ -1324,7 +1357,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)
@@ -1391,6 +1424,7 @@ function abstract_apply(interp::AbstractInterpreter, argtypes::Vector{Any}, sv::
     end
     retinfos = ApplyCallInfo[]
     retinfo = UnionSplitApplyCallInfo(retinfos)
+    effects = EFFECTS_TOTAL
     for i = 1:length(ctypes)
         ct = ctypes[i]
         arginfo = infos[i]
@@ -1440,7 +1474,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
@@ -1662,8 +1696,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)
 
@@ -1813,7 +1847,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)
@@ -1886,7 +1920,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})
     if e.head === :static_parameter
         n = e.args[1]::Int
         t = Any
@@ -1901,13 +1935,20 @@ function abstract_eval_value_expr(interp::AbstractInterpreter, e::Expr, vtypes::
     end
 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(e.mod, e.name, sv)
     end
@@ -1915,16 +1956,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
@@ -1937,30 +1978,27 @@ 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})::RTEffects
     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)
-            tristate_merge!(sv, callinfo.effects)
-            sv.stmt_info[sv.currpc] = callinfo.info
-            t = callinfo.rt
+            (; rt, effects, info) = abstract_call(interp, ArgInfo(ea, argtypes), sv)
+            if isa(sv, InferenceState)
+                sv.stmt_info[sv.currpc] = info
+            end
         end
+        return RTEffects(rt, effects)
     elseif ehead === :new
         t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
         is_nothrow = true
@@ -2007,9 +2045,9 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
         else
             is_nothrow = false
         end
-        tristate_merge!(sv, Effects(EFFECTS_TOTAL;
+        return RTEffects(t, Effects(EFFECTS_TOTAL;
             consistent = !ismutabletype(t) ? ALWAYS_TRUE : TRISTATE_UNKNOWN,
-            nothrow = is_nothrow ? ALWAYS_TRUE : ALWAYS_FALSE))
+            nothrow = is_nothrow ? ALWAYS_TRUE : TRISTATE_UNKNOWN))
     elseif ehead === :splatnew
         t, isexact = instanceof_tfunc(abstract_eval_value(interp, e.args[1], vtypes, sv))
         is_nothrow = false # TODO: More precision
@@ -2026,11 +2064,10 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
                 t = PartialStruct(t, at.fields::Vector{Any})
             end
         end
-        tristate_merge!(sv, Effects(EFFECTS_TOTAL;
-            consistent = !ismutabletype(t) ? ALWAYS_TRUE : TRISTATE_UNKNOWN,
-            nothrow = is_nothrow ? ALWAYS_TRUE : ALWAYS_FALSE))
+        return RTEffects(t, Effects(EFFECTS_TOTAL;
+            consistent = ismutabletype(t) ? TRISTATE_UNKNOWN : ALWAYS_TRUE,
+            nothrow = is_nothrow ? ALWAYS_TRUE : TRISTATE_UNKNOWN))
     elseif ehead === :new_opaque_closure
-        tristate_merge!(sv, Effects()) # TODO
         t = Union{}
         if length(e.args) >= 4
             ea = e.args
@@ -2046,47 +2083,29 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
                     argtypes = most_general_argtypes(t)
                     pushfirst!(argtypes, t.env)
                     callinfo = abstract_call_opaque_closure(interp, t,
-                        ArgInfo(nothing, argtypes), sv, #=check=#false)
+                        ArgInfo(nothing, argtypes), sv)
                     sv.stmt_info[sv.currpc] = OpaqueClosureCreateInfo(callinfo)
                 end
             end
         end
+        return RTEffects(t, Effects())
     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 = EFFECTS_UNKNOWN
-        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             ? ALWAYS_TRUE : effects.nothrow,
-                override.terminates_globally ? ALWAYS_TRUE : effects.terminates_globally,
-                effects.nonoverlayed         ? true        : false,
-                override.notaskstate         ? ALWAYS_TRUE : effects.notaskstate)
-        end
-        tristate_merge!(sv, effects)
+        return abstract_eval_foreigncall(interp, e, vtypes, sv)
     elseif ehead === :cfunction
-        tristate_merge!(sv, EFFECTS_UNKNOWN)
         t = e.args[1]
         isa(t, Type) || (t = Any)
         abstract_eval_cfunction(interp, e, vtypes, sv)
+        return RTEffects(t, EFFECTS_UNKNOWN)
     elseif ehead === :method
-        tristate_merge!(sv, EFFECTS_UNKNOWN)
         t = (length(e.args) == 1) ? Any : Nothing
+        return RTEffects(t, EFFECTS_UNKNOWN)
     elseif ehead === :copyast
-        tristate_merge!(sv, EFFECTS_UNKNOWN)
         t = abstract_eval_value(interp, e.args[1], vtypes, sv)
         if t isa Const && t.val isa Expr
             # `copyast` makes copies of Exprs
             t = Expr
         end
+        return RTEffects(t, EFFECTS_UNKNOWN)
     elseif ehead === :invoke || ehead === :invoke_modify
         error("type inference data-flow error: tried to double infer a function")
     elseif ehead === :isdefined
@@ -2107,7 +2126,7 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             if isdefined(sym.mod, sym.name)
                 t = Const(true)
             end
-        elseif isexpr(sym, :static_parameter)
+        elseif isa(sym, Expr) && sym.head === :static_parameter
             n = sym.args[1]::Int
             if 1 <= n <= length(sv.sptypes)
                 spty = sv.sptypes[n]
@@ -2119,9 +2138,10 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
     elseif false
         @label always_throw
         t = Bottom
-        tristate_merge!(sv, EFFECTS_THROWS)
+        return RTEffects(t, EFFECTS_UNKNOWN)
     else
-        t = abstract_eval_value_expr(interp, e, vtypes, sv)
+        t = abstract_eval_value_expr(interp, e, sv)
+        return RTEffects(t, EFFECTS_UNKNOWN)
     end
     @assert !isa(t, TypeVar) "unhandled TypeVar"
     if isa(t, DataType) && isdefined(t, :instance)
@@ -2136,7 +2156,65 @@ function abstract_eval_statement(interp::AbstractInterpreter, @nospecialize(e),
             sv.pclimitations = IdSet{InferenceState}()
         end
     end
-    return t
+    return RTEffects(t, EFFECTS_UNKNOWN)
+end
+
+function abstract_eval_foreigncall(interp::AbstractInterpreter, fcall::Expr, vtypes::Union{VarTable, Nothing}, sv::Union{InferenceState, IRCode}, mi::Union{MethodInstance, Nothing}=nothing)
+    args = fcall.args
+    abstract_eval_value(interp, args[1], vtypes, sv)
+    mi′ = mi === nothing ? sv.linfo : mi
+    t = sp_type_rewrap(args[2], mi′, true)
+    for i = 3:length(args)
+        if abstract_eval_value(interp, args[i], vtypes, sv) === Bottom
+            t = Bottom
+        end
+    end
+    effects = EFFECTS_UNKNOWN
+    cconv = 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             ? ALWAYS_TRUE : effects.nothrow,
+            override.terminates_globally ? ALWAYS_TRUE : effects.terminates_globally,
+            effects.nonoverlayed         ? true        : false,
+            override.notaskstate         ? ALWAYS_TRUE : effects.notaskstate)
+    else
+        effects = EFFECTS_UNKNOWN
+    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)
+    tristate_merge!(sv, effects)
+    e = e::Expr
+    @assert !isa(rt, TypeVar) "unhandled TypeVar"
+    rt = maybe_singleton_const(rt)
+    if !isempty(sv.pclimitations)
+        if rt isa Const || rt === Union{}
+            empty!(sv.pclimitations)
+        else
+            rt = LimitedAccuracy(rt, sv.pclimitations)
+            sv.pclimitations = IdSet{InferenceState}()
+        end
+    end
+    return rt
 end
 
 function abstract_eval_global(M::Module, s::Symbol)
@@ -2148,7 +2226,7 @@ function abstract_eval_global(M::Module, s::Symbol)
     return ty
 end
 
-function abstract_eval_global(M::Module, s::Symbol, frame::InferenceState)
+function abstract_eval_global(M::Module, s::Symbol, frame::Union{InferenceState, IRCode})
     ty = abstract_eval_global(M, s)
     isa(ty, Const) && return ty
     if isdefined(M,s)
diff --git a/base/compiler/compiler.jl b/base/compiler/compiler.jl
index 8b6da7902457a..0e51286cfe471 100644
--- a/base/compiler/compiler.jl
+++ b/base/compiler/compiler.jl
@@ -156,6 +156,10 @@ include("compiler/ssair/ir.jl")
 include("compiler/inferenceresult.jl")
 include("compiler/inferencestate.jl")
 
+include("compiler/ssair/basicblock.jl")
+include("compiler/ssair/domtree.jl")
+include("compiler/ssair/ir.jl")
+
 include("compiler/typeutils.jl")
 include("compiler/typelimits.jl")
 include("compiler/typelattice.jl")
@@ -164,7 +168,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..8c33905044c8b 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`,
diff --git a/base/compiler/inferencestate.jl b/base/compiler/inferencestate.jl
index a40f63c701200..78d03a44f9af0 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
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 6c17bbc7868f2..854844a8a8ed5 100644
--- a/base/compiler/ssair/driver.jl
+++ b/base/compiler/ssair/driver.jl
@@ -14,3 +14,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 3a6333470fabe..c9ca4c7feb3c1 100644
--- a/base/compiler/ssair/inlining.jl
+++ b/base/compiler/ssair/inlining.jl
@@ -1098,7 +1098,7 @@ function inline_invoke!(
     end
     result = info.result
     if isa(result, ConcreteResult)
-        item = concrete_result_item(result, state)
+        item = const_result_item(result, state)
     else
         argtypes = invoke_rewrite(sig.argtypes)
         if isa(result, ConstPropResult)
@@ -1280,10 +1280,14 @@ function compute_inlining_cases(info::ConstCallInfo,
             result = results[j]
             any_fully_covered |= match.fully_covers
             if isa(result, ConcreteResult)
-                case = concrete_result_item(result, state)
+                case = const_result_item(result, state)
                 push!(cases, InliningCase(result.mi.specTypes, case))
             elseif isa(result, ConstPropResult)
                 handled_all_cases &= handle_const_prop_result!(result, argtypes, flag, state, cases, true)
+            elseif isa(result, InferenceResult)
+                handled_all_cases &= handle_inf_result!(result, argtypes, flag, state, cases, true)
+            elseif isa(result, SemiConcreteResult)
+                handled_all_cases &= handle_semi_concrete_result!(result, cases, true)
             else
                 @assert result === nothing
                 handled_all_cases &= handle_match!(match, argtypes, flag, state, cases, #=allow_abstract=#true)
@@ -1347,7 +1351,16 @@ function handle_const_prop_result!(
     return true
 end
 
-function concrete_result_item(result::ConcreteResult, state::InliningState)
+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 const_result_item(result::ConstResult, state::InliningState)
     if !isdefined(result, :result) || !is_inlineable_constant(result.result)
         case = compileable_specialization(state.et, result.mi, result.effects)
         @assert case !== nothing "concrete evaluation should never happen for uncompileable callsite"
@@ -1474,7 +1487,7 @@ function assemble_inline_todo!(ir::IRCode, state::InliningState)
                     sig, state, todo)
             else
                 if isa(result, ConcreteResult)
-                    item = concrete_result_item(result, state)
+                    item = const_result_item(result, state)
                 else
                     item = analyze_method!(info.match, sig.argtypes, flag, state)
                 end
diff --git a/base/compiler/ssair/ir.jl b/base/compiler/ssair/ir.jl
index 93ca66cb7c931..74680e5351627 100644
--- a/base/compiler/ssair/ir.jl
+++ b/base/compiler/ssair/ir.jl
@@ -1053,15 +1053,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..70dcda7678410
--- /dev/null
+++ b/base/compiler/ssair/irinterp.jl
@@ -0,0 +1,410 @@
+
+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::Vector{UInt8})::CodeInfo
+    end
+
+    isa(src, CodeInfo) || return src
+
+    return inflate_ir(src, mi)
+end
+
+function tristate_merge!(ir::IRCode, e::Effects)
+    nothing
+end
+
+function abstract_call_gf_by_type(interp::AbstractInterpreter, @nospecialize(f),
+                                  arginfo::ArgInfo, @nospecialize(atype),
+                                  sv::IRCode, max_methods::Int)
+    return CallMeta(Any, false, Effects())
+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′ = inst.args[1]::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_const_args(argtypes, #=start_idx=#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)
+    function update_phi!(from, to)
+        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 === :new
+                if isa(inst, PhiNode)
+                    rt = abstract_eval_phi(interp, inst, nothing, ir)
+                else
+                    (;rt, effects) = abstract_eval_statement_expr(interp, inst, nothing, ir)
+                    # All other effects already guaranteed effect free by construction
+                    if effects.nothrow === ALWAYS_TRUE
+                        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
+                rr = concrete_eval_invoke(interp, ir, mi_cache, sv, inst)
+                if rr !== nothing
+                    if !(typ ⊑ rr)
+                        ir.stmts[idx][:type] = rr
+                        return true
+                    end
+                end
+            elseif inst.head === :foreigncall
+                (; rt) = abstract_eval_foreigncall(interp, inst, nothing, ir, mi)
+                if rt !== nothing
+                    if !(typ ⊑ rt)
+                        ir.stmts[idx][:type] = rt
+                        return true
+                    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, argtypes)
+    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()
+
+    ultimate_rt = Union{}
+    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, bb, idx)
+        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]
+            typ = ir.stmts[idx][:type]
+            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]
+            typ = ir.stmts[idx][:type]
+            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]
+        ultimate_rt = tmerge(ultimate_rt, argextype(inst.val, ir))
+    end
+    return ultimate_rt
+end
+
+function ir_abstract_constant_propagation(interp::AbstractInterpreter, mi_cache, frame::InferenceState, mi::MethodInstance, ir, argtypes)
+    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
+        return _ir_abstract_constant_propagation(interp, mi_cache, frame, mi, ir, argtypes)
+    end
+end
diff --git a/base/compiler/stmtinfo.jl b/base/compiler/stmtinfo.jl
index 72b4c8b829c06..d61926fedd885 100644
--- a/base/compiler/stmtinfo.jl
+++ b/base/compiler/stmtinfo.jl
@@ -60,8 +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 dcf7409c7bde4..fa57eabe257fd 100644
--- a/base/compiler/tfuncs.jl
+++ b/base/compiler/tfuncs.jl
@@ -1860,8 +1860,8 @@ function builtin_nothrow(@nospecialize(f), argtypes::Vector{Any}, @nospecialize(
     return _builtin_nothrow(f, argtypes, rt)
 end
 
-function builtin_tfunction(interp::AbstractInterpreter, @nospecialize(f), argtypes::Vector{Any},
-                           sv::Union{InferenceState,Nothing})
+function builtin_tfunction(interp::AbstractInterpreter, @nospecialize(f), argtypes::Array{Any,1},
+                           sv::Union{InferenceState,IRCode,Nothing})
     if f === tuple
         return tuple_tfunc(argtypes)
     end
diff --git a/base/compiler/typeinfer.jl b/base/compiler/typeinfer.jl
index 86aa6e4affa46..9dcba50a270c8 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, ...)
 
@@ -321,13 +323,15 @@ function CodeInstance(
         relocatability)
 end
 
-function maybe_compress_codeinfo(interp::AbstractInterpreter, linfo::MethodInstance, ci::CodeInfo)
+function maybe_compress_codeinfo(interp::AbstractInterpreter, linfo::MethodInstance, ci::CodeInfo, ipo_effects::Effects)
     def = linfo.def
     toplevel = !isa(def, Method)
     if toplevel
         return ci
     end
     if may_discard_trees(interp)
+        # TODO: We may want to check is_concrete_eval_eligible(ipo_effects) here, but at the moment,
+        #       inlineable is also required for semi-concrete constprop.
         cache_the_tree = ci.inferred && (ci.inlineable || isa_compileable_sig(linfo.specTypes, def))
     else
         cache_the_tree = true
@@ -357,7 +361,7 @@ function transform_result_for_cache(interp::AbstractInterpreter, linfo::MethodIn
     if inferred_result isa CodeInfo
         inferred_result.min_world = first(valid_worlds)
         inferred_result.max_world = last(valid_worlds)
-        inferred_result = maybe_compress_codeinfo(interp, linfo, inferred_result)
+        inferred_result = maybe_compress_codeinfo(interp, linfo, inferred_result, ipo_effects)
     end
     # The global cache can only handle objects that codegen understands
     if !isa(inferred_result, Union{CodeInfo, Vector{UInt8}, ConstAPI})
diff --git a/base/compiler/utilities.jl b/base/compiler/utilities.jl
index 82748669e4387..9f6b812ad96de 100644
--- a/base/compiler/utilities.jl
+++ b/base/compiler/utilities.jl
@@ -238,6 +238,15 @@ function singleton_type(@nospecialize(ft))
     return nothing
 end
 
+function maybe_singleton_const(@nospecialize(t))
+    if isa(t, DataType) && isdefined(t, :instance)
+        return Const(t.instance)
+    elseif isconstType(t)
+        return Const(t.parameters[1])
+    end
+    return t
+end
+
 ###################
 # SSAValues/Slots #
 ###################
diff --git a/base/essentials.jl b/base/essentials.jl
index 74a2551b814e2..3cdb6ff92cdfe 100644
--- a/base/essentials.jl
+++ b/base/essentials.jl
@@ -767,6 +767,12 @@ struct Colon <: Function
 end
 const (:) = Colon()
 
+# TODO: Change lowering to do this automatically
+@eval struct Val{x}
+    (T::Type{Val{x}} where x)() = $(Expr(:new, :T))
+end
+
+
 """
     Val(c)
 
@@ -787,8 +793,7 @@ julia> f(Val(true))
 "Good"
 ```
 """
-struct Val{x}
-end
+Val
 
 Val(x) = Val{x}()
 
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 77b74969b099b..04a2abb179d32 100644
--- a/test/compiler/inference.jl
+++ b/test/compiler/inference.jl
@@ -4118,3 +4118,39 @@ struct Issue45780
 end
 f45780() = Val{Issue45780(@Base.Experimental.opaque ()->1).oc()}()
 @test (@inferred f45780()) == Val{1}()
+
+# backedge insertion for Any-typed, effect-free frame
+const CONST_DICT = let d = Dict()
+    for c in 'A':'z'
+        push!(d, c => Int(c))
+    end
+    d
+end
+Base.@assume_effects :total_may_throw getcharid(c) = CONST_DICT[c]
+@noinline callf(f, args...) = f(args...)
+function entry_to_be_invalidated(c)
+    return callf(getcharid, c)
+end
+@test Base.infer_effects((Char,)) do x
+    entry_to_be_invalidated(x)
+end |> Core.Compiler.is_foldable
+@test fully_eliminated(; retval=97) do
+    entry_to_be_invalidated('a')
+end
+getcharid(c) = CONST_DICT[c] # now this is not eligible for concrete evaluation
+@test Base.infer_effects((Char,)) do x
+    entry_to_be_invalidated(x)
+end |> !Core.Compiler.is_foldable
+@test !fully_eliminated() do
+    entry_to_be_invalidated('a')
+end
+
+# 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 Core.Compiler.return_type(call_pure_annotated_loop, Tuple{Int}) == Val{1}
\ No newline at end of file