Virtual functions execution in symbolic object

[S1eGa]

KLEE issue. Whenever object of class with virtual functions is made symbolic, we are generating many tests cases and waiting for forever in the end.

Consider the following test case:

#include <cassert>
#include "klee/klee.h"

struct A {
  int x = 10;
  virtual void foo() {
    x += 1;
  }
};

struct B : A {
  virtual void foo() {
    x += 2;
  }
};

int main() {
  A *a = new B();
  klee_make_symbolic(a, sizeof(B), "a");
  a->x = 100;
  a->foo();
  assert(a->x == 101); 
}

We are expect to generate 1 test, that will fail assert.

Instead we are getting weird test cases, as shown below, and non of them fails the assertion, and KLEE does not stop the execution.

KLEE: Using STP solver backend
KLEE: WARNING ONCE: Alignment of memory from call "_Znwm" is not modelled. Using alignment of 8.
KLEE: ERROR: exmple.cpp:21: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: exmple.cpp:21: invalid function pointer
KLEE: NOTE: now ignoring this error at this location

Compiled and executed with:

clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone example.cpp
klee example.bc

[ladisgin]

@getn1ght, add klee run command and example without io

[S1eGa]

@getn1ght, add klee run command and example without io

Updated.

[S1eGa]

The problem is likely in klee_make_symbolic: a pointer to virtual functions table stored in class instance, and we will clear it, if make object symbolic; e.g., this problem does not seems to appear if we have only base class.

[ladisgin]

moved to UnitTestBot/klee#63