KLEE on integer overflow?

[Mark R. Tuttle]

*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.


*Is there a list of all the things that KLEE can be made to check for*?

Things like bad pointers and division by zero, while generating inputs to
induce coverage?


*What is the most effective way to become more deeply plugged into the KLEE
community?*

Is there a workshop or publication venue where people tend to
congregate? Where
do people go to brainstorm about potential applications and solutions? This
list is the only resource I’m aware of.


Thanks,
Mark


Mark Tuttle, tuttle-***@public.gmane.org

[Luca Dariz]

Post by Mark R. Tuttle
*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.

Best Regards,
Luca Dariz

[Luca Dariz]

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
*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