I think you are hitting a bug in the counterexample cache. If you
disable it (--use-cex-cache=false), you should be able to avoid it. We
need to fix that soon, as the cache is often important for performance.
Cristian
On 02/02/2016 20:24, ThanhVu (Vu) Nguyen wrote:
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
<nguyenthanh...@gmail.com <mailto:nguyenthanh...@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
_______________________________________________
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
