DIP 1006 - Preliminary Review Round 1

[Timon Gehr]

On 05.03.2018 21:55, Walter Bright wrote:
> On 3/5/2018 7:48 AM, Timon Gehr wrote:
>> Again: assert is @safe. Compiler hints are @system. Why should assert 
>> give compiler hints?
> 
> Asserts give expressions that must be true.

"Trust the programmer" does not always scale.

> Why not take advantage of them?

For some use cases it might be fine, but not for others, because you 
can't know whether the program and the assertions are really consistent.

Basically, I think the flags should be:

-check-{assert,invariant,precondition,postcondition,...}={on,off,assume}

E.g.:

$ dmd -check-assert=on test.d     # throw on assertion failure
$ dmd -check-assert=off test.d    # ignore assertions
$ dmd -check-assert=assume test.d # assertions are assumptions for code 
generation

Then the spec says that "assume" is potentially dangerous and can break 
@safe-ty guarantees, like -boundscheck=off.

> See Spec# which based an entire language around that notion:
> 
>   https://en.wikipedia.org/wiki/Spec_Sharp
> ...

Spec# is the opposite of what you claim. It verifies statically that the 
conditions actually hold. Also, it is type safe. (I.e. no UB.)

> Some possible optimizations based on this are:
> 
> 1. elimination of array bounds checks
> 2. elimination of null pointer checks
> 3. by knowing a variable can take on a limited range of values, a 
> cheaper data type can be substituted
> 4. elimination of checks for 'default' switch values
> 5. elimination of overflow checks
> 
> dmd's optimizer currently does not extract any information from 
> assert's. But why shut the door on that possibility?
> ...

We should not do that, and it is not what I am arguing for. Sorry if 
that did not come across clearly.

> 
>> But the whole point of having memory safety is to not have UB when the 
>> programmer screwed up. Behavior not foreseen by the programmer (a bug) 
>> is not the same as behavior unconstrained by the language 
>> specification (UB).
> 
> It's the programmer's option to leave those runtime checks in if he 
> wants to.
> ...

My point is that either leaving them in or turning failures into UB are 
too few options. Also, @safe is a bit of a joke if there is no way to 
_disable contracts_ without nullifying the guarantees it's supposed to give.

> 
>> 'in'-contracts catch AssertError when being composed. How can the 
>> language not be designed to support that?
> 
> That is indeed an issue. It's been proposed that in-contracts throw a 
> different exception, say "ContractException" so that it is not UB when 
> they fail. There's a bugzilla ER on this. (It's analogous to asserts in 
> unittests not having UB after they fail.)
> ...

This is ugly, but I don't think there is a better solution.

> 
>> - I usually don't want UB in programs I am working on. I want the 
>> runtime behavior of the programs to be determined by the source code, 
>> such that every behavior observed in the wild (intended or unintended) 
>> can be traced back to the source code (potentially in a 
>> non-deterministic way, e.g. void initialization of an integer 
>> constant). This should be the case always, even if me or someone else 
>> on my team made a mistake. The @safe D subset is supposed to give this 
>> guarantee. What good is @safe if it does not guarantee absence of 
>> buffer overrun attacks?
> 
> It guarantees it at the option of the programmer via a command line switch.
> ...

You mean, leave in checks?

> 
>> - Using existing assertions as compiler hints is not necessary. 
>> (Without having checked it, I'm sure that LDC/GDC have a more suitable 
>> intrinsic for this already.)
>>
>> As far as I can discern, forcing disabled asserts to give compiler 
>> hints has no upsides.
> 
> I suspect that if:
> 
>      compiler_hint(i < 10);
> 
> were added, there would be nothing but confusion as to its correct usage 
> vs assert vs enforce. There's already enough confusion about the latter 
> two.

I have never understood why. The use cases of assert and enforce are 
disjoint.

> In fact, I can pretty much guarantee it will be rarely used correctly.
> ...

Me too, but that's mostly because it will be rarely used.

> 
>> I know. Actually version(assert) assert(...); also works. However, 
>> this is too verbose, especially in contracts.
> 
> You can wrap it in a template.
> ...

That won't work for in contracts if they start catching 
ContractException instead of AssertError. Also, I think we'd actually 
like to _shorten_ the contract syntax (there is another DIP on this).

For other uses, a function suffices, but I ideally want to keep using 
standard 'assert'. Everybody already knows what 'assert' means.

> 
>> I'd like a solution that does not require me to change the source 
>> code. Ideally, I just want the Java behavior (with reversed defaults).
> 
> But you'll have to change the code to compiler_hint().
> ...

I don't, because I don't want that behavior. Others who want that 
behavior also should not have to. This should be a compilation switch.

> 
>> (enforce is _completely unrelated_ to the current discussion.)
> 
> It does just what you ask (for the regular assert case).
> ...

No. "enforce" does not document that the programmer thinks that the 
condition will never fail. It's not a contract. Hence, enforcements are 
never removed from the executable, because it would not make sense to do 
so, so they definitely do not fit my requirements.

> 
>>> It being UB was my doing, not Mathias'. DIP1006 is not redefining the 
>>> semantics of what assert does.
>> This is not really about assert semantics, this is about the semantics 
>> of "disabling the check".
> 
> It is very much about the semantics of assert.
> 
> 
>> There was no "-check=off" flag before.
> 
> Yes there was, it's the "release" flag.
> ...

Depends on what you mean by "off". :o)

In my book, "-release" is "-check-assert=assume -boundscheck=safeonly". 
A very strange combination!

> 
>> The DIP uses terminology such as "disable assertions" as opposed to 
>> "disable assertion checks (but introduce compiler hints)".
> 
> Yes, the language could be more precise, but I couldn't blame Mathias 
> for that.

I don't understand why that would be necessary. The point of the 
preliminary DIP review is not to blame the author for the DIP's 
shortcomings, it's to collect feedback on the DIP to make it better, 
ideally in an interactive way. It is also very well possible that 
Mathias was simply unaware of the UB behavior with -release.

> I also disagree with the word "hint", because it implies 
> things like "this branch is more likely to be taken" to guide code 
> generation decisions, rather than "assume X is absolutely always 
> incontrovertibly true and you can bet the code on it".
> 

Makes sense. I'll call them "assumptions" from now on.