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

[Kirill Bogdanov]

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 10
a[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