[klee-dev] questions about klee-array

[Qiao Kang]

Hi Cristian,

Thanks for the reply, very helpful!! I did use klee_assume to specify the
range of the symbolic index.

I also found that the more read/write operations I perform to the array,
the time also grows very fast.

For instance, in this example I run the loop N times, each iteration has 1
read and 1 write:

// x[N] and y[N] are symbolic inputs, assumed to be 0~4095
int a[4096] = {0};
for (i from 0 to N-1) {
  a[x[i]] += 1;
  if (a[y[i]] > 1){
    // path1
  } else {
    // path2
  }
}

Is it fair to say that the constraint complexity grows exponentially with N?

Thanks,
Qiao


On Wed, Sep 4, 2019 at 10:37 AM Cadar, Cristian <c.cadar at imperial.ac.uk>
wrote:

> 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
> >
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed