Trusted Manifesto (page 2)

February 09, 2015

Re: Trusted Manifesto

Posted by Steven Schveighoffer
in reply to Walter Bright

Permalink

Steven Schveighoffer

Posted in reply to Walter Bright

Permalink

This is headed in the right direction, I think. Comments below.

On 2/9/15 3:19 AM, Walter Bright wrote:
> Andrei and I have learned a lot from the @trusted discussions. It's
> clear the way we were approaching the problem was inadequate. So we came
> up with a proposal based on the ideas and criticisms of the participants
> in the references. It involves no language changes, but offers usage
> guidelines that we believe are workable. Tell us what you think!
> ----------------------------------------------------
>
> Trusted Manifesto
> -----------------
>
> Memory safety in D has the usual definition: a memory-safe program never
> reads
> uninitialized memory and never reads or writes memory with a type
> incompatible
> with the type it was written. The aim of D's
> @safe, @trusted, and @system attributes is to provide as much
> mechanically verified to be safe code as possible.
>
>
> Functions
> ---------
>
> Function signatures inform what must be true about a function. If
> a function is marked as @safe, it must contain only @safe code. This
> safety must be mechanically checkable.
>
> Sometimes, an unsafe operation is needed even in a function
> that is overall safe. For example,
> here's a function that returns an upper case version of its
> input string:
>
>    string toUpper(string s) @safe
>    {
>       char[] r = new char[s.length];
>       foreach (i, c; s)
>      r[i] = toUpper(c);
>       return cast(string)r; // <== unsafe operation
>    }
>
> The compiler rejects this function because it's declared as safe but
> contains an
> unsafe operation.
> Review of the whole function shows that the operation, in this instance,
> is safe.
> One way to deal with that is to do what is called an "escape", meaning
> telling the compiler "I know what I'm doing, so allow this operation":
>
>    string toUpper(string s) @safe
>    {
>       char[] r = new char[s.length];
>       foreach (i, c; s)
>      r[i] = toUpper(c);
>
>       static string trustedCast(char[] r) @trusted
>       {
>          return cast(string)r;
>       }
>
>       return trustedCast(r);
>    }
>
> This will pass typechecking. However, the only reason it is safe is
> because the context
> in which trustedCast() is called makes it safe. In other words, a manual
> review of the surrounding
> context is necessary, which violates the @safe promise that its contents
> are mechanically
> checkable.
>
> I.e. the trustedCast() function is an "escape" that injects unsafety
> into its surrounding
> contents.
>
> This leads to:
>
> RULE 1: @trusted code accessible from @safe code must expose a safe
> interface to unsafe operations.
>
> @trusted must not be used to inject unsafety into surrounding context
> that is marked @safe.
> @safe code must be mechanically verifiable to be safe, and subverting
> that is not acceptable.
>
> COROLLARY 1: @trusted functions should be as small as possible to
> encapsulate the unsafe operation
> without injecting unsafety into @safe code.
>
> In the case of toUpper(), it is necessary to review the entire function
> to verify that the cast is safe,
> so it is properly written:
>
>    string toUpper(string s) @trusted
>    {
>       char[] r = new char[s.length];
>       foreach (i, c; s)
>      r[i] = toUpper(c);
>       return cast(string)r;
>    }

This I don't disagree with. The issue is mostly that the entire function marked as @trusted allows for future additions that are unintentionally un-@safe. But we can work with this for now and see how it goes.

> Use of local @trusted functions with safe interfaces is encouraged to
> minimize the amount of safety code review required.

An example here would be good. Perhaps the memcpy example.

>
>
> Generic Functions
> -----------------
>
> Generic functions are templates that accept compile time parameters in
> the form of types, values or aliases to other functions.
> Whether the function is @safe or @system is not checkable until the
> template function is instantiated with explicit
> arguments. If the template function is marked as @safe, then it can only
> be instantiated with arguments that expose
> safe operations.
>
> If the template function is marked @safe, then RULE 1 applies.
>
> But that reduces the genericity of the function. The compiler is able to

genericness

> deduce whether a template function is @safe or @system
> when it is instantiated. For maximum utility, we need a way to specify
> that:
>
>      This template function is @safe if the generic and non-generic
> operations it uses are @safe as well,
>      otherwise it is @system.
>
> Consider a function to make an immutable array copy of a range:
>
>    immutable(ElementType!Range)[] toArray(Range)(Range r)
>    {
>       alias ElementType!Range E;
>       alias Unqual!E U;
>       U[] a = new U[r.length];
>       foreach (i, e; r)
>      a[i] = e;
>       return cast(immutable)a; // <== unsafe operation
>    }
>
> Being a template function without specified attributes, the compiler
> will infer the attributes.
> But with the unsafe cast, toArray() will always be inferred to be
> @system. But the rest
> of the code is safe. If toArray is marked as @trusted,
>
>    immutable(ElementType!Range)[] toArray(Range)(Range r) @trusted
>    {
>       alias ElementType!Range E;
>       alias Unqual!E U;
>       U[] a = new U[r.length];
>       foreach (i, e; r)
>      a[i] = e;
>       return cast(immutable)a; // <== unsafe operation
>    }
>
> then if the range primitives (front, empty, popFront) exposed by the
> argument to r
> happen to be @system, then those are invalidly assumed to be trustable.
> Every usage
> of toArray() would need to be reviewed for safety, which is impractical.
>
> What is needed is a way to isolate the unsafe operation, and enable the
> compiler to
> infer the rest. In other words, a local exemption from overall safety
> deduction is needed.
>
> Introducing the 'trusted' template to be put in std.conv:
>
>    @trusted auto trusted(alias fun)() { return fun(); }
>
> and used:
>
>    immutable(ElementType!Range)[] toArray(Range)(Range r)
>    {
>       alias ElementType!Range E;
>       alias Unqual!E U;
>       U[] a = new U[r.length];
>       foreach (i, e; r)
>      a[i] = e;
>
>       import std.conv : trusted;
>       auto result = trusted!(() => cast(immutable)a);
>       return result;
>    }
>
> Use of the trusted escape requires the programmer to review the context
> to determine if
> it really is safe. The compiler will infer safety from the rest of the
> operations.

I actually like this. It is one step closer to the mechanically verified trusted function we have been asking for. In fact, it's exactly like that, as it will break existing if you happened to add @system calls inside this function.

However, there is a large hole in your example:

Object[] o = ...;

auto o2 = toArray(o);

Now, we have o and o2. o2 is all immutable references to objects that are also in o as mutable.

The above function is not safe. This is a demonstration that even with mechanically verified @safe code with seemingly correct escapes, you cannot assume anything, especially with templates. I don't really like std.conv.trusted. It doesn't add enough value. What is wrong with using a lambda directly?

auto result = (() @trusted => cast(immutable)a)();

> RULE 2: Usage of escapes are only allowable in functions for which
> safety is inferred,
> and never when calling into as-of-yet not defined generic functions.
>
> But how can it be verified that toArray() is safe otherwise?
>
> RULE 3: An @safe unittest must be used to verify safety when escapes are
> used.
>
>    @safe unittest
>    {
>       ... TODO: test toArray() ...
>    }

This rule is misworded. The unit test does not verify that it's @safe, it only verifies that @safe can be applied to the function, even if the function isn't actually @safe.

I'd say:

RULE 3: A @safe unittest must be used to verify the function can be called as @safe when escapes are used. However, this does NOT verify safety, that still must be manually checked.

> A unittest may also be constructed that verifies via static assert that
> if a type
> with @system operations is passed to the function, that the function is
> inferred
> as @system.
>
> The programmer must still verify that the usage of escapes that leak
> unsafety into the surrounding context is safe.
>
> RULE 4: Escape unsafety must not inject unsafety beyond the template
> function it is used in.
>
> Alternatives
> ------------
>
> 1. if(0) block
>
> Provide an @trusted local function that fully encapsulates the unsafe
> code and its context,
> providing a safe interface. For the operations on template parameters
> that may or may not be
> safe inside the local function, represent them in an if(0) block of code:
>
>    if (0) // safety inference
>    {
>      Unqual!T tmp = cast(Unqual!T)item;
>      emplaceRef!(Unqual!T)(tmp, cast(Unqual!T)item);
>    }
>
>    @trusted void emplace()
>    {
>      auto bigData = _data.arr.ptr[0 .. len + 1];
>
>      emplaceRef!(Unqual!T)(bigData[len], cast(Unqual!T)item);
>
>      //We do this at the end, in case of exceptions
>      _data.arr = bigData;
>    }
>    emplace();
>
> Although this works, it requires duplication of code in a rather
> careful, tedious, and essentially
> unmaintainable manner. It also simply looks wrong, although it could be
> made more palatable by
> enclosing it in a template.
>
> 2. isSafe!T template
>
> Such a template would test that all operations on type T are @safe. The
> template function could
> then be marked @trusted. The troubles with this are (a) it is all or
> nothing with T, i.e. if a
> template function only used an @safe subset of T, it still would not be
> accepted and (b) it does
> not do proper inference of the safety of a template function.
>
> 3. @system escape
>
> @system would be used for escaping unsafe code in an @trusted function,
> or in an un-attributed function
> it would instruct compiler to not use the escaped code when deducing
> trustworthiness. Unsafe code in an @trusted function
> not so marked would generate an error. While this works, it would
> essentially break every @trusted function
> already in existence. It is a somewhat nicer syntax than the
> std.conv.trusted template, but the backwards compatibility
> issue makes it unworkable. It offers a technical advantage over
> std.conv.trusted in that @system will not be
> allowed in @safe functions, while not allowing std.conv.trusted escapes
> in @safe function would be by convention.

I understand the idea of rejecting this to avoid breaking code.

However, let's consider 3 things:

1. you may break @trusted code, but when you do, it points to code that may not have been scrutinized as well as it should have been.
2. It allows making @safe functions with @trusted escapes @trusted functions with @system escapes. This is a better marking system than what we have today.
3. Having the user tag properly what is non-safe and what is safe, allows for other mechanical verification later on. For example tagging data as @system so normal @trusted code cannot touch it without marking as well.

-Steve

On Monday, 9 February 2015 at 11:43:00 UTC, Walter Bright wrote:
> On 2/9/2015 2:54 AM, John Colvin wrote:
>> It seems to me that rules 2 and 3 could be helped along by tooling (compiler or
>> external).
>
> Sounds good, but I'd like to see how this works in practice before going further with it. The nice thing about this proposal is it involves no language changes. It'll allow us to gain experience before committing to language changes.

Until you said this, I was feeling bad that language changes were just completely off the table. I'm not a long-term member of the D community, but a lot of the excitement I get from following D is its "relentless pursuit of perfection", to borrow someone else's slogan. I see a surprising willingness from the early adopters to endure breaking changes for the sake of the long run, and I feel like the pursuit of perfection should utilize this willingness as much as possible. (This might be one of the language changes which is "dfixable", granting it significantly lower switching costs.)

That said, I really like your approach. It's like you're building the scaffolding first, and willing to build the statue itself (i.e. language changes) later, should the scaffolding prove too shaky.

I think the risk here is that a number of users will commit to the scaffolding, only to find their code saturated with it when it is found to be inadequate. To accommodate this risk:

1. Adopt a tone of experimentation, rather than a tone of authority, when imposing these rules. This will help people understand the risks and encourage them to give feedback.

2. Bear in mind an escape hatch. Try to imagine how a codebase which enforces these rules might transition out of them, should it become necessary.

As to the rules themselves, they seem like an admirable attempt to do what's possible within the existing language, to which I have no opposition, assuming they are found in unbiased assessment to work.

Forums