Trusted Manifesto

[John Colvin via Digitalmars-d]

On Monday, 9 February 2015 at 08:19:24 UTC, 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;
>   }
>
> Use of local @trusted functions with safe interfaces is 
> encouraged to minimize the amount of safety code review 
> required.
>
>
> 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 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.
>
> 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() ...
>   }
>
> 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.
>
> References
> ----------
>
> https://github.com/D-Programming-Language/phobos/pull/2966
>
> http://forum.dlang.org/post/mb0uvr$2fdb$1@digitalmars.com
>
> Acknowledgements
> ----------------
>
> Everyone who participated in the references!

Looks great.

It seems to me that rules 2 and 3 could be helped along by 
tooling (compiler or external).