5 ms·

One problem I have from a mathematical standpoint with dealing with overflow is often you may want the check to apply to an entire expression rather than indivi

One problem I have from a mathematical standpoint with dealing with overflow is often you may want the check to apply to an entire expression rather than individual operations. For instance, the expression "x + y - z" may cause an overflow when adding x and y, but may be "recovered" when subtracting z. We could change the expression to "x + (y - z)" but now we have to resign ourselves to the fact that addition is no longer associative, and requires the programmer to know which operations should be grouped together. Is there a way to do bounds checking of some sort on these expressions to ensure there is no overflow in a decidable way?

dbaupp 11y ago
Yeah, it can definitely be annoying when an expression as a whole doesn't overflow, but subexpressions do... however, chains of addition and subtraction are special in this regard, even something like (x + y) / 2 (from binary search) is problematic. Of course, chains of + and - like that do pop up, so maybe an analysis of them would be valuable. In any case, that sort of recovery is a major reason that overflow is defined to wrap when checking is off: errors may cancel out.
simcop2387 11y ago
And x + (y - z) doesn't even fix the problem. y-z can still underflow, while (x+y) - z wouldn't. Being able to do it on the expression overall would be ideal.
- openasocket 11y ago
  Yeah, I'm wondering how that would look at the assembly level. In the "x + y - z" example we get an overflow from the "x + y" and an underflow when we add z. So you'd have to check if the number of overflows and the number of underflows are equal, and the assembly would probably be really slow. You'd want some kind of bounds check optimization to try and remove as many of those checks as you can. Fortunately, I don't think these issues will appear too often (at least they haven't in my experience), and you can probably get away with just adding unit tests. To be completely thorough you should probably use some sort of formal modeling and proof system, which I would like to see someone try and develop for Rust.

dbaupp 11y ago

Yeah, it can definitely be annoying when an expression as a whole doesn't overflow, but subexpressions do... however, chains of addition and subtraction are special in this regard, even something like (x + y) / 2 (from binary search) is problematic. Of course, chains of + and - like that do pop up, so maybe an analysis of them would be valuable. In any case, that sort of recovery is a major reason that overflow is defined to wrap when checking is off: errors may cancel out.

simcop2387 11y ago

And x + (y - z) doesn't even fix the problem. y-z can still underflow, while (x+y) - z wouldn't. Being able to do it on the expression overall would be ideal.

openasocket 11y ago
Yeah, I'm wondering how that would look at the assembly level. In the "x + y - z" example we get an overflow from the "x + y" and an underflow when we add z. So you'd have to check if the number of overflows and the number of underflows are equal, and the assembly would probably be really slow. You'd want some kind of bounds check optimization to try and remove as many of those checks as you can. Fortunately, I don't think these issues will appear too often (at least they haven't in my experience), and you can probably get away with just adding unit tests. To be completely thorough you should probably use some sort of formal modeling and proof system, which I would like to see someone try and develop for Rust.