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
Please let me know if the definition above looks wrong to you.
Finally, if you want informal examples, the Wikipedia page has