Dynamic detection of signed integer overflow

Hello,

I thought about doing a dynamic detection of signed integer overflow for OpenCL kernels based on the generated LLVM IR.

A problem seems to be that the LLVM IR does not differentiate between signed and unsigned types in general. But for instance for additions it should be possible to use the "nsw" flag as indicator that the operations involves signed types. Is this a legal assumption so far?
The next problem I discovered is that the "nsw" flag is not generated for additions involving vector types (http://lists.llvm.org/pipermail/cfe-dev/2011-May/014908.html).

Is there any other method how I could get information only from the LLVM IR about whether signed types are involved in arithmetic operations? Or do you know any other project with the same or a similar goal of dynamic detection of signed integer overflow (for OpenCL)?

Regards,

Moritz

Hello Moritz,

What kind of dynamic detection are you planning to do? Do you want to
check each computation or build some kind of conditions statically that
imply overflows? In the latter case this might be interesting for you:

There is currently a patch pending [1] that will allow Polly [2] to
statically determine conditions under which a signed overflow will (not)
happen. However, by default it will only check expressions that
influence control or memory access functions in regions that are
analyzed by Polly.

We also used Polly to model OpenCL kernels recently and could provide
you with patches that allow (a lot but not all) kernels to be described
to a certain degree (the rest is overapproximated).

If any of this sounds interesting, you can also contact me directly.

Cheers,
  Johannes

[1] http://reviews.llvm.org/D11977
[2] http://polly.llvm.org/

P.S.
  I added some colleges to the CC that participated in the projects
  described above.

Hello Johannes,

Currently I have planned to check each computation during a simulation of the kernel based on the LLVM IR. But for the future Polly might also be interesting. I will have a closer look and may get back to you when I have questions.

Thanks,
Moritz

Moritz,

While implementing the dynamic integer overflow checks that eventually lead to UBSan, we did two implementations: one based on generated IR and the other inside Clang. The latter approach was better and is the one that stuck.

John

Thanks John, seems like a dynamic runtime instrumentation is then not a good idea. I had a look at the UBSan features in Clang and I might be able to use them instead. But it seems like that vector operations are not instrumented with overflow checks if I specify the option -fsanitize=signed-integer-overflow. Am I missing some other option or is there a special reason why vector operations are not checked?

Regards,

Moritz

Thanks John, seems like a dynamic runtime instrumentation is then not a good idea. I had a look at the UBSan features in Clang and I might be able to use them instead. But it seems like that vector operations are not instrumented with overflow checks if I specify the option -fsanitize=signed-integer-overflow. Am I missing some other option or is there a special reason why vector operations are not checked?

I might be misunderstanding you, and I haven't looked at this code lately, but the goal of UBSan is to check C's rules for integer UBs. Since C does not have vectors, I'm not sure exactly what you are expecting here. Could you give a bit more detail?

John

OpenCL as a language is a modified C99, which does have, amongst a few
other things, support for vector types for basic types (char, short, int,
long and their unsigned variants as well as floating point types half,
float and double).

So, there is probably some work required to implement this for OpenCL's
native vector support. I haven't looked at the code, so can't say if
there's any particular difficulty in this particular case.

I might be misunderstanding you, and I haven't looked at this code lately, but the goal of UBSan is to check C's rules for integer UBs. Since C does not have vectors, I'm not sure exactly what you are expecting here. Could you give a bit more detail?

I just wondered whether the checks might have been implemented for vector types as well since Clang features vector extensions for the C language.

OpenCL as a language is a modified C99, which does have, amongst a few other things, support for vector types for basic types (char, short, int, long and their unsigned variants as well as floating point types half, float and double).

So, there is probably some work required to implement this for OpenCL's native vector support. I haven't looked at the code, so can't say if there's any particular difficulty in this particular case.

I will have a look then. In general, is there any interest to lift the UBSan implementation to include checks for vector types, even if they are not part of the C language?

Thanks,

Moritz

I just wondered whether the checks might have been implemented for vector types as well since Clang features vector extensions for the C language.

Ah, no, I don't believe so. And making these checks efficient might be challenging. Adding them sounds useful to whatever extent the vector users care about overflows (I hope they care...).

John