Improve support for arrays of unknown element size

[btj]

Currently, verifying programs that involve arrays whose element size is not statically known, like arrays of structs, is encumbered by the need to manually invoke the mul_mono_l lemma to prove that pointer arithmetic stays within bounds. Indeed, if sizeof(T) is not a literal number, then p + i where p is of type T * and i is of integral type, involves nonlinear arithmetic, and proof obligations like 0 <= p + i and p + i <= UINTPTR_MAX are not discharged automatically. They typically require invocations of mul_mono_l(0, i, sizeof(T)) (to prove that 0 <= i * sizeof(T) given 0 <= i) and mul_mono_l(i, n, sizeof(T)) (to prove that i * sizeof(T) <= n * sizeof(T) given i <= n).

See examples/array_of_struct.c for an example of this.

This problem will become much more pressing when VeriFast moves to targetless verification ( #143 ), where sizeof(int) and sizeof(T *) are not literals. Then, examples like arraylist.c (array of pointers) and mergesort_and_binarysort.c (array of ints) will need such lemma calls as well.

[btj]

Proof obligations in array_of_struct.c that currently require explicit lemma calls:

A. Unsigned multiplication underflow check: 0 <= n * s given 0 <= n; requires mul_mono_l(0, n, s). This multiplication is the argument to a malloc call.

B. Unsigned multiplication overflow check: n * s <= u given n <= u / s; requires div_rem_nonneg(u, s)(*) and mul_mono_l(n, u / s, s). This multiplication is the argument to a malloc call.

C. Precondition of chars_split(p, k): s <= m * s given 1 <= m; requires mul_mono_l(1, m, s)

Here, s is in each case of the form sizeof(T).

(*) Here, u / s appears in the C code so we should probably just invoke div_rem_nonneg(a, b) automatically when we evaluate a / b (or a % b).

[btj]

Proof obligations in arraylist.c that will require explicit lemma calls under targetless verification:

A. Unsigned multiplication underflow check: 0 <= n * s given 0 <= n; requires mul_mono_l(0, n, s). This multiplication is the argument to a malloc call.

B. Unsigned multiplication overflow check: n * s <= u given n <= u / s; requires div_rem_nonneg(u, s) and mul_mono_l(n, u / s, s). This multiplication is the argument to a malloc call.

C. Unsigned multiplication underflow check: 0 <= n * s given 0 <= n; requires mul_mono_l(0, n, s). This multiplication is the third argument to a memcpy call that copies an array of n pointers. The proof obligation can alternatively be discharged by invoking pointers_to_chars, which causes n * s to appear as the second argument of a chars chunk; the chars_inv autolemma then produces s * n = length(cs). By the length_nonnegative autolemma, we then get the PO. If pointers_to_chars is not invoked explicitly, it is invoked implicitly, but only after n * s is checked for underflow.

D. Unsigned multiplication overflow check: i * s <= u given i <= n and n * s <= u; requires mul_mono_l(i, n, s)

E. Pointer arithmetic underflow check: 0 <= p + i * s given 0 <= p and 0 <= i; requires mul_mono_l(0, i, s) or pointer_limits(p + i * s).

F. Pointer arithmetic overflow check: p + (i + 1) * s <= u given i + 1 <= n and p + n * s <= u; requires mul_mono_l(i + 1, n, s) or pointer_limits(p + i * s).