Re: bug#36370: 27.0.50; XFIXNAT called on negative numbers

[Pip Cet]

On Fri, Jun 28, 2019 at 5:46 PM Paul Eggert <address@hidden> wrote:
> Pip Cet wrote:
> > It's way too easy
> > to do something like
> >
> > eassume(ptr->field >= 0 && f(ptr));
> >
> > when what you mean is
> >
> > eassume(ptr->field >= 0);
> > eassume(f(ptr));
>
> These mean the same thing.

I'm really convinced they don't. Can you humor me and explain why
they're equivalent?

I'm considering this test case:
====
int global;

extern int f(void);

#define eassume0(cond) ((cond) ? (void) 0 : __builtin_unreachable ())
#ifdef ASSUME_GNULIB
#define eassume eassume0
#else
#define eassume(cond) (__builtin_constant_p (!(cond) == !(cond)) ?
eassume0(cond) : (void) 0)
#endif

int main(void)
{
#ifdef TWO_ASSUMES
  eassume (global == 0);
  eassume (f ());
#else
  eassume (global == 0 && f ());
#endif

  global++;
}
====
with this external function:
====
extern int global;

int f(void)
{
  return ++global;
}
====

I believe, and that is what my patch is based on, that the compiler
should be free to "use" the first eassume and ignore the second one,
resulting in this machine code:

    movl    $1, global(%rip)
    xorl    %eax, %eax
    ret

No call to f, it just sets global.

Without -DTWO_ASSUMES, the compiler cannot split the assumption.

> Both tell the compiler that a certain condition (A &&
> B) is known to be true, and that behavior is undefined if (A && B) is false.

Again, no. The split eassumes tell the compiler that A, B, and A && B
would all evaluate to true or fail to evaluate. The single eassume()
only covers the last of those three cases.

> The
> fact that Gnulib+GCC implements them differently is a 
> quality-of-implementation
> issue, not a semantics issue.

Are you really saying that the single-assume case is equivalent to the
single-instruction program?

> > I'm saying that the programmer is
> > allowed to assume that the expression passed to assume either has been
> > evaluated, or hasn't been, with no in-between interpretations allowed
> > to the compiler.
>
> I don't see why that assumption is valid. It's OK if GCC partially evaluates 
> the
> expression. As a silly example, eassume (0 * dump_core () + getchar ()) is not
> required to call dump_core, even if the compiler generates a call to getchar.

That's because && implies a sequence point, and * doesn't.

> Perhaps we should change the comments in verify.h to make this point clearer.

I'm sorry to be selfish, but I'd really rather understand where I've
gone wrong, first.