On 8/2/2014 1:06 PM, Artur Skawina via Digitalmars-d wrote:
> There's nothing wrong with `assume`, it's very useful for optimizations.
> But it's too dangerous to tack `assume` onto `assert`. If they are kept
> separate then it's at least possible to carefully audit every 'assume'.
> People *will* use them for micro-optimizations, and they *will* make
> mistakes.

This seems contradictory. You say it is fine to have assume affect optimization, i.e. insert bugs if the assumes are wrong, but not fine to check at runtime that the assumes are correct?

On 8/2/2014 1:23 PM, Andrei Alexandrescu wrote:
> Assume we choose that, there's still murky ground:
>
> @system fun(int[] p) {
>     gun(p.ptr + p.length);
> }
>
> @safe gun(int* p) {
>     if (p) *p = 42;
> }
>
> This passes semantic checking but is unsafe and unsafety is in the @safe
> code. Well, that's fine, we might say. The problem is this works against
> our stance that "inspect @system code by hand, @safe code will take care
> of itself". The problem is that pointers just past the end have this
> weird property "the pointer is okay but not for dereferencing".

We could establish a rule for @safe that function arguments that are pointers must be pointers to valid memory, not past the end.

On 8/3/14, 8:10 AM, Walter Bright wrote:
> On 8/2/2014 1:23 PM, Andrei Alexandrescu wrote:
>> Assume we choose that, there's still murky ground:
>>
>> @system fun(int[] p) {
>>     gun(p.ptr + p.length);
>> }
>>
>> @safe gun(int* p) {
>>     if (p) *p = 42;
>> }
>>
>> This passes semantic checking but is unsafe and unsafety is in the @safe
>> code. Well, that's fine, we might say. The problem is this works against
>> our stance that "inspect @system code by hand, @safe code will take care
>> of itself". The problem is that pointers just past the end have this
>> weird property "the pointer is okay but not for dereferencing".
>
> We could establish a rule for @safe that function arguments that are
> pointers must be pointers to valid memory, not past the end.

I think that's a good stance. -- Andrei

On Sunday, 3 August 2014 at 15:06:56 UTC, Walter Bright wrote:
> On 8/2/2014 1:06 PM, Artur Skawina via Digitalmars-d wrote:
>> There's nothing wrong with `assume`, it's very useful for optimizations.
>> But it's too dangerous to tack `assume` onto `assert`. If they are kept
>> separate then it's at least possible to carefully audit every 'assume'.
>> People *will* use them for micro-optimizations, and they *will* make
>> mistakes.
>
> This seems contradictory. You say it is fine to have assume affect optimization, i.e. insert bugs if the assumes are wrong,

Yes

> but not fine to check at runtime that the assumes are correct?

No, it would be fine for assume to do runtime checks on debug. I.e. The semantics you want assert to have, would be fine for assume. But I'd also expect assume to be used much more conservatively than assert. And the naming is much clearer this way.

On Sunday, 3 August 2014 at 15:16:31 UTC, Andrei Alexandrescu wrote:
> On 8/3/14, 8:10 AM, Walter Bright wrote:
>> We could establish a rule for @safe that function arguments that are
>> pointers must be pointers to valid memory, not past the end.
>
> I think that's a good stance. -- Andrei

Agreed, see my other post. In fact, if I remember correctly this is not the first time that a variant of this question pops up and I think we already came to this conclusion at least once.

Of course, this also entails that it must be impossible to obtain such a pointer in @safe code. Right now, there are a still a few holes in that regard (see Bugzilla), e.g. someArray[$ .. $].ptr.

Cheers,
David

On 08/03/2014 05:00 PM, Paolo Invernizzi wrote:
> On Sunday, 3 August 2014 at 14:10:29 UTC, Timon Gehr wrote:
>> On 08/03/2014 03:01 PM, Paolo Invernizzi wrote:
>>> On Sunday, 3 August 2014 at 10:49:39 UTC, Timon Gehr wrote:
>>>> On 08/03/2014 11:15 AM, Paolo Invernizzi wrote:
>>>>> because every few milliseconds an assert is triggered
>>>>
>>>> Right, and software does not have security holes because otherwise
>>>> they would obviously be exploited every few milliseconds during
>>>> in-house testing.
>>>
>>> That is a totally different matter:
>>
>> Well, no.
>>
>>> security holes are about things that
>>> the programmer is _totally missing_,
>>
>> The programmer(s!) may be _totally missing_ the conditions that lead
>> to an assertion failure. In fact, unless assertions are intentionally
>> misused, this is always the case.
>>
>>> and someone is seeing and exploiting that.
>>
>> (Undefined behaviour introduced in this way may be exploitable.)
>
> If the assertion triggers, that's not undefined behaviour:

It will from now on be in -release, this is what this is all about.

> it's a bug,
> already implanted in the code, that the assertion is surfacing
> _avoiding_ undefined behaviour occurring from the really next line of code.
> ...

Most bugs do not lead to undefined behaviour. E.g. you can write buggy code in a language that does not have the concept.


> Security holes are not related to assertions at all, they are related in
> unpredictable state that the program has reached, outside of the view of
> the programmers.
> ...

And what do you think a wrong assertion is the manifestation of? (Hint: The assertion talks about the program state.)

> Assertions are only checks that the reasoning about the flow and the
> conditions is going in the way that was originally intended. If you have
> failures,

But that is not the scenario. You don't turn on -release in order to disable assertions that you _know_ are failing.

> and you want to cope with them, you MUST remove the failing
> assertions from the code, and turn them in specific code to cope with
> the faulty condition.
>
> Something like 'warning mate! the commented assertion is triggered from
> time to time,

Why do you assume they had noticed that the assertion was wrong?

> That was a stereotypical example;

You were not in the position to introduce a stereotypical example. If Johannes says that some code will break, and you say "I don't buy this", then you cannot introduce an example to argue against, where the additional circumstances are such that you have an easy point. This is a straw man. You need to argue against the existence of the broken code. I.e. you need to argue for an (approximate) universal. If you introduce an example, you need to argue that the 'example' is actually the only (likely) way that code could be broken by this change. I.e. you'd need to argue that wrong assertions are always caught before they are part of a build where they are disabled. (You might also pursue the alternative direction of admitting that this is a possibility, but saying that it is very unlikely to happen, and then justify that opinion. ("That's true, this might happen, but I don't think this change will lead to many catastrophes, because..."))

> what I was trying to argue it's that also if we do some dirty tricks to keep the train on the rails,

(That's still part of the made up scenario.)

> if the program logic is flowed  [sic]

Maybe it hasn't been flawed in the -release build before because the faulty assertion was the only thing that was faulty, but nobody knew that it was faulty before the released system went down.

> you can have an avalanche effect in some cases:

Note again, 'some cases'. Those are again different cases than Johannes had in mind.

> everything seems to work fine for a good amount of time until the snowball comes down,
> violates catastrophically the program logic and boom.

Again, in other cases, the -release program will operate as expected.

An analogy, to be taken with a grain of salt: Planes crash sometimes, even though this is not part of their intended design. It would still be a bad idea to install bombs in some planes that explode when they seem about to crash according to _some_ of many simple tests of measured parameters proposed by one of (possibly) _many_ designers of the plane, especially if those tests were proposed without knowledge that this was going to be their purpose.

On 08/03/14 17:06, Walter Bright via Digitalmars-d wrote:
> On 8/2/2014 1:06 PM, Artur Skawina via Digitalmars-d wrote:
>> There's nothing wrong with `assume`, it's very useful for optimizations. But it's too dangerous to tack `assume` onto `assert`. If they are kept separate then it's at least possible to carefully audit every 'assume'. People *will* use them for micro-optimizations, and they *will* make mistakes.
> 
> This seems contradictory. You say it is fine to have assume affect optimization, i.e. insert bugs if the assumes are wrong, but not fine to check at runtime that the assumes are correct?

I'm saying there's nothing wrong with having an assume(-like) directive; by default `assume` should of course check the condition at RT just like `assert` does [1].

I'm against _redefining_ `assert` to mean `assume`. In practice there will always be a possibility of an assert failing at RT due to eg a different environment or inputs[2]. If programs always were perfect and absolutely bug-free, asserts and diagnostics would never be required at all...

Do you really think that it is unreasonable to expect that, in a language called *D*, a very well known decades old C concept isn't redefined? That wouldn't be appropriate even for a language called "Mars"...

Of course everybody initially expects that an 'assert' in D acts like
the C equivalent. There isn't anything in the "spec" (ie dlang.org) that
even hints at D's assert being different. ("[...] if the result is false,
an AssertError is thrown. If the result is true, then no exception is
thrown.[...]"). I just looked at the "contracts" page for the first time
ever, and found this: "assert in function bodies works by throwing an
AssertError, which can be caught and handled". That could reasonably be
interpreted to mean that a failing assertion in D still leaves the program
in a well defined valid (!) state.

Most people who are already aware of `assert` will know a definition like
this one: http://pubs.opengroup.org/onlinepubs/009695399/functions/assert.html
"assert - insert program diagnostics [...] The assert() macro shall insert
diagnostics into programs".
Nobody expects that disabling diagnostics introduces undefined behavior.
Hence, slightly inaccurate or not 100% up-to-date asserts are not considered
a real problem. And they are not a problem. Except in D?

artur

[1] An `__assume` that never checks at RT would also be useful for low-level
    code, where failure is not an option.

[2] Asserts are not for /directly/ validating inputs, yes, but inputs are
    often necessary to get the program to an invalid state.

On Saturday, 2 August 2014 at 21:36:11 UTC, Tobias Pankrath wrote:
> Don't you agree, that a program that throws AssertError in non -release* build is broken?
>
> * this is not the opposite of debug

Let's go to the definitions:

Total correctness:
The program can be proved to always terminate normally and return the correct result.

Total correctness is extremely difficult to achieve on a regular computer.

Partial correctness:
The program can be proved to always return the correct result if it terminates normally.

Partial correctness is what you should aim for. What goes on if it does not terminate depends on many factors. E.g. the FDIV bug in the Intel CPU:

http://en.wikipedia.org/wiki/Pentium_FDIV_bug

The FDIV bug is a good example that extensive testing is not enough and that you need either exhaustive testing or formal proofs to assert correctness.

Equally clearly, the FDIV bug is not the result of an incorrect program. It is the result of an incorrect "axiom" in the CPU (the execution environment).

On Sunday, 3 August 2014 at 16:29:18 UTC, Timon Gehr wrote:
> On 08/03/2014 05:00 PM, Paolo Invernizzi wrote:
>> On Sunday, 3 August 2014 at 14:10:29 UTC, Timon Gehr wrote:
>>> On 08/03/2014 03:01 PM, Paolo Invernizzi wrote:
>>>> On Sunday, 3 August 2014 at 10:49:39 UTC, Timon Gehr wrote:
>>>>> On 08/03/2014 11:15 AM, Paolo Invernizzi wrote:
>>>
>>>> and someone is seeing and exploiting that.
>>>
>>> (Undefined behaviour introduced in this way may be  exploitable.)
>>
>> If the assertion triggers, that's not undefined behaviour:
>
> It will from now on be in -release, this is what this is all about.

If an assert triggers, and you want go anyway with '-release', you should remove it from the code, that's my point. No problem at all with inferring optimisations from it.

>> it's a bug, already implanted in the code, that the assertion is surfacing
>> _avoiding_ undefined behaviour occurring from the really next line of code.
>> ...
>
> Most bugs do not lead to undefined behaviour. E.g. you can write buggy code in a language that does not have the concept.

But most yes: to me, an undefined behaviour is the situation where I've developed the code for having 'a' in one place, and I have 'b'. If this is not, literally undefined behaviour, I donno how I should name it.

>> Security holes are not related to assertions at all, they are related in
>> unpredictable state that the program has reached, outside of the view of the programmers.
>
> And what do you think a wrong assertion is the manifestation of? (Hint: The assertion talks about the program state.)

Again, the assertion will trigger on that, so I'm not entering the 'donno what happened here' state: the program will halt. No security risk at all, also if the assert expression is crappy code.

If you want to keep the safety net also in '-release' just stop using asserts and use enforce, at least you are clearly signalling the developer intention. Or, simply, don't use '-release', but that to me it's a little abuse of the use of assert...

>> Assertions are only checks that the reasoning about the flow and the
>> conditions is going in the way that was originally intended. If you have failures,
>
> But that is not the scenario. You don't turn on -release in order to disable assertions that you _know_ are failing.
>
>> and you want to cope with them, you MUST remove the failing
>> assertions from the code, and turn them in specific code to cope with
>> the faulty condition.
>>
>> Something like 'warning mate! the commented assertion is triggered from
>> time to time,
>
> Why do you assume they had noticed that the assertion was wrong?

I don't understand now: I notice it because the program terminate with a stack trace telling me an assertion was triggered. What are you meaning? I guess it's a pretty common practise to have testers stress the application with asserts on, prior to put it in production with assertion disabled once you are confident that the program is not buggy.

>> That was a stereotypical example;
>
> You were not in the position to introduce a stereotypical example. If Johannes says that some code will break, and you say "I don't buy this", then you cannot introduce an example to argue against, where the additional circumstances are such that you have an easy point. This is a straw man.

I don't think it's a straw man, because I've not changed anything that Johannes has said.

> You need to argue against the existence of the broken code. I.e. you need to argue for an (approximate) universal.

I'm arguing, like others, that to me the code was already broken, but it seems that we can't agree on what broken means.

> If you introduce an example, you need to argue that the 'example' is actually the only (likely) way that code could be broken by this change.
> I.e. you'd need to argue that wrong assertions are always caught before they are part of a build where they are disabled.

That's what usually happens, if you have a good test coverage, and a good testing period.

> (You might also pursue the alternative direction of admitting that this is a possibility, but saying that it is very unlikely to happen, and then justify that opinion. ("That's true, this might happen, but I don't think this change will lead to many catastrophes, because..."))

The point was simply that I don't think that such a change will summon voices claiming that the language has broken again some codebase.

That is an easy rebuttal, because it's caused by a, IMHO, bad practical usage of the assert statement.

>> what I was trying to argue it's that also if we do some dirty tricks to keep the train on the rails,
>
> (That's still part of the made up scenario.)
>
>> if the program logic is flowed  [sic]
>
> Maybe it hasn't been flawed in the -release build before because the faulty assertion was the only thing that was faulty, but nobody knew that it was faulty before the released system went down.

Ok, now I've understood: are you arguing, (correct me if I'm wrong, I'm not searching a strawman, really!) that probably there are bugs, and that bugs are wrong assert expressions, that are wrongly modelling the intended state of the program in an assert expression?

And in that case, are you arguing that the utility of the '-release' flags is that, obliterating the assert code, it raises the quality of the code because it's some sort of "dead code elimination?".

It's that?

>> everything seems to work fine for a good amount of time until the snowball comes down,
>> violates catastrophically the program logic and boom.
>
> Again, in other cases, the -release program will operate as expected.

If I've grasped your point in the previous reply, yes, maybe.

> An analogy, to be taken with a grain of salt: Planes crash sometimes, even though this is not part of their intended design. It would still be a bad idea to install bombs in some planes that explode when they seem about to crash according to _some_ of many simple tests of measured parameters proposed by one of (possibly) _many_ designers of the plane, especially if those tests were proposed without knowledge that this was going to be their purpose.

I think that something similar is happening: the avionic system is disabled if the results coming out from two different implementation of "how the plane should fly" diverge. It's the same as they are running without '-release', and checking mutually the state of the flight devices and parameters.

The are 'aborting', and leaving all the control to man instead of going on: it's like they are not using '-release' at all, and it's like they are using 'enforce' all over the place, no assume or assert at all.

---
Paolo

On 08/03/2014 11:03 PM, Paolo Invernizzi wrote:
> ...
>
> But most yes: to me, an undefined behaviour is the situation where I've
> developed the code for having 'a' in one place, and I have 'b'.  If this
> is not, literally undefined behaviour, I donno how I should name it.
> ...

You could name it a bug, or a programming error. Undefined behaviour is something specific. If a program contains undefined behaviour, this means that a conforming implementation can generate any arbitrary behaviour.

> ...
>>> everything seems to work fine for a good amount of time until the
>>> snowball comes down,
>>> violates catastrophically the program logic and boom.
>>
>> Again, in other cases, the -release program will operate as expected.
>
> If I've grasped your point in the previous reply, yes, maybe.
> ...

Ok. This was Johannes' point.