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.
