Re: [klee-dev] klee and overshift error
Thank you Andrew and Dan for your response. I have tried to measure the coverage with the generated test cases and it is very low. The test cases are generated based on choosing N and X variables ( main inputs of the libquntukm program) to be symbolic inside the code with using klee_make_symbolic. I also tried KLEE with Hmmer program in SPEC benchmark to generate more test cases with using klee_make_symbolic but I still couldn't achieve a high coverage. Do you have any suggestions to generate more test case and achieving high coverage using Klee with SPEC benchmarks?Thank you. On Saturday, 22 July 2017, 16:49, Andrew Santosa wrote: Hi BNM, KLEE may report overshift error upon encountering Shl, AShr or LShr of LLVM.It is reported when KLEE determines that the shift amount is greater than the bitwidth of the data beingshifted. I happen to have a copy of SPEC CPU 2006. At Line 108 of classic.c there is a loop whose entrycondition includes a left shift. It is possible that nothing gets reported when the program is run natively. Best,Andrew On Sun Jul 16 2017 00:38:50 GMT+0800 (SGT), BNM wrote: Hello, I have tried to run Klee with libQuantum in SPEC benchmarks. The duration of running Klee with this benchmark lasted more than 24 hours and all the test cases contained overshift error. KLEE: ERROR: /klee/libqu/classic.c:108: overshift error I would like to know what is the cause of this error? Is it related to the choice of the symbolic variable? Without using KLEE the benchmark works well. Thank you, ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee and overshift error
On 22 July 2017 at 16:49, Andrew Santosa wrote: > Hi BNM, > > KLEE may report overshift error upon encountering Shl, AShr or LShr of LLVM. > It is reported when KLEE determines that the shift amount is greater than > the bitwidth of the data being > shifted. Slight correction. KLEE will report an error if the shift width is greater than **or equal to** the bitwidth being shifted because at the LLVM IR level (and at the level of C) this is undefined behaviour. > > KLEE: ERROR: /klee/libqu/classic.c:108: overshift error > I would like to know what is the cause of this error? Is it related to the > choice of the symbolic variable? Without using KLEE the benchmark works If you really don't care about the undefined behaviour you can remove the check by passing `-check-overshift=0` to klee. You should be careful though. Having undefined behaviour in your program may cause you problems. HTH, Dan. ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] klee and overshift error
Hi BNM, KLEE may report overshift error upon encountering Shl, AShr or LShr of LLVM.It is reported when KLEE determines that the shift amount is greater than the bitwidth of the data beingshifted. I happen to have a copy of SPEC CPU 2006. At Line 108 of classic.c there is a loop whose entrycondition includes a left shift. It is possible that nothing gets reported when the program is run natively. Best,Andrew On Sun Jul 16 2017 00:38:50 GMT+0800 (SGT), BNM wrote: Hello, I have tried to run Klee with libQuantum in SPEC benchmarks. The duration of running Klee with this benchmark lasted more than 24 hours and all the test cases contained overshift error. KLEE: ERROR: /klee/libqu/classic.c:108: overshift error I would like to know what is the cause of this error? Is it related to the choice of the symbolic variable? Without using KLEE the benchmark works well. Thank you, ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] klee and overshift error
Hello, I have tried to run Klee with libQuantum in SPEC benchmarks. The duration of running Klee with this benchmark lasted more than 24 hours and all the test cases contained overshift error. KLEE: ERROR: /klee/libqu/classic.c:108: overshift error I would like to know what is the cause of this error? Is it related to the choice of the symbolic variable? Without using KLEE the benchmark works well. Thank you, ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev