Re: [PATCH] verify: new macro 'assume'

[Pádraig Brady]

This looks very useful thanks.
Comments below.

On 10/03/2013 06:30 AM, Paul Eggert wrote:
> 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 \

Minor point. Would it be more general to use !defined NDEBUG,
since this is a runtime operation very similar to assert()
and that honors NDEBUG.  Also, I don't suppose assert() is a more
portable equivalent of this block?

> +       && (__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)))

As a matter of interest what warnings are printed here.
Are those warnings dependent on optimization levels?

> +#endif
> +
>  /* @assert.h omit end@  */
>  
>  #endif
> 

thanks!
Pádraig.