Date: Tue, 27 Aug 2013 12:18:48 -0700

On Tue, Aug 27, 2013 at 11:59 AM, Richard Smith <richardsmith_at_[hidden]> wrote:

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

I think that particular implementation is forbidden. The rule in

[expr.reinterpret.cast]p4 is: "A pointer can be explicitly converted

to any integral type large enough to hold it. The mapping function is

implementation-defined." Since it's a "function", it has to map a

domain value to only one value in the range.

Jeffrey

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

I think that particular implementation is forbidden. The rule in

[expr.reinterpret.cast]p4 is: "A pointer can be explicitly converted

to any integral type large enough to hold it. The mapping function is

implementation-defined." Since it's a "function", it has to map a

domain value to only one value in the range.

Jeffrey

Received on 2013-08-27 21:19:10