Notes

2015-11-13

While browsing information about compilers I found it difficult to find a formal definition of SSA form (Static Single Assignment). For whatever reason, it's often under-specified or simplifed. So anyway, if you are like me and like formal definitions, here it is.

A program is in SSA form when:

• Variables are assigned only once.
• All the uses of a variable are dominated by the unique definition.
• The φ nodes are at the beginning basic blocks.
• The φ nodes have one argument for each predecessor of their basic block.
• Uses of φ arguments are counted at the end of the corresponding predecessor.

The concept of domination is from graph theory: an instruction A dominates another B when all the paths from the entry point of the program to B go through A.

Please let me know if the definition above looks wrong to you. Finally, if you want informal examples, the Wikipedia page has plenty!