Software Assurance Reference Dataset

[H. S. Teoh via Digitalmars-d]

On Thu, Jun 26, 2014 at 04:47:24PM -0700, Andrei Alexandrescu via Digitalmars-d wrote:
> On 6/26/14, 4:16 PM, Timon Gehr wrote:
> >- Annotations can include a formal proof.
> 
> If a function can be annotated with what other functions it calls
> (non-transitively), I agree that it can be guaranteed with local
> semantic checking that a program won't overflow. However requiring
> such annotations would be onerous, and deducing them would require
> whole program analysis.
> 
> >We've had similar discussions before. Why do we _still_ have to argue
> >about the _possibility_ of having a system that is helpful for
> >proving stack overflows (or other bad behaviours) absent?
> >
> >You can say "out of scope" or "not a priority" or "this should be
> >realized in third-party tool support" but not "it is impossible".
> 
> I also seem to reckon Walter is in the other extreme (he asserts it
> can't be done at all, period). My understanding is that it can be done
> but only with annotations or whole program analysis.
[...]

I think the compiler should be able to tell, at least for the simplest
cases, whether something will definitely stop recursing. Proving that
something will *not* stop recursing is unsolvable in the general case,
but even if we restrict it to a solvable subset, it's still far from
trivial for the compiler to invent such a proof (unless we restrict it
so much that it excludes too many useful algorithms).

One approach is to have the user supply a proof that the compiler can
then check -- in general, if a proof exists at all, it should be
checkable. Such checks furthermore can probably be done fast enough so
as to not adversely affect current compilation times (unless the proof
is ridiculously complex, which for practical real-world applications I
don't think will happen).

However, absence of proof is not proof of absence; just because neither
the compiler nor the user is able to come up with a proof that something
will stop recursing, doesn't mean that it definitely won't stop
recursing. So the compiler cannot definitively reject the code as
definitely overflowing the stack. But we *can* make it so that the user
tells the compiler "please stop compilation if neither of us can supply
a proof that this function will stop recursing". But it has to be
opt-in, because there will be many real-world applications that cannot
be proven to stop recursing, even though in practice they always will,
so we cannot make this a language default.

One particular example that comes to mind is the compiler itself: as it
parses the input program, there is in theory no guarantee that the input
won't have an arbitrarily deep nesting, such that the AST generated by
the parser will be infinitely deep, because you cannot statically prove
that the input will terminate. You don't know if the input file is
actually connected to the output pipe of a program that prints an
infinite series of ever-deeper nested structs, for example.  However, in
practice, such input never occurs, so we generally don't worry about
such contrived possibilities.  But this does mean that there can be no
proof of termination of recursion, even user-supplied ones -- because
there *are* cases where the parser *will* recurse forever, even if it
never happens in practice. Not accounting for that possibility
invalidates the proof, so any proof will always be rejected.  Therefore,
it is impossible to prove that recursion in the compiler is finite, even
though in practice it always is.


T

-- 
"Life is all a great joke, but only the brave ever get the point." -- Kenneth Rexroth