On 6/15/2014 12:44 AM, David Nadlinger wrote:
> On Wednesday, 11 June 2014 at 16:50:30 UTC, Walter Bright wrote:
>> On 6/11/2014 4:34 AM, Timon Gehr wrote:
>>> Not memory safe implies (is supposed to imply) not @safe but not @safe does not
>>> imply not memory safe.
>>
>> @safe in D == memory safe.
>
> What Timon is saying is that not all memory safe code is verifiably @safe.

In D, they are defined to be the same thing, so the statement makes no sense.

>
> @safe => memory safe, but not memory safe => @safe.
>
> David

David Nadlinger:

> @safe => memory safe, but not memory safe => @safe.

Apparently that's not true, according to the post on the LLVM blog linked here:
http://forum.dlang.org/thread/okratgxrikskmylmwrrx@forum.dlang.org

Bye,
bearophile

On Wednesday, 11 June 2014 at 16:50:30 UTC, Walter Bright wrote:
> On 6/11/2014 4:34 AM, Timon Gehr wrote:
>> Not memory safe implies (is supposed to imply) not @safe but not @safe does not
>> imply not memory safe.
>
> @safe in D == memory safe.

Why? I found dozens of cases when @safe is broken, let alone other issues in bugzilla.

After thinking about the @safety in D my conclusion is that it is impossible to evaluate memory and safety correctness of a code in which static type says nothing about where an object is allocated. Contrary to popular wisdom, one can have fixed array on heaps, classes on stack, etc. If any code which is potentially not safe is rejected, this would lead to lots of false positives making using the language very inconvenient. Even in that case, safety cannot be guaranteed by the language due to other issues, like separate compilation, etc. By the way, memory safety is also compromised by compiler bugs which make him generate buggy code. Note, when I counted memory safety problems, codegen issues were not counted.

@safe should not be considered as feature which ensures that the code is memory safe, but as a feature rejecting code with high probability of memory bugs. The difference is very important.

I have reached this conclusion some years ago and nothing has change in D since then which make me reconsidering my opinion (including that @safe holes were not fixed).

Note, that I do not critique the language, it is fine. It is very good system level language with powerful modelling features. It is not good at verifying memory correctness, because in such languages (unlike managed ones) burden of memory correctness lies mostly on programmer. If he thinks that he can outsource memory correctness to @safe, there is high probability that he would be suddenly surprised.

On 06/15/2014 10:33 AM, Walter Bright wrote:
>>
>> What Timon is saying is that not all memory safe code is verifiably
>> @safe.
>
> In D, they are defined to be the same thing,

Since when?

http://dlang.org/function

"Function Safety

Safe functions are functions that are _statically checked_ to exhibit _no possibility of undefined behavior_. Undefined behavior is often used as a vector for malicious attacks.

Safe Functions

Safe functions are marked with the @safe attribute.

The following operations are not allowed in safe functions:"

I.e. the documentation has two (conflicting) definitions and none of them is the one you claim there is.

> so the statement makes no sense.

Then please indicate how to fix the documentation. If you are going to claim the Humpty Dumpty privilege, I'll back off. Thanks.

On 06/11/2014 11:35 AM, Walter Bright wrote:
> What's not provable? Why would bit copying a struct not be memory safe?

Since you claim memory safe is the same as verifiably @safe, you are asking:

> What's not provable? Why would bit copying a struct not be verifiably @safe?

struct S{ int x; }

void main()@safe{
    S s,t;
    memcpy(&s,&t,S.sizeof); // error
}

So, what is it that you are trying to bring across?

On 6/15/2014 2:48 AM, Timon Gehr wrote:
> On 06/15/2014 10:33 AM, Walter Bright wrote:
>>>
>>> What Timon is saying is that not all memory safe code is verifiably
>>> @safe.
>>
>> In D, they are defined to be the same thing,
>
> Since when?
>
> http://dlang.org/function
>
> "Function Safety
>
> Safe functions are functions that are _statically checked_ to exhibit _no
> possibility of undefined behavior_. Undefined behavior is often used as a vector
> for malicious attacks.
>
> Safe Functions
>
> Safe functions are marked with the @safe attribute.
>
> The following operations are not allowed in safe functions:"
>
> I.e. the documentation has two (conflicting) definitions and none of them is the
> one you claim there is.
>
>> so the statement makes no sense.
>
> Then please indicate how to fix the documentation. If you are going to claim the
> Humpty Dumpty privilege, I'll back off. Thanks.


I don't know why the documentation says that. D's @safe is about memory safety, not undefined behavior.

Note that the list of eschewed behaviors are possibly memory corrupting. Signed integer overflow, for example, is not listed.

On 6/15/2014 2:30 AM, Maxim Fomin wrote:
> On Wednesday, 11 June 2014 at 16:50:30 UTC, Walter Bright wrote:
>> On 6/11/2014 4:34 AM, Timon Gehr wrote:
>>> Not memory safe implies (is supposed to imply) not @safe but not @safe does not
>>> imply not memory safe.
>>
>> @safe in D == memory safe.
>
> Why? I found dozens of cases when @safe is broken, let alone other issues in
> bugzilla.

Those are bugs. We aim to fix them.


> By the way, memory safety is also compromised by compiler bugs which make him
> generate buggy code. Note, when I counted memory safety problems, codegen issues
> were not counted.

I don't think we should mix intention with bugs. Bugs need to get fixed.


> I have reached this conclusion some years ago and nothing has change in D since
> then which make me reconsidering my opinion (including that @safe holes were not
> fixed).

I do welcome help in fixing bugs.

On 6/15/2014 2:30 AM, Maxim Fomin wrote:
> I found dozens of cases when @safe is broken, let alone other issues in
> bugzilla.

I have added the keyword 'safe' to bugzilla. I'd appreciate it if you would go through the bugzilla issues you've identified with @safe, and mark them with the 'safe' keyword.

Thanks!

On 06/15/2014 08:44 PM, Walter Bright wrote:
> On 6/15/2014 2:48 AM, Timon Gehr wrote:
>> On 06/15/2014 10:33 AM, Walter Bright wrote:
>>>>
>>>> What Timon is saying is that not all memory safe code is verifiably
>>>> @safe.
>>>
>>> In D, they are defined to be the same thing,
>>
>> Since when?
>>
>> http://dlang.org/function
>>  ...
>>
>>> so the statement makes no sense.
>>
>> Then please indicate how to fix the documentation. If you are going to
>> claim the
>> Humpty Dumpty privilege, I'll back off. Thanks.
>
>
> I don't know why the documentation says that. D's @safe is about memory
> safety, not undefined behavior.
> ...

Note that this is frustratingly unhelpful for deciphering your point about "memory safe" <=> "verifiably @safe" by definition. Are you defining "memory safe" or "verifiably @safe"?

> Note that the list of eschewed behaviors are possibly memory corrupting.

It is an incomplete list. I'd rather see an incomplete list of _allowed_ behaviours instead of an incomplete list of eschewed behaviours. In any case, I don't see how any list of (syntactic) verifiable properties of the code is supposed to be equivalent to the (non-trivial semantic) memory safety property. Are you assuming @trusted as an oracle for memory safety and saying @trusted code is 'verifiably @safe' code? (That's not the intended reading.)

> Signed integer overflow, for example, is not listed.
>

Are you trying to say that signed integer overflow is undefined behaviour in D?  (This would again contradict the documentation.)

On 6/15/2014 3:45 PM, Timon Gehr wrote:
>> I don't know why the documentation says that. D's @safe is about memory
>> safety, not undefined behavior.
>> ...
>
> Note that this is frustratingly unhelpful for deciphering your point about
> "memory safe" <=> "verifiably @safe" by definition. Are you defining "memory
> safe" or "verifiably @safe"?

I don't understand your question. I don't know what is unhelpful about saying that @safe refers to memory safety.


>> Note that the list of eschewed behaviors are possibly memory corrupting.
>
> It is an incomplete list.

I ask that you enumerate the missing items, put the list in bugzilla, and tag them with the 'safe' keyword.


> In any case, I
> don't see how any list of (syntactic) verifiable properties of the code is
> supposed to be equivalent to the (non-trivial semantic) memory safety property.

The list is not restricted to syntactic issues.


> Are you assuming @trusted as an oracle for memory safety and saying @trusted
> code is 'verifiably @safe' code? (That's not the intended reading.)

Not at all. Where does the spec suggest that?


>> Signed integer overflow, for example, is not listed.
> Are you trying to say that signed integer overflow is undefined behaviour in D?
> (This would again contradict the documentation.)

I know the spec says it follows 2's complement arithmetic. I'm not 100% confident we can rely on that for all 2's complement CPUs, and furthermore we have a bit of a problem in relying on optimizers built for C/C++ which rely on it being undefined behavior.

In any case, it is still not an issue for @safe.

On 06/16/2014 01:06 AM, Walter Bright wrote:
> On 6/15/2014 3:45 PM, Timon Gehr wrote:
>>> I don't know why the documentation says that. D's @safe is about memory
>>> safety, not undefined behavior.
>>> ...
>>
>> Note that this is frustratingly unhelpful for deciphering your point
>> about
>> "memory safe" <=> "verifiably @safe" by definition. Are you defining
>> "memory
>> safe" or "verifiably @safe"?
>
> I don't understand your question. I don't know what is unhelpful about
> saying that @safe refers to memory safety.
> ...

You stated the two to be equivalent earlier, which is impossible.

>
>>> Note that the list of eschewed behaviors are possibly memory corrupting.
>>
>> It is an incomplete list.
>
> I ask that you enumerate the missing items, put the list in bugzilla,
> and tag them with the 'safe' keyword.
>
>
>> In any case, I
>> don't see how any list of (syntactic) verifiable properties of the
>> code is
>> supposed to be equivalent to the (non-trivial semantic) memory safety
>> property.
>
> The list is not restricted to syntactic issues.
> ...

(Yes it is, but that is not important because here the problem here is clearly that these terms have wildly different meanings in different communities.)

The important distinction is between verifiable and non-verifiable. @safe cannot be equivalent to memory safe because @safe is verifiable and memory safe is not.

>
>> Are you assuming @trusted as an oracle for memory safety and saying
>> @trusted
>> code is 'verifiably @safe' code? (That's not the intended reading.)
>
> Not at all. Where does the spec suggest that?
> ...

I'm just trying to find the definition/theorem we do not agree on.

>
>>> Signed integer overflow, for example, is not listed.
>> Are you trying to say that signed integer overflow is undefined
>> behaviour in D?
>> (This would again contradict the documentation.)
>
> I know the spec says it follows 2's complement arithmetic. I'm not 100%
> confident we can rely on that for all 2's complement CPUs, and
> furthermore we have a bit of a problem in relying on optimizers built
> for C/C++ which rely on it being undefined behavior.
>
> In any case, it is still not an issue for @safe.

Maybe not in practice (though I'll not bet on it), but a conforming implementation can do _anything at all_ if undefined behaviour occurs, including behaving as if memory had been corrupted.