This commit adds a formal specification of tvdiff_usec and a partial specification of subtract_timeval. These may be proved using Frama-C. The existing functions ignored overflow, but it is possible to call the functions with parameters that will cause overflow. So to create a formal specification I had to modify the functions to signal overflow. Luckily GCC and Clang have convenient __builtin*s which make this easy, but Frama-C did not know about the builtins so I had to add axioms for them. This required modifying the callers in nbdkit-rate-filter and nbdkit-stats-filter for the new signature. Neither existing call site cared about overflow so we ignore it. A regular test is added although it will be skipped unless Frama-C is available. Note this test can take a few seconds to run. Note this does not remove test-tvdiff.c. Now we have formally proven the functions to be correct there is no need to test them, but since the test exists we may as well keep it. --- common/include/Makefile.am | 8 ++- common/include/test-proof.sh | 49 ++++++++++++++ common/include/test-tvdiff.c | 4 +- common/include/tvdiff.h | 124 ++++++++++++++++++++++++++++++++--- filters/rate/bucket.c | 4 +- filters/stats/stats.c | 6 +- 6 files changed, 177 insertions(+), 18 deletions(-) diff --git a/common/include/Makefile.am b/common/include/Makefile.am index a7d0d026..0521f65b 100644 --- a/common/include/Makefile.am +++ b/common/include/Makefile.am @@ -45,13 +45,14 @@ EXTRA_DIST = \ nextnonzero.h \ random.h \ rounding.h \ + test-proof.sh \ tvdiff.h \ unix-path-max.h \ $(NULL) # Unit tests. -TESTS = \ +check_PROGRAMS = \ test-ascii-ctype \ test-ascii-string \ test-byte-swapping \ @@ -63,7 +64,10 @@ TESTS = \ test-random \ test-tvdiff \ $(NULL) -check_PROGRAMS = $(TESTS) +TESTS = \ + test-proof.sh \ + $(check_PROGRAMS) \ + $(NULL) test_ascii_ctype_SOURCES = test-ascii-ctype.c ascii-ctype.h test_ascii_ctype_CPPFLAGS = -I$(srcdir) diff --git a/common/include/test-proof.sh b/common/include/test-proof.sh new file mode 100755 index 00000000..3d9fd424 --- /dev/null +++ b/common/include/test-proof.sh @@ -0,0 +1,49 @@ +#!/usr/bin/env bash +# nbdkit +# Copyright (C) 2020 Red Hat Inc. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are +# met: +# +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# +# * Neither the name of Red Hat nor the names of its contributors may be +# used to endorse or promote products derived from this software without +# specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY RED HAT AND CONTRIBUTORS ''AS IS'' AND +# ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, +# THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +# PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL RED HAT OR +# CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF +# USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +# ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT +# OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +# SUCH DAMAGE. + +# Test formal specifications using frama-c. + +source ../../tests/functions.sh +set -e +set -x + +requires frama-c -version +requires frama-c -wp-h + +sources="tvdiff.h" + +# For how to get Frama-C to exit with an error if the proof fails, +# see: https://git.frama-c.com/pub/frama-c/-/issues/34 +frama-c -wp -wp-rte $sources \ + -cpp-extra-args="-I../.. -DFRAMA_C=1" \ + -wp-par=`nproc` \ + -then -report-classify -report-status -report-unclassified-unknown ERROR diff --git a/common/include/test-tvdiff.c b/common/include/test-tvdiff.c index abefb2e7..1bf6523b 100644 --- a/common/include/test-tvdiff.c +++ b/common/include/test-tvdiff.c @@ -46,7 +46,9 @@ #define TEST_TVDIFF(tv1, tv2, expected) \ do { \ - int64_t actual = tvdiff_usec (&(tv1), &(tv2)); \ + int64_t actual; \ + \ + tvdiff_usec (&(tv1), &(tv2), &actual); \ \ if (actual != (expected)) { \ fprintf (stderr, \ diff --git a/common/include/tvdiff.h b/common/include/tvdiff.h index cec83458..7680ae30 100644 --- a/common/include/tvdiff.h +++ b/common/include/tvdiff.h @@ -37,28 +37,134 @@ #include <config.h> +#include <stdbool.h> +#include <stdint.h> #include <sys/time.h> -/* Return the number of µs (microseconds) in y - x. */ -static inline int64_t -tvdiff_usec (const struct timeval *x, const struct timeval *y) +/*@ + predicate valid_timeval (struct timeval tv) = + tv.tv_sec >= 0 && tv.tv_usec >= 0 && tv.tv_usec < 1000000; + logic integer tv_to_microseconds (struct timeval tv) = + tv.tv_sec * 1000000 + tv.tv_usec; + */ + +#ifdef FRAMA_C + +/*@ + assigns *r; + behavior success: + assumes INT64_MIN <= a + b <= INT64_MAX; + ensures *r == a + b; + ensures \result == \false; + behavior overflow: + assumes !(INT64_MIN <= a + b <= INT64_MAX); + ensures \result == \true; + */ +extern bool __builtin_add_overflow (int64_t a, int64_t b, int64_t *r); +/*@ + assigns *r; + behavior success: + assumes INT64_MIN <= a - b <= INT64_MAX; + ensures *r == a - b; + ensures \result == \false; + behavior overflow: + assumes !(INT64_MIN <= a - b <= INT64_MAX); + ensures \result == \true; + */ +extern bool __builtin_sub_overflow (int64_t a, int64_t b, int64_t *r); +/*@ + assigns *r; + behavior success: + assumes INT64_MIN <= a * b <= INT64_MAX; + ensures *r == a * b; + ensures \result == \false; + behavior overflow: + assumes !(INT64_MIN <= a * b <= INT64_MAX); + ensures \result == \true; + */ +extern bool __builtin_mul_overflow (int64_t a, int64_t b, int64_t *r); + +#endif /* FRAMA_C */ + +/* Return the number of µs (microseconds) *r = *y - *x. + * On overflow, returns -1. + */ +/*@ + requires \valid_read (x) && \valid_read (y); + requires valid_timeval (*x) && valid_timeval (*y); + requires \valid (r); + assigns *r; + behavior success: + assumes INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x) + <= INT64_MAX; + ensures \result == 0; + ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x); + behavior failure: + assumes !(INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x) + <= INT64_MAX); + ensures \result == -1; + ensures *r == 0; + complete behaviors; + disjoint behaviors; + */ +static inline int +tvdiff_usec (const struct timeval *x, const struct timeval *y, + int64_t *r) { int64_t usec; - usec = (y->tv_sec - x->tv_sec) * 1000000; - usec += y->tv_usec - x->tv_usec; - return usec; + if (__builtin_sub_overflow (y->tv_sec, x->tv_sec, &usec)) { + overflow: + *r = 0; + return -1; + } + if (__builtin_mul_overflow (usec, 1000000, &usec)) + goto overflow; + if (__builtin_add_overflow (usec, y->tv_usec - x->tv_usec, &usec)) + goto overflow; + + *r = usec; + return 0; } -/* Return timeval difference as another struct timeval. z = y - x. */ -static inline void +/* Return timeval difference as another struct timeval z = y - x. + * On overflow, returns -1. + */ +/*@ + requires \valid_read (x) && \valid_read (y); + requires valid_timeval (*x) && valid_timeval (*y); + requires \valid (z); + assigns *z; + behavior success: + assumes INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x) + <= INT64_MAX; + ensures \result == 0; + // XXX alt-ergo 2.2.0 cannot prove this: + // ensures tv_to_microseconds (*z) == + // tv_to_microseconds (*y) - tv_to_microseconds (*x); + // note that the result is not a valid_timeval because + // z->tv_sec could be negative + behavior failure: + assumes !(INT64_MIN <= tv_to_microseconds (*y) - tv_to_microseconds (*x) + <= INT64_MAX); + ensures \result == -1; + ensures z->tv_sec == 0 && z->tv_usec == 0; + complete behaviors; + disjoint behaviors; + */ +static inline int subtract_timeval (const struct timeval *x, const struct timeval *y, struct timeval *z) { - int64_t usec = tvdiff_usec (x, y); + int64_t usec; + if (tvdiff_usec (x, y, &usec) == -1) { + z->tv_sec = z->tv_usec = 0; + return -1; + } z->tv_sec = usec / 1000000; z->tv_usec = usec % 1000000; + return 0; } #endif /* NBDKIT_TVDIFF_H */ diff --git a/filters/rate/bucket.c b/filters/rate/bucket.c index b3addac6..2accb810 100644 --- a/filters/rate/bucket.c +++ b/filters/rate/bucket.c @@ -127,9 +127,7 @@ bucket_run (struct bucket *bucket, uint64_t n, struct timespec *ts) /* Work out how much time has elapsed since we last added tokens to * the bucket, and add the correct number of tokens. */ - usec = tvdiff_usec (&bucket->tv, &now); - if (usec < 0) /* Maybe happens if system time not monotonic? */ - usec = 0; + tvdiff_usec (&bucket->tv, &now, &usec); add = bucket->rate * usec / 1000000; add = MIN (add, bucket->capacity - bucket->level); diff --git a/filters/stats/stats.c b/filters/stats/stats.c index 639ceacf..3b633cdf 100644 --- a/filters/stats/stats.c +++ b/filters/stats/stats.c @@ -164,7 +164,7 @@ stats_unload (void) int64_t usecs; gettimeofday (&now, NULL); - usecs = tvdiff_usec (&start_t, &now); + tvdiff_usec (&start_t, &now, &usecs); if (fp && usecs > 0) { ACQUIRE_LOCK_FOR_CURRENT_SCOPE (&lock); print_stats (usecs); @@ -247,10 +247,10 @@ static inline void record_stat (nbdstat *st, uint32_t count, const struct timeval *start) { struct timeval end; - uint64_t usecs; + int64_t usecs; gettimeofday (&end, NULL); - usecs = tvdiff_usec (start, &end); + tvdiff_usec (start, &end, &usecs); ACQUIRE_LOCK_FOR_CURRENT_SCOPE (&lock); st->ops++; -- 2.29.0.rc2