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: [email protected]
To: [email protected]
CC: [email protected]
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 <[email protected]> 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: [email protected]
To: [email protected]
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
[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
