Type inference is achieved by profiling values, predicting what types operations will produce based on those profiles, inserting type checks based on the type predictions, and then attempting to construct type proofs about the types of values based on the type checks.
o.x * o.x + o.y * o.y
The propagation of SpecTypes derived at value profiles to all operations and variables in a function is performed using a standard forward data flow formulation, implemented as a flow-insensitive fixpoint. This is one of the first phases of DFG compilation, and is only activated once the Baseline JIT decides, based on its execution count, that a function would be better off executing optimized code. See DFGPredictionPropagationPhase.cpp.
After each value in a function is labeled with a predicted type, we insert speculative type checks based on those predictions. For example, in a numeric operation (like 'o.x * o.y'), we insert speculate-double checks on the operands of the multiplication. If a speculation check fails, execution is diverted from optimized DFG code back to the Baseline JIT. This has the effect of proving the type for subsequent code within the DFG. Consider how the simple addition operation 'a + b' will be decomposed, if 'a' and 'b' both had SpecInt32 as their predicted type:
check if a is Int32 -> else OSR exit to Baseline JIT check if b is Int32 -> else OSR exit to Baseline JIT result = a + b // integer addition check if overflow -> else OSR exit to Baseline JIT
After this operation completes, we know that:
- 'a' is an integer.
- 'b' is an integer.
- the result is an integer.
Any subsequent operations on either 'a' or 'b' do not need to check their types. Likewise for operations on the result. The elimination of subsequent checks is achieved by a second data flow analysis, called simply the DFG CFA. Unlike the prediction propagation phase, which is concerned with constructing type predictions, the CFA is concerned with constructing type proofs. The CFA, found in DFGCFAPhase.cpp and DFGAbstractInterpreterInlines.cpp, follows a flow-sensitive forward data flow formulation. It also implements sparse conditional constant propagation, which gives it the ability to sometimes prove that values are constants, as well as proving their types.
Putting this together, the expression 'o.x * o.x + o.y * o.y' will only require type checks on the value loaded from 'o.x' and the value loaded from 'o.y'. After that, we know that the values are doubles, and we know that we only have to emit a double multiply path followed by a double addition. When combined with type check hoisting, DFG code will usually execute a type check at most once per heap load.