I've been proposing that we add a function to check whether a function is
soundly labelled in RTLabs, for three reasons:
1. If we run short of time we can use it as a runtime check rather than proving
that the Clight programs are soundly labelled and that sound labelling is
preserved.
2. It will be faster; in particular, we'll be able to test whether some
programs are soundly labelled before attempting to prove the transformations
correct.
3. We'll have the option of importing RTLabs code.
The requirements for labels at the head of the function and after each branch
are easy to check, but the bound on the number of instructions until a cost
label is more difficult. However, it does live in Prop, so we don't actually
need to calculate and store the bound, just prove that the checker says yes
iff it exists.
So, the obvious checker is to traverse the function from the entry point
keeping a set of the CFG labels seen since the last cost label, and failing if
we spot a loop without a cost label. We then need to prove the existence or
otherwise of a bound.
To make this a little easier, perhaps we can keep the labels in a list (with a
proof that they are not cost labels, then reuse the bad_label_list definition
and loop_soundness_contradiction lemma from the unrepeating proof in
RTLabs/Traces.ma to construct the proof that there's no bound.
Questions:
- Intuitively, the control flow graph ought to be connected, but do we check
that, require it, or cope without it? If we want to reject functions with
dead code we'll have to add that to the spec. Otherwise we'll need to
check all of the components of the CFG in order to prove that there's a
bound for every instruction.
-----
27th Aug:
There's a problem in the above: when we see a branch we must check both branches
for a bound, so we can't just trace the function one instruction at a time from
the start. Unless, that is, we check before that each branch is followed by
cost labels. We already do that, so we can just do one at a time.
[It gets a bit sketchy below because I started trying a couple of different
directions, then just wrote the code instead. See the code for the final
version.]
So, we
- Write a checking function which takes a set of CFG labels which haven't been
checked yet (but are cost labels, or successors of cost labels?), a list
giving a string of (successive) labels which we are currently looking for
a cost label for, and a set of labels which we have already got a bound for.
It looks at the next instruction, and
+ for cost labels moves the list into the set of labels we have a bound
for and continues from the successor of the cost label (with the cost
label in the list),
+ for branches moves the list into the set of labels including the branch
itself and continues with one of the branches and puts the other into
the set of labels to check
+ for everything else
a function which checks for a bound for a particular label in the CFG by
saying yes if it's a branch (because the prior check means the successors are
cost labels); says yes if it's a return statement; says yes if the (necessarily
single) successor has already been checked; says yes if the successor is a cost
label; says no if it's in the list of labels being checked; recursively checks
the successor otherwise. How to witness termination? One possibility is
|set of nodes to check|.
Keep set of unchecked nodes rather than checked nodes because we only need
an emptiness check (by cardinality?) and a choice fn, rather than equiv
checking and minus (we already have that, but we'd need to do it every outer
iteration and reason around it).