[klee-dev] questions about klee-array

[Cadar, Cristian]

Yes, our array acceleration work is integrated into the mainline (use 
option -optimize-array=all) and on your example it reduces the time on 
my machine from ~80s to only ~4s.  However, there is another issue 
there, which was discussed on the mailing list several times before: 
since the indexes are completely unconstrained, they could refer to any 
other memory object, causing a lot of unnecessary forking.  If you 
constrain the indexes to be in-bounds (klee_assume(x >= 0); 
klee_assume(x < 4096); same for y), KLEE should be much faster, even 
without the array optimization.

Cristian

On 04/09/2019 02:01, Qiao Kang wrote:
> 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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>