[Issue 10751] Propagate some value ranges from contracts

d-bugmail at puremagic.com d-bugmail at puremagic.com
Mon Aug 5 20:25:45 PDT 2013


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


hsteoh at quickfur.ath.cx changed:

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


--- Comment #1 from hsteoh at 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: -------


More information about the Digitalmars-d-bugs mailing list