Re: assume, assert, enforce, <at> safe

On 7/30/14, 3:39 PM, Joseph Rushton Wakeling via Digitalmars-d wrote:
> On 31/07/14 00:01, Walter Bright via Digitalmars-d wrote:
>> 7. using enforce() to check for program bugs is utterly wrong.
>> enforce() is a
>> library creation, the core language does not recognize it.
>
> A question on that.
>
> There are various places in Phobos where enforce() statements are used
> to validate function input or class constructor parameters.

Yah, Phobos is a bit inconsistent about that. TDPL discusses the matter: 
if a library is deployed in separation from the program(s) it serves, it 
may as well handle arguments as "input". That's what e.g. the Windows 
API is doing - it consistently considers all function arguments 
"inputs", scrubs them, and returns error codes for all invalid inputs it 
detects. In contracts, the traditional libc/Unix interface does little 
checking, even a strlen(NULL) will segfault.

Phobos is somewhere in the middle - sometimes it verifies arguments with 
enforce(), some other times it just uses assert().

Andrei

Re: checkedint call removal

On 7/30/2014 3:20 PM, Artur Skawina via Digitalmars-d wrote:
> On 07/30/14 23:42, Walter Bright via Digitalmars-d wrote:
>> On 7/30/2014 2:34 PM, Timon Gehr wrote:
>>> He understands that and notes that this contradicts the promise of  <at> safe.
>>
>> No, it does not.  <at> safe never promises that "all your asserts are correct".
>>
>>  <at> safe's promise is one of memory safety, not a promise of program correctness.
>
>     void f(ubyte[] a)  <at> safe { assert(a.length>99); a[88] = a[77]; }

The compiler will insert array bounds checking for you.

assume, assert, enforce, <at> safe

I'd like to sum up my position and intent on all this.

1. I can discern no useful, practical difference between the notions of assume 
and assert.

2. The compiler can make use of assert expressions to improve optimization, even 
in -release mode.

3. Use of assert to validate input is utterly wrong and will not be supported. 
Use such constructs at your own risk.

4. An assert failure is a non-recoverable error. The compiler may assume that 
execution does not proceed after one is tripped. The language does allow 
attempts to shut a program down gracefully after one is tripped, but that must 
not be misconstrued as assuming that the program is in a valid state at that point.

5. assert(0); is equivalent to a halt, and the compiler won't remove it.

6. enforce() is meant to check for input errors (environmental errors are 
considered input).

7. using enforce() to check for program bugs is utterly wrong. enforce() is a 
library creation, the core language does not recognize it.

8.  <at> safe is a guarantee of memory safety. It is not a guarantee that a program 
passes all its assert expressions. -release does not disable  <at> safe.

9. -noboundscheck does disable  <at> safe's array bounds checks, however, the 
compiler may assume that the array index is within bounds after use, even 
without the array bounds check.
(Continue reading)

Trass3r via Digitalmars-d | 30 Jul 21:46 2014

Re: 64-bit DMD for windows?

Is there a PR now?

Re: checkedint call removal

On 07/30/2014 09:16 PM, H. S. Teoh via Digitalmars-d wrote:
> On Wed, Jul 30, 2014 at 07:09:41PM +0000, via Digitalmars-d wrote:
>> On Wednesday, 30 July 2014 at 18:25:43 UTC, H. S. Teoh via Digitalmars-d
>> wrote:
>>> If you want the check to always be there, use enforce, not assert.
>>
>> Doesn't help:
>>
>>      module a;
>>      void bar(int x) {
>>          assert(x > 0);
>>          writeln("x = ", x);
>>      }
>>      // --------
>>      module b;
>>      import a;
>>      void foo(int x) {
>>          enforce(x > 0);
>>          bar(x);
>>      }
>>
>> If `assert` is treated like `assume` (under Ola's definitions), then
>> `enforce` can be optimized away.
>
> Wait, what? I thought the whole point of enforce is that it will *not*
> be removed by the compiler, no matter what?
>
>
> T
>
(Continue reading)

via Digitalmars-d | 30 Jul 21:25 2014

Re: checkedint call removal

On Wednesday, 30 July 2014 at 18:48:21 UTC, H. S. Teoh via 
Digitalmars-d wrote:
> 1) When compiling in non-release mode:
> 	assert(...) means "I believe condition X holds, if it doesn't I
> 		screwed up big time, my program should abort"

Assert(X) means, the specification requires theorem X to be 
proved by all implicit or explicit axioms/assumptions made prior 
to this either implicitly or explicitly.

> 	assume(...) means as "I believe condition X holds, if it 
> doesn't
> 		I screwed up big time, my program should abort"

Assume(X) means, the specification specifies (axiom) X (to hold).

> 2) When compiling in release/optimized mode:
> 	assert(...) means "Trust me, I've made sure condition X holds,
> 		please optimize my code by not bothering to check
> 		condition X again"

No. Assert(X) does not change any meaning. You just turned off 
program verification. Assumes and asserts are annotations.

> 	assume(...) means "Trust me, I've made sure condition X holds,
> 		please optimize my code by making use of condition X"

Assume(X) means that the specification defines X to hold at this 
point.

(Continue reading)

How Optlink works

http://i.imgur.com/iRNrBE4.gif

via Digitalmars-d | 30 Jul 21:09 2014

Re: checkedint call removal

On Wednesday, 30 July 2014 at 18:25:43 UTC, H. S. Teoh via 
Digitalmars-d wrote:
> If you want the check to always be there, use enforce, not 
> assert.

Doesn't help:

     module a;
     void bar(int x) {
         assert(x > 0);
         writeln("x = ", x);
     }
     // --------
     module b;
     import a;
     void foo(int x) {
         enforce(x > 0);
         bar(x);
     }

If `assert` is treated like `assume` (under Ola's definitions), 
then `enforce` can be optimized away.

Re: checkedint call removal

On 07/30/2014 08:46 PM, H. S. Teoh via Digitalmars-d wrote:
> I can't think of a real-life scenario where you'd want to distinguish
> between the two kinds of optimizations in (2).

That was never up to debate and that distinction is indeed rather pointless.

Re: checkedint call removal

On 7/30/2014 11:24 AM, H. S. Teoh via Digitalmars-d wrote:
> If you want the check to always be there, use enforce, not assert.

enforce is NOT for checking program logic bugs, it is for checking for possible 
environmental failures, like writing to a read-only file.

If you want an assert to be there even in release mode,

     assert(exp) => exp || assert(0)

Re: checkedint call removal

On 7/30/2014 8:28 AM, H. S. Teoh via Digitalmars-d wrote:
>[...]

Exactly right.


Gmane