§ SSA as linear typed language
- Control flow is linear in a basic block: ie, we can have a sea of nodesrepresentation, where each terminator instruction produces linear controlflow tokens:
br: token[-1] --> token.
brcond: token[-1] -> -> (token, token),
return: token[-1] -> (). This ensures that each branching only happens once,thereby "sealing their fate. On the other hand, reguar instructions alsotake a "control token", but don't consume it. so for example,
add: token -> (name, name) -> name.
- Next question: is dominance also somehow 'linear'?
- Answer: yes. We need quantitative types. When we branch from basic block
1/2A to the control tokens from
(%tokb, %tokc) = br cond %cond0 B, C.Now, if someone builds a token that's at a basic block
D that is mergedinto by both
B, C, they will receive a "full"
A that they can use.Pictorially: