4 ms·

> x = y+1; return x; Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a sign

> x = y+1; return x; Funny you should use that specific example, because your analysis fails to account for the case where a) this is C or C++, b) y has a signed integer type, and c) its value is the maximum value of said type. In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds. This is exactly the sort of corner case that fuzzing is designed to reveal. Formal analysis of the function would, of course, also flag the fact that the set of values of y for which the program is well-defined is not the entire domain of its type.

skissane 6y ago
> In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.
anyfoo 6y ago
I did not fail to take that into account: > it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x) And it does not matter, since the point of formal verification is to help taking those issues into account.
- Sharlin 6y ago
  Pardon me if I'm missing something, but I only see the "natural number" case and the "unsigned" case (the latter of which is indeed well-defined to wrap around to zero in C and C++), but I was talking about the case where x and y have, say, type signed int. Then all bets are off if y happens to equal INT_MAX in some execution, because the compiler is allowed to optimize with the assumption that that literally cannot happen. At least as far as the C standard is concerned. So my point was that in the real world, even such a trivial function may not only yield unexpected results but indeed cause the whole program to have arbitrary, undefined behavior.

skissane 6y ago

> In that case the behavior is, infamously, undefined, and anything can happen including accessing memory out of bounds Undefined per the standard, yes. Undefined per a particular implementation? Well, that’s up to each particular implementation. A compiler is free to make stronger guarantees than the standard requires. And, a formal verification is allowed to presume a particular compiler, and rely on whatever stronger guarantees it makes. Which means of course that the verification is only valid as long as that compiler is used, and changing the compiler requires revisiting the verification (even if only just to confirm that the new compiler makes the same guarantees) - but, in many cases, especially the cases in which formal verification is in the most demand (safety critical systems), that’s an acceptable limitation.

anyfoo 6y ago

I did not fail to take that into account: > it will always return either y+1 (with y treated as a natural number, not a finite width integer), or 0 (if y was the maximum value in the unsigned data type of x) And it does not matter, since the point of formal verification is to help taking those issues into account.

Sharlin 6y ago
Pardon me if I'm missing something, but I only see the "natural number" case and the "unsigned" case (the latter of which is indeed well-defined to wrap around to zero in C and C++), but I was talking about the case where x and y have, say, type signed int. Then all bets are off if y happens to equal INT_MAX in some execution, because the compiler is allowed to optimize with the assumption that that literally cannot happen. At least as far as the C standard is concerned. So my point was that in the real world, even such a trivial function may not only yield unexpected results but indeed cause the whole program to have arbitrary, undefined behavior.