Checked Arithmetics

When working with data from an unknown source, it is often useful to be able to perform "checked arithmetics" to avoid overflows in computations. A common example is when computing the size of a buffer: 

void createImage(Nat width, Nat height) {
    Nat size = width * height * 4;
    Buffer buffer = buffer(size);
    // Index into 'buffer'...
}

However, if width and height are too large the multiplication will overflow, causing the allocation to be too small. As such, subsequent accesses into the buffer may be out of bounds (note that accesses to buffer are checked, so nothing bad will happen unless you access the buffer from machine code).

In these cases, one would need to check that none of the multiplications overflow. This is tedious to do, and not easy to get right. To help, the Storm standard library provides core.CheckedNat and core.CheckedWord. Both behave like a (simplified version of) core.Nat and core.Word respectively. The difference is that all arithmetic operations are checked for overflow. When this happen, they turn into a special "error" value, that makes any further calculations fail. The error value is thereby propagated to the end without having to check for errors at each step.

Other numbers can be automatically converted to core.CheckedNat and core.CheckedWord respectively. Thereby, as soon as one value in an expression is a checked value, the other ones will be converted accordingly as well (given the proper evaluation order). For example, the createImage function can be rewritten as follows to avoid overflows: 

void createImage(Nat width, Nat height) {
    CheckedNat size = CheckedNat(width) * CheckedNat(height) * 4;
    unless (value = size.nat)
        fail "Integer overflow!";
    Buffer buffer = buffer(size);
    // Index into 'buffer'...
}

As can be noted above, the nat member is used to convert the checked version to a normal Nat. This function returns a Maybe<Nat> that needs to be checked in a weak cast. It is also possible to check whether an error has occurred using error.