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

[Kuchta, Tomasz]

You may want to check if you have stack limit set to unlimited (you can do this using ulimit -s).

Best regards,
Tomek

> On 27 Feb 2015, at 10:52, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:
> 
> 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
>> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 6199 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150227/81abb556/attachment.bin>