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

[Urmas Repinski]

Hi Kirill.

The solution is easy actually.

> Is it correct that klee_assume() takes constraint with symbolic variables? While in my example n is not symbolic.
Yes, its correct, use any variables (not symbolic only) in klee_assume, and only inputs, that satisfy assumption, will be generated.

About the second problem i suggest to use klee_assume
 
 void klee_assume(int constraint) {
  
if (!constraint) klee_silent_exit(0);

}


> What I want to achieve is by applying certain search strategies 
(e.g. Depth First) I want KLEE instead of traversing a=1,2,3... but to 
give me a=500  as a one of the first test cases. > if I change 500 to 5M I will be waiting forever for the answer while it is right here. 

> Let me give you second example to explain what I want to get. 
> .....

During the bubble some counter is introduced, cnt1 in your example. As far as i understand this counter is increased every time swap is performed during bubble sort.
All you have to do is simply next to statement

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

line

klee_assume(cnt1==30); or with any other value you want to test.

This will make sure, that only inputs, that produce 30 swaps for sorting, will be generated. Others will be skipped.

klee_assume()  is actually very useful function, if you want to add to program some function, that does nothing, but exists, use klee_assume(true), if you want to skip some input generation, when certain conditions within the program trigger, use klee_assume(false), not klee_assert as it were suggested.

Hope this is that you need,
Urmas Repinski.

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

Hi Urmas,
Thanks for your answer!
Is it correct that klee_assume() takes constraint with symbolic variables? While in my example n is not symbolic.

What I want to achieve is by applying certain search strategies (e.g. Depth First) I want KLEE instead of traversing a=1,2,3... but to give me a=500  as a one of the first test cases. if I change 500 to 5M I will be waiting forever for the answer while it is right here. 


Let me give you second example to explain what I want to get. Imagine that I have a symbolic integer array#define N 10a[N];klee_make_symbolic(&a, sizeof(a), "a");


And I passing it to a bubble sort function, where I counting number of swaps that function performs to sort an array.cnt1 = BubbleSort(&a[0] , n);

Finally, I have a condition, where I comparing number of swaps to some value. Meaning that I want KLEE to come up with an input array such that number of swaps performed by the KLEE is 30 in this example. 
if (cnt1 == 30){	klee_assert(0);}
My question is, Can the KLEE see the relationship between symbolic input integer array and the number of swaps that function need to perform. 

Thanks!Kirill




On 25 March 2014 11:12, Urmas Repinski <urrimus at hotmail.com> wrote:




Hi, Kirill.

First of all, it is not clear what type of inputs should be generated.
In the example below all integers will be generated, starting from 0 ... including 500. 
klee_assert function will trigger __assert_fail klee function, this possibly will terminate input generation process, possibly not, i am not very sure.


Anyway it is possible that you want something more meaningful, if input 500 should be generated, or input 500 should not be generated.

In this case better to use klee_assume function:

 void klee_assume(int constraint) {
  
if (!constraint) klee_silent_exit(0);

}


{int a;
klee_make_symbolic(&a, sizeof(a), "a");
int i =0 ;
int n =1;
for (i =0; i < a;i++){

n++;
}
klee_assume(n==500); or klee_assume(n!=500);
Will generate a=500 or all a-s, except 500.

Urmas Repinski.

Date: Tue, 25 Mar 2014 09:33:26 +0000
From: kirill.sc at gmail.com

To: klee-dev at imperial.ac.uk
Subject: [klee-dev] KLEE relationship between loop length and counter.

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