@system blocks and safer @trusted (ST) functions
Paul Backus
snarwin at gmail.com
Sun Jul 25 17:47:40 UTC 2021
On Sunday, 25 July 2021 at 16:29:38 UTC, Bruce Carneal wrote:
> Machine advantage comes in other forms. Firstly, we now have a
> properly segregated code base. @safe always means 'machine
> checkable'. Zero procedural @trusted code review errors in
> that now easily identified class.
I have already demonstrated that this is false. Here's my example
from the previous thread on this topic, rewritten slightly to use
the new-style `@trusted`/`@system` syntax from your proposal:
```d
module example;
size_t favoriteNumber() @safe { return 42; }
int favoriteElement(ref int[50] array) @trusted
{
// This is memory safe because we know favoriteNumber returns
42
@system {
return array.ptr[favoriteNumber()];
}
}
```
I make the following claims:
1. This code is memory-safe. No matter how you call
`favoriteElement`, it will not result in undefined behavior, or
allow undefined behavior to occur in `@safe` code.
2. `favoriteNumber` is 100% machine-checkable `@safe` code.
3. Changes to `favoriteNumber` must be manually reviewed in order
to ensure they do not result in memory-safety violations.
The only way to ensure that `@safe` code never requires manual
review is to enforce coding standards that forbid functions like
`favoriteElement` from ever being merged in the first place.
One example of a set of coding standards that would reject
`favoriteElement` is:
1. Every `@system` block must be accompanied by a comment
containing a proof (formal or informal) of memory safety.
2. A memory-safety proof for a `@system` block may not rely on
any knowledge about symbols defined outside the block other than
* knowledge that is implied by their type signatures.
* knowledge that is implied by their documentation and/or any
standards they are known to conform to.
`favoriteElement` satisfies condition (1), but not condition
(2)--there is nothing in `favoriteNumber`'s documentation or type
signature that guarantees it will return 42.
I believe (though I cannot prove) that any set of coding
standards capable of rejecting `favoriteElement` under your
proposal is also (mutatis mutandis) capable of rejecting
`favoriteElement` in the current language. If this were true,
then the proposal would be of no value--we could simply implement
those coding standards and reap their benefits right away, with
no language changes required.
If you can give an example of a set of coding standards that
rejects `favoriteElement` under your proposal but fails to reject
`favoriteElement` in the D language as it currently exists, I
would be very interested in seeing it.
More information about the Digitalmars-d
mailing list