[klee-dev] KLEE relationship between loop length and counter.

[Urmas Repinski]

Hi Kirill.

I had already suggested to try to use klee_assume instead of klee_assert.

This should be the solution.

Thank You,
Urmas Repinski.

Date: Tue, 25 Mar 2014 17:02:46 +0000
Subject: Re: [klee-dev] KLEE relationship between loop length and counter.
From: kirill.sc at gmail.com
To: c.cadar at imperial.ac.uk; urrimus at hotmail.com
CC: klee-dev at imperial.ac.uk

Thank you for your answers,
It is very helpful, but I don't think its entirely answers my question. Below I have added my entire code of the example (to reduce confusion where possible)

1. When KLEE comes to the line "if (cnt1 == 30)" what type of the constraint its generated? Does this constraint mathematically related to the symbolic array "a" somehow (e.g. are "a" and "cnt" part of the same expression in STP solver)?  Can I print this data constraint? 
2. I've been monitoring test cases generated by KLEE under different search strategies. Generated test cases were not dependant on the value 30 or "cnt1 < 30" or "cnt1 > 30". KLEE was following the same pattern regardless of the the condition that I would specify for the assertion. This observation makes me believe that KLEE "blindly" searches through all possible input array orderings until it happens to find the one that satisfies condition for "number of swaps being equal to 30". 
3. Different search strategies take different time to find a solution, which is expected. 4. Time increases exponentially as I increase input array size (#define N 9).
What I am trying to say is that KLEE does not "understand" relationship between order of the input array and the number of swaps that it takes to order it . 
Is this statement correct? 
Practically, is it possible to rearrange my code or add some arguments when running klee, so that I can find solutions (at least one) in reasonable time for the arrays of size more than 9 ? (apart from using cloud9 and parallelizing )

  Thank you very much!
#define N 9int cnt = 0; int main() {

    int i;    int a[N];

    klee_make_symbolic(&a, sizeof(a), "a");

    int cnt1 = 0;

    cnt1 = BubbleSort(&a[0] , N);

    if (cnt1 == 30){
   printf("Assert\n");

   klee_assert(0);
    }
    printf("%i \n", cnt1);
    return 0;
}


//simple bubble sort takes pointer to int array and number of elements
int BubbleSort(int* a, int n){
   int swap = 1;
   int i =0;

   int temp =0;
   int cnt = 0;
   while (swap){
      swap = 0;      for (i= 0; i < n-1; i++){


         if (a[i] > a[i+1]){            //swap            temp = a[i];            a[i] = a[i+1];
            a[i+1] = temp;            swap = 1;            cnt+=1;
         }
      }    }

    return cnt;
}



On 25 March 2014 15:32, Cristian Cadar <c.cadar at imperial.ac.uk> wrote:

Hi Kirill,



KLEE does not perform any kind of abstraction for loops. In your example, the order in which paths are explored is dictated by the search heuristics employed.



Cristian



On 25/03/14 09:33, Kirill Bogdanov wrote:


Hello Everyone,

(Sorry for the previous email, it has been sent by mistake before I

finished it!)



Could you please let me know if what I am doing cannot be achieved with

KLEE and if it can, how can I do it?



1. Please consider my usage example below. The problem that I am

observing is that KLEE does not sees relationship between loop length

and the counter "n".

In my experiments (with different search strategies) KLEE always

encountered assertion by a blind search, and usually after generating

500 test cases.



{

int a;

klee_make_symbolic(&a, sizeof(a), "a");

int i =0 ;

int n =1;

for (i =0; i < a;i++){

n++;

}

if (n == 500)

klee_assert(0);

return 0;

}



Is this is something that is fundamentally impossible in KLEE, or can be

achieved by rewriting my example?





Thank you very much!





_______________________________________________

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