| History log of /src/usr.bin/vndcompress/offtab.c |
| Revision | | Date | Author | Comments |
| 1.15 |
| 29-Jul-2017 |
riastradh | 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.
|
| 1.14 |
| 16-Apr-2017 |
riastradh | Justify the last unjustified assertion here.
Sprinkle a few more assertions to help along the way.
(Actually, it was justified; I just hadn't made explicit the relation
to the value of fdpos that all two callers specify.)
|
| 1.13 |
| 25-Jan-2014 |
riastradh | branches: 1.13.4; 1.13.8; 1.13.10; 1.13.14; 1.13.18;
Get SIZE_MAX and OFF_MAX straight...
|
| 1.12 |
| 25-Jan-2014 |
riastradh | Factor out an offtab_compute_window_position routine.
|
| 1.11 |
| 25-Jan-2014 |
riastradh | Fix some more integer overflow/truncation issues.
Arithmetic in C is hard. Let's go shopping!
|
| 1.10 |
| 23-Jan-2014 |
joerg | Mark offtab_bug[x] as dead.
|
| 1.9 |
| 22-Jan-2014 |
riastradh | Fix $NetBSD$ tag.
|
| 1.8 |
| 22-Jan-2014 |
riastradh | Simplify vndcompress offtab_compute_window_size.
|
| 1.7 |
| 22-Jan-2014 |
riastradh | Fix typo in comment.
|
| 1.6 |
| 22-Jan-2014 |
riastradh | Remove silly comment in offtab_reset_write.
|
| 1.5 |
| 22-Jan-2014 |
riastradh | Split guard in offtab_write_window into offtab_maybe_write_window.
|
| 1.4 |
| 22-Jan-2014 |
riastradh | Seek if necessary at end of offtab_reset_read.
Fixes vnduncompress with a small window, and makes offtab_reset_read
symmetric with offtab_reset_write.
|
| 1.3 |
| 22-Jan-2014 |
riastradh | Judicious (and justified) casts to avoid signed/unsigned comparisons.
|
| 1.2 |
| 22-Jan-2014 |
riastradh | Implement machinery for fixed-size windows into the offset table.
|
| 1.1 |
| 22-Jan-2014 |
riastradh | Abstract handling of the cloop2 offset table.
Preparation for converting it to use a fixed-size window.
|
| 1.13.18.1 |
| 21-Apr-2017 |
bouyer | Sync with HEAD
|
| 1.13.14.1 |
| 26-Apr-2017 |
pgoyette | Sync with HEAD
|
| 1.13.10.2 |
| 07-Dec-2014 |
martin | Pull up following revision(s) (requested by riastradh in ticket #1138):
usr.bin/vndcompress/Makefile 1.3-1.13
usr.bin/vndcompress/common.h 1.1-1.6
usr.bin/vndcompress/main.c 1.1-1.3
usr.bin/vndcompress/offtab.c 1.1-1.13
usr.bin/vndcompress/offtab.h 1.1-1.2
usr.bin/vndcompress/utils.c 1.1-1.4
usr.bin/vndcompress/utils.h 1.1-1.3
usr.bin/vndcompress/vndcompress.1 1.7-1.14
usr.bin/vndcompress/vndcompress.c 1.8-1.24
usr.bin/vndcompress/vndcompress.h delete
usr.bin/vndcompress/vnduncompress.c 1.1-1.11
Rewrite vndcompress to support SIGINFO and restart after interrupt.
Make it generally more robust in the process.
|
| 1.13.10.1 |
| 25-Jan-2014 |
martin | file offtab.c was added on branch netbsd-6 on 2014-12-07 13:57:58 +0000
|
| 1.13.8.2 |
| 20-Aug-2014 |
tls | Rebase to HEAD as of a few days ago.
|
| 1.13.8.1 |
| 25-Jan-2014 |
tls | file offtab.c was added on branch tls-maxphys on 2014-08-20 00:05:05 +0000
|
| 1.13.4.2 |
| 22-May-2014 |
yamt | sync with head.
for a reference, the tree before this commit was tagged
as yamt-pagecache-tag8.
this commit was splitted into small chunks to avoid
a limitation of cvs. ("Protocol error: too many arguments")
|
| 1.13.4.1 |
| 25-Jan-2014 |
yamt | file offtab.c was added on branch yamt-pagecache on 2014-05-22 11:42:51 +0000
|
