On 07/30/14 13:56, Daniel Murphy via Digitalmars-d wrote:
> "Artur Skawina via Digitalmars-d"  wrote in message news:mailman.217.1406713015.16021.digitalmars-d@puremagic.com...
> 
>> `assert` is for *verifying* assumptions. It must not allow them to leak/escape. Otherwise a single not-100%-correct assert could defeat critical runtime checks.
> 
> All you're saying is you want them to have different names,

"D - the language that redefines commonly used and universally understood terms and concepts"?

> not that it can't work the way Walter and I have described.

Possible != sane.

The main problem isn't even the terminology; it's the consequences wrt safety and correctness.

>  If your assertions are invalid and you're compiling with -release, the compiler is free to generate invalid code.  -release is dangerous.  -release is telling the compiler that the code you wrote is correct,  and it can rely on it to be correct.

Consider a service/program that handles user supplied data. It
uses several third-party libs, one for parsing and validating the
inputs, another for some other processing/communication, etc.
One is carefully written with security in mind and can safely
deal with every possible valid or invalid input. Another was not
considered security sensitive and designed to work on valid data.
The input requirements are just documented and only checked via
asserts. Now the programmer implementing that service only needs
to make a single mistake, so that an invalid (or just unexpected)
input is passed to the less hardened lib. In a production setting
the asserts are not present, but the assumptions have leaked to
the other libs, and some of the carefully written checks have been
statically eliminated by the compiler. Code that was perfectly safe
gained an invisible (!) security hole, because of an innocent
looking assert statement in a different code base.

artur

"Artur Skawina via Digitalmars-d"  wrote in message news:mailman.227.1406728603.16021.digitalmars-d@puremagic.com...

> "D - the language that redefines commonly used and universally
> understood terms and concepts"?

Yes, see pure for another example.  "D - the pragmatic language"

> > not that it can't work the way Walter and I have described.
>
> Possible != sane.
>
> The main problem isn't even the terminology; it's the consequences
> wrt safety and correctness.

Yes, this is a much more useful discussion to have than what other people have definined assert to do.

> Consider a service/program that handles user supplied data. It
> uses several third-party libs, one for parsing and validating the
> inputs, another for some other processing/communication, etc.
> One is carefully written with security in mind and can safely
> deal with every possible valid or invalid input. Another was not
> considered security sensitive and designed to work on valid data.
> The input requirements are just documented and only checked via
> asserts. Now the programmer implementing that service only needs
> to make a single mistake, so that an invalid (or just unexpected)
> input is passed to the less hardened lib. In a production setting
> the asserts are not present, but the assumptions have leaked to
> the other libs, and some of the carefully written checks have been
> statically eliminated by the compiler. Code that was perfectly safe
> gained an invisible (!) security hole, because of an innocent
> looking assert statement in a different code base.

Yes, it is a very powerful and dangerous optimization capability.  If the optimization benefits are not worth the potential escalation of code wrong-ness, then don't enable it.  If security is more important than speed, don't disable assertion and bounds checks.

If used wrong it will do the wrong thing.  This is already true of compiler optimizations.  The optimizer may turn invalid code into security problems - have a google around and you'll find some examples. 

On Wednesday, 30 July 2014 at 14:11:24 UTC, Daniel Murphy wrote:
>
> If used wrong it will do the wrong thing.  This is already true of compiler optimizations.  The optimizer may turn invalid code into security problems - have a google around and you'll find some examples.

I think the point here is that usually, when the optimiser changes the semantics of valid code, it's considered a bug in the optimiser.

-Wyatt

On 7/30/14, 4:17 AM, "Ola Fosheim Grøstad" <ola.fosheim.grostad+dlang@gmail.com>" wrote:
> On Wednesday, 30 July 2014 at 03:32:50 UTC, Walter Bright wrote:
>> On 7/29/2014 7:08 PM, Timon Gehr wrote:
>>> Of course version(assert) is a language feature. Always double-check
>>> your claims.
>>>
>>> It's even documented: http://dlang.org/version.html
>>
>> You're right. My mistake. I'd forgotten about that.
>>
>>
>>>> Not a bit. The distinction utterly escapes me.
>>> This is unfortunate, but I don't know what else to say.
>>
>> I don't either. I still have no idea what the difference between
>> assume(i<6) and assert(i<6) is supposed to be.
>
> main(){
>    foobar();
>    assert(false==true)
> }
>
> With assert():
>
> main(){
>    foobar();
> }

Could you show an example that's a bit more complex and useful? I'm with Walter that I don't see any difference between assert and assume.

For example:

---
int x = ...;
int y = ...;

assert(x + y == 3);

writeln(x + y);
---

If the assert fails then the program crashes in non-release mode. So after the assert the compiler knows that "x + y == 3" so that it can replace "writeln(x + y)" with "writeln(3)" (assuming the compiler is the smartest on earth).

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.

With assume... what's the difference? You say the compiler should replace it anyway because that's what you assume? There's nothing left at release mode to verify that for you.

Could you elaborate this example using assert and assume?

Thanks!

"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'. 

"Wyatt"  wrote in message news:wpyvrdoofziktwqkzqbf@forum.dlang.org...

> I think the point here is that usually, when the optimiser changes the semantics of valid code, it's considered a bug in the optimiser.

s/usually/always/

The thing is, code containing an assertion that is not always true is not valid code. 

On 7/30/14, 12:54 AM, David Bregman wrote:
> On Wednesday, 30 July 2014 at 03:32:50 UTC, Walter Bright wrote:
>> I don't either. I still have no idea what the difference between
>> assume(i<6) and assert(i<6) is supposed to be.
>
> assert:
> is a runtime check of the condition.
> is a debugging/correctness checking feature.
> is used when the expression is believed true, but is not proven so.
> (if it was proven, then there is no purpose in asserting it with a
> redundant runtime check that is guaranteed to never activate.)
>
> assume:
> passes a hint to the optimizer to allow better code generation.
> is used when the expression is proven to be true (by the programmer,
> like @trusted).

Thanks for the summary! It seems to me indeed there's little assume does that can't be done with assert today.

> The only relation between the two is that if a runtime check for (x) is
> inserted at some point, it is safe to insert an assume(x) statement
> afterwards, because x is known true at that point.

So then one might redefine assert to always insert an assume right afterwards.

> 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.

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


Andrei

On Wednesday, 30 July 2014 at 14:51:34 UTC, 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.

Bad... bad... things...

On 7/30/14, 4:56 AM, Daniel Murphy wrote:
> "Artur Skawina via Digitalmars-d"  wrote in message
> news:mailman.217.1406713015.16021.digitalmars-d@puremagic.com...
>
>> `assert` is for *verifying* assumptions. It must not allow them
>> to leak/escape. Otherwise a single not-100%-correct assert could
>> defeat critical runtime checks.
>
> All you're saying is you want them to have different names, not that it
> can't work the way Walter and I have described.  If your assertions are
> invalid and you're compiling with -release, the compiler is free to
> generate invalid code.  -release is dangerous.  -release is telling the
> compiler that the code you wrote is correct,  and it can rely on it to
> be correct.

Exactly! -- Andrei

On 7/30/14, 6:43 AM, Daniel Murphy wrote:
> "Andrei Alexandrescu"  wrote in message
> news:lr8tcf$l1t$1@digitalmars.com...
>
>> Fancier: exp || assert(0) is still an expression.
>
> Fancier is not always better.

It's better when you need an expression. -- Andrei