digitalmars.D.bugs - [Issue 10751] New: Propagate some value ranges from contracts
- d-bugmail puremagic.com (45/45) Aug 03 2013 http://d.puremagic.com/issues/show_bug.cgi?id=10751
- d-bugmail puremagic.com (37/37) Aug 05 2013 http://d.puremagic.com/issues/show_bug.cgi?id=10751
- d-bugmail puremagic.com (13/17) Aug 06 2013 http://d.puremagic.com/issues/show_bug.cgi?id=10751
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
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
http://d.puremagic.com/issues/show_bug.cgi?id=10751One 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