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 < [email protected]> 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
