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.