120 | | sp := stack<k + 4>; |

121 | | m[stack<k + 1>] := k_info_table; |

122 | | m[stack<k + 2>] := a; |

123 | | m[stack<k + 3>] := b; |

124 | | m[stack<k + 4>] := c; |

125 | | k: // on entry to k, sp == stack<k+3> |

126 | | x := m[stack<k + 2>] |

127 | | y := m[stack<k + 3>] |

128 | | }}} |

129 | | |

| 121 | if <> then goto L0; else goto L2; |

| 122 | L0: |

| 123 | sp := stack<L1 + 2>; |

| 124 | m[stack<L1 + 1>] := L1_info_table; |

| 125 | m[stack<L1 + 2>] := a; |

| 126 | call f returns to L1; |

| 127 | L1: // on entry to L1, sp == stack<L1+3> |

| 128 | x := m[stack<L1 + 2>]; |

| 129 | y := m[stack<L1 + 3>]; |

| 130 | ... <uses y> |

| 131 | goto L4; |

| 132 | L2: |

| 133 | sp := stack<L3 + 2>; |

| 134 | m[stack<L3 + 1>] := L3_info_table; |

| 135 | m[stack<L3 + 2>] := a; |

| 136 | call f returns to L3; |

| 137 | L3: // on entry to L3, sp == stack<L3+3> |

| 138 | x := m[stack<L3 + 2>]; |

| 139 | y := m[stack<L3 + 3>]; |

| 140 | goto L4; |

| 141 | L4: |

| 142 | m[stack<x>] := x; |

| 143 | ... <possibly uses y> |

| 144 | }}} |

| 145 | |

| 146 | What about a procedure's incoming and outgoing parameters, which should appear at the young end of the stack? |

| 147 | |

| 148 | Invariant: A load from a stack slot must be preceded by a spill to that stack slot. And we should visit that spill before the reload. Otherwise, something has gone horribly wrong. |