g++ and aliasing bools

[Mark Mitchell]

--On Friday, January 25, 2002 01:38:53 PM -0500 David Edelsohn 
<dje@watson.ibm.com> wrote:

>>>>>> Paolo Carlini writes:
>
>>> Honestly, I cannot imagine why the bulk of the C aliasing analysis
>>> machinery could not be used for it!!!!
>
> Mark,
>
> 	You originally contributed c_get_alias_set().  Would you please
> provide us with a reference to the proof showing that it is safe for C?

Your question is at best facetious.  You clearly intend to point
out that I did not provide a proof originally.  I did not, but that
doesn't make it right.  Part of the reason I am asking for a proof
now is that the original changes resulted in problems which a took
a while to untangle.  That was a mistake; one I have learned from.

In addition, the rules which I implemented were much simpler than
the sorts of things that can appear with overlaid class types in
C++.  I have already spent days debugging C++ alias set problems
(everything from vtables to multiple inheritance) so I am once-bitten
twice-shy in that regard.  There have been almost no alias set bugs
resulting in the generation of incorrect C code in ages -- much
better evidence than "this patch doesn't cause any regressions"
that the code is correct.

Furthermore, I did not ask for a proof that some piece of C code
was correct (as you do above), I asked for a proof that an
algorithm was correct.

Finally, you ignore the key point: either the proof is easy, or the
problem is hard.

None the less, I'm happy to provide a sketch.  I will do the version
without restrict (that was added later) and without the assignment of
alias sets to structs (Kenner added that later), and without
type-punning for unions (this is optional under ANSI/ISO C).

This is from memory; there might be minor mistakes.  Also note that
the code has changed considerably from my original version, which
makes it harder to see the structure.

1. The C aliasing rules say that if you reference memory using one
   type, you may not reference it using another types, unless:

   - The types are signed/unsigned variants of each other.

   - The types very only in their cv-qualification.

   - One of them is (possibly cv-qualified) "char".

2. Alias sets have the following semantics:

   - Two things in the same alias set may alias one another.

   - Things in two distinct alias sets may alias if one is
     a "subset" of another, under transitive closure.

   - All alias sets are a subset of a special alias set
     called "alias set zero".  (An immediate consequence is
     that something in alias set zero can alias everything.)

Let T be the set of all C types.  Let TA be a relation on TxT such
that (t1, t2) \in TA if and only if t and u may alias.

Similarly, let S be the set of all alias sets.  Let SA be relation on
SxS that (s1, s2) \in SA if and only if s1 and s2 may alias.  (Note
that in the original incarnation, there were no subsets other than
the fact that everything was a subset of alias set zero, so this
relation is well-defined statically.)

What we wish to prove is that C's lang_get_alias_set assigns
alias sets to type safely.  In particular, let f be
c_get_alias_set, and then:

Then, we wish to show that, for all t, u \in T:

   (t, u) \in TA \implies f(t), f(u)) \in SA

(We do not need if and only if for correctness.)

The proof is by induction.  All aggregate types are mapped
to alias set zero which aliases everything; therefore, we
need only consider non-aggregate types.  The code says:

  if (TREE_CODE (t) == INTEGER_TYPE && TREE_UNSIGNED (t))
    {
      tree t1 = signed_type (t);

      return get_alias_set (t1);
    }

Therefore, signed and unsigned variants of types get the same alias
set.

The code says:

  t = TYPE_MAIN_VARIANT (t);
  if (TYPE_P (t) && TYPE_ALIAS_SET_KNOWN_P (t))
    return TYPE_ALIAS_SET (t);

Therefore, if a cv-qualified type and its unqualified variant will
get the same alias set.  By transitivity, so will all cv-qualified
variants of the type.

The code says that:

  /* If this is a char *, the ANSI C standard says it can alias
     anything.  Note that all references need do this.  */
  if (TREE_CODE_CLASS (TREE_CODE (t)) == 'r'
      && TREE_CODE (TREE_TYPE (t)) == INTEGER_TYPE
      && TYPE_PRECISION (TREE_TYPE (t)) == TYPE_PRECISION (char_type_node))
    return 0;

Therefore, "char" is mapped to alias set zero, completing the proof.

--
Mark Mitchell                   mark@codesourcery.com
CodeSourcery, LLC               http://www.codesourcery.com