Signed integer overflow -- undefined behavior

[j-hui]

I found two bugs that are related to integer overflow---these will be checked into the low-regression test suite in #30 .

I shrank these down into these two programs:

MultOverflowIndirect:

entrypoint:
  fun1()

fun1() {
  *int v0 = var 999999
  int v1 = *v0
  if((0 < (v1 * v1))) {
    after 2 then v0 = 0
  } else {
  }
  *int v3 = var 0
  wait [v3]
}

And MultOverflow:

entrypoint:
  fun1()

fun1() {
  *int v0 = var 999999
  if((0 < (v0 * v0))) {
  } else {
  }
  *int v3 = var 0
  wait [v3]
}

These have the same general cause, but two different symptoms. The cause is that signed integer overflow is undefined in C, allowing it to optimize a statement like 0 < (v * v) into 1 when the value of v is known to be non-zero, allowing the conditional and the computation of its condition to be pruned out altogether. Meanwhile, the Haskell interpreter naively evaluates the computation, which overflows.

In MultOverflowIndirect, this seems to cause the interpreter to take the else branch instead. Meanwhile, in MultOverflow, where I inlined the v0 value, it crashes for some reason.

I'm not familiar enough with the interpreter to directly diagnose this issue, but I know that @Rewbert came across this exact same issue before with integer arithmetic. His solution was to wrap + in a function _add, which would spook the optimizer enough that the problem went away. But it doesn't seem like a complete solution, since it doesn't address the root cause, and an aggressive-enough optimizer would probably be able to inline _add and prune out the branch anyway.

[j-hui]

A possible solution is to "define" the behavior of integer overflow by typedefing i32 to unsigned integers in C, and then overloading the comparison operators < and > to also check against signed int max. But that's still pretty hacky and I suspect it's fragile.

Another solution is to make signed integer overflow also undefined in SSM, and reflect that in the interpreter. And this would require some modification in the trace comparator to account for what that means. But I'm not sure undefined behavior is such a great idea in a langauge spec, since it means that the compiler is allowed to be less predictable.

[Rewbert]

I didn't really know what to do here either :/ I always opt for whatever is simplest and works lol, even if its a hack. Hacks are indeed fragile though. Perhaps reflecting in the trace somehow that its undefined is best, but I am not sure how to do that best

[j-hui]

@sedwards-lab suggested I look at what other languages do.

Java silently underflows or overflows, though Java 8 also provides the {add,subtract,etc.}Exact static methods which throw an exception on over/underflow.

Haskell leaves over/underflow behavior undefined. It seems to exhibit wraparound behavior in the REPL and at least in some instances of the compiled code, but it leaves the crash encountered in MultOverflow unexplained. For the purposes of our interpreter, overflow and underflow should be checked for and handled explicitly.

LLVM uses wraparound behavior by default for both signed and unsigned arithemtic, but allows this to be disabled using the nuw and nsw flags. When those flags are present and overflow happens, the result is a poison value (somewhere in between undef and full-blown undefined behavior).

The matter of whether LLVM compiles to machine code with efficient overflow checks was studied and written about by John Regehr. This suggests to me that naively implementing the overflow checks ourselves in C is not necessarily the best solution, since the efficiency of our code will be subject to the whims of the C compiler and optimizer.

Golang explicitly specifies wraparound behavior, which precludes some compiler optimizations. In particular, one cannot assume x < x + 1 is always true.

The solution used by both Rust and Zig is to use different behavior depending on the compilation mode: for debug builds, overflows are checked and throw an exception, while for release builds, overflows go unchecked. A discussion about integer overflow in Rust can be found here.

[j-hui]

I added the not-urgent label since this is probably something we can punt, as long as we give some concrete answer we can work off of for now.

Perhaps reflecting in the trace somehow that its undefined is best, but I am not sure how to do that best

We can do this by adding an additional event condition, Undefined, such that a trace containing such an event is equivalent to any other trace. Not the most elegant solution, semantically, but it'll do for now.

[Rewbert]

When would we emit such an event? Wouldn't we need to check for the overflows in order to know when to emit it?

It's true that it's not urgebt. I'd be fine with whatever quick hacks would let us progress.

[j-hui]

When evaluating expressions, we could convert all integer values to Integer, and check that the resulting value is within range before converting back. This obviously kills performance but that's not a big deal in the interpreter, where correctness is paramount.

On Mon, Jun 28, 2021, 3:19 PM Robert Krook @.***> wrote:

When would we emit such an event? Wouldn't we need to check for the overflows in order to know when to emit it?

It's true that it's not urgebt. I'd be fine with whatever quick hacks would let us progress.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Rewbert/ssm-edsl/issues/32#issuecomment-869957359, or unsubscribe https://github.com/notifications/unsubscribe-auth/AC2A5DFEBUG67FNQ4H7TX6LTVDDNRANCNFSM47KP6G5Q .

[sedwards-lab]

@j-hui how did you verify it was the C compiler's optimization that was doing this? I could see the product of two large positive integers producing in a negative two's complement integer after overflow.

[j-hui]

I tried playing around with this with Godbolt Compiler Explorer. The simplest example can be found here: https://godbolt.org/z/8xjqhxTjW

Basically, we're compiling this:

if (0 <= x * x)
  printf("then");
else
  printf("else");

If x is 999999, squaring it will overflow, which, for 32-bit 2's complement, is a negative int. But since overflow leads to undefined behavior, the compiler can effective assume it won't ever happen for the sake of optimization, and assume that anything of the form 0 <= x * x is always true when x is a signed integer type.

With -O2, both GCC and Clang optimize out the else branch and directly evalute printf("then"). With -O0, Clang does the expected thing, and naively leaves both branches in. The odd thing is that with -O0, GCC optimizes out the else branch anyway (same as -O2). Compiler optimizations that depend on undefined behavior like this are something we definitely want to take care with.

---

@sedwards-lab , to answer your question, I put in an example that more closely resembles what is in the test case: https://godbolt.org/z/avrGcxfx3. The difference is that x is declared as a local variable and given an immediate value of 999999.

It turns out that, with -O2, both GCC and Clang take advantage of this information and do some constant folding, and prune out the "unreachable" branch. Interestingly, they make different choices: GCC chooses the then branch, which is what causes our test case to fail, while Clang chooses the else branch. Neither are wrong: they are both valid as a consequence of undefined behavior.

[Rewbert]

I initially encountered this and asked @svenssonjoel about it, but the code behaved differently on his machine (valid since it's all just undefined).

If we do implement the fix where we emit an Undefined trace item, it would be interesting to see statistics of how many cases actually fall within this category (QuickCheck has machinery for this).

[sedwards-lab]

My latest thought: determinism uber alles should be a central goal of all of our work. I'd like integer arithmetic to have completely defined behavior, including overflow. The problem here seems to be that C compilers don't have completely deterministic integer arithmetic semantics, which is very unfortunate. What I'd like to do is to somehow generate deterministic C code for this example. I don't know how

[Rewbert]

For my specific version of gcc I noticed that

int a = -some number-;
int b = -some other number-;
return a + b < 0;

would return false in the case that a + b overflows. I would expect it to return true, but gcc 'optimized' the code and essentially removed all instructions related to a + b. After playing around I noticed that if I did something like this and compiled it with -DDEFINED_INTEGER_PLUS

#ifdef DEFINED_INTEGER_PLUS

int add(int a, int b) { return a + b; }
#define ADD(a,b) add(a,b)

#else

#define ADD(a,b) (a + b)

#endif
...
...
...
int a = -some number-;
int b = -some other number-;
return ADD(a,b) < 0

gcc was no longer able to notice the overflow and optimize away the instructions. This does not seem robust and I am not sure to what extent this works. It's a quick hack.

[j-hui]

@Rewbert this really only works if we can reliably prevent gcc from inlining the add function. The only way I'm aware of doing so is to add the __attribute__ ((noinline)) annotation to prevent inlining, though that ties us to gcc and gcc-compatible compilers (it's not part of the C standard).

@sedwards-lab +1 for determinism. But would reliably crashing on overflow be a reasonable semantics? I'm interested in this (rather than mandating overflow behavior) because we can do what Rust/Zig do: add in explicit checks for debug builds which crash on overflow, while removing these checks for release builds.

If we want to reliably but efficiently implement overflow behavior, we would probably need to sidestep C. The hard way to do this would be to hard-code the assembly code for each platform, but a somewhat easier way could be to implement each arithmetic operation in LLVM IR (for which overflow is well-defined) to take advantage of LLVM's various backends, and link it in; with a linker that supports link-time optimization these could all be inlined, to avoid all the unnecessary jumps.

[j-hui]

@sedwards-lab and I discussed this issue offline, and came to the following conclusions:

• At the semantic level, we should mandate some kind of deterministic behavior, the simplest of which is to just say that both signed and unsigned integers should wraparound upon overflow. This is just simpler to convey than requiring that the program should crash for debug builds, since we don't yet have a well-defined notion of (1) "crash" or (2) "debug build".
• For the Haskell implementation, we can evaluate all arithmetic expressions using Integer (which won't overflow since these are arbitrarily sized), and then do a bound check upon returning to the fixed-size representation.
• For the C implementation, although signed integer overflow causes UB, unsigned integer overflow is well-defined to wraparound. So we can efficiently implement the wraparound behavior by representing all signed integers as uN_t, and taking care to cast to and from signed representations for the purposes of sign-sensitive operations like comparisons and division.

I need to look into what the C standard says about casting between signed and unsigned integer representations, since that is essential to our C implementation strategy being at all reliable.

[Rewbert]

Sounds like a nice plan!

[j-hui]

Closed by #78 ; remaining issue of UB overflow tracked in #84.