Hi Qiao, In your example, the number of paths depends exponentially on N.
As a side note, please include self-contained C programs, not pseudocode. This avoids misunderstandings and also makes it easy for everyone to quickly run the code. Best, Cristian On 04/09/2019 16:57, Qiao Kang wrote: > 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.ca...@imperial.ac.uk > <mailto:c.ca...@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@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk> > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev