[klee-dev] bug in klee/stp

[Marek Chalupa]

Hi,

On 02/02/16 11:35, Pablo González de Aledo wrote:
> Hi Marek :-)
>
> Have in mind that klee uses bit-vector arithmetics to interact with the
> SMT solver, and things can get a little bit weird when you do so.
>
> if n is a '1' followed by 31 zeros (in binary), it is indeed a negative
> number, but when you divide by two (shift the one one position to the
> right), it magically becomes positive.

but clang generates sdiv instruction, it should not be equivalent to 
shifting bits one position to the right, or should it? I think that sdiv 
.., 2  should keep the sign, except for the corner cases like sdiv -1, 2 
where I would expect the result to be 0. And we certainly don't hit the 
corner cases, klee says that n == -9 or n == -5 (depends on assumptions)

Thanks
Marek


> You can see the counter-example generated by klee with "ktest-tool
> --write-ints klee-last/test000001.ktest" and the queries to the
> SMT-solver with "klee -use-query-log=all:smt2 file.bc"
>
> Regards.
>
> 2016-02-02 10:06 GMT+01:00 Marek Chalupa <mchqwerty at gmail.com
> <mailto:mchqwerty at gmail.com>>:
>
>     Hi list,
>
>     I have this small trivial program:
>
>
>     #include <assert.h>
>
>     int main(void)
>     {
>        int n;
>        klee_make_symbolic(&n, sizeof n, "n");
>        klee_assume(n < 0);
>
>        if (n/2 > 0)
>          assert(0);
>
>        return 0;
>     }
>
>
>     KLEE (on master from git) says that the assertion is violated,
>     although since n is negative, then n/2 should not be greater than 0
>     and the assert() should be never called. I suppose it is a bug, or
>     did I overlook something?
>
>     P.S. If the condition is just (n > 0), then everything is fine. The
>     assumption can be even (n < -1) or (n < -1 && n > -10) (in which
>     case I get that the assumption is provably false, which is weird also)
>
>     Thanks,
>     Marek
>
>     _______________________________________________
>     klee-dev mailing list
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>