source: etc/campbell/dev-notes/2012-09-18-goto-label-skips.txt

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: 2.4 KB
Line 
1It's possible to remove one of the skips in RTLabs that's breaking the cost
2properties by changing the Clight syntax and translation to Cminor (see
32012-08-29-cost-label-bug.txt), but there's still one caused by the need to
4have
5
6  exit: cost: skip;
7
8in the else clause of the loop guard (see my email to the cerco list for
9details).
10
11One approach to fix this would be the original plan B: to forget about avoiding
12the skips and introduce an RTLabs transformation to remove them.  This
13is a bit tricky when there is a chain of several skips, although we
14could keep the changes to Clight and the transformation and just remove
15single skips (or iterate to a fixed point), which is easier.
16
17Otherwise, the obvious ideas for changing the Cminor to RTLabs
18translation are:
19
20 1. build up the label map during translation rather than
21    preinitialising it - except that we need it to translate gotos,
22    possibly before the labels they go to
23
24 2. supply the label to use for the CFG node to add_stmt
25 3. change the label of the enclosed statement's translation
26
272 and 3 break with
28
29  l1: l2: s;
30
31because we'll generate different labels for l1 and l2; and for 3 we'd
32have to know that the statement isn't already referred to by something
33in the graph.
34
35A variant on 1 that might work would be to have a special goto statement
36that takes a Cminor statement [1], that we rewrite to a proper skip to
37the right label afterwards.  The difficulty with this is having to rule
38out the special statement everywhere after construction, or using an
39alternative definition during construction.
40
41Or... put in some kind of dummy statement, and construct a mapping
42
43  RTLabs CFG label ⇀ Cminor goto label
44
45for goto statements, and a mapping
46
47  Cminor goto label → RTLabs CFG label
48
49for the goto labels (where the CFG label is for the enclosed statement,
50we don't need to generate anything for the goto label).  This might even
51simplify the invariant handling a little because the dummy statement for
52gotos won't break the graph closure.
53
54
55[1] Aside: at the moment gotos get translated into skips with the
56appropriate destination, but we could avoid generating anything by
57setting the entry point straight to the label instead, and adjusting the
58invariant on the entry point to match (it currently *must* be in the
59partially complete graph).  This might cause problems with fixing
60labels, though.  (Imagine being given l: goto l;)
61
62Oh, this is what the prototype does.
Note: See TracBrowser for help on using the repository browser.