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

Jan 26, 2019

Victor Porton

Jan 26, 2019

Victor Porton

Jan 26, 2019

Jan 27, 2019

Jan 28, 2019

Feb 27, 2019

Mar 17, 2019

Mar 28, 2019

https://issues.dlang.org/show_bug.cgi?id=19621 Neia Neutuladh <dhasenan@gmail.com> changed: What |Removed |Added ---------------------------------------------------------------------------- Keywords| |spec Priority|P1 |P3 Status|NEW |RESOLVED CC| |dhasenan@gmail.com Resolution|--- |WONTFIX Severity|major |minor --- Comment #1 from Neia Neutuladh <dhasenan@gmail.com> --- Making it defined behavior would forbid memoizing based on reference equality and sharing immutable data between threads. It might mean that string constants must be copied on program startup so they're not in read-only memory. It would mean that immutable means no more than const. This would be a major change requiring a DIP, and it would certainly be rejected. Now. In order to make it *not* be undefined behavior to cast something to immutable while other mutable references exist to that data, and *only* be undefined behavior to write to that data, you'd have to increase the scope of "what behavior is potentially undefined" to every time you write to memory that might have more than one reference to it. For instance: --- void doSomething(ubyte[]); auto buf = new ubyte[512]; doSomething(buf); buf[0] = 1; --- Should that be potentially undefined behavior? That's what we would have to do in order to make things more consistent between those to aspects of the spec, and that really should be well-defined behavior. 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. --

January 27, 2019

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

Posted by ag0aep6g

Permalink

ag0aep6g

Permalink

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

ag0aep6g <ag0aep6g@gmail.com> changed:

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

--- Comment #2 from ag0aep6g <ag0aep6g@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-@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-@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.

--

https://issues.dlang.org/show_bug.cgi?id=19621 --- Comment #3 from ag0aep6g <ag0aep6g@gmail.com> --- (In reply to ag0aep6g from comment #2) > As for a solution, maybe we can amend the definition of @trusted. https://github.com/dlang/dlang.org/pull/2561 --

https://issues.dlang.org/show_bug.cgi?id=19621 Dlang Bot <dlang-bot@dlang.rocks> changed: What |Removed |Added ---------------------------------------------------------------------------- Keywords| |pull --- Comment #4 from Dlang Bot <dlang-bot@dlang.rocks> --- @aG0aep6G updated dlang/dlang.org pull request #2561 "spec: close a loophole in definition of `@trusted`" fixing this issue: - fix issue 19621 - The specification is self-contradictory on immutability https://github.com/dlang/dlang.org/pull/2561 --

https://issues.dlang.org/show_bug.cgi?id=19621 ZombineDev <petar.p.kirov@gmail.com> changed: What |Removed |Added ---------------------------------------------------------------------------- CC| |petar.p.kirov@gmail.com --

https://issues.dlang.org/show_bug.cgi?id=19621 Dlang Bot <dlang-bot@dlang.rocks> changed: What |Removed |Added ---------------------------------------------------------------------------- Status|REOPENED |RESOLVED Resolution|--- |FIXED --- Comment #5 from Dlang Bot <dlang-bot@dlang.rocks> --- dlang/dlang.org pull request #2561 "spec: close a loophole in definition of `@trusted`" was merged into master: - d0e4fcfab19c07baf978bc9eed926da1a61dc07e by aG0aep6G: fix issue 19621 - The specification is self-contradictory on immutability https://github.com/dlang/dlang.org/pull/2561 --

Forums