[klee-dev] KLEE aborts on some small examples

[Cristian Cadar]

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
> <nguyenthanhvuh at gmail.com <mailto: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
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>