[klee-dev] The incorrect result obtained from KLEE (BVTypeCheck: terms in atomic formulas must be of equal length)

[Cristian Cadar]

I cannot reproduce this on my machine.  Can you open an issue at 
https://github.com/klee/klee/issues, giving more details on your 
configuration and how you ran KLEE?

Best,
Cristian

On 26/02/15 09:52, Yu-Fang Chen wrote:
> We tried two versions of STP (r940 and the latest) and KLEE gives us
> the message "BVTypeCheck: terms in atomic formulas must be of equal
> length" with both versions.
>
> Below is the program we run using klee and the output.
>
> PROGRAM:
>
> #include <assert.h>
> #include <klee/klee.h>
> #define N 5
>
> int avg (int x[N])
> {
>    int i;
>    int ret;
>    ret = 0;
>    for (i = 0; i < N; i++) {
>      ret = ret + x[i];
>    }
>    return ret / N;
> }
>
> int main ()
> {
>    int x[N];
>    int temp;
>    int ret;
>    int ret2;
>    int ret5;
>
>    klee_make_symbolic(x, sizeof x, "x");
>
>    ret = avg(x);
>
>    temp=x[0];x[0] = x[1]; x[1] = temp;
>    ret2 = avg(x);
>    temp=x[0];
>    int i;
>    for(i =0 ; i<N-1; i++){
>       x[i] = x[i+1];
>    }
>    x[N-1] = temp;
>    ret5 = avg(x);
>
>    if(ret != ret2 || ret !=ret5){
>      ERROR:
>        goto ERROR;
>    }
>    return 1;
> }
>
>
>
> OUTPUT:
>
> KLEE: output directory is "XXXXXX"
> valuewidth of lhs of EQ: 32
> valuewidth of rhs of EQ: 64
> indexwidth of lhs of EQ: 0
> indexwidth of rhs of EQ: 0
> Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length
>
> 338:(EQ
>    142:0x00000002
>    336:0x000000000000003F)
>
> 0
> error: STP Error: BVTypeCheck: terms in atomic formulas must be of equal length
> 0  klee            0x0000000000d9cb7f
> 1  klee            0x0000000000d9d089
> 2  libpthread.so.0 0x00007f0ac3162bd0
> 3  libc.so.6       0x00007f0ac239f037 gsignal + 55
> 4  libc.so.6       0x00007f0ac23a2698 abort + 328
> 5  klee            0x000000000062cbc9
> 6  klee            0x0000000000dcebcf BEEV::FatalError(char const*,
> BEEV::ASTNode const&, int) + 127
> 7  klee            0x0000000000dcf4f4 BEEV::BVTypeCheck(BEEV::ASTNode
> const&) + 1940
> 8  klee            0x0000000000db37a6 vc_iteExpr + 54
> 9  klee            0x0000000000632731
> klee::STPBuilder::bvVarRightShift(klee::ExprHandle, klee::ExprHandle)
> + 225
> 10 klee            0x000000000063380c
> klee::STPBuilder::constructSDivByConstant(klee::ExprHandle, unsigned
> int, unsigned long) + 428
> 11 klee            0x00000000006365d1
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*) + 7649
> 12 klee            0x0000000000633f13
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*) + 323
> 13 klee            0x0000000000634c72
> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*) + 1154
> 14 klee            0x0000000000633f13
> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*) + 323
> 15 klee            0x0000000000630393
> STPSolverImpl::computeInitialValues(klee::Query const&,
> std::vector<klee::Array const*, std::allocator<klee::Array const*> >
> const&, std::vector<std::vector<unsigned char, std::allocator<unsigned
> char> >, std::allocator<std::vector<unsigned char,
> std::allocator<unsigned char> > > >&, bool&) + 387
> 16 klee            0x000000000061bd15
> CexCachingSolver::getAssignment(klee::Query const&,
> klee::Assignment*&) + 245
> 17 klee            0x000000000061cf6b
> CexCachingSolver::computeValidity(klee::Query const&,
> klee::Solver::Validity&) + 843
> 18 klee            0x000000000061a815
> CachingSolver::computeValidity(klee::Query const&,
> klee::Solver::Validity&) + 149
> 19 klee            0x000000000062956b
> IndependentSolver::computeValidity(klee::Query const&,
> klee::Solver::Validity&) + 315
> 20 klee            0x00000000005f7eee
> klee::TimingSolver::evaluate(klee::ExecutionState const&,
> klee::ref<klee::Expr>, klee::Solver::Validity&) + 366
> 21 klee            0x00000000005caaa2
> klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>,
> bool) + 226
> 22 klee            0x00000000005d6ae3
> klee::Executor::executeInstruction(klee::ExecutionState&,
> klee::KInstruction*) + 9123
> 23 klee            0x00000000005d96d6
> klee::Executor::run(klee::ExecutionState&) + 1798
> 24 klee            0x00000000005d9fdd
> klee::Executor::runFunctionAsMain(llvm::Function*, int, char**,
> char**) + 1805
> 25 klee            0x00000000005b5c1c main + 6956
> 26 libc.so.6       0x00007f0ac2389ea5 __libc_start_main + 245
> 27 klee            0x00000000005bed31
> Aborted (core dumped)
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>