4 ms·
Add(x,y): Assert( x >= 0 && y>= 0 ) z = x + y Assert( z >= x && z >= y ) return z There’s definitely smarter ways to do this, bu
by appellations 1y ago
Add(x,y):
Assert( x >= 0 && y>= 0 )
z = x + y
Assert( z >= x && z >= y )
return z
There’s definitely smarter ways to do this, but in practice there is always some way to encode the properties you care about in ways that your assertions will be violated. If you can’t observe a violation, it’s not a violation https://en.wikipedia.org/wiki/Identity_of_indiscernibles https://en.wikipedia.org/wiki/Identity_of_indiscernibles
- deleted 1y ago[deleted]
- bluGill 1y agoIn some languages overflow is asserted as a can't happen and so the optimizer will remove your checks
- appellations 1y agoCare to share a language where the compiler infers the semantic meaning of asserts and optimizes them away? I’ve never heard of this optimization.
- MindSpunk 1y agoSigned overflow is UB in C/C++ and several compilers will skip explicit overflow checks as a result. See: https://godbolt.org/z/WehcWj3G5 https://godbolt.org/z/WehcWj3G5
- mrkeen 1y agoC. This is a great thread: https://mastodon.social/@regehr/113821964763012870 https://mastodon.social/@regehr/113821964763012870 (That was one of my texts at uni)
- Maxatar 1y agoC and C++
- appellations 1y agoBest I can tell is that overflow is undefined behavior for signed ints in C/C++ so -O3 with gcc might remove a check that could only be true if UB occurred. The compound predicate in my example above coupled with the fact that the compiler doesn’t reason about the precondition in the prior assert (y is non-negative) means this specific example wouldn’t be optimized away, but bluGill does have a point. An example of an assert that might be optimized away: int addFive(int x) { int y = x + 5; assert(y >= x); return y; }
- comex 1y agoClang is a bit smarter than GCC here (for some definition of 'smart') and does optimize the original version: https://gcc.godbolt.org/z/3Y4aheG6x https://gcc.godbolt.org/z/3Y4aheG6x
- uecker 1y agoYes, you can not meaningfully assert anything after UB in C/C++. But you can let the compiler add the trap for overflow -fsanitize=signed-integer-overflow -sanitize-trap=all, or you could also write your assertion in a way where it does not rely on the result (e.g. ckd_add), or you use "volatile" to write in a way the compiler is not allowed to assume anything.