CVS commit: src/usr.bin/vndcompress

["Taylor R Campbell" <riastradh%netbsd.org@localhost>]

Module Name:    src
Committed By:   riastradh
Date:           Sat Jul 29 21:04:07 UTC 2017

Modified Files:
        src/usr.bin/vndcompress: common.h offtab.c vndcompress.c
            vnduncompress.c

Log Message:
Clarify compile-time and run-time arithmetic safety assertions.

This is an experiment with a handful of macros for writing the
checks, most of which are compile-time:

MUL_OK(t, a, b)         Does a*b avoid overflow in type t?
ADD_OK(t, a, b)         Does a + b avoid overflow in type t?
TOOMANY(t, x, b, m)     Are there more than m b-element blocks in x in type t?
                        (I.e., does ceiling(x/b) > m?)

Addenda that might make sense but are not needed here:

MUL(t, a, b, &p)        Set p = a*b and return 0, or return ERANGE if overflow.
ADD(t, a, b, &s)        Set s = a+b and return 0, or return ERANGE if overflow.

Example:

        uint32_t a = ..., b = ..., y = ..., z = ..., x, w;

        /* input validation */
        error = MUL(size_t, a, b, &x);
        if (error)
                fail;
        if (TOOMANY(uint32_t, x, BLKSIZ, MAX_NBLK))
                fail;
        y = HOWMANY(x, BLKSIZ);
        if (z > Z_MAX)
                fail;
        ...
        /* internal computation */
        __CTASSERT(MUL_OK(uint32_t, Z_MAX, MAX_NBLK));
        w = z*y;

Obvious shortcomings:

1. Nothing checks your ctassert matches your subsequent arithmetic.
   (Maybe we could have BOUNDED_MUL(t, x, xmax, y, ymax) with a
   ctassert inside.)

2. Nothing flows the bounds needed by the arithmetic you use back
   into candidate definitions of X_MAX/Y_MAX.

But at least the reviewer's job is only to make sure that (a) the
MUL_OK matches the *, and (b) the bounds in the assertion match the
bounds on the inputs -- in particular, the reviewer need not derive
the bounds from the context, only confirm they are supported by the
paths to it.

This is not meant to be a general-purpose proof assistant, or even a
special-purpose one like gfverif <http://gfverif.cryptojedi.org/>.
Rather, it is an experiment in adding a modicum of compile-time
verification with a simple C API change.

This also is not intended to serve as trapping arithmetic on
overflow.  The goal here is to enable writing the program with
explicit checks on input and compile-time annotations on computation
to gain confident that overflow won't happen in the computation.


To generate a diff of this commit:
cvs rdiff -u -r1.7 -r1.8 src/usr.bin/vndcompress/common.h
cvs rdiff -u -r1.14 -r1.15 src/usr.bin/vndcompress/offtab.c
cvs rdiff -u -r1.28 -r1.29 src/usr.bin/vndcompress/vndcompress.c
cvs rdiff -u -r1.13 -r1.14 src/usr.bin/vndcompress/vnduncompress.c

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.