[klee-dev] KLEE on integer overflow?

[Luca Dariz]

Il 14/10/2014 03:25, Mark R. Tuttle ha scritto:
> Thanks, Luca.  Can you estimate how complete your branch is for the
> overflow instrinsics?  Is this something I could complete with a bit of
> advice from you?  -Mark
>
> On Mon, Oct 13, 2014 at 6:00 PM, Luca Dariz <l.dariz at imamoter.cnr.it
> <mailto:l.dariz at imamoter.cnr.it>> wrote:
>
>     Il 13/10/2014 23:47, Mark R. Tuttle ha scritto:
>
>         *Can KLEE check for integer overflow?*
>
>         Since KLEE is based on STP and STP is based on a theory of bit
>         vectors,
>         I had hoped it might be easy for KLEE to check for an overflow
>         bit.Since
>         CLANG has -fsanitize=unsigned-integer-__overflow and
>         -fsanitize=integer I
>         had hoped it would be easy to compile with these flags and run
>         KLEE, but
>         KLEE does not appear to support the LLVM arithmetic with overflow
>         intrinsics like llvm.uadd.with.overflow.* that CLANG inserts.
>
>
>     Hi Mark,
>     the implementation of these intrinsics is just incomplete, I started
>     to expand it to detect unsigned integer overflow in this branch
>     https://github.com/luckyluke/__klee/tree/detect-overflow
>     <https://github.com/luckyluke/klee/tree/detect-overflow>.
>
>     Best Regards,
>     Luca Dariz
>
>

Hi Mark,

for now only the checks related to -fsanitize=unsigned-integer-overflow 
are tested, I started working on -fsanitize=signed-integer-overflow but 
it is not complete yet. I attach the temporary patch based on my 
detect-overflow branch, if you want to try it or enhance. Please note 
that signed multiplication overflow still does not work, and divrem is 
missing.

As an advice, in order to consider all the possible corner cases, I 
found useful to have a look at the LLVM compiler-rt library, which 
contains the code that expand the llvm.*.with.overflow intrinsics, just 
in case you want to add some additional checks.

I re-add klee-dev since somehow I left it out of this thread.

Hope this helps,
Luca Dariz

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signed-integer.patch
Type: text/x-patch
Size: 10379 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20141014/a6a28e59/attachment.bin>