[klee-dev] questions about klee-array

[Cadar, Cristian]

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.cadar at imperial.ac.uk 
> <mailto: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 <mailto: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 <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>