Reworking after run through with Paolo.

[libguestfs-talks.git] / 2020-frama-c / 5400-timeval.html

diff --git a/2020-frama-c/5400-timeval.html b/2020-frama-c/5400-timeval.html
index 296d281..c9ee443 100644 (file)
--- a/2020-frama-c/5400-timeval.html
+++ b/2020-frama-c/5400-timeval.html
@@ -4,27 +4,94 @@
 
 <h1>nbdkit tvdiff_usec</h1>
 
+<p>
+<a href="https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html">https://www.redhat.com/archives/libguestfs/2020-October/msg00085.html</a>
+</p>
+
 <pre class="code">
-  /*@
-    requires \valid_read (x) && \valid_read (y);
-    requires valid_timeval (*x) && valid_timeval (*y);
-    requires \valid (r);
-    assigns *r;
-    behavior success:
-      ensures \result == 0;
-      ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
-              INT64_MIN <= diff <= INT64_MAX &&
-              *r == diff;
-    behavior failure:
-      ensures \result == -1;
-      ensures *r == 0;
-      ensures \let diff = tv_to_microseconds (*y) - tv_to_microseconds (*x);
-              !(INT64_MIN <= diff <= INT64_MAX);
-    complete behaviors;
-    disjoint behaviors;
-   */
-  static inline int
-  tvdiff_usec (const struct timeval *x, const struct timeval *y,
-               int64_t *r)
-  ...
+/*@
+  predicate valid_timeval (struct timeval tv) =
+    tv.tv_sec &gt;= 0 &amp;&amp; tv.tv_usec &gt;= 0 &amp;&amp; tv.tv_usec &lt; 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 &lt;= a + b &lt;= INT64_MAX;
+     ensures *r == a + b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN &lt;= a + b &lt;= 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 &lt;= a - b &lt;= INT64_MAX;
+     ensures *r == a - b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN &lt;= a - b &lt;= 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 &lt;= a * b &lt;= INT64_MAX;
+     ensures *r == a * b;
+     ensures \result == \false;
+   behavior overflow:
+     assumes !(INT64_MIN &lt;= a * b &lt;= 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) &amp;&amp; \valid_read (y);
+  requires valid_timeval (*x) &amp;&amp; valid_timeval (*y);
+  requires \valid (r);
+  assigns *r;
+  behavior success:
+    assumes INT64_MIN &lt;= tv_to_microseconds (*y) - tv_to_microseconds (*x)
+                      &lt;= INT64_MAX;
+    ensures \result == 0;
+    ensures *r == tv_to_microseconds (*y) - tv_to_microseconds (*x);
+  behavior failure:
+    assumes !(INT64_MIN &lt;= tv_to_microseconds (*y) - tv_to_microseconds (*x)
+                        &lt;= 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;
+
+  if (__builtin_sub_overflow (y-&gt;tv_sec, x-&gt;tv_sec, &amp;usec)) {
+  overflow:
+    *r = 0;
+    return -1;
+  }
+  if (__builtin_mul_overflow (usec, 1000000, &amp;usec))
+    goto overflow;
+  if (__builtin_add_overflow (usec, y-&gt;tv_usec - x-&gt;tv_usec, &amp;usec))
+    goto overflow;
+
+  *r = usec;
+  return 0;
+}
 </pre>