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

           Summary: Propagate some value ranges from contracts
           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 2013-08-03 04:28:59 PDT ---
I suggest to take a bit more seriously D contract programming, to increase a little its usefulness.

So I think the following code should compile:


char foo(immutable uint digit)
in {
    assert(digit < 10);
} body {
    return digit + '0'; // Error.
}
uint bar()
out(result) {
    assert(result < 100);
} body {
    return 99;
}
void main() {
    ubyte x = bar(); // Error.
}


DMD 2.064alpha gives:

test.d(5): Error: cannot implicitly convert expression (digit + 48u) of type
uint to char
test.d(14): Error: cannot implicitly convert expression (bar()) of type uint to
ubyte


In the first case 'digit' is immutable and the pre-condition asserts it can't be bigger than 9, so the result should be cast-able to char implicitly.

In the second case the post-condition tells that the result of 'bar' is an uint that fits in the range of an ubyte.

(Probably if D contracts become a bit more useful their usage will increase a little. Every useless cast removed from the code reduces the chance of bugs.)

-- 
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=10751


hsteoh@quickfur.ath.cx changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |hsteoh@quickfur.ath.cx


--- Comment #1 from hsteoh@quickfur.ath.cx 2013-08-05 20:25:43 PDT ---
One obstacle to implementing this enhancement is that D contracts allows arbitrary code inside the contract block. It's non-trivial to automatically extract value range information. For example, if instead of assert(digit < 10), I wrote assert(abs(3*digit*digit - 10) < 9), then the compiler will have to solve a quadratic equation in order to get a value range out of the expression. But since arbitrary expressions are allowed, I can easily write a 6th order polynomial on digit, and it will require unreasonable compiler resources to extract value range from it. Worse yet, I can write an arbitrary expression using abs, which is known to be undecidable.

If we restrict ourselves to simple expressions (i.e., the compiler will not attempt value range analysis on anything more complex than expressions of the form parameter < intLiteral), then it is within reach of implementation. However, since contracts allow arbitrary code, not just expressions, we have another kind of problem:

auto func(int x)
in {
   int y = x-1;
   while (complexCond(x,y))
      y = func(x,y);
   assert(x < y);
}
body {
 ...
}

You still can't handle the general case for value range extraction, since it requires solving the equivalent of the halting problem.

So the only implementable value range analysis can only support a very limited form of contracts -- only asserts with simple expressions.

-- 
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=10751



--- Comment #2 from bearophile_hugs@eml.cc 2013-08-06 01:27:36 PDT ---
(In reply to comment #1)
> One obstacle to implementing this enhancement is that D contracts allows arbitrary code inside the contract block.

I discussed this problem with Walter. He didn't see the need for specialized contract programming expressions with a very limited semantics (as in Ada, C# contrats, etc).


> So the only implementable value range analysis can only support a very limited form of contracts -- only asserts with simple expressions.

OK.

(So I presume you have to write the contract, and then you watch the compiler if it's able to infer or not statically the range. I think this is a bit weird, but I presume Walter likes it.)

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