On Fri, Jun 28, 2019 at 5:46 PM Paul Eggert <egg...@cs.ucla.edu> 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.