Monday, May 19, 2014

Using real arithmetic to eliminate bounds checking

This post is a repost of a question I asked on Lambda the Ultimate.
The usual problem with eliminating array bounds checking is that integer arithmetic is undecidable. For example, the compiler can't figure out that you can index into an array of m·n elements using an expression like i·n+j, even if it's known statically that 0≤i<m and 0≤j<n. Or rather, that particular problem is simple, but it's hard to come up with a general algorithm that would work for many different programs. To solve that problem, some people are trying to use dependent types and machine-checkable proofs, like Hongwei Xi, or restrict their attention to Presburger arithmetic (which is decidable but doesn't support multiplication), like Corneliu Popeea.
To take a different approach to the problem, we can note that statements like "if i ∈ [0,m-1] and j ∈ [0,n-1], then i·n+j ∈ [0,m·n-1]" (all segments are closed) can be interpreted and proved in real arithmetic, instead of integer arithmetic. The nice thing is that real arithmetic is decidable. If that approach works, we can have a language with integer-parameterized types like "array of n elements" and "integer between m and n", and have a simple definition of what the type checker can and cannot automatically prove about programs using such types, without having to write any proofs explicitly.
Of course the system will be limited by the fact that it's talking about reals rather than integers. For example, there will be problems with integer-specific operations on type parameters, like division and remainder, but I don't know how often these will be required.
In the comments to my post on LtU, Tom Primožič has carried out some experiments with several SMT solvers, including Microsoft's Z3. Indeed, it turns out that integer solvers can't handle the above example with matrix addressing, but a real arithmetic solver does the job easily. Here's a translation of the matrix addressing example, which you can try out in Z3's online interface:
(declare-const i Int)
(declare-const j Int)
(declare-const m Int)
(declare-const n Int)
(assert (and (<= 0 i) (<= i (- m 1))))
(assert (and (<= 0 j) (<= j (- n 1))))
(assert (and (<= 0 n) (<= 0 m)))

(assert (not (<= (+ (* i n) j) (- (* m n) 1))))
(check-sat-using qfnra-nlsat)

Note that the last line invokes the nonlinear real arithmetic solver NLSat. If you replace the last line with (check-sat) to use the default integer solver instead, it will timeout and fail to find a proof.

No comments:

Post a Comment