[Libguestfs] [PATCH nbdkit] common/include/tvdiff.h: Add formal specification.
Richard W.M. Jones
rjones at redhat.com
Sat Oct 17 15:15:28 UTC 2020
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
More information about the Libguestfs
mailing list