On Tue, Aug 27, 2013 at 11:37 AM, John Spicer <jhs_at_[hidden]> wrote:

>
> On Aug 27, 2013, at 1:39 PM, Jeffrey Yasskin <jyasskin_at_[hidden]> wrote:
>
> > On Tue, Aug 27, 2013 at 10:28 AM, Xavier Leroy <Xavier.Leroy_at_[hidden]>
> wrote:
> >> On 27/08/13 17:48, Jeffrey Yasskin wrote:
> >>>> - 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?
> >>
> >> No one tried, as far as I know. We (as a community) are still a long
> >> way from formalizing the complete semantics of a "big" language like
> >> C++, but an even longer way from formalizing specs for its standard
> >> library...
> >>
> >> There are plausible ways to formalize this total order at the source
> >> language level. But, as Gabriel wrote, the difficulty is to ensure
> >> that your source-level semantics is not making predictions that the
> >> compiler could invalidate later.
> >>
> >> In other words: at the end of the day, your pointers are just bit
> >> patterns that the hardware compares as if they were integers. If you
> >> could chase this hardware ordering of pointers back every compilation
> >> pass, it should be the case that the source-level ordering you obtain
> >> is one of those allowed by your source-level semantics. Proving this
> >> kind of properties sounds very challenging to me.
> >
> > Mhmm. It sounds like you probably can't model the
> > implementation-defined conversion to intptr_t yet either? Since
> > T*->intptr_t->T* has to be an identity map, and intptr_t is totally
> > ordered.
> >
> > If that's the case, it sounds like making operator< on T* a total
> > order would reduce the fraction of C++ that's currently formalizable
> > but wouldn't make it any harder to formalize the whole language?
>
> I think there would need to be one restriction (that may already exist,
> I'm not sure). I think an ordering of pointers would require that all of
> the pointers point to objects or within an object. I think we would have
> to prohibit attempting to find the order of "one past the last element" vs.
> another pointer as those could end up being the same even though they refer
> to different (logical) things, except in the case that is defined by the
> language (where the other points to an element of the array).
>
> With that rule, this function would provide ordering (where unsigned long
> is replaced with the appropriate type for a given implementation):
>
> typedef unsigned long integral_type_large_enough_to_hold_pointer;
> bool less(void* p1, void* p2) {
> integral_type_large_enough_to_hold_pointer i1, i2;
> i1 =
> reinterpret_cast<integral_type_large_enough_to_hold_pointer>(p1);
> i2 =
> reinterpret_cast<integral_type_large_enough_to_hold_pointer>(p2);
> return i1 < i2;
> }
>
> The actual operator need not be implemented that way, but given that with
> a rule such as the one above you *could* implement it that way, there does
> not seem to be a reason not to support ordering of pointers (with such a
> rule).


I don't think the above implementation is guaranteed to work; I don't
believe we have any guarantee that converting the same pointer value to an
integral type multiple times will yield the same integral value. (For
instance, I believe a conforming implementation could maintain a table of
pointers, to which it adds entries each time a pointer is cast to an
integer, and the integer value could be merely an index into that table.)