Description
SSA2 is a FirstOrder, SimplyTyped IntermediateLanguage, a slight variant of the SSA IntermediateLanguage,
Like SSA, a SSA program consists of a collection of datatype declarations, a sequence of global statements, and a collection of functions, along with a distinguished "main" function. Each function consists of a collection of basic blocks, where each basic block is a sequence of statements ending with some control transfer.
Unlike SSA, SSA2 includes mutable fields in objects and makes the vector type constructor n-ary instead of unary. This allows optimizations like RefFlatten and DeepFlatten to be expressed.
Implementation
ssa2.sig ssa2.funssa-tree2.sig ssa-tree2.fun
Type Checking
Type checking of a SSA2 program verfies the following:
-
no duplicate definitions (tycons, cons, vars, labels, funcs)
-
no out of scope references (tycons, cons, vars, labels, funcs)
-
variable definitions dominate variable uses
-
case transfers are exhaustive and irredundant
-
Enter/Leave profile statements match
-
"traditional" well-typedness
type-check2.sig type-check2.fun
Details and Notes
SSA is an abbreviation for Static Single Assignment.