[PATCH] verify: new macro 'assume'

[Paul Eggert]

This is taken from Emacs, and should be generally useful.
* doc/verify.texi (assume): Document it.
* lib/verify.h (assume): New macro.
(__has_builtin): Expand to 0 if not defined.
---
 ChangeLog       |  8 ++++++++
 doc/verify.texi | 37 +++++++++++++++++++++++++++++++------
 lib/verify.h    | 24 ++++++++++++++++++++++++
 3 files changed, 63 insertions(+), 6 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 5934344..9eb2479 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2013-10-02  Paul Eggert  <address@hidden>
+
+       verify: new macro 'assume'
+       This is taken from Emacs, and should be generally useful.
+       * doc/verify.texi (assume): Document it.
+       * lib/verify.h (assume): New macro.
+       (__has_builtin): Expand to 0 if not defined.
+
 2013-09-26  Eric Blake  <address@hidden>
 
        dup2, dup3: work around another cygwin crasher
diff --git a/doc/verify.texi b/doc/verify.texi
index df721d9..41b3df4 100644
--- a/doc/verify.texi
+++ b/doc/verify.texi
@@ -16,17 +16,19 @@
 @findex verify
 @findex verify_expr
 
-The @samp{verify} module supports compile-time tests, as opposed to
-the standard @code{assert} macro which supports only runtime tests.
-Since the tests occur at compile-time, they are more reliable, and
-they require no runtime overhead.
+This module provides a header file @file{verify.h} that defines
+macros related to compile-time verification.
 
-This module provides a header file @file{verify.h} that defines two
-macros: @code{verify (@var{V})} and @code{verify_expr
+Two of these macros are @code{verify (@var{V})} and @code{verify_expr
 (@var{V}, @var{EXPR})}.  Both accept an integer constant expression
 argument @var{V} and verify that it is nonzero.  If not, a compile-time error
 results.
 
+These two macros implement compile-time tests, as opposed to
+the standard @code{assert} macro which supports only runtime tests.
+Since the tests occur at compile-time, they are more reliable, and
+they require no runtime overhead.
+
 @code{verify (@var{V});} is a declaration; it can occur outside of
 functions.  In contrast, @code{verify_expr (@var{V}, @var{EXPR})} is
 an expression that returns the value of @var{EXPR}; it can be used in
@@ -60,6 +62,15 @@ within a @code{struct} or @code{union} specifier, in place 
of an
 ordinary member declaration.  Second, they require the programmer to
 specify a compile-time diagnostic as a string literal.
 
+The @file{verify.h} header defines one more macro, @code{assume
+(@var{E})}.  This macro expands to an expression of type @code{void}
+that causes the compiler to assume that the expression @var{E} yields
+a nonzero value.  @var{E} should be of a scalar type, and should not
+have side effects; it may or may not be evaluated.  The behavior is
+undefined if @var{E} would yield zero.  The main use of @code{assume}
+is optimization, as the compiler may be able to generate better code
+if it knows that @var{E} is true.
+
 Here are some example uses of @code{verify} and @code{verify_expr}.
 
 @example
@@ -87,4 +98,18 @@ verify (~ (time_t) -1 == 0);
    even when T is narrower than unsigned int.  */
 #define MAX_UNSIGNED_VAL(t) \
    ((T) verify_expr (0 < (T) -1, -1))
+
+/* Return T divided by UCHAR_MAX + 1.  Behavior is undefined
+   if T is negative, and in the typical case where UCHAR_MAX
+   is 255 the compiler can therefore implement the division
+   by shifting T right 8 bits, an optimization that would
+   not be valid if T were negative.  */
+time_t
+time_index (time_t t)
address@hidden
+  assume (0 <= t);
+  return t / (UCHAR_MAX + 1);
address@hidden
+
+
 @end example
diff --git a/lib/verify.h b/lib/verify.h
index d42d075..bf40b02 100644
--- a/lib/verify.h
+++ b/lib/verify.h
@@ -250,6 +250,30 @@ template <int w>
 
 #define verify(R) _GL_VERIFY (R, "verify (" #R ")")
 
+#ifndef __has_builtin
+# define __has_builtin(x) 0
+#endif
+
+/* Assume that R always holds.  This lets the compiler optimize
+   accordingly.  R should not have side-effects; it may or may not be
+   evaluated.  Behavior is undefined if R is false.  */
+
+#if (__has_builtin (__builtin_unreachable) \
+     || 4 < __GNUC__ + (5 <= __GNUC_MINOR__))
+# define assume(R) ((R) ? (void) 0 : __builtin_unreachable ())
+#elif 1200 <= _MSC_VER
+# define assume(R) __assume (R)
+#elif (defined lint \
+       && (__has_builtin (__builtin_trap) \
+           || 3 < __GNUC__ + (3 < __GNUC_MINOR__ + (4 <= 
__GNUC_PATCHLEVEL__))))
+  /* Doing it this way helps various packages when configured with
+     --enable-gcc-warnings, which compiles with -Dlint.  It's nicer
+     when 'assume' silences warnings even with older GCCs.  */
+# define assume(R) ((R) ? (void) 0 : __builtin_trap ())
+#else
+# define assume(R) ((void) (0 && (R)))
+#endif
+
 /* @assert.h omit end@  */
 
 #endif
-- 
1.8.3.1