[ redirected away from the -patches list because I want to ask a more general
theoretical question about compiler development ]
Richard Guenther wrote:
> During points-to pointer equivalence sets are computed by adding
> special RESTRICT heap-variables to points-to sets of targets of
> pointer conversions to restrict, global restrict qualified pointers
> and restrict qualified pointer arguments.
>
> A RESTRICT in the points-to set of a restrict qualified pointer
> acts as a filter for NONLOCAL and ANYTHING. The RESTRICT in the
> points-to sets make pointers based on each other conflict,
> non-restrict qualified pointers conflict with restrict qualified
> pointers if they point to anonymous memory (NONLOCAL or ANYTHING)
> or otherwise.
> Comments? Holes in my treatment of restrict?
I'd guess there has to be some way in formal logic or propositional calculus
by which we could take descriptions such as Richard's above, and the
description of restrict semantics in the standard, and reduce them each to a
pile of propositions that we could feed into a theorem-proving system and get
it to prove they were identical.
But I'm guessing: this kind of area is a million miles outside anything I'm
familiar with. However, we've got a load of very clever academic types on the
list here, so I thought I'd throw it open for discussion. There have been a
bunch of papers and a few big projects in academia on provable compiler
correctness, but they all seem very ambitious and not like anything we could
make an applied use of in GCC; but is there some simpler, practical and
well-understood tool-set already existing that we could put into use for small
jobs such as the above?
cheers,
DaveK
