On Thursday, 17 June 2021 at 19:06:31 UTC, Paul Backus wrote:

Yes, but if I make size() @trusted and fix the bug then interface is provably safe?

class A {

    this() @trusted {
        ptr = &buffer[0];
        offset = 0;
    }

    int get() @trusted { return ptr[offset]; }
    void set(int i) @trusted { this.offset = i&1; }
    int size() @trusted { return 2;}
private:
    int[2] buffer;
    int* ptr;
    int offset;
}



  Also, if I do this, it is probably safe, because of the invariant that is checked?

class A {

this() @trusted {
    ptr = &buffer[0];
    offset = 0;
}

int get() @trusted { return ptr[offset]; }
void set(int i) @trusted { this.offset = i&1; }
int size()@safe{ offset=2; return 2;}
invariant{ assert(0<= offset && offset <=1 ); }

private:
int[2] buffer;
int* ptr;
int offset;
}

On Thursday, 17 June 2021 at 20:25:22 UTC, Ola Fosheim Grøstad wrote:

Assuming issue 20941 is fixed, yes.

[...]

    invariant{ assert(0<= offset && offset <=1 ); }

Yes.

On Thursday, 17 June 2021 at 20:33:33 UTC, Paul Backus wrote:

[…]

Thanks.

There seems to be many interpretations of what safe means though. Right now, safe interfacing with C seems like opening Pandora's box.

Probably a good idea to write up a set of best practice rules for making safe interfacing with C libraries (with examples).

On Thursday, 17 June 2021 at 20:42:20 UTC, Ola Fosheim Grøstad wrote:

A lot of people on the D forums have an incomplete or incorrect understanding of what memory safety means, and how D's @safe, @trusted and @system attributes can be used to help prove a program memory-safe. The interpretation that I and ag0aep6g have been describing is the correct one.

Re: interfacing with C, the best guarantee you can reasonably hope to achieve is "my @trusted code is memory safe as long as the C functions I'm calling behave as specified in the relevant documentation or standard." I go into more detail about this in my blog post on memory safety in D.

On Thursday, 17 June 2021 at 20:57:27 UTC, ag0aep6g wrote:

I mean that this should satisfy the requirements (fixed a bug that allowed ptr to be changed after construction):

class A {

    this() @trusted {
        ptr = &buffer[0];
        offset = 0;
    }

    int get() @trusted { return ptr[offset]; }
    void set(int i) @trusted { this.offset = i&1; }
    int size()@trusted{ return 2;}
private:
    int[2] buffer;
    const(int*) ptr;
    int offset;
}

1. There is no way for @safe code to make this unsafe.

2. I have through audit proven that all methods keep offset within the required range.

Then the requirements need to be made more explicit, because people seem to disagree as to what is required.

No, that is not what I want. I want to define the necessary invariants to uphold safety. Then prove that my class remains within the constraints.

Yes, preventing @safe code from writing to some variables might make that task easier. In the meanwhile I can just make all methods @trusted.

But @trusted requires you to manually audit the invariants needed, so why force a weakening of the invariants that are needed to make it safe? That makes no sense, if you already are required to conduct a manual audit. The compiler has no say in this either way.

People will do it, and they will be correct and sensible for doing so. By requiring an audit we already presume that the auditor has the required skillset to reason about these issues at a formal level!

On Thursday, 17 June 2021 at 21:00:13 UTC, Paul Backus wrote:

Yet I would answer "no" where you answered "yes" above.

The question was: "Yes, but if I make size() @trusted and fix the bug then interface is provably safe?".

The corresponding code:

class A {

    this() @trusted {
        ptr = &buffer[0];
        offset = 0;
    }

    int get() @trusted { return ptr[offset]; }
    void set(int i) @trusted { this.offset = i&1; }
    int size() @trusted { return 2;}
private:
    int[2] buffer;
    int* ptr;
    int offset;
}

In my opinion, that code is fundamentally equivalent to this (regarding the safety of get):

int get(int* ptr, int offset) @trusted { return ptr[offset]; }

That function does not have a safe interface, because it exhibits undefined behavior wenn called like get(new int, 1000), which @safe code can do.

private, other methods, the constructor - those things don't matter.

On Wednesday, 16 June 2021 at 23:52:02 UTC, Bruce Carneal wrote:

Ok, I think I understand better what you meant now.

So, essentially, one is currently forced to make perfectly @safe code @trusted because if there is any possibility that a @safe method contains a bug (even if 100% unlikely) that affects assumptions made in @trusted code then that @safe method can no longer be considered safe.

So basically one wants @trusted code to be checked by the compiler just like @safe, and then instead explicitly turn off the checking in a more narrow unsafe region within the @trusted method.

Unless pending DIPs turn out to remove this issue completely. Time will show, I guess.

On Thursday, 17 June 2021 at 21:00:13 UTC, Paul Backus wrote:

There is a difference between proving a program memory safe and having to assume that all @safe code is maximally broken. Which is what is required here.

Also, ag0aep6g are not happy with proving that the class is memory safe. It has to be memory safe when non-pointer values are overwritten with garbage. He wants you to look at each @trusted method in isolation, not the class as a whole.

More tricky that that I think. If I obtain a DOM node from a C library, then that DOM node points to the parent node, and so on, effectively I could have the entire C heap in my hands.

You basically either have to create slow wrappers around everything or manually modify the C-bindings so you give less information to the D compiler than the C compiler has (basically censor out back pointers from the struct)??

Or maybe not. Either way, it is not trivial to reason about the consequences that you get from obtaining not just objects from C-code, but nodes in a connected graph.

I haven't tried to create such safe bindings, maybe I am wrong. Maybe there are some easy patterns one can follow.