http://d.puremagic.com/issues/show_bug.cgi?id=5906

           Summary: Just pre-conditions at compile-time when arguments are
                    static
           Product: D
           Version: D2
          Platform: All
        OS/Version: All
            Status: NEW
          Severity: enhancement
          Priority: P2
         Component: DMD
        AssignedTo: nobody@puremagic.com
        ReportedBy: bearophile_hugs@eml.cc


--- Comment #0 from bearophile_hugs@eml.cc 2011-04-28 16:19:57 PDT ---
This enhancement proposal was getting lost in a thread, so I have added it here too.

DMD currently runs functions at compile time only if their call is in a context where a compile-time value is expected, to avoid troubles (C++0X uses a keyword to avoid those problems). This is OK.


Note: DMD is able to run contracts too at compile-time, as you see in this
program (at the r1 enum):


import std.ctype: isdigit;
int foo(string text, int x)
in {
    assert(x >= 0 && x < text.length);
    foreach (c; text[0 .. x])
        assert(isdigit(c));
} body {
    return 0;
}
enum r1 = foo("123xxx", 4); // Error: assert(isdigit(cast(dchar)c)) failed
void main(string[] args) {
    auto r2 = foo(args[2], (cast(int)args.length) - 5);
    auto r3 = foo("123xxx", 4);
}


DMD 2.052 shows:
test.d(3): Error: assert(x > 0) failed
test.d(7): Error: cannot evaluate foo(-1) at compile time
test.d(7): Error: cannot evaluate foo(-1) at compile time


This is my idea: when you call a function where all its arguments are known at compile-time (as at the r3 variable) the compiler runs just the pre-condition of that function at compile-time. Uf a pre-condition can't run at compile-time, the compiler just ignores it silently, and later this pre-condition will run normally at run-time.

Note that I am not suggesting to run the whole function, and not its post-condition, just its pre-condition.

Running just the pre-condition is different from running the whole function
because:
- Pre-conditions are usually small or smaller than function bodies;
- Pre-conditions are usually meant to be fast (and not slower than the function
body), so they are probably not too much heavy to run. pre-conditions, unlike
debug{} code are meant to run often, sometimes even in normal usage of
programs;
- My pre-conditions are often pure. If this enhancement request gets accepted,
D programmers will be encouraged to write more pure preconditions. Even if a
function is not marked as "pure", what matters in this discussion is to its
pre-condition to be CTFE-pure. (Functions can run at compile-time even if they
aren't pure. They need to be pure just in the code path run at compile time).


Walter:

> Instead, we opted for a design that either must run at compile time, or must run at run time. Not one that decides one way or the other in an arbitrary, silent, and ever-changing manner.
> 
> The user must make an explicit choice if code is to be run at compile time or run time.

This problem is important for the normally run CT functions, and I agree with this decision. But it's much less important the idea presented here, because finding bug is almost never a deterministic process, it's usually probabilistic. People find only some bugs (people today find new bugs even in old very-high-quality C code used by everyone), lint tools (including the static analysis flag done by Clang) find only some other bugs, and usually different lints find different bugs. One important thing for those tools is to reduce false positives as much as possible (even if this increases false negatives a little), and the idea presented here doesn't produce false alarms (if the pre-conditions are correct).


This feature is useful because in your code I often have struct literals like (I assume their constructor has a pre-condition):

Foo f1 = Foo(10, -20);

The compiler is able at compile-time to tell this line of code is wrong because for example -20 is not acceptable. This is useful in many situations. This feature works only if the arguments are known at compile-time, this is a strong limitation of the idea presented here, but I think it's better to have it anyway.

Even if this feature sometimes gets "disabled" by turning a CTFE-pure function pre-condition into not CTFE-pure code, the programmer doesn't need to worry a lot about this, because even if this change doesn't allow to catch this bug in the code, other bugs too are not found by the compiler. All static analysis tools do the same, they sometimes find a bug, but if you change the code in a way they don't fully understand, they don't find the bug any more.

The feature I have proposed here is not a language feature, it's a compiler feature (the only change is in user code, that's encouraged to create CTFE-pure pre-conditions). This means that even if DMD doesn't want this idea, future D compilers will be free to adopt it. I think this is a cheap but useful compiler feature to add. It's a cheap feature because the compiler is kept simple (to catch contract bugs when arguments are not statically known the compiler needs some kind of constraint solver, that is not a simple thing).

A disadvantage of the idea presented here is that compilation times may become longer.

In the program shown the variable r2 is a situation where not all arguments of foo() are known at compile-time, so here the foo pre-condition is not run. The variable r2 is a situation where one argument of foo is known at run-time, and in this case the pre-condition contains a part (assert(x>=0&&x<text.length)) that's able to use this information to catch a bug. So an improvement of the idea is to perform this partial test. This looks less easy to implement, there is no need to implement this second idea too.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #1 from bearophile_hugs@eml.cc 2012-12-24 02:47:41 PST ---
In Ada 2012 there is a "Static_Predicate" aspect: http://www.ada-auth.org/standards/12rm/html/RM-3-2-4.html

It allows to attach a compile-time predicate that verifies the validity of a subtype (there is also "Dynamic_Predicate").


So an idea to reduce the problems underlined by Walter is to add "static preconditions" (note the static before the "in" (currently this code is not allowed):


import std.ascii: isDigit;
int foo(string text, int x)
static in {
    assert(x >= 0 && x < text.length);
    foreach (c; text[0 .. x])
        assert(isDigit(c));
} body {
    return 0;
}

void main() {}



Adding "static" to a precondition means the compiler will try to run the precondition at compile-time where possible, and at run-time where it's not possible. So the not-static preconditions are run only at run time, avoiding unwanted explosions of compilation times.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906


Walter Bright <bugzilla@digitalmars.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |bugzilla@digitalmars.com


--- Comment #2 from Walter Bright <bugzilla@digitalmars.com> 2012-12-25 03:03:59 PST ---
Right now, there's a clear distinction between compile time and run time computation. For the canonical example:

    assert(0);

We certainly do not want to run that at compile time, because it's only supposed to fail if control flow reaches there. For compile time, we've got:

    static assert(0);

which only runs at compile time.

From my POV, the "run it at compile time if possible" is fraut with problems. There's so much in D that relies on, for example, *failing* to compile an expression, that having a wishy-washy construct like the proposal raises a big flag of "there be dragons".

I'm strongly opposed to this proposal.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906


bearophile_hugs@eml.cc changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |RESOLVED
         Resolution|                            |INVALID


--- Comment #3 from bearophile_hugs@eml.cc 2012-12-25 03:25:54 PST ---
(In reply to comment #2)

> From my POV, the "run it at compile time if possible" is fraut with problems.

I understand. So the "static in" (static pre-condition) can't choose to work at compile-time or run-time. If present it must always run at compile-time. Probably the "Static_Predicate" aspect of Ada 2012 does the same.

So I close this enhancement request as invalid, and I will reopen it if and when I (or someone else) find some better ideas.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #4 from bearophile_hugs@eml.cc 2012-12-25 03:42:02 PST ---
If I write:

void main() {
    byte x = 200;
}


The compiler refuses that code statically, it means it performs a run-time test
of the value:
test.d(2): Error: cannot implicitly convert expression (200) of type int to
byte


But if I write code like this:

void main(string[] args) {
    byte x = args.length;
}


It does not perform that test at compile-time, because it can't, the value is known only at run-time.


What I'm trying to archive here is a way to emulate that built-in behavour in user-defined types. This means if I define a MyByte type (that is an integral struct value with the same admissible values interval as a signed byte), I'd like a way to define MyByte contracts so this code produces a compile-time error in the first assignment and a run-time error in the second assignment:


void main(string[] args) {
    MyByte x = 200; // compile-time error here
    MyByte x = 200 + args.length; // run-time error here
}


That's why I have suggested a "static in". But according to your answer my solution is not good enough.

Other better ideas are welcome.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #5 from bearophile_hugs@eml.cc 2012-12-25 03:42:49 PST ---
(In reply to comment #4)

> The compiler refuses that code statically, it means it performs a run-time test of the value:

Sorry, I meant a compile-time test.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #6 from bearophile_hugs@eml.cc 2013-02-27 15:56:31 PST ---
(In reply to comment #4)

> But if I write code like this:
> 
> void main(string[] args) {
>     byte x = args.length;
> }
> 
> 
> It does not perform that test at compile-time, because it can't, the value is known only at run-time.

That code too is statically refused because a size_t is out of bounds of a byte.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906


yebblies <yebblies@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |yebblies@gmail.com


--- Comment #7 from yebblies <yebblies@gmail.com> 2013-03-08 01:25:47 EST ---
I agree with Walter, nothing should be ctfe'd unless the code explicitly asks for it.

However...

If the contracts are fairly simple, like in this function:

int func(int a, int b)
in
{
    assert(a + b != 12);
}
out(result)
{
    assert(result >= 20);
}
body
{
    return 15;
}

It would be possible for the compiler to use constant-folding (not ctfe) to verify the assertions can pass, in the pre- and post-conditions.

eg.
func(3, 9); Error: function call func(3, 9) cannot pass precondition

or
Error: 'return 15' cannot pass postcondition

This can be done by converting precondition bodies to expressions then const-folding them.  Non-trivial, but possible.

This only makes sense if we define violating a function's precondition as invalid code.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #8 from bearophile_hugs@eml.cc 2013-03-07 12:15:52 PST ---
(In reply to comment #7)

> This can be done by converting precondition bodies to expressions then const-folding them.  Non-trivial, but possible.

Thank you for the note, that seems better than having nothing.


> This only makes sense if we define violating a function's precondition as invalid code.

This seems OK. What are possible downsides of this?

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------

http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #9 from yebblies <yebblies@gmail.com> 2013-03-08 13:33:42 EST ---
(In reply to comment #8)
> (In reply to comment #7)
> 
> > This can be done by converting precondition bodies to expressions then const-folding them.  Non-trivial, but possible.
> 
> Thank you for the note, that seems better than having nothing.
> 
> 
> > This only makes sense if we define violating a function's precondition as invalid code.
> 
> This seems OK. What are possible downsides of this?

struct S(int a)
{
    void fun(int b) in { assert(a != b); } body {}
}

void main()
{
    foreach(i; TypeTuple!(1, 2, 3, 4))
    {
        auto s = S!i();
        if (i != 4)
            s.fun(4);
    }
}

This code would error 'cannot call S.fun with b == 4' etc even though S.fun never actually gets called with 4.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------