Hi everyone, 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)? Regards, Florian [1] http://baldur.iti.uka.de/llbmc/
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. Ciao, Duncan.
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.
On Aug 11, 2011, at 5:17 AM, Florian Merz wrote:> Hi everyone, > > 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)?In contrast to the other folks, I think that this makes perfect sense, and NSW/NUW are the right thing to use. It would be valid for instcombine to delete "sext(trunc_nsw x)" when the source and dest types are the same, similarly "zext(trunc_nuw x)". The semantics are very similar to the left shift operator and many others. -Chris
On Aug 11, 2011, at 11:03 AM, Chris Lattner wrote:> > On Aug 11, 2011, at 5:17 AM, Florian Merz wrote: > >> Hi everyone, >> >> 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)? > > In contrast to the other folks, I think that this makes perfect sense, and NSW/NUW are the right thing to use.I agree that there's some abstract consistency in providing nsw/nuw for trunc, even if no current frontends would ever emit it, but I do not get the impression that Florian actually wants the optimizer making random transformations based on the assumed undefined behavior of these truncations. John.
Tobias Grosser
2011-Sep-30 14:59 UTC
[LLVMdev] Definition of C/C++ integral conversion(was Re: nsw/nuw for trunc)
On 08/11/2011 02:56 PM, Duncan Sands wrote:> 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.Hi Duncan, sorry for digging out such an old thread. You stated that '(signed char) 999' is perfectly well defined in C/C++. I just looked into the C++ standard [1] and could not find this. The section that seems to apply is: ---------------------------------------------------- 4.7 Integral conversions 1) An rvalue of an integer type can be converted to an rvalue of another integer type. An rvalue of an enumeration type can be converted to an rvalue of an integer type. 2) If the destination type is unsigned, the resulting value is the least unsigned integer congruent to the source integer [..] 3) If the destination type is signed, the value is unchanged if it can be represented in the destination type (and bit-field width); otherwise, the value is implementation-defined. ---------------------------------------------------- 4.7.3 suggest to me, that the standard does not define a result for '(signed char) 999'. I assume you know this section, but I could not find a reason why this section should not apply in this case. Any ideas? I just came across this looking at the following code: float foo(float *A, long element) { int converted = element; return A[converted]; } which is lowered to define float @foo(float* %A, i64 %element) nounwind uwtable { entry: %conv = trunc i64 %element to i32 %idxprom = sext i32 %conv to i64 %arrayidx = getelementptr inbounds float* %A, i64 %idxprom %value = load float* %arrayidx ret float %value } LLVM cannot optimize away the trunc operations, which does not only result in slower code, but also in SCEV being overly complex (which blocks further optimizations). Using integer types for index expression, is a pretty common pattern, and it would be great if we could optimize this. Thanks Tobi [1] http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2005/n1905.pdf