|
Last change
on this file was
2394,
checked in by campbell, 7 years ago
|
|
I've kept the odd note on bits of CerCo? work I've been doing. James suggested
that it might be useful if these were recorded in the repository just in case
they contain some useful information that doesn't get recorded elsewhere.
|
|
File size:
1.2 KB
|
| Line | |
|---|
| 1 | Tailcalls present a problem in the production of our structured traces for |
|---|
| 2 | RTLabs programs. Function calls involve four states of the RTLabs abstract |
|---|
| 3 | machine: |
|---|
| 4 | |
|---|
| 5 | 1. A normal state about to execute one of the function call instructions, |
|---|
| 6 | 2. A call state with the function, arguments and return register made plain, |
|---|
| 7 | 3. A normal state about to execute to execute the return instruction, and |
|---|
| 8 | 4. A return state with the frame elided. |
|---|
| 9 | |
|---|
| 10 | For the purposes of the structured traces the call state is classified as the |
|---|
| 11 | call and the return state the return. However, with tail calls there is no |
|---|
| 12 | explicit return instruction or state --- it behaves more like a jump. Worse, |
|---|
| 13 | the call state has no record of the fact that a tail call is happening, so it |
|---|
| 14 | isn't easy to match them up without changing either the semantics, or the |
|---|
| 15 | classification of which state is the "call". |
|---|
| 16 | |
|---|
| 17 | The lack of support for tail calls breaks two things: the termination proofs |
|---|
| 18 | obtained from the excluded middle aren't going to make sense (because they |
|---|
| 19 | insist on well-bracketing, and we're missing return states), and the |
|---|
| 20 | as_after_return property won't be provable because the return may not match up |
|---|
| 21 | with the function call. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
