"Tofu Ninja"  wrote in message news:dtjqnyucskwnqjvksawg@forum.dlang.org...

> Question?
> If an if condition throws or returns in its body is it ok for the optimizer to 'assume' that the condition is false after and make optimizations for it? If so then every one complaining that assert gets removed in -release should really just be using enforce.

Yes.  In fact, it's required that an optimizer do this in order not to be considered garbage.

> The possibility for the optimizer to make the same optimizations for assert can be done for enforce, the only difference is that it does not get removed in -release....

Not quite.  With enforce, it is impossible (ignoring hardware or optimizer errors) for the condition to be false if the enforce was not triggered. Because the assert is not checked, the condition could be false and the code could do something awful.

Also, the optimizer can only use the enforce's assumption _after_ it has checked the condition.  Since with assert it doesn't need to check, it can go backwards and assume the previous code will never produce a value that can violate the assertion.

if (y > 7) // x can't possibly be >= 5, so this can't be true
 x = y + 1;
assert(x < 5);

if (y > 7) // the program will throw if >= 5, but that doesn't mean it can't be true
 x = y + 1;
enforce(x < 5);

Assert is much much more powerful. 

On Wednesday, 30 July 2014 at 14:51:34 UTC, Andrei Alexandrescu wrote:
>> If assert degenerates to assume in release mode, any bugs in the program
>> could potentially cause a lot more brittleness and unexpected/undefined
>> behavior than they otherwise would have. In particular, code generation
>> based on invalid assumptions could be memory unsafe.
>
> I think gcc does that.

It makes more sense in C because it's not memory safe anyways. In D, assume would not be @safe, so to have asserts become assumes in release mode seems problematic. Perhaps the assume could be omitted in safe code, similar to how bounds checks are retained for safe code even in release.

> Also, it's unclear to me what the optimizer would be supposed to do if an assumption turns out to be false.
>

One example is a switch statement, if we hint to the compiler (via assume) that the default case is unreachable, the compiler can potentially generate something like a jump table with no bounds check. To generate memory safe code, the compiler needs to insert the bounds check even though the assume says it's not needed.

On Wednesday, 30 July 2014 at 15:49:33 UTC, Daniel Murphy wrote:
> "Tofu Ninja"  wrote in message news:dtjqnyucskwnqjvksawg@forum.dlang.org...
>
>> Question?
>> If an if condition throws or returns in its body is it ok for the optimizer to 'assume' that the condition is false after and make optimizations for it? If so then every one complaining that assert gets removed in -release should really just be using enforce.
>
> Yes.  In fact, it's required that an optimizer do this in order not to be considered garbage.
>
>> The possibility for the optimizer to make the same optimizations for assert can be done for enforce, the only difference is that it does not get removed in -release....
>
> Not quite.  With enforce, it is impossible (ignoring hardware or optimizer errors) for the condition to be false if the enforce was not triggered. Because the assert is not checked, the condition could be false and the code could do something awful.
>
> Also, the optimizer can only use the enforce's assumption _after_ it has checked the condition.  Since with assert it doesn't need to check, it can go backwards and assume the previous code will never produce a value that can violate the assertion.
>
> if (y > 7) // x can't possibly be >= 5, so this can't be true
>  x = y + 1;
> assert(x < 5);
>
> if (y > 7) // the program will throw if >= 5, but that doesn't mean it can't be true
>  x = y + 1;
> enforce(x < 5);
>
> Assert is much much more powerful.

Ok so what is sounds like, is that assert is really what every one claims assume is and enforce is what every one claims assert is...

Maybe a documentation change on assert is all that is needed, it seems like the docs describe assert as something similar to enforce. Maybe it should be described in a way similar to assume with the added benefit that in non-release modes it will actually check that it is true at runtime. Also if that was changed then the documentation on version(assert) would need changing too.

On Wednesday, 30 July 2014 at 15:12:58 UTC, Ary Borenszweig wrote:
> On 7/30/14, 11:44 AM, Daniel Murphy wrote:
>> "Ary Borenszweig"  wrote in message news:lravtd$2siq$1@digitalmars.com...
>>
>>> Now, if you compile in release mode, according to Walter, all the
>>> "asserts" are gone (which, as a side note, is something I don't like:
>>> in every case it should throw an AssertError). So the question is: can
>>> the compiler still replace that writeln call? It should, but since
>>> there's nothing there preventing x + y to be different than 3 (the
>>> assertion is gone), the compiler can't replace it anymore.
>>
>> That's the whole point - the compiler theoretically can optimize as if
>> the assert is checked.
>>
>> (This example uses assert(0) because this behaviour is actually in the
>> spec)
>>
>> if (x != 3) assert(0);
>> if (x == 3) deleteAllMyFiles();
>>
>> The compiler is allowed to treat assert(0) as unreachable - and if it's
>> unreachable then it must be impossible for x to be != 3.
>>
>> So it becomes:
>>
>> deleteAllMyFiles();
>>
>> He's asking for assert to mean 'check this condition' and assume to mean
>> 'optimize as if this is a mathematical identity'.
>
> And how is that different if instead of:
>
> if (x != 3) assert(0);
>
> you write:
>
> assume(x != 3);
>
> ?

assert(0) is treated as a special case, different from assert(someRuntimeExpression)

On 07/30/2014 05:33 PM, Daniel Murphy wrote:
> "Timon Gehr"  wrote in message news:lrb2o9$314b$1@digitalmars.com...
>
>> > Because there is no way you can prove say OpenGL drivers to be correct.
>> > They are a black box provided by the execution environment.
>>
>> I see. (Though I secretly still dare to hope for verified OpenGL
>> drivers, or something analogous: it is not completely out of reach
>> theoretically; the machine can be given a quite precise formal
>> specification.)
>
> But even if the drivers are verified, the hardware might be buggy!  And
> if the hardware's verified,

My understanding is it often is.

> the power source might be unstable!

You should verify power source stability.

On a more serious note, are you trying to argue that there are no pragmatic differences in software quality based on the obvious fact that the system running the software is implemented on top of uncertain physics?

On 7/30/2014 7:51 AM, Andrei Alexandrescu wrote:
> Also, it's unclear to me what the optimizer would be supposed to do if an
> assumption turns out to be false.

The program is no longer valid at that point.

"Tofu Ninja"  wrote in message news:nwudcquzsuyrrlawxxyu@forum.dlang.org...

> Ok so what is sounds like, is that assert is really what every one claims assume is and enforce is what every one claims assert is...

Does it actually check the condition is true?
theoretical assert: in debug mode
D's assert: in debug mode
assume: no
enforce: always

Does it allow the compiler to remove code using normal control-flow analysis?
theoretical assert: in debug mode
D's assert: always
assume: always
enforce: always

Does it allow the compiler to remove any code that disagrees with the condition? (or is unnecessary when the condition is true?)
theoretical assert: no
D's assert: in release mode
assume: always
enforce: no

> Maybe a documentation change on assert is all that is needed, it seems like the docs describe assert as something similar to enforce. Maybe it should be described in a way similar to assume with the added benefit that in non-release modes it will actually check that it is true at runtime. Also if that was changed then the documentation on version(assert) would need changing too.

Yeah, it would probably be a good idea to make it very clear what the compiler is allowed to assume.  The current docs are somewhat accurate, but could be more specific.  If the 'assume' behaviour is possible with forms other than 'assert(0)' is not specified. 

On 7/30/2014 8:21 AM, Daniel Murphy wrote:
> "Andrei Alexandrescu"  wrote in message news:lrb20i$30jl$1@digitalmars.com...
>
>> So then I see nothing that assume can do that assert can't. -- Andrei
>
> assume can avoid confusing people that think D's assert means something it doesn't.

This reminds me of that old Basic program:

    ... code ...
    REM halt program
    STOP
    REM if skidding
    STOP

On Wednesday, 30 July 2014 at 15:49:33 UTC, Daniel Murphy wrote:
> "Tofu Ninja"  wrote in message news:dtjqnyucskwnqjvksawg@forum.dlang.org...
>
>> Question?
>> If an if condition throws or returns in its body is it ok for the optimizer to 'assume' that the condition is false after and make optimizations for it? If so then every one complaining that assert gets removed in -release should really just be using enforce.
>
> Yes.  In fact, it's required that an optimizer do this in order not to be considered garbage.
>
>> The possibility for the optimizer to make the same optimizations for assert can be done for enforce, the only difference is that it does not get removed in -release....
>
> Not quite.  With enforce, it is impossible (ignoring hardware or optimizer errors) for the condition to be false if the enforce was not triggered. Because the assert is not checked, the condition could be false and the code could do something awful.
>
> Also, the optimizer can only use the enforce's assumption _after_ it has checked the condition.  Since with assert it doesn't need to check, it can go backwards and assume the previous code will never produce a value that can violate the assertion.
>
> if (y > 7) // x can't possibly be >= 5, so this can't be true
>  x = y + 1;
> assert(x < 5);
>
> if (y > 7) // the program will throw if >= 5, but that doesn't mean it can't be true
>  x = y + 1;
> enforce(x < 5);
>
> Assert is much much more powerful.

So what is the recommended way of inserting a check of the sort that Ola would like?

debug enforce(expr);

perhaps? Seeing as that statement is completely missing outside of debug mode, the compiler can't do anything much about it.


P.S. What about version(assert)? Could the optimiser work with this:

if(x > 7) x++;
version(assert) auto testResult = x;
assert(x <= 7);

On 7/30/14, 12:19 PM, Daniel Murphy wrote:
> "Ary Borenszweig"  wrote in message news:lrb21p$30lf$1@digitalmars.com...
>
>> > He's asking for assert to mean 'check this condition' and assume to
>> mean
>> > 'optimize as if this is a mathematical identity'.
>>
>> And how is that different if instead of:
>>
>> if (x != 3) assert(0);
>>
>> you write:
>>
>> assume(x != 3);
>
> Because if assert only means 'check this condition' then the optimizer
> can't optimize based on the assumption that it's true.

Assert means: check this condition and terminate the program if it doesn't hold.

So why can't the compiler optimize based on this?