Propagate some value ranges from contracts

[dlangBugzillaToGithub]

bearophile_hugs reported this on 2013-08-03T04:28:59Z

Transferred from https://issues.dlang.org/show_bug.cgi?id=10751

CC List

Description

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.)

[dlangBugzillaToGithub]

hsteoh commented on 2013-08-05T20:25:43Z

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.

[dlangBugzillaToGithub]

bearophile_hugs commented on 2013-08-06T01:27:36Z

(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.)