stack level analysis

[skaller]

I'm trying to figure out a reasonable way to do stack level analysis.

A first order analysis is like so:

• every instruction has a stack delta range.
• This is the minimum and maximum possible net change to the stack evaluating the instruction.
• A straight line sequence has a delta range which is the sum of the range end points.
• I think the only single instruction where the minimum and maximum delta differ is cdrop
• Branches of a condition could have different deltas
• The deltas for a loop must be zero otherwise the program could over or underflow the stack.
• The deltas can be tracked by a single linear scan or recursive descent

What we would like is a way to assign a validation level to the program.

• If the stack delta range at the end of the program is empty, i.e. the minimum and maximum deltas are equal,
  the program can be considered verified with respect to consistent stack use.
• if any loop has non-zero deltas, the program is very likely broken

Now this leaves the problem of divergence due to conditionals.
If that happens inside a loop, the program is likely broken.

However two conditionals in sequence could re-adjust the stack, so we need to work hard especially inside
a loop, to figure out if that is, or might be, the case. In particular, if the same condition is tested twice in two conditionals, one after the other, and the opposite branch has the opposite delta, the delta then can re-converge.

I think this needs data flow analysis which is normally extremely hard.
However in MVM the situation is not so bad. Ignoring repeat, there's only one way to branch backwards,
in a while loop, and while loops must have zero deltas (or we just give up).
So the remaining analysis, including inside a loop, ie purely flow towards the end.
And since there are no gotos, control forks from conditionals are always followed by joins.

So we might be able to notice that two conditionals have net zero deltas (more generally any sequence) and
assume the branches must be taken so that this occurs. In particular we can print an annotation next
to these conditionals and explain the programmer must prove the requirements (even if the analysis program cannot).

However this requires more than merely tracking the minimum and maximum stack levels, it means tying the difference to particular branches, that is, to the boolean on the top of the stack when the if is encountered.

if.true  # branch 1
  drop
else  # branch 2
  push.1
end # join 
...
if.true # branch 3
  drop
else branch 4
  push.1
end # join: branch 3 must be taken if branch 2 was previously, branch 4 if branch 3 was previously

We can prove this if we can prove the condition on the stack before the first if is the not of that before the second if.
Which has a trivial constraint c1 + c2 = 1.

If there are say three conditionals, or more complex deltas, it's a lot harder.