Jeffrey Yasskin <jyasskin_at_[hidden]> writes:

| Thanks for chiming in!
|
| On Tue, Aug 27, 2013 at 1:00 AM, Xavier Leroy <Xavier.Leroy_at_[hidden]> wrote:
| >> [Semantics of pointer comparisons]
| >> Xavier Leroy, the author of CompCert, and I have had long discussions
| >> about this about a year ago. He is on the list, so he will add
| >> clarifications or corrections when he gets a chance. Last time (last
| >> Spring) we talked again about this, he said he has made some adjuments,
| >> but I don't recall the details.
| >
| > Yes, I'll chime in. Just a bit of context for the members of this
| > list: as part of the formal verification of the CompCert compiler, I
| > and others have been giving formal semantics to a large subset of ISO
| > C, and (with Tahina Ramananandro and Gabriel Dos Reis) to some aspects
| > of C++ too.
| >
| > >From the standpoint of formal semantics, it is easier to account for
| > undefined behaviors (when everything can happen, incl. crashing) than
| > for defined-but-unspecified behaviors (when several but not all
| > outcomes are possible). And of course accounting for
| > defined-and-uniquely-specified behaviors is easier too.
| >
| > The example that Gabriel was alluding to is equality tests between a
| > pointer "one past" the end of an object and a pointer to the beginning
| > of another object. In C and C++, if I'm not mistaken, this is defined
| > behavior but can return true or false at the whim of the
| > implementation. This nondeterminism was difficult to account for in
| > CompCert's semantics, so in the end we treat it as undefined behavior,
| > while still defining comparisons involving pointers "one past" as long
| > as the pointers are within the same object.
| >
| > Coming back to the proposal of making "<" a total (but unspecified
| > order on pointers):
| >
| > - As a semanticist, I think it would be challenging to formalize, for
| > the general reasons given above.
|
| How do you model std::less<T*>, which already requires this total but
| unspecified order?

Ths standards semantocs of std::less<T*> is very abstract. In
particular it isn't related to anything having to do with object extents
or aliasing. In particular it isn't required to be "p < q". Cast to
uintptr_t and compare the result is just acceptable.

-- Gaby

|
| > - As a programmer, I see how this could be very useful to implement
| > various generic data structures, or to choose a "canonical"
| > representative between several semantically-equivalent data structures.
| >
| > - As a compiler writer, I can see a few useful optimizations that this
| > change would invalidate. Here is an example:
| >
| > int x[2];
| > int * p;
| > ...
| > if (p <= x + 1) {...} else {...}
| >
| > With the current semantics, "p <= x + 1" is only defined if p points
| > within x, so it is equivalent to "p != x + 2", which gives useful
| > aliasing information in the two branches of the conditional.
| > This is a contrived example, though.
| >
| > - As an amateur of garbage-collected languages, I see a problem with
| > relocating garbage collection. (C++ doesn't require a GC, but it is
| > my understanding that the C++ committee is trying to make C++
| > compatible with the use of a GC.) A relocating GC can move objects
| > around, changing their absolute addresses. So, the unspecified
| > total order on pointers could change during the execution of the
| > program: before a GC, we have "p < q"; then q is moved, and then
| > "p > q". This would make the total order unusable to
| > e.g. order binary search trees...
| _______________________________________________
| ub mailing list
| ub_at_[hidden]
| http://www.open-std.org/mailman/listinfo/ub