On Thu, Feb 18, 2016 at 07:30:34PM +0100, Timon Gehr via Digitalmars-d wrote:
> On 18.02.2016 17:37, H. S. Teoh via Digitalmars-d wrote:
[...]
> >1) Casting an array of elements with indirections (in this case Object[]) to void[] is questionable at best, outright unsafe at worst, as shown here. Even if we were to rewrite readData() and mark it @trusted, it still raises the question of what a @trusted function can legally do with void[], which is essentially a type-erased array, that justifies being tagged as @trusted.  How can a function do anything that doesn't break @safety if all type information about the array has been erased, and it essentially sees it only as a ubyte[]? I'm inclined to say that @trusted functions should only be allowed to receive const(void)[] as parameter, not void[].
> >
> >	https://issues.dlang.org/show_bug.cgi?id=15702
> >
> 
> No problem here. There is no way to assign to a void[] without doing 2.

Sure there is:

	void breakSafety(void[] data) @safe
	{
		union U {
			void[] d;
			int[] arr;
		}
		U u;
		u.d = data;
		u.arr[0] = 0xFF; // kaboom
	}


> >2) To add salt to the wound, though, blatantly casting void[] to T[] is allowed in @safe code, thus, readData() can even get away with claiming to be @safe, when in fact it is anything but.
> >
> >	https://issues.dlang.org/show_bug.cgi?id=15672
> 
> This is the culprit.

It's only one of many culprits. As long as there is any way around @safe, the entire system of guarantees breaks down.


T

-- 
Question authority. Don't ask why, just do it.

On Thursday, 18 February 2016 at 18:41:58 UTC, H. S. Teoh wrote:
> On Thu, Feb 18, 2016 at 07:30:34PM +0100, Timon Gehr via Digitalmars-d wrote:
>> No problem here. There is no way to assign to a void[] without doing 2.
>
> Sure there is:
>
> 	void breakSafety(void[] data) @safe
> 	{
> 		union U {
> 			void[] d;
> 			int[] arr;
> 		}
> 		U u;
> 		u.d = data;
> 		u.arr[0] = 0xFF; // kaboom
> 	}

Well, unions with an array in them can't be @safe. That's clearly a bug, regardless of whether void[] is involved or not.

Regardless, as far as I can tell, there is zero @safety problem with converting to void[]. You'll never get corrupted memory with that  conversion. It's converting back that risks screwing everything up. And that's what can't be @safe.

> It's only one of many culprits. As long as there is any way around @safe, the entire system of guarantees breaks down.

Of course, and we went about things the wrong way with @safe. It should have been done via whitelisting, whereas we've done it via blacklisting. Given that fact, we're pretty much permanently at risk of @safe being broken.

- Jonathan M Davis

On Thu, Feb 18, 2016 at 06:55:18PM +0000, Jonathan M Davis via Digitalmars-d wrote:
> On Thursday, 18 February 2016 at 18:41:58 UTC, H. S. Teoh wrote:
[...]
> >It's only one of many culprits. As long as there is any way around @safe, the entire system of guarantees breaks down.
> 
> Of course, and we went about things the wrong way with @safe. It should have been done via whitelisting, whereas we've done it via blacklisting. Given that fact, we're pretty much permanently at risk of @safe being broken.
[...]

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


T

-- 
Why are you blatanly misspelling "blatant"? -- Branden Robinson

On 18.02.2016 19:41, H. S. Teoh via Digitalmars-d wrote:
> On Thu, Feb 18, 2016 at 07:30:34PM +0100, Timon Gehr via Digitalmars-d wrote:
>> On 18.02.2016 17:37, H. S. Teoh via Digitalmars-d wrote:
> [...]
>>> 1) Casting an array of elements with indirections (in this case
>>> Object[]) to void[] is questionable at best, outright unsafe at
>>> worst, as shown here. Even if we were to rewrite readData() and mark
>>> it @trusted, it still raises the question of what a @trusted function
>>> can legally do with void[], which is essentially a type-erased array,
>>> that justifies being tagged as @trusted.  How can a function do
>>> anything that doesn't break @safety if all type information about the
>>> array has been erased, and it essentially sees it only as a ubyte[]?
>>> I'm inclined to say that @trusted functions should only be allowed to
>>> receive const(void)[] as parameter, not void[].
>>>
>>> 	https://issues.dlang.org/show_bug.cgi?id=15702
>>>
>>
>> No problem here. There is no way to assign to a void[] without doing 2.
>
> Sure there is:
>
> 	void breakSafety(void[] data) @safe
> 	{
> 		union U {
> 			void[] d;
> 			int[] arr;
> 		}
> 		U u;
> 		u.d = data;
> 		u.arr[0] = 0xFF; // kaboom
> 	}
> ...

That's in essence just a different way to cast void[] to int[]. Steven's example disproves my previous claim though. Still, I don't think the conversion is the problem. It's the mutation of memory without type information.


>
>>> 2) To add salt to the wound, though, blatantly casting void[] to T[]
>>> is allowed in @safe code, thus, readData() can even get away with
>>> claiming to be @safe, when in fact it is anything but.
>>>
>>> 	https://issues.dlang.org/show_bug.cgi?id=15672
>>
>> This is the culprit.
>
> It's only one of many culprits. As long as there is any way around
> @safe, the entire system of guarantees breaks down.
>
>

If you want to verify guarantees, @safe should be specified by inclusion and ideally, type safety should be proved formally (after applying a few fixes). This first requires a formal language semantics.
That's already a lot of effort, and after that you still don't have a verified implementation.

On Thu, Feb 18, 2016 at 01:58:24PM -0500, Steven Schveighoffer via Digitalmars-d wrote:
> On 2/18/16 11:37 AM, H. S. Teoh via Digitalmars-d wrote:
> >While @safe is a good idea in principle, the current implementation is rather lackluster.
> 
> IMO, I think safe code should disallow casting that doesn't involve a runtime function that verifies safety (such as casting an object to another type, or invoking a @safe opCast), including casting array types.

But isn't casting from, say, long[] to int[] @safe? Last time I checked, druntime does actually convert .length correctly as well, so that converting, say, int[] to long[] won't let you overrun the array by accessing the last elements of the long[].

But obviously casting Object[] to long[] would be a very bad idea, and should not be allowed in @safe. Scarily enough, this code currently compiles without any complaint from the compiler:

	void main() @safe
	{
		Object[] objs = [ new Object() ];
		long[] longs = cast(long[]) objs;
		longs[0] = 12345;
	}

Yikes. Apparently you don't even need void[] to break @safe here. :-(


> And implicit casts to void[] should be disallowed.
> 
> This would be a painful restriction, which is why I think it won't happen :(
[...]

As far as I can tell, implicit casting to const(void)[] shouldn't be a cause for concern -- if all you can do with it is to read the data (e.g., a hexdump debugging function for printing out the byte representation of something), there shouldn't be any problems. It's when you write to the void[] that bad things begin to happen.


T

-- 
Государство делает вид, что платит нам зарплату, а мы делаем вид, что работаем.

On 2/18/16 2:25 PM, H. S. Teoh via Digitalmars-d wrote:
> On Thu, Feb 18, 2016 at 01:58:24PM -0500, Steven Schveighoffer via Digitalmars-d wrote:
>> On 2/18/16 11:37 AM, H. S. Teoh via Digitalmars-d wrote:
>>> While @safe is a good idea in principle, the current implementation
>>> is rather lackluster.
>>
>> IMO, I think safe code should disallow casting that doesn't involve a
>> runtime function that verifies safety (such as casting an object to
>> another type, or invoking a @safe opCast), including casting array
>> types.
>
> But isn't casting from, say, long[] to int[] @safe? Last time I checked,
> druntime does actually convert .length correctly as well, so that
> converting, say, int[] to long[] won't let you overrun the array by
> accessing the last elements of the long[].

Probably. But there is always @trusted escapes. We are guaranteed @safety if we just disallow casting whatsoever.

It doesn't sit well with me that casting is a standard mechanism to use in @safe code. Casting is supposed to be a red flag. Even converting between object types, I think casting is just a terrible requirement.

Maybe it's too restrictive, I don't know. It's unlikely to happen in any case.

> But obviously casting Object[] to long[] would be a very bad idea, and
> should not be allowed in @safe. Scarily enough, this code currently
> compiles without any complaint from the compiler:
>
> 	void main() @safe
> 	{
> 		Object[] objs = [ new Object() ];
> 		long[] longs = cast(long[]) objs;
> 		longs[0] = 12345;
> 	}
>
> Yikes. Apparently you don't even need void[] to break @safe here. :-(

The difference here is that you have a cast. Casting to void[] doesn't require one.

>> And implicit casts to void[] should be disallowed.
>>
>> This would be a painful restriction, which is why I think it won't
>> happen :(
> [...]
>
> As far as I can tell, implicit casting to const(void)[] shouldn't be a
> cause for concern -- if all you can do with it is to read the data
> (e.g., a hexdump debugging function for printing out the byte
> representation of something), there shouldn't be any problems. It's when
> you write to the void[] that bad things begin to happen.

Possibly casting to const(T)[] should be OK for @safe code. But again, a conservative approach that disallows casts is what I would do. Note that you can't print out bytes from a void[], you would need a ubyte[].

-Steve

On Thu, Feb 18, 2016 at 08:23:24PM +0100, Timon Gehr via Digitalmars-d wrote:
> On 18.02.2016 19:41, H. S. Teoh via Digitalmars-d wrote:
[...]
> >	void breakSafety(void[] data) @safe
> >	{
> >		union U {
> >			void[] d;
> >			int[] arr;
> >		}
> >		U u;
> >		u.d = data;
> >		u.arr[0] = 0xFF; // kaboom
> >	}
> >...
> 
> That's in essence just a different way to cast void[] to int[]. Steven's example disproves my previous claim though. Still, I don't think the conversion is the problem. It's the mutation of memory without type information.

Fair enough.  But mutating memory *with* type information isn't necessarily safer either:

	void fun(int*[] intPtrs) {
		union U {
			int*[] ptrs;
			long[] longs;
		}
		U u;
		u.ptrs = intPtrs;
		u.longs[0] = 12345; // oops
	}

Basically, when it comes to @safe, one of the intrinsic requirements is that arbitrary values must not be reinterpreted as pointers. In a sense, it doesn't matter how you get there -- whether by implicit cast to void[], or by unions, or whatever -- as soon as there is a way to reinterpret an arbitrary value as a pointer, @safe is broken. The arbitrary can be another pointer, and may even be a pointer to a type with a compatible binary representation, but the point remains. For example:

	void safeFunc() @safe { ... }
	void unsafeFunc() @system { ... }

	union FuncPtrs {
		void function() @safe fun1;
		void function() @system fun2;
	}
	FuncPtrs ptrs;
	ptrs.fun1 = &unsafeFunc();
	ptrs.fun2();			// oops

>From the POV of binary representation, both fun1 and fun2 are
essentially the same -- they are just function pointers: 32-bit or 64-bit addresses of some executable code. However, the breakage here is caused by reinterpreting a pointer to a @system function as a pointer to a @safe function.  At no time do we lose type information, but as soon as we have reintepretation of something as a pointer, @safe is out the window.


[...]
> >>>2) To add salt to the wound, though, blatantly casting void[] to T[] is allowed in @safe code, thus, readData() can even get away with claiming to be @safe, when in fact it is anything but.
> >>>
> >>>	https://issues.dlang.org/show_bug.cgi?id=15672
> >>
> >>This is the culprit.
> >
> >It's only one of many culprits. As long as there is any way around @safe, the entire system of guarantees breaks down.
> >
> >
> 
> If you want to verify guarantees, @safe should be specified by
> inclusion and ideally, type safety should be proved formally (after
> applying a few fixes).
> This first requires a formal language semantics.
> That's already a lot of effort, and after that you still don't have a
> verified implementation.

I'm not sure how feasible it is to do a formal proof with the current dmd code, since you'd have to freeze it, and as soon as the next PR is merged, the proof is potentially invalidated.

However, a good start is to make *everything* in the language @system by default, and then have a whitelist of things that are @safe. Currently, our implementation is to assume @safety by default and then add things to a @system blacklist as we discover them.  This is the wrong approach, since we don't know what loopholes currently exist that can be exploited, and the number of combinations of language features is far too large for us to be ever sure that we've plugged all the holes. It's better to start conservatively by assuming everything is @system, and as people find more valid use cases that ought to be @safe, those can be added to the whitelist after careful vetting.  This is essentially the idea behind:

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


T

-- 
You have to expect the unexpected. -- RL

On 18.02.2016 21:57, H. S. Teoh via Digitalmars-d wrote:
>> >If you want to verify guarantees, @safe should be specified by
>> >inclusion and ideally, type safety should be proved formally (after
>> >applying a few fixes).
>> >This first requires a formal language semantics.
>> >That's already a lot of effort, and after that you still don't have a
>> >verified implementation.
> I'm not sure how feasible it is to do a formal proof with the current
> dmd code, since you'd have to freeze it, and as soon as the next PR is
> merged, the proof is potentially invalidated.

The most obvious reason why it is infeasible to formally prove correctness of the current dmd code is that it is not correct.

On Thu, Feb 18, 2016 at 08:37:10AM -0800, H. S. Teoh via Digitalmars-d wrote: [...]
> It's bad enough that some Phobos modules (*ahem*std.socket*cough*) liberally sprinkle @trusted on every function without regard to whether it's truly justified
[...]

I don't like being the guy who only whines but does nothing about it, so here's an attempt at plugging at least one of the holes in the @safe cheese grater:

	https://github.com/D-Programming-Language/phobos/pull/4011

Here's an existing one that plugs another hole in the cheese grater:

	https://github.com/D-Programming-Language/phobos/pull/4009

More to come, hopefully. More cheese grater plugs from other contributors will be warmly welcomed, I'm sure (hint, hint!).


T

-- 
Making non-nullable pointers is just plugging one hole in a cheese grater. -- Walter Bright

On 2/19/16 2:00 PM, H. S. Teoh via Digitalmars-d wrote:
> On Thu, Feb 18, 2016 at 08:37:10AM -0800, H. S. Teoh via Digitalmars-d wrote:
> [...]
>> It's bad enough that some Phobos modules (*ahem*std.socket*cough*)
>> liberally sprinkle @trusted on every function without regard to
>> whether it's truly justified
> [...]
>
> I don't like being the guy who only whines but does nothing about it, so
> here's an attempt at plugging at least one of the holes in the @safe
> cheese grater:
>
> 	https://github.com/D-Programming-Language/phobos/pull/4011
>
> Here's an existing one that plugs another hole in the cheese grater:
>
> 	https://github.com/D-Programming-Language/phobos/pull/4009
>
> More to come, hopefully. More cheese grater plugs from other
> contributors will be warmly welcomed, I'm sure (hint, hint!).

Stick with ship as your metaphore. You *want* holes in your cheese grater ;)

-Steve