www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.bugs - [Issue 10751] New: Propagate some value ranges from contracts

reply d-bugmail puremagic.com writes:
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



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: -------
Aug 03 2013
next sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=10751


hsteoh quickfur.ath.cx changed:

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



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: -------
Aug 05 2013
prev sibling parent d-bugmail puremagic.com writes:
http://d.puremagic.com/issues/show_bug.cgi?id=10751






 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

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: -------
Aug 06 2013