Re: g++ and aliasing bools

[Daniel Berlin <dan at dberlin dot org>]

On Fri, 25 Jan 2002, Robert Dewar wrote:

> I agree with Richard, there are no undecidability problems here, we are
> talking about static proofs that two objects cannot be aliased.

You would be incorrect.
Type based aliasing says "we have some sets of types that we know alias each other, 
if you have one of these types, and we can tell you whether you may 
alias some other set of types".
The language semantics don't necessarily give you enough to be able to 
place all types in the right sets. If it doesn't, you are back to 
undecidability.
In the case of C++, they don't.
Given no C++ ABI restrictions, it's undecidable, because we don't know 
what pieces of vtables, etc, are shared. You cannot determine, based soley 
on what you find in the C++ standard, whether two types alias, for all 
cases.  Thus, you cannot determine properly, using only the C++ standard, 
the alias set a type necessarily belongs to.  Worse, using only the C++ 
standard, you might end up being just plain wrong, and saying two things 
alias that don't, or the other way around.  It's completely implementation 
dependent.
Nothing in the C++ language will let me prove whether or not two objects share a vtable or not.
The question is whether our C++ abi provides enough to enable us to build 
all the sets properly.
The whole issue is whether i'm going to write up a formal proof of whether 
we our C++ ABI lets us do it for some restricted subset, using C 
semantics.
I'm not going to write that up.
It's just too difficult to go about formally proving.

> Either we can prove that, or we assume that they are aliased. The issue of whether
> they are *really* aliased at run time is interesting, but irrelevant.