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

[Kirill Bogdanov]

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 9
int 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