source: etc/campbell/dev-notes/2012-10-18-front-end-correctness.txt

Last change on this file was 2434, checked in by campbell, 7 years ago

Misc notes.

File size: 1.2 KB
Line 
1Clight to Cminor
2----------------
3
4This looks like it will be an n:m simulation with n,m≥1.  We need to allow n>1
5because statements like Sbreak can take several steps to find the appropriate
6continuation (unlike, say, Sreturn, which uses call_cont to find the right
7one in one step).  However, it won't take zero steps as we always generate an
8statement to be consumed for each step of the Clight (even for steps which
9process the continuation - we still have something like a goto to match the
10skip against).
11
12When compiling loops we're going to need to match states like
13
14  skip, Kfor a2 a3 s k   <--->  skip, kseq (goto entry) k'
15
16Presumably some kind of invariant on goto labels is required, perhaps that
17goto labels are unique or equivalently that any label produced is found by the
18label lookup function.  This might be enough (as a hyp for the construction of
19the simulation relation):
20
21∀EX,INV,KINV.
22  find_label_always entry (f_body f) Kend EX f en INV KINV =
23    Some ? 〈[loop body],[suitable continuation]〉.
24
25We can then step back through the loop.
26
27Cminor to RTLabs
28----------------
29
30Here we have to allow for statements that disappear (skips and goto labels) as
31well as large expansions as expressions are broken down.
Note: See TracBrowser for help on using the repository browser.