Jeffrey Yasskin <jyasskin_at_[hidden]> writes:

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

Hmm, I am unsure the use of the wording "mapping function" was meant to
imply that, or if we are reading too much into it.

-- Gaby