[LLVMdev] nsw/nuw for trunc

[Florian Merz]

Hi Duncan,

Am Thursday, 11. August 2011, 15:56:22 schrieb Duncan Sands:
> Hi Florian,
> 
> > we'd like to be able to check for loss of information in trunc operations
> > in our LLVM-based bounded model checker [1]. For this it is important if
> > the trunc was on a signed or unsigned integer, so we need nsw and nuw
> > flags for this. Would you accept a patch that adds these flags to LLVM
> > (and possibly clang)?
> 
> nsw/nuw don't mean signed/unsigned arithmetic.  They mean that
> signed/unsigned overflow in the operation results in undefined behaviour. 
> As far as I know, truncating a large signed value to a too small signed
> integer type does not result in undefined behaviour.  For example, the
> result of (signed char)999 is perfectly well defined.  So it seems to me
> that nsw/nuw on truncate (which is what this cast turns into in LLVM)
> don't make any sense.  Also, a truncate operation doesn't need to be
> signed or unsigned, since the operation performed is exactly the same (the
> same set of input bits -> the same set of output bits) regardless of the
> sign of the original types.

You're perfectly right. But we'd like to check if the number represented is 
still the same after truncating, or if the value of the number changed due to 
the truncation.

For example let's consider truncating from 16bit to 8bit:

Truncating 0x0180 (384 in decimal) to 8bit results in 0x80 (128 in decimal). 
The value changed so we'd like to report this to the user of our model 
checker. This is easy to do so far, no problems there. It get's more 
complicated if we consider signed integers:

0x0080 (128 in decimal) would be truncated to 0x80. If we interpret this as an 
unsigned integer, this is still 128 in decimal and no information is lost.
But if we interpret it as signed, we turned a positive number into a negative 
number (-128), and therefore the value was not preserved. So in order to know 
if this instruction can have this kind of overflow, we need to know if the 
result of the truncation is supposed to be interpreted as signed or unsigned.

If we had nsw and nuw flags for truncations we'd know when to check for this 
kind of overflow and when not. The compiler likely doesn't need these flags and 
can still ignore them, for us they would be useful.

I hope this explanation makes our intention more clear.

Regards, 
 Florian

> Ciao, Duncan.