source: etc/campbell/dev-notes/2012-05-02-label-switch.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: 1.5 KB
1We add cost labels to switch statements by putting a cost label on each possible
2branch.  When the semantics executes a switch, it models fall-through by
3transforming the tail of the labeled_statements from the matching case
4through to the end into a sequence of statements.
6So (in pseudocode)
8  Swhile 2 (LScase 1 s1 (LScase 2 s2 (LScase 3 s3 (LSdefault sd))))
10steps to
12  Sseq s2 (Sseq s3 sd)
14Hence after cost labelling we will get
16  Sseq (Scost c2 s2) (Sseq (Scost c3 s3) (Scost cd sd))
18So we somehow have to allow for the extra steps at each new cost label, and
19the appearance of cost labels in the middle of a normal looking statement.
21We can perhaps express this by relating states that involve the transformation
22from labeled_statements to a single statement.  I'm still tempted to rework the
23switch statements properly, though, and get my Duff's Device.
27That almost worked: for each LScase we can match the step for the Sseq to
28the Sseq+Scost in the transformed version, but it falls down at LSdefault.
29We can't associate that last cost label with the execution of the Sswitch
30because we might Sgoto a label in the previous case.
32I see three choices:
34 1. use a weaker form of simulation (matching zero steps to the cost label
35    at LSdefault),
36 2. hack the Clight semantics to add an extra dummy statement, or
37 3. show the result *except* for the labeled_statements case, then prove it
38    afterwards by showing that the cost label can be folded into the execution
39    of the subsequent statement.
413 sounds like the most fun.  And worked.
Note: See TracBrowser for help on using the repository browser.