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

[Yu-Fang Chen]

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)