[klee-dev] KLEE aborts on some small examples

[ThanhVu (Vu) Nguyen]

any idea on why Klee crashes with this small example ?  is it because of
the STP solver not capable of dealing with these constraints ?

Vu

On Wed, Jan 27, 2016 at 3:54 PM, ThanhVu (Vu) Nguyen <
nguyenthanhvuh at gmail.com> wrote:

> Hi,
>
> here's a small program that causes Klee to abort
>
> divbin.c
>
> #include <klee/klee.h>
>
> #include <stdio.h>
>
> #include <assert.h>
>
> #include <stdlib.h>  //required for afloat to work
>
>
>
> int mainQ(int A, int B) {
>
>
>
>   assert(A > 0 && B > 0);
>
>
>   int q = 0; int r = A; int b = B;
>
>
>
>   while(r>=b) b=2*b;
>
>   while(b!=B) {
>
>     q = 2*q; b = b/2;
>
>     if (r >= b) {
>
>       q = q + 1; r = r - b;
>
>     }
>
>   }
>
>   return q;
>
> }
>
> int main(int argc, char **argv) {
>
>     int A;
>
>     klee_make_symbolic(&A, sizeof(A), "A");
>
>     klee_assume(-10 <= A);
>
>     klee_assume(A <= 10);
>
>     int B;
>
>     klee_make_symbolic(&B, sizeof(B), "B");
>
>     klee_assume(-10 <= B);
>
>     klee_assume(B <= 10);
>
>     mainQ(A,B);
>
>     return 0;
>
> }
>
> debian Wed Jan 27:15:50:51 (14145)
>
> $ clang -I ~/Src/Devel/KLEE/klee/include -emit-llvm -c
> /var/tmp/DIG2_dL0xtJ/divbin.c.klee_assert.c -o
> /var/tmp/DIG2_dL0xtJ/divbin.c.klee_assert.c.o
>
> debian Wed Jan 27:15:50:53 (14146)
>
> $ klee --allow-external-sym-calls -optimize --max-time=5.
> -output-dir=/var/tmp/DIG2_dL0xtJ/divbin.c.klee_assert.c.o-klee-out
> /var/tmp/DIG2_dL0xtJ/divbin.c.klee_assert.c.o
>
> KLEE: output directory is
> "/var/tmp/DIG2_dL0xtJ/divbin.c.klee_assert.c.o-klee-out"
>
> *KLEE: ERROR: (location information missing) ASSERTION FAIL: A > 0 && B >
> 0*
>
> *KLEE: NOTE: now ignoring this error at this location*
>
> KLEE: WARNING: unable to compute initial values (invalid constraints?)!
>
> array A[4] : w32 -> w8 = symbolic
>
> array B[4] : w32 -> w8 = symbolic
>
> (query [(Slt 4294967285
>
>               N0:(ReadLSB w32 0 A))
>
>          (Slt N0 11)
>
>          (Slt 4294967285
>
>               N1:(ReadLSB w32 0 B))
>
>          (Slt N1 11)
>
>          (Slt 0 N0)
>
>          (Slt 0 N1)
>
>          (Eq false (Slt N0 N1))
>
>          (Eq false
>
>              (Slt N0 N2:(Shl w32 N1 1)))
>
>          (Slt N0 N3:(Shl w32 N2 1))
>
>          (Eq false
>
>              (Slt (Sub w32 N0 N4:(SDiv w32 N3 2))
>
>                   N5:(SDiv w32 N4 2)))
>
>          (Eq N5 N1)]
>
>         false)
>
> KLEE: WARNING: unable to get symbolic solution, losing test case
>
> klee: CexCachingSolver.cpp:268: virtual bool
> CexCachingSolver::computeValidity(const klee::Query&,
> klee::Solver::Validity&): Assertion `a && "computeValidity() must have
> assignment"' failed.
>
> 0  libLLVM-3.4.so.1 0x00007f3f54fb5362
> llvm::sys::PrintStackTrace(_IO_FILE*) + 34
>
> 1  libLLVM-3.4.so.1 0x00007f3f54fb4e0c
>
> 2  libpthread.so.0  0x00007f3f540128d0
>
> 3  libc.so.6        0x00007f3f52c05147 gsignal + 55
>
> 4  libc.so.6        0x00007f3f52c06528 abort + 328
>
> 5  libc.so.6        0x00007f3f52bfe266
>
> 6  libc.so.6        0x00007f3f52bfe312
>
> 7  klee             0x00000000004e0f1e
> CexCachingSolver::computeValidity(klee::Query const&,
> klee::Solver::Validity&) + 1566
>
> 8  klee             0x00000000004ddb3d
> CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&)
> + 109
>
> 9  klee             0x00000000004ee3f3
> IndependentSolver::computeValidity(klee::Query const&,
> klee::Solver::Validity&) + 275
>
> 10 klee             0x00000000004b8a39
> klee::TimingSolver::evaluate(klee::ExecutionState const&,
> klee::ref<klee::Expr>, klee::Solver::Validity&) + 233
>
> 11 klee             0x0000000000491190
> klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool) +
> 224
>
> 12 klee             0x0000000000497781
> klee::Executor::executeInstruction(klee::ExecutionState&,
> klee::KInstruction*) + 8369
>
> 13 klee             0x000000000049a72e
> klee::Executor::run(klee::ExecutionState&) + 1614
>
> 14 klee             0x000000000049afc1
> klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) +
> 1681
>
> 15 klee             0x00000000004798b0 main + 11312
>
> 16 libc.so.6        0x00007f3f52bf1b45 __libc_start_main + 245
>
> 17 klee             0x0000000000481dcf
>
> Aborted
>
>
> Is this just a limitation of Klee (e.g., cannot deal with nonlinear
> arithmetic ?) or there's some tricks I can do to make it to work ?
>
>
> Thanks,
> Vu
>
-------------- next part --------------
HTML attachment scrubbed and removed