On Friday, 6 February 2015 at 08:58:05 UTC, Walter Bright wrote:
> On 2/6/2015 12:31 AM, Kagamin wrote:
>> On Thursday, 5 February 2015 at 23:39:39 UTC, Walter Bright wrote:
>>>  static void trustedMemcopy(T[] dest, T[] src) @trusted
>>>  {
>>>    assert(src.length == dest.length);
>>>    memcpy(dest.ptr, src.ptr, src.length * T.sizeof);
>>>  }
>>
>> Should be enforce: assert doesn't guard against malicious usage.
>
> Cue my endless attempts to explain the difference between input errors and logic errors :-(

Well, ok, not enforce:

static void trustedMemcopy(T[] dest, T[] src) @trusted
{
  if(src.length != dest.length)assert(false);
  memcpy(dest.ptr, src.ptr, src.length * T.sizeof);
}

On Friday, 6 February 2015 at 13:28:59 UTC, Steven Schveighoffer wrote:
> The bottom line of my reasoning is that code changes over time, by different people. Context is forgotten. It's much better to have the compiler verify you know what you are doing when working with @trusted than it is to just allow anyone to inject code anywhere.

Actually, I think this argument goes against what you are arguing for. Anything within a @trusted section has a big warning sign attached to it that says "cannot modify this without detailed review". But the compiler cannot verify that a @safe function with local @trusted blocks are actually safe, so it only buys you a false sense of security.

It is also much easier to bring a large @trusted block to safety than a small one, e.g. to have one big @trusted chunk that does:

1. obtain resource
2. process resource
3. copy resource
4. free resource
5. return copy

The problem is the process around @trusted given that there will be no sound verification system in D.

Maybe it should have been called "@manually_proven_safe" instead, to discourage use...

FWIW, and now that I think I understand how @trusted is supposed to be used, the arguments are valid. But I also:

1. Agree with H S Teoh on the maintainability aspect. Depending on humans reviewing the code is never going to work out. And even if it did, subsequent edits might break everything. It's a lot harder to review a 2-line diff to an existing function for trustworthiness than the original one when it was first written. I've lost count of how many code reviews I've approved at work that introduced subtle crashy bugs. And let's face it, reviewing a @trusted D function is no different from reviewing C code.

2. Agree with Dicebot that reviewing a 50-line function and making sure it isn't naughty is quite hard. Not impossible, but hard to guarantee its safety.

Unfortunately, I have no suggestions on how to make it better. The "@safe block/local function in a @trusted function" idea sounds promising, but I don't know how well it'd work out in practice.

Atila


On Thursday, 5 February 2015 at 23:39:39 UTC, Walter Bright wrote:
> Consider the following code excerpted from std.array.join:
>
>   static U trustedCast(U, V)(V v) @trusted { return cast(U) v; }
>   return trustedCast!RetType(result);
>
> This is because the compiler would complain that the following line would not be @safe:
>
>   return cast(RetType)(result);
>
> The rationale is "I know it's safe, so I'll create an @trusted wrapper to eliminate the error." What comes next is "that's cumbersome. How about a better syntax:"
>
>   trusted {
>      return cast(RetType)(result);
>   }
>
> ? It's the rationale behind "unsafe" blocks that appear in other languages. It seems like a perfectly reasonable request.
>
> The trouble with it is, what if the cast is converting from an integer to a pointer? That could lead to memory corruption. The code allows a potentially memory corrupting operation to be inserted into code that is otherwise @safe.
>
> The only way to deal with it is to then manually review everything about 'RetType' and 'result' to prove to oneself that it is not converting random bit patterns into pointers. In other words, one is manually reviewing @safe code for memory corruption errors.
>
> This is an abject failure of @safe, @trusted, and @system.
>
> The solution is to regard @trusted as a means of encapsulating unsafe operations, not escaping them. Encapsulating them means that the interface from the @trusted code is such that it is usable from safe code without having to manually review the safe code for memory safety. For example (also from std.array):
>
>   static void trustedMemcopy(T[] dest, T[] src) @trusted
>   {
>     assert(src.length == dest.length);
>     memcpy(dest.ptr, src.ptr, src.length * T.sizeof);
>   }
>
> I don't have to review callers of trustedMemory() because it encapsulates an unsafe operation (memcpy) with a safe interface.
>
> The reason @trusted applies only to functions, and not to blocks of code, is that functions are the construct in D that provides an interface. Arbitrary blocks of code do not have a structured interface. Adding @trusted { code } support will encourage incorrect uses like the opening example. The existence of @trusted blocks will require review of every line of code in the function that encloses it, and transitively every function that calls it!
>
> Adding @trusted as a function attribute, on the other hand, only requires review of the function's interface to determine if it is acceptable to use in safe code. Safety review of its callers is unnecessary.

On Friday, 6 February 2015 at 14:00:24 UTC, Atila Neves wrote:
> 1. Agree with H S Teoh on the maintainability aspect. Depending on humans reviewing the code is never going to work out.

Of course it can work out. You need a formalized process and a group of people with training in math or comp.sci to do the review.

Proving memory safety for a single function in a semi-formal manner is not like proving full correctness.

I suggest the following:

1. @trusted should only be used on high priority code (not to gain minor speed ups)

2. @trusted code should always carry the safety-proof as embedded comments

3. @trusted templates should carry the most stringent type constraints (and proof required to weaken them)

4. At least 3 reviewers with knowledge of compsci/math MUST verify the soundness of the proof.

5. Have a list of volunteers that are called in by email to review @trusted code.

If only 2% is @trusted then this should work out fine. The alternative is to give up @safe completely or completely change the typesystem.

6. @trusted code should be self contained so that changes in called functions don't break the proof...

On 2/6/15 8:42 AM, "Ola Fosheim =?UTF-8?B?R3LDuHN0YWQi?= <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Friday, 6 February 2015 at 13:28:59 UTC, Steven Schveighoffer wrote:
>> The bottom line of my reasoning is that code changes over time, by
>> different people. Context is forgotten. It's much better to have the
>> compiler verify you know what you are doing when working with @trusted
>> than it is to just allow anyone to inject code anywhere.
>
> Actually, I think this argument goes against what you are arguing for.
> Anything within a @trusted section has a big warning sign attached to it
> that says "cannot modify this without detailed review". But the compiler
> cannot verify that a @safe function with local @trusted blocks are
> actually safe, so it only buys you a false sense of security.

That is kind of the point behind H.S. Teoh's idea that @trusted code should be default @safe with @system escapes instead of today where it's default @system. If nothing else, it has discouraged the use of @trusted to mark code for extra scrutiny.

I'm coming to agree with him. Having a function marked @safe doesn't tell you whether there are @trusted blocks, and any @trusted blocks (despite the idea of having the compiler tell you when data was generated/touched by @trusted code) can bring into suspect the whole function. So marking a function @safe, and having it mean "this function has NO TRUSTED OR SYSTEM CODE in it whatsoever, is probably the right move, regardless of any other changes.

In fact, I would propose that it should be an error for @safe functions to have any non-static functions inside them (i.e. any place where the aliasing of @safe data is implicit). This is a departure from my previous position, but I think it still fits if we allow @trusted to mean what H.S. Teoh's proposal means.

> It is also much easier to bring a large @trusted block to safety than a
> small one, e.g. to have one big @trusted chunk that does:
>
> 1. obtain resource
> 2. process resource
> 3. copy resource
> 4. free resource
> 5. return copy
>
> The problem is the process around @trusted given that there will be no
> sound verification system in D.

What we really want is:

1. A way to say "this function needs extra scrutiny"
2. Mechanical verification as MUCH AS POSSIBLE, and especially for changes to said function.

Yes, we can do 2 manually if necessary. But having a compiler that never misses on pointing out certain bad things is so much better than not having it.

> Maybe it should have been called "@manually_proven_safe" instead, to
> discourage use...

@assume_safe would probably be the right moniker since that's what we use elsewhere. But it's water under the bridge now...

-Steve

On Friday, 6 February 2015 at 13:42:40 UTC, Ola Fosheim Grøstad wrote:
>
> "cannot modify this without detailed review".
>
This quote from Ola, here?  That basically describes my job maintaining big piles of legacy C: the compiler verifies nothing, so every change to the anything in the API of "safe" functions or anything in their entire call chain must be painstakingly reviewed.

A single change generally takes me several days of research, verification, and testing.  I fixed about 150 potential memory issues (and several really dumb logic errors) with Clang's static analysis when I first inherited the code; it took weeks.  (And now writing new stuff using this "safe" API is turning up memory safety issues anyway!)

So from my perspective, calling this situation "completely impractical" reveals a stunning gift for understatement.  Is this really the best we can do after however many years?  Because it blows.

The current @trusted semantics (and accompanying politics) make it exceedingly clear that @safe is meaningless for anything beyond trivial, one-off tools that will never receive maintenance.

-Wyatt

On Friday, 6 February 2015 at 15:10:18 UTC, Steven Schveighoffer wrote:
> into suspect the whole function. So marking a function @safe, and having it mean "this function has NO TRUSTED OR SYSTEM CODE in it whatsoever, is probably the right move, regardless of any other changes.

But that would break if you want to call a @safe function with a @trusted function reference as a parameter? Or did I misunderstand what you meant here?

And... what happens if you bring in a new architecture that requires @trusted implementation of a library function that is @safe on other architectures?

> 1. A way to say "this function needs extra scrutiny"
> 2. Mechanical verification as MUCH AS POSSIBLE, and especially for changes to said function.
>
> Yes, we can do 2 manually if necessary. But having a compiler that never misses on pointing out certain bad things is so much better than not having it.

I am not sure if it is worth the trouble. If you are gonna conduct a semi formal proof, then you should not have a mechanical sleeping pillow that makes you sloppy. ;-)

Also if you do safety reviews they should be separate from the functional review and only focus on safety.

Maybe it would be interesting to have an annotation for @notprovenyet, so that you could have regular reviews during development and then scan the source code for @trusted functions that need a safety review before you a release is permitted? That way you don't have to do the safety review for every single mutation of the @trusted function.

>> Maybe it should have been called "@manually_proven_safe" instead, to
>> discourage use...
>
> @assume_safe would probably be the right moniker since that's what we use elsewhere. But it's water under the bridge now...

Yeah, it was merely the psychological effect that one might hestitate to actually type in "I have proven this" without thinking twice about it. "I trust this code" is an easy claim... ;-)

On Friday, 6 February 2015 at 15:14:14 UTC, Wyatt wrote:
> So from my perspective, calling this situation "completely impractical" reveals a stunning gift for understatement.  Is this really the best we can do after however many years?  Because it blows.
>
> The current @trusted semantics (and accompanying politics) make it exceedingly clear that @safe is meaningless for anything beyond trivial, one-off tools that will never receive maintenance.

I don't get this. If:

1. @safe actually works.

2. @trusted sections are written without dependencies

3. @trusted are formally proven safe

4. @trusted functions rarely change

5. @trusted is 0-2% of the codebase

Then how is this more work than implementing something like a linear type system that is both tedious for the programmer and has taken Rust 8 years to get into working shape...?

Jonathan recently said he would like to volunteer some, and he has mentioned a background with math/proofs. If he is willing to do safety review, then so I am, then so will someone else who feel like refreshing their training in program verification... Use the resources you have. Those resources, we do have, I think. Unused.

The resources we obviously don't have is experts on type systems and automated proof and verification engines.

On Friday, 6 February 2015 at 15:14:14 UTC, Wyatt wrote:
> On Friday, 6 February 2015 at 13:42:40 UTC, Ola Fosheim Grøstad wrote:
>>
>> "cannot modify this without detailed review".
>>
> This quote from Ola, here?  That basically describes my job maintaining big piles of legacy C: the compiler verifies nothing, so every change to the anything in the API of "safe" functions or anything in their entire call chain must be painstakingly reviewed.
>
> A single change generally takes me several days of research, verification, and testing.  I fixed about 150 potential memory issues (and several really dumb logic errors) with Clang's static analysis when I first inherited the code; it took weeks.
>  (And now writing new stuff using this "safe" API is turning up memory safety issues anyway!)
>
> So from my perspective, calling this situation "completely impractical" reveals a stunning gift for understatement.  Is this really the best we can do after however many years?  Because it blows.
>
> The current @trusted semantics (and accompanying politics) make it exceedingly clear that @safe is meaningless for anything beyond trivial, one-off tools that will never receive maintenance.
>
> -Wyatt

Exactly the reason why I never liked C and C++ only makes it better if everyone on team stays away from Cisms and uses the safer alternatives.

Now the C and C++ world finally accepted the use of static analyzers, but I had the displeasure to try to find pointer related issues without one, back in the .com days. As you say, it takes weeks.

Regarding D, maybe @trusted should go away and only keep @system (== unsafe in other languages), as it can hardly give any extra security guarantee.

However, I don't see how to solve the human review process, as that is an halting problem.

--
Paulo