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: [email protected] To: [email protected]; [email protected] CC: [email protected] 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 <[email protected]> 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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
