1 | I've been proposing that we add a function to check whether a function is |
---|
2 | soundly labelled in RTLabs, for three reasons: |
---|
3 | |
---|
4 | 1. If we run short of time we can use it as a runtime check rather than proving |
---|
5 | that the Clight programs are soundly labelled and that sound labelling is |
---|
6 | preserved. |
---|
7 | |
---|
8 | 2. It will be faster; in particular, we'll be able to test whether some |
---|
9 | programs are soundly labelled before attempting to prove the transformations |
---|
10 | correct. |
---|
11 | |
---|
12 | 3. We'll have the option of importing RTLabs code. |
---|
13 | |
---|
14 | The requirements for labels at the head of the function and after each branch |
---|
15 | are easy to check, but the bound on the number of instructions until a cost |
---|
16 | label is more difficult. However, it does live in Prop, so we don't actually |
---|
17 | need to calculate and store the bound, just prove that the checker says yes |
---|
18 | iff it exists. |
---|
19 | |
---|
20 | So, the obvious checker is to traverse the function from the entry point |
---|
21 | keeping a set of the CFG labels seen since the last cost label, and failing if |
---|
22 | we spot a loop without a cost label. We then need to prove the existence or |
---|
23 | otherwise of a bound. |
---|
24 | |
---|
25 | To make this a little easier, perhaps we can keep the labels in a list (with a |
---|
26 | proof that they are not cost labels, then reuse the bad_label_list definition |
---|
27 | and loop_soundness_contradiction lemma from the unrepeating proof in |
---|
28 | RTLabs/Traces.ma to construct the proof that there's no bound. |
---|
29 | |
---|
30 | Questions: |
---|
31 | |
---|
32 | - Intuitively, the control flow graph ought to be connected, but do we check |
---|
33 | that, require it, or cope without it? If we want to reject functions with |
---|
34 | dead code we'll have to add that to the spec. Otherwise we'll need to |
---|
35 | check all of the components of the CFG in order to prove that there's a |
---|
36 | bound for every instruction. |
---|
37 | |
---|
38 | |
---|
39 | ----- |
---|
40 | |
---|
41 | 27th Aug: |
---|
42 | |
---|
43 | There's a problem in the above: when we see a branch we must check both branches |
---|
44 | for a bound, so we can't just trace the function one instruction at a time from |
---|
45 | the start. Unless, that is, we check before that each branch is followed by |
---|
46 | cost labels. We already do that, so we can just do one at a time. |
---|
47 | |
---|
48 | [It gets a bit sketchy below because I started trying a couple of different |
---|
49 | directions, then just wrote the code instead. See the code for the final |
---|
50 | version.] |
---|
51 | |
---|
52 | So, we |
---|
53 | |
---|
54 | - Write a checking function which takes a set of CFG labels which haven't been |
---|
55 | checked yet (but are cost labels, or successors of cost labels?), a list |
---|
56 | giving a string of (successive) labels which we are currently looking for |
---|
57 | a cost label for, and a set of labels which we have already got a bound for. |
---|
58 | |
---|
59 | It looks at the next instruction, and |
---|
60 | + for cost labels moves the list into the set of labels we have a bound |
---|
61 | for and continues from the successor of the cost label (with the cost |
---|
62 | label in the list), |
---|
63 | + for branches moves the list into the set of labels including the branch |
---|
64 | itself and continues with one of the branches and puts the other into |
---|
65 | the set of labels to check |
---|
66 | + for everything else |
---|
67 | |
---|
68 | |
---|
69 | a function which checks for a bound for a particular label in the CFG by |
---|
70 | saying yes if it's a branch (because the prior check means the successors are |
---|
71 | cost labels); says yes if it's a return statement; says yes if the (necessarily |
---|
72 | single) successor has already been checked; says yes if the successor is a cost |
---|
73 | label; says no if it's in the list of labels being checked; recursively checks |
---|
74 | the successor otherwise. How to witness termination? One possibility is |
---|
75 | |set of nodes to check|. |
---|
76 | |
---|
77 | |
---|
78 | Keep set of unchecked nodes rather than checked nodes because we only need |
---|
79 | an emptiness check (by cardinality?) and a choice fn, rather than equiv |
---|
80 | checking and minus (we already have that, but we'd need to do it every outer |
---|
81 | iteration and reason around it). |
---|