I do not have any solution I am 100% happy with to the overflow dilemma in the previous post. Here is one of the solutions that does not make me 100% happy.
The first (partial) solution is: program so that overflows correspond exactly to unwanted circumstances (and then it becomes meaningful to verify the absence of overflows. There are great automatic tools for that. Have you heard of them?)
“Program so that…” sounds abstract, but it may be as simple as using larger integer types that won't overflow for all intermediate computations:
s = (int)((long long) u1 - (long long)u2);
Then the desired property (variable
s contains the mathematical difference of
u2) entirely rests on the final conversion from
long long to
This solution doesn't apply in the common situation where the code is already written and gratuitous changes to it are prohibited. Also, you need to have an integer type large enough to contain all intermediate computations without overflows. In this example,
unsigned int is 32-bit and
long long is 64-bit, but the standard does not prevent
unsigned int to be 64-bit and the same size as
long long, in which case the conversion from
unsigned int to
long long could overflow. Rte would only insert additional assertions for the two intermediate conversions that we have added in the assignment. This wouldn't help; it would only make things worse.
“Won't the generated code be less efficient?”, you rightly ask. That all depends on the compiler. Optimizing compilers have no trouble at all optimizing the above assignment so that it uses only one 32-bit subtraction. On the Linux workstation on which I tried this, both
clang -m32 -O0 and
gcc -m32 -O0 did. It is amusing, because the code generated by both compilers with
-O0 is ugly (gratuitously moving registers to memory and then to registers again) but, even with optimizations disabled, they still both get the fact that it is only necessary to compute the least significant 32 bits of the result.
With optimizations, both Clang and GCC generate clean code that naturally still uses a single 32-bit subtraction:
$ gcc -S -O2 -m32 t.c $ cat t.s ... f: pushl %ebp movl %esp, %ebp movl 8(%ebp), %eax subl 12(%ebp), %eax popl %ebp ret
As an anecdote, when generating x86-64 code (and therefore having 64-bit subtraction available as a single instruction, with only the drawback of a slightly larger encoding),
gcc -O0keeps using 32-bit subtraction but
clang -O0uses 64-bit subtraction. This does not reveal anything about the compilers: it does not make sense to compare for efficiency the code they generate with optimization disabled.
That's all for this post.