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.

Modified files:

Index: src/usr.bin/vndcompress/common.h
diff -u src/usr.bin/vndcompress/common.h:1.7 src/usr.bin/vndcompress/common.h:1.8
--- src/usr.bin/vndcompress/common.h:1.7	Sun Apr 16 23:43:57 2017
+++ src/usr.bin/vndcompress/common.h	Sat Jul 29 21:04:07 2017
@@ -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.
@@ -83,6 +83,16 @@
 #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:
  *
  *   0 < blocksize			(duh)

Index: src/usr.bin/vndcompress/offtab.c
diff -u src/usr.bin/vndcompress/offtab.c:1.14 src/usr.bin/vndcompress/offtab.c:1.15
--- src/usr.bin/vndcompress/offtab.c:1.14	Sun Apr 16 23:50:40 2017
+++ src/usr.bin/vndcompress/offtab.c	Sat Jul 29 21:04:07 2017
@@ -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 of
 	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, uint3
 		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,
 		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)

Index: src/usr.bin/vndcompress/vndcompress.c
diff -u src/usr.bin/vndcompress/vndcompress.c:1.28 src/usr.bin/vndcompress/vndcompress.c:1.29
--- src/usr.bin/vndcompress/vndcompress.c:1.28	Mon Apr 17 00:02:45 2017
+++ src/usr.bin/vndcompress/vndcompress.c	Sat Jul 29 21:04:07 2017
@@ -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
 		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
 
 		/* 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
 		 * (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
 			    (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 __un
 	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, con
 	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, con
 	    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 *
 	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 *
 				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, ui
 
 	/* 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);

Index: src/usr.bin/vndcompress/vnduncompress.c
diff -u src/usr.bin/vndcompress/vnduncompress.c:1.13 src/usr.bin/vndcompress/vnduncompress.c:1.14
--- src/usr.bin/vndcompress/vnduncompress.c:1.13	Mon Apr 17 00:03:33 2017
+++ src/usr.bin/vndcompress/vnduncompress.c	Sat Jul 29 21:04:07 2017
@@ -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, con
 
 	/* 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, con
 	/*
 	 * 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, con
 			    ": 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,

Reply via email to