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.
This commit is contained in:
riastradh 2017-07-29 21:04:07 +00:00
parent 3dd9fc4cd5
commit 76d4b81251
4 changed files with 79 additions and 61 deletions

View File

@ -1,4 +1,4 @@
/* $NetBSD: common.h,v 1.7 2017/04/16 23:43:57 riastradh Exp $ */
/* $NetBSD: common.h,v 1.8 2017/07/29 21:04:07 riastradh Exp $ */
/*-
* Copyright (c) 2013 The NetBSD Foundation, Inc.
@ -82,6 +82,16 @@
#define CLR(t, f) ((t) &= ~(f))
#define ISSET(t, f) ((t) & (f))
/*
* Bounds checks for arithmetic.
*/
#define ADD_OK(T, A, B) ((A) <= __type_max(T) - (B))
#define MUL_OK(T, A, B) ((A) <= __type_max(T)/(B))
#define HOWMANY(X, N) (((X) + ((N) - 1))/(N))
#define TOOMANY(T, X, N, M) (!ADD_OK(T, X, (N) - 1) || HOWMANY(X, N) > (M))
/*
* We require:
*

View File

@ -1,4 +1,4 @@
/* $NetBSD: offtab.c,v 1.14 2017/04/16 23:50:40 riastradh Exp $ */
/* $NetBSD: offtab.c,v 1.15 2017/07/29 21:04:07 riastradh Exp $ */
/*-
* Copyright (c) 2014 The NetBSD Foundation, Inc.
@ -30,7 +30,7 @@
*/
#include <sys/cdefs.h>
__RCSID("$NetBSD: offtab.c,v 1.14 2017/04/16 23:50:40 riastradh Exp $");
__RCSID("$NetBSD: offtab.c,v 1.15 2017/07/29 21:04:07 riastradh Exp $");
#include <sys/types.h>
#include <sys/endian.h>
@ -95,18 +95,18 @@ offtab_compute_window_position(struct offtab *offtab, uint32_t window_start,
const uint32_t window_size = offtab_compute_window_size(offtab,
window_start);
__CTASSERT(MAX_WINDOW_SIZE <= (SIZE_MAX / sizeof(uint64_t)));
__CTASSERT(MUL_OK(size_t, MAX_WINDOW_SIZE, sizeof(uint64_t)));
*bytes = (window_size * sizeof(uint64_t));
assert(window_start <= offtab->ot_n_offsets);
__CTASSERT(MAX_N_OFFSETS <= (OFF_MAX / sizeof(uint64_t)));
__CTASSERT(MUL_OK(off_t, MAX_N_OFFSETS, sizeof(uint64_t)));
const off_t window_offset = ((off_t)window_start *
(off_t)sizeof(uint64_t));
assert(offtab->ot_fdpos <= OFFTAB_MAX_FDPOS);
__CTASSERT(OFFTAB_MAX_FDPOS <=
(OFF_MAX - (off_t)MAX_N_OFFSETS*sizeof(uint64_t)));
assert(offtab->ot_fdpos <= (OFF_MAX - window_offset));
__CTASSERT(ADD_OK(off_t, OFFTAB_MAX_FDPOS,
(off_t)MAX_N_OFFSETS*sizeof(uint64_t)));
assert(ADD_OK(off_t, offtab->ot_fdpos, window_offset));
*pos = (offtab->ot_fdpos + window_offset);
}
@ -220,7 +220,7 @@ offtab_init(struct offtab *offtab, uint32_t n_offsets, uint32_t window_size,
offtab->ot_window_size = window_size;
assert(offtab->ot_window_size <= offtab->ot_n_offsets);
offtab->ot_window_start = (uint32_t)-1;
__CTASSERT(MAX_WINDOW_SIZE <= (SIZE_MAX / sizeof(uint64_t)));
__CTASSERT(MUL_OK(size_t, MAX_WINDOW_SIZE, sizeof(uint64_t)));
offtab->ot_window = malloc(offtab->ot_window_size * sizeof(uint64_t));
if (offtab->ot_window == NULL)
err(1, "malloc offset table");
@ -293,13 +293,13 @@ offtab_reset_read(struct offtab *offtab,
return false;
if (offtab->ot_window_size < offtab->ot_n_offsets) {
__CTASSERT(MAX_N_OFFSETS <= (OFF_MAX / sizeof(uint64_t)));
__CTASSERT(MUL_OK(off_t, MAX_N_OFFSETS, sizeof(uint64_t)));
const off_t offtab_bytes = ((off_t)offtab->ot_n_offsets *
(off_t)sizeof(uint64_t));
assert(offtab->ot_fdpos <= OFFTAB_MAX_FDPOS);
__CTASSERT(OFFTAB_MAX_FDPOS <=
(OFF_MAX - (off_t)MAX_N_OFFSETS*sizeof(uint64_t)));
assert(offtab->ot_fdpos <= (OFF_MAX - offtab_bytes));
__CTASSERT(ADD_OK(off_t, OFFTAB_MAX_FDPOS,
(off_t)MAX_N_OFFSETS*sizeof(uint64_t)));
assert(ADD_OK(off_t, offtab->ot_fdpos, offtab_bytes));
const off_t first_offset = (offtab->ot_fdpos + offtab_bytes);
if (lseek(offtab->ot_fd, first_offset, SEEK_SET) == -1) {
(*offtab->ot_report)("lseek to first offset 0x%"PRIx64,
@ -387,21 +387,21 @@ offtab_reset_write(struct offtab *offtab)
}
/* Compute the number of bytes in the offset table. */
__CTASSERT(MAX_N_OFFSETS <= OFF_MAX/sizeof(uint64_t));
__CTASSERT(MUL_OK(off_t, MAX_N_OFFSETS, sizeof(uint64_t)));
const off_t offtab_bytes = ((off_t)offtab->ot_n_offsets *
sizeof(uint64_t));
/* Compute the offset of the first block. */
assert(offtab->ot_fdpos <= OFFTAB_MAX_FDPOS);
__CTASSERT(OFFTAB_MAX_FDPOS <=
(OFF_MAX - (off_t)MAX_N_OFFSETS*sizeof(uint64_t)));
assert(offtab->ot_fdpos <= (OFF_MAX - offtab_bytes));
__CTASSERT(ADD_OK(off_t, OFFTAB_MAX_FDPOS,
MAX_N_OFFSETS*sizeof(uint64_t)));
assert(ADD_OK(off_t, offtab->ot_fdpos, offtab_bytes));
const off_t first_offset = (offtab->ot_fdpos + offtab_bytes);
/* Assert that it fits in 64 bits. */
__CTASSERT(MAX_N_OFFSETS <= UINT64_MAX/sizeof(uint64_t));
__CTASSERT(OFFTAB_MAX_FDPOS <=
(UINT64_MAX - (uint64_t)MAX_N_OFFSETS*sizeof(uint64_t)));
__CTASSERT(MUL_OK(uint64_t, MAX_N_OFFSETS, sizeof(uint64_t)));
__CTASSERT(ADD_OK(uint64_t, OFFTAB_MAX_FDPOS,
(uint64_t)MAX_N_OFFSETS*sizeof(uint64_t)));
/* Write out the first window with the first offset. */
offtab->ot_window_start = 0;
@ -439,10 +439,12 @@ offtab_checkpoint(struct offtab *offtab, uint32_t n_offsets, int flags)
offtab_maybe_write_window(offtab, 0, n_offsets);
if (ISSET(flags, OFFTAB_CHECKPOINT_SYNC)) {
__CTASSERT(MAX_N_OFFSETS <= (OFF_MAX / sizeof(uint64_t)));
__CTASSERT(MUL_OK(off_t, MAX_N_OFFSETS, sizeof(uint64_t)));
const off_t sync_bytes = ((off_t)n_offsets *
(off_t)sizeof(uint64_t));
assert(offtab->ot_fdpos <= (OFF_MAX - sync_bytes));
__CTASSERT(ADD_OK(off_t, OFFTAB_MAX_FDPOS,
MAX_N_OFFSETS*sizeof(uint64_t)));
assert(ADD_OK(off_t, offtab->ot_fdpos, sync_bytes));
if (fsync_range(offtab->ot_fd, (FFILESYNC | FDISKSYNC),
offtab->ot_fdpos, (offtab->ot_fdpos + sync_bytes))
== -1)

View File

@ -1,4 +1,4 @@
/* $NetBSD: vndcompress.c,v 1.28 2017/04/17 00:02:45 riastradh Exp $ */
/* $NetBSD: vndcompress.c,v 1.29 2017/07/29 21:04:07 riastradh Exp $ */
/*-
* Copyright (c) 2013 The NetBSD Foundation, Inc.
@ -30,7 +30,7 @@
*/
#include <sys/cdefs.h>
__RCSID("$NetBSD: vndcompress.c,v 1.28 2017/04/17 00:02:45 riastradh Exp $");
__RCSID("$NetBSD: vndcompress.c,v 1.29 2017/07/29 21:04:07 riastradh Exp $");
#include <sys/endian.h>
#include <sys/stat.h>
@ -148,7 +148,7 @@ vndcompress(int argc, char **argv, const struct options *O)
err(1, "malloc uncompressed buffer");
/* XXX compression ratio bound */
__CTASSERT(MAX_BLOCKSIZE <= (SIZE_MAX / 2));
__CTASSERT(MUL_OK(size_t, 2, MAX_BLOCKSIZE));
void *const compbuf = malloc(2 * (size_t)S->blocksize);
if (compbuf == NULL)
err(1, "malloc compressed buffer");
@ -178,10 +178,11 @@ vndcompress(int argc, char **argv, const struct options *O)
/* Fail noisily if we might be about to overflow. */
/* XXX compression ratio bound */
__CTASSERT(MAX_BLOCKSIZE <= (UINTMAX_MAX / 2));
__CTASSERT(MUL_OK(uint64_t, 2, MAX_BLOCKSIZE));
__CTASSERT(MUL_OK(off_t, 2, MAX_BLOCKSIZE));
assert(S->offset <= MIN(UINT64_MAX, OFF_MAX));
if ((2 * (uintmax_t)readsize) >
(MIN(UINT64_MAX, OFF_MAX) - S->offset))
if (!ADD_OK(uint64_t, S->offset, 2*(uintmax_t)readsize) ||
!ADD_OK(off_t, S->offset, 2*(uintmax_t)readsize))
errx(1, "blkno %"PRIu32" may overflow: %ju + 2*%ju",
S->blkno, (uintmax_t)S->offset,
(uintmax_t)readsize);
@ -197,8 +198,9 @@ vndcompress(int argc, char **argv, const struct options *O)
* (b) how far we are now in the output file, and
* (c) where the last block ended.
*/
assert(S->blkno <= (UINT32_MAX - 1));
assert(complen <= (MIN(UINT64_MAX, OFF_MAX) - S->offset));
assert(ADD_OK(uint32_t, S->blkno, 1));
assert(ADD_OK(uint64_t, S->offset, complen));
assert(ADD_OK(off_t, (off_t)S->offset, (off_t)complen));
assert((S->blkno + 1) < S->n_offsets);
{
sigset_t old_sigmask;
@ -231,7 +233,8 @@ vndcompress(int argc, char **argv, const struct options *O)
(size_t)n_written, n_padding);
/* Account for the extra bytes in the output file. */
assert(n_padding <= (MIN(UINT64_MAX, OFF_MAX) - S->offset));
assert(ADD_OK(uint64_t, S->offset, n_padding));
assert(ADD_OK(off_t, (off_t)S->offset, (off_t)n_padding));
{
sigset_t old_sigmask;
block_signals(&old_sigmask);
@ -304,14 +307,13 @@ info_signal_handler(int signo __unused)
/* Carefully calculate our I/O position. */
assert(S->blocksize > 0);
__CTASSERT(MAX_N_BLOCKS <= (UINT64_MAX / MAX_BLOCKSIZE));
__CTASSERT(MUL_OK(uint64_t, MAX_N_BLOCKS, MAX_BLOCKSIZE));
const uint64_t nread = ((uint64_t)S->blkno * (uint64_t)S->blocksize);
assert(S->n_blocks > 0);
__CTASSERT(CLOOP2_OFFSET_TABLE_OFFSET <=
(UINT64_MAX / sizeof(uint64_t)));
__CTASSERT(MAX_N_BLOCKS <= ((UINT64_MAX / sizeof(uint64_t)) -
CLOOP2_OFFSET_TABLE_OFFSET));
__CTASSERT(MUL_OK(uint64_t, MAX_N_BLOCKS, sizeof(uint64_t)));
__CTASSERT(ADD_OK(uint64_t, CLOOP2_OFFSET_TABLE_OFFSET,
MAX_N_BLOCKS*sizeof(uint64_t)));
const uint64_t nwritten = (S->offset <= (CLOOP2_OFFSET_TABLE_OFFSET +
((uint64_t)S->n_blocks * sizeof(uint64_t)))?
0 : S->offset);
@ -324,7 +326,9 @@ info_signal_handler(int signo __unused)
: 0);
/* Format the status. */
assert(S->n_checkpointed_blocks <= (UINT64_MAX / S->blocksize));
assert(S->n_checkpointed_blocks <= MAX_N_BLOCKS);
assert(S->blocksize <= MAX_BLOCKSIZE);
__CTASSERT(MUL_OK(uint64_t, MAX_N_BLOCKS, MAX_BLOCKSIZE));
const int n = snprintf_ss(buf, sizeof(buf),
"vndcompress: read %"PRIu64" bytes, wrote %"PRIu64" bytes, "
"compression ratio %"PRIu64"%% (checkpointed %"PRIu64" bytes)\n",
@ -360,8 +364,9 @@ checkpoint_signal_handler(int signo __unused)
assert(S->cloop2_fd >= 0);
/* Take a checkpoint. */
assert(S->blocksize > 0);
assert(S->blkno <= (UINT64_MAX / S->blocksize));
assert(S->blkno <= MAX_N_BLOCKS);
assert(S->blocksize <= MAX_BLOCKSIZE);
__CTASSERT(MUL_OK(uint64_t, MAX_N_BLOCKS, MAX_BLOCKSIZE));
warnx_ss("checkpointing %"PRIu64" bytes",
((uint64_t)S->blkno * (uint64_t)S->blocksize));
compress_checkpoint(S);
@ -465,15 +470,16 @@ compress_init(int argc, char **argv, const struct options *O,
assert(S->size <= OFF_MAX);
/* Find number of full blocks and whether there's a partial block. */
S->n_full_blocks = (S->size / S->blocksize);
assert(S->n_full_blocks <=
(UINT32_MAX - ((S->size % S->blocksize) > 0)));
S->n_blocks = (S->n_full_blocks + ((S->size % S->blocksize) > 0));
assert(S->n_full_blocks <= S->n_blocks);
if (S->n_blocks > MAX_N_BLOCKS)
__CTASSERT(0 < MIN_BLOCKSIZE);
assert(0 < S->blocksize);
if (TOOMANY(off_t, (off_t)S->size, (off_t)S->blocksize,
(off_t)MAX_N_BLOCKS))
errx(1, "image too large for block size %"PRIu32": %"PRIu64,
S->blocksize, S->size);
__CTASSERT(MAX_N_BLOCKS <= UINT32_MAX);
S->n_full_blocks = S->size/S->blocksize;
S->n_blocks = HOWMANY(S->size, S->blocksize);
assert(S->n_full_blocks <= S->n_blocks);
assert(S->n_blocks <= MAX_N_BLOCKS);
/* Choose a window size. */
@ -481,10 +487,10 @@ compress_init(int argc, char **argv, const struct options *O,
DEF_WINDOW_SIZE);
/* Create an offset table for the blocks; one extra for the end. */
__CTASSERT(MAX_N_BLOCKS <= (UINT32_MAX - 1));
__CTASSERT(ADD_OK(uint32_t, MAX_N_BLOCKS, 1));
S->n_offsets = (S->n_blocks + 1);
__CTASSERT(MAX_N_OFFSETS == (MAX_N_BLOCKS + 1));
__CTASSERT(MAX_N_OFFSETS <= (SIZE_MAX / sizeof(uint64_t)));
__CTASSERT(MUL_OK(size_t, MAX_N_OFFSETS, sizeof(uint64_t)));
__CTASSERT(CLOOP2_OFFSET_TABLE_OFFSET <= OFFTAB_MAX_FDPOS);
offtab_init(&S->offtab, S->n_offsets, window_size, S->cloop2_fd,
CLOOP2_OFFSET_TABLE_OFFSET);
@ -607,10 +613,10 @@ compress_restart(struct compress_state *S)
if (!offtab_prepare_get(&S->offtab, 0))
return false;
const uint64_t first_offset = offtab_get(&S->offtab, 0);
__CTASSERT(MAX_N_OFFSETS <= UINT64_MAX/sizeof(uint64_t));
__CTASSERT(sizeof(struct cloop2_header) <=
(UINT64_MAX - MAX_N_OFFSETS*sizeof(uint64_t)));
const uint64_t expected = sizeof(struct cloop2_header) +
__CTASSERT(MUL_OK(uint64_t, MAX_N_OFFSETS, sizeof(uint64_t)));
__CTASSERT(ADD_OK(uint64_t, sizeof(struct cloop2_header),
MAX_N_OFFSETS*sizeof(uint64_t)));
const uint64_t expected = sizeof(struct cloop2_header) +
((uint64_t)S->n_offsets * sizeof(uint64_t));
if (first_offset != expected) {
warnx("first offset is not 0x%"PRIx64": 0x%"PRIx64,
@ -638,7 +644,7 @@ compress_restart(struct compress_state *S)
return false;
}
/* XXX compression ratio bound */
__CTASSERT(MAX_BLOCKSIZE <= (SIZE_MAX / 2));
__CTASSERT(MUL_OK(size_t, 2, MAX_BLOCKSIZE));
if ((2 * (size_t)S->blocksize) <= (end - start)) {
warnx("block %"PRIu32" too large:"
" %"PRIu64" bytes"
@ -771,7 +777,7 @@ compress_block(int in_fd, int out_fd, uint32_t blkno, uint32_t blocksize,
/* Compress the block. */
/* XXX compression ratio bound */
__CTASSERT(MAX_BLOCKSIZE <= (ULONG_MAX / 2));
__CTASSERT(MUL_OK(unsigned long, 2, MAX_BLOCKSIZE));
const unsigned long uncomplen =
(VNDCOMPRESS_COMPAT? blocksize : readsize); /* XXX */
unsigned long complen = (uncomplen * 2);

View File

@ -1,4 +1,4 @@
/* $NetBSD: vnduncompress.c,v 1.13 2017/04/17 00:03:33 riastradh Exp $ */
/* $NetBSD: vnduncompress.c,v 1.14 2017/07/29 21:04:07 riastradh Exp $ */
/*-
* Copyright (c) 2013 The NetBSD Foundation, Inc.
@ -30,7 +30,7 @@
*/
#include <sys/cdefs.h>
__RCSID("$NetBSD: vnduncompress.c,v 1.13 2017/04/17 00:03:33 riastradh Exp $");
__RCSID("$NetBSD: vnduncompress.c,v 1.14 2017/07/29 21:04:07 riastradh Exp $");
#include <sys/endian.h>
@ -141,7 +141,7 @@ vnduncompress(int argc, char **argv, const struct options *O __unused)
/* Allocate compression buffers. */
/* XXX compression ratio bound */
__CTASSERT(MAX_BLOCKSIZE <= (SIZE_MAX / 2));
__CTASSERT(MUL_OK(size_t, 2, MAX_BLOCKSIZE));
void *const compbuf = malloc(2 * (size_t)blocksize);
if (compbuf == NULL)
err(1, "malloc compressed buffer");
@ -154,9 +154,9 @@ vnduncompress(int argc, char **argv, const struct options *O __unused)
/*
* Uncompress the blocks.
*/
__CTASSERT(MAX_N_OFFSETS <= (OFF_MAX / sizeof(uint64_t)));
__CTASSERT(sizeof(header) <=
(OFF_MAX - (MAX_N_OFFSETS * sizeof(uint64_t))));
__CTASSERT(MUL_OK(off_t, MAX_N_OFFSETS, sizeof(uint64_t)));
__CTASSERT(ADD_OK(off_t, sizeof(header),
(MAX_N_OFFSETS * sizeof(uint64_t))));
__CTASSERT(OFF_MAX <= UINT64_MAX);
uint64_t offset = (sizeof(header) +
((uint64_t)n_offsets * sizeof(uint64_t)));
@ -175,7 +175,7 @@ vnduncompress(int argc, char **argv, const struct options *O __unused)
": 0x%"PRIx64,
blkno, start);
/* XXX compression ratio bound */
__CTASSERT(MAX_BLOCKSIZE <= (SIZE_MAX / 2));
__CTASSERT(MUL_OK(size_t, 2, MAX_BLOCKSIZE));
if ((2 * (size_t)blocksize) <= (end - start))
errx(1, "block %"PRIu32" too large"
": %"PRIu64" bytes from 0x%"PRIx64" to 0x%"PRIx64,