Hi Freek,

On Sun, 11 Oct 2020 at 20:27, Freek Wiedijk <freek_at_[hidden]> wrote:

> Dear Peter (CC all),
>
> >Within the domain it's addressing, it's doing exactly what Freek suggests:
> >there is some abstract state, recording provenance info, which "takes
> >precedence" in the sense that that is what is used for provenance UB
> >checks, then one falls back to the concrete model when eg reading
> >a pointer value that has been manipulated bytewise.
>
> My point is that in your model the abstract state is just
> something supplementary on top of a memory consisting
> of bytes. That's clumsy, because it will get *very*
> complicated (effective types, provenance, wobbliness,
> and you probably will have to add other stuff later).
> I think it's much cleaner to have an "abstract memory"
> as a first class thing (and then maybe have the "memory
> consisting of bytes" as the thing that is supplementary,
> although having both on an equal footing appeals to me more.)
>
> So if I have an pointer to the end of a subobject next to
> a pointer to the start of the next adjacent subobject, in
> my abstract memory it's immediately clear which is which.
> With the "provenance" approach as you propose it, it's not,
> I think.
>

As I said, the proposal of this TS is not intended to be the last word
on all this - it's just not possible to address every problem at once
within the constraints of available ISO committee time (or, for that
matter,
ours). We have to take this one step at a time.

The TS deliberately does not distinguish pointers to different subobjects,
but that's
because of what we choose to address, not because one can't. It's
also orthogonal to whether one phrases things in terms of
concrete state augmented with some "ghost" state, or in terms of interlinked
abstract and concrete models.



>
> When you have unions it gets even worse. Unions are where
> the hard problems are, the rest is much easier.
>
> When you poke bytes into a union, which variant will you get?
> And what can change the variant of a union? (In Robbert's
> CH2O model, he had annotations of pointers for that.)
> Does the provenance approach say something about that?
> In the TS for the upcoming meeting I just see something about
> type punning, but I'm talking about pointers pointing *into*
> the union object, not subobjects *of* the union object.
> I think the problems here become much more apparent when
> you take a "first class" abstract memory model as the basis.
>

The TS model is only talking about per-allocation provenance, so no,
it's not talking about union variants in that sense. Though it does talk
about what
happens from integer/pointer casts arising from union punning.


>
> To argue that what I propose is really different (I think):
> if you go in a *very* deep recursion with on every level
> a local variable of which you take the pointer, your model
> (which has bytes as the primitive notion) will eventually
> run out of object representations, right? Mine won't,
> because unless you start poking at bytes or intptr_t
> representations of those pointers, there *are* no bytes,
> it's all just abstract values. My proposed model really
> can have arbitrarily deep recursion, even when a finite
> size pointer type will get arbitrarily many different values.
>

Having finite-size pointer types in the model seems to me to be a clear
positive thing, not a negative, so I'm not sure what you're saying here.


>
> So I'm not sure I buy the claim that what you propose will
> in the end be the same as what I would like.
>

I'm certainly not claiming that you will certainly like it :-) But
I don't so far see that it's doing anything essentially different.

Peter



> Freek
>