[klee-dev] questions about klee-array

[Qiao Kang]

Hi all,

When I run klee, I found it is quite slow to resolve array constraints if
the array size is large.

For instance (x, y are both symbolic variables):

int a[4096] = {0};
a[x] = 1;
if (a[y] > 0){
  // path1
} else {
  // path2
}

It takes serveral seconds to finish, and the time scales with the size of
the array.

Then I found a paper "Accelerating Array Constraints in Symbolic Execution"
- ISSTA 2017, and seems that this paper aims at address this problem.

I'm quite interested in reproducing the results of this paper, but I cannot
build klee-array from source, because it relies on LLVM 3.4 and it is not
available from ubuntu software repos.

I'm downloading the vm image (ova file) but it is very slow (200K/s).

My questions are:
1) Is the poor performance I have observed expected?
2) Is klee-array integrated in the klee mainstream?
3) If not, how can I build klee-array from source which relies on earlier
version of LLVM?
4) Can I download the ova from other sources like google drive?

Thank you very much,
Qiao
-------------- next part --------------
HTML attachment scrubbed and removed