| # Interval Arithmetic |
| |
| Regular arithmetic says things like: if `x` has the value `3` and `y` has the |
| value `20`, then the expression `(x + y)` has the value `23`. |
| |
| Interval arithmetic says things like: if `x`'s value is in the |
| [range](/doc/note/ranges-and-rects.md) `3 ..= 5` and `y`'s value is in the |
| range `20 ..= 63`, then the expression `(x + y)`'s value is in the range `23 |
| ..= 68`. |
| |
| With integer interval arithmetic, addition is trivial: the lower and upper |
| (inclusive) bounds of a sum is the sum of the lower and upper bounds. |
| Multiplication is still straightforward, with care needed when possibly |
| multiplying by a negative number: `((x * 2) > x)` is false when `x` is |
| negative. Other arithmetic operations, like divisions, shifts and even bitwise |
| operations ('and' and 'or') are still computable, although more complicated. |
| |
| |
| ## Bounds / Overflow Checking |
| |
| In Wuffs, integer interval arithmetic is used for bounds and overflow checking. |
| For example, this program snippet: |
| |
| ``` |
| var a : array[256] base.32 |
| var x : base.u32[0 ..= 2] |
| var y : base.u32[0 ..= 100] |
| |
| etcetera |
| |
| return a[(x * y) + 80] |
| ``` |
| |
| fails to compile, because the range of the expression `((x * y) + 80)` is `[0 |
| ..= 280]`, part of which falls outside of the array `a`'s acceptable indexes: |
| the range `[0 ..= 255]`. |
| |
| |
| ## `i = i + 1` Doesn't Compile |
| |
| Similarly, this program snippet: |
| |
| ``` |
| var i : base.u32[0 ..= 10] |
| |
| etcetera |
| |
| i = i + 1 |
| ``` |
| |
| fails the compile-time bounds / overflow checker, because the assignment's |
| RHS's (Right Hand Side's) range, `[1 ..= 11]`, is not wholly contained by the |
| LHS (Left Hand Side) variable's range: `i` has range `[0 ..= 10]`. If `i` had |
| an unrefined type, such as `base.u32`, then this is essentially an overflow |
| check. |
| |
| |
| ## Masking Array Indexes |
| |
| A common pattern is for the array length to be a power of 2, e.g. `256` is |
| `0x100`, and the index expression to be and-ed with a mask value one less than |
| that length, e.g. `255` is `0xFF`. Continuing the example above: |
| |
| ``` |
| return a[((x * y) + 80) & 0xFF] |
| ``` |
| |
| will compile, since the range of `(((x * y) + 80) & 0xFF)` is `[0 ..= 255]`. |
| This is equal to and therefore trivially wholly contained by `a`'s acceptable |
| index range. |
| |
| |
| ## Interaction with Facts |
| |
| For an expression like `(i + 1)`, the relevant interval for the sub-expression |
| `i` starts with `i`'s possibly-refined type, `base.u32[0 ..= 10]`. This is a |
| static concept - a variable's type cannot change - but can be further narrowed |
| by dynamic constraints, or [facts](/doc/note/facts.md). For example, while a |
| bare `i = i + 1` will never pass the bounds/overflow checker, making that |
| assignment conditional can pass: |
| |
| ``` |
| var i : base.u32[0 ..= 10] |
| |
| etcetera |
| |
| if i <= 4 { |
| i = i + 1 |
| } |
| ``` |
| |
| Inside that if-block, up until the assignment to `i`, the range of possible `i` |
| values are the intersection of two ranges. The first range comes from the type: |
| `[0 ..= 10]`. The second range comes from the if-condition: `[-∞ ..= 4]`. The |
| intersection is `[0 ..= 4]`, and the range of possible values for the |
| expression `(i + 1)` is therefore `[1 ..= 5]`. Since `[1 ..= 5]` is wholly |
| contained by the LHS variable's type's range, `[0 ..= 10]`, the assignment is |
| valid. |
| |
| |
| ## Slices and Arrays |
| |
| Recall the difference between [slices and |
| arrays](/doc/note/slices-arrays-and-tables.md): slices have dynamic (run-time |
| determined) length, arrays have static (compile-time determined) length. For an |
| index expresssion like `s[expr]` or `a[expr]`, bounds-checking an array-index |
| can be done by interval arithmetic and refinement types alone, but |
| bounds-checking a slice-index can only be done by an if-condition or |
| while-condition (or, less frequently, an [iterate |
| loop](/doc/note/iterate-loops.md)), introducing a dynamic fact: |
| |
| ``` |
| var s : slice base.u8 |
| var x : base.u8 |
| |
| etcetera |
| |
| // The "0 <= expr" can be omitted if the compiler can prove that the |
| // range of expr's possible values does not contain any negative values. |
| // This is trivial if the expression expr is just a variable that has an |
| // unsigned integer type. |
| while (0 <= expr) and (expr < s.length()) { |
| x = s[expr] |
| etcetera |
| } |
| ``` |
| |
| |
| ## Go Programming Language Library |
| |
| For those programmers wishing to work with integer interval arithmetic, the |
| [`github.com/google/wuffs/lib/interval`](https://godoc.org/github.com/google/wuffs/lib/interval) |
| package is usable without requiring anything else Wuffs-related. Specifically, |
| that package depends only on the standard `math/big` package. |