llvm dev - Sep 2015 - 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.

On 09/13, Pflanzer, Moritz via llvm-dev wrote:
> 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
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
-- 

Johannes Doerfert
Researcher / PhD Student

Compiler Design Lab (Prof. Hack)
Saarland University, Computer Science
Building E1.3, Room 4.31

Tel. +49 (0)681 302-57521 : doerfert at cs.uni-saarland.de
Fax. +49 (0)681 302-3065  : http://www.cdl.uni-saarland.de/people/doerfert
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 213 bytes
Desc: not available
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150913/073becff/attachment.sig>

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 
> On 13 Sep 2015, at 12:41, Johannes Doerfert <doerfert at
cs.uni-saarland.de> wrote:
> 
> 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.
> 
> On 09/13, Pflanzer, Moritz via llvm-dev wrote:
>> 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
>> _______________________________________________
>> LLVM Developers mailing list
>> llvm-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
> 
> -- 
> 
> Johannes Doerfert
> Researcher / PhD Student
> 
> Compiler Design Lab (Prof. Hack)
> Saarland University, Computer Science
> Building E1.3, Room 4.31
> 
> Tel. +49 (0)681 302-57521 : doerfert at cs.uni-saarland.de
> Fax. +49 (0)681 302-3065  : http://www.cdl.uni-saarland.de/people/doerfert

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

> On 14 Sep 2015, at 08:25, John Regehr <regehr at cs.utah.edu> wrote:
> 
> 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