On Tue, Jun 23, 2009 at 4:53 PM, Dave
Korn<dave.korn.cyg...@googlemail.com> wrote:
> [ 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?
We should have proper testsuite coverage for language features.
In this case the XPASS on the vector testcase shows me a major
flaw in my implementation:
int a[N];
__attribute__ ((noinline)) int
foo (int * __restrict__ b, int k){
...
with the proposed patch b would not alias a. Maybe desirable
for optimization but certainly not what the C language suggests.
Thus I'm back to a separate representation and oracle treatment
for restrict. Bah. That'll cost.
Richard.
