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).

John.