[Issue 19621] The specification is self-contradictory on immutability

[d-bugmail at puremagic.com]

https://issues.dlang.org/show_bug.cgi?id=19621

ag0aep6g <ag0aep6g at gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           Keywords|                            |safe
             Status|RESOLVED                    |REOPENED
                 CC|                            |ag0aep6g at gmail.com
         Resolution|WONTFIX                     |---

--- Comment #2 from ag0aep6g <ag0aep6g at gmail.com> ---
(In reply to Neia Neutuladh from comment #1)
> ---
> void doSomething(ubyte[]);
> 
> auto buf = new ubyte[512];
> doSomething(buf);
> buf[0] = 1;
> ---
> 
> Should that be potentially undefined behavior?

As far as I understand, you're hinting at things like this:

----
immutable(ubyte)[] ia;
void doSomething(ubyte[] arg) @trusted
{
    ia = cast(immutable) arg; /* UB or not? */
}
----

If the cast had defined behavior, then that `doSomething` would be correctly
`@trusted`. The function itself wouldn't exhibit undefined behavior. It would
just set the program up to exhibit UB later on, in @safe code. And there's the
problem. @safe code must never ever exhibit undefined behavior. So
`doSomething` can't be @trusted. The cast or the assignment to `ia` must be
invalid. (Making `buf[0] = 1;` non- at safe would be silly.)


> By making only the cast to immutable potentially undefined, and then writing
> to something cast from immutable undefined, the total amount of undefined
> behavior is reasonably limited.

As far as I see, the problem exists in both directions. When casting immutable
away is okay, then we have this:

----
ubyte[] ma;

void doSomething(immutable ubyte[] arg) @trusted
{
    ma = cast(ubyte[]) arg; /* Not UB according to the spec. */
}

void main() @safe
{
    auto buf = new immutable ubyte[512]; /* all zeroes */
    doSomething(buf);
    ma[0] = 1; /* Writing a one over an immutable zero. UB in @safe code. Not
good. */
}
----

The spec tries to address this problem by stating that "one must assume the
responsibility to ensure the immutability of the data, as the compiler will no
longer be able to statically do so." Unfortunately, that's not really
compatible with how @safe and @trusted are defined. We need to put the safety
violation into non- at safe code. Else we have a hole in @safe.

I'm reopening this issue. As far as I see, Victor is correct, and the two parts
of the spec are at odds with each other. Both directions of casting create a
mutable and an immutable view of the same data. Either that is okay, or it
isn't.

As for a solution, maybe we can amend the definition of @trusted. The spec
currently only says that "[trusted] functions [must] not exhibit any undefined
behavior if called by a safe function." What if we add that they also must not
affect the safety of any following @safe code? I.e., after calling a trusted
function, one must be able to assume that @safe code still cannot exhibit
undefined behavior.

With such an addition, the examples of `doSomething` above would both be
invalid, because the author cannot guarantee the safety of following @safe
code. But the casts themselves could be allowed in both directions.

--