www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 5906] New: Just pre-conditions at compile-time when arguments are static

reply d-bugmail puremagic.com writes:
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: -------
Apr 28 2011
next sibling parent d-bugmail puremagic.com writes:
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: -------
Dec 24 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Dec 25 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Dec 25 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Dec 25 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Dec 25 2012
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Feb 27 2013
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Mar 07 2013
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Mar 07 2013
prev sibling next sibling parent d-bugmail puremagic.com writes:
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: -------
Mar 07 2013
prev sibling next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #10 from bearophile_hugs eml.cc 2013-03-07 19:25:12 PST ---
(In reply to comment #9)


 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.


I see, thank you for the answer.
If the pre-condition analysis (constant folding) is done after a normal step of
dead branch removal, then maybe that error will not be shown.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Mar 07 2013
prev sibling next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #11 from bearophile_hugs eml.cc 2013-03-07 19:29:40 PST ---
(In reply to comment #10)


 If the pre-condition analysis (constant folding) is done after a normal step of
 dead branch removal, then maybe that error will not be shown.


Currently it doesn't happen, and this generates an error (you need a "static
if" to make the error go away):


import std.typetuple;
void main() {
    int[4] a;
    foreach (i; TypeTuple!(1, 2, 3, 4)) {
        if (i != 4)
            a[i]++;
    }
}

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
Mar 07 2013
prev sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=5906



--- Comment #12 from yebblies <yebblies gmail.com> 2013-03-08 14:33:58 EST ---
(In reply to comment #10)

 
 I see, thank you for the answer.
 If the pre-condition analysis (constant folding) is done after a normal step of
 dead branch removal, then maybe that error will not be shown.



 Currently it doesn't happen, and this generates an error (you need a "static
if" to make the error go away):


That is an interesting point.

I seriously doubt that would be enough anyway, I think you would need full flow
analysis to work out which paths can actually be taken.

Another good example is this:

int div(int a, int b)
in
{
    assert(b != 0, "Division by zero!");
}
body
{
    return a / b;
}

void main(string[] args)
{
    auto i = 3 / 0; // Fails at compile time
    auto j = div(3, 0); // Would fail at compile time if this was implemented
}

So maybe it is acceptable.

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