[klee-dev] KLEE aborts on some small examples

[ThanhVu (Vu) Nguyen]

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