Libguestfs - Oct 2020 - [PATCH nbdkit] common/include/tvdiff.h: Add formal specification.

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