Indeed. You have a double-dereference there, and KLEE cannot reason
symbolically about this, so it's forking into all possible cases
(alternatively it could choose only one option). There is a discussion
about double-dereferences in the paper describing KLEE's predecessor EXE
(http://www.doc.ic.ac.uk/~cristic/papers/exe-tissec-08.pdf).
Cristian
On 08/01/14 17:54, Paul Marinescu wrote:
As Cristian pointed in the previous reply, the answer lies in object
resolution. klee does not report 3 paths, it reports 3 possible
executions, all of which follow the same path. What differs between
these 3 executions is the value of ptr, i.e. the object it points to.
Paul
On 8 Jan 2014, at 18:48, Sandeep <[email protected]
<mailto:[email protected]>> wrote:
Hello Cristian,
I am the original author of the code that you looked at.
Let me explain my intention of the code (pasted below).
I am intentionally storing the addresses of xi's in a array of
pointers. Also I am constraining x to take values 1,2 and 3.
My expectation is that only one path of the if condition got explored
as all possible values of the symbolic variable x will make
*temp > 0.
int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **) malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4));
return foo(x,10,20,30,40);
}
But Klee is reporting three paths.
Also ktest-tool gives the following information:
ktest file : 'klee-last/test000002.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 2
ktest file : 'klee-last/test000003.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 3
ktest file : 'klee-last/test000001.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1
Can you please explain why I am getting this result.
With Thanks
Sandeep
On 1/7/2014 12:32 PM, Cristian Cadar wrote:
See http://www.mail-archive.com/[email protected]/msg00891.html
Cristian
On 07/01/14 18:26, Pablo González de Aledo wrote:
I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.
May be the next code is simpler, and still explains the issue.
int main() {
int a;
int array[] = {1,2,3,4,5};
klee_make_symbolic(&a, sizeof(a), "a");
if(array[a] == 3)
return 0;
else
return 1;
}
Why does Klee generate 17 solutions when only one is possible (a ==
2) ?
Thanks.
2014/1/7 Cristian Cadar <[email protected]
<mailto:[email protected]>>
I only had a brief look at your code, but it looks like you are
storing the addresses of the x_i variables into the array, which is
likely not what you intended.
Cristian
On 18/12/13 06:39, Sandeep wrote:
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x
so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to
happen. But
in addition it is reporting two other paths for x = 1 and x =2,
despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path
(as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int
x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x,
sizeof(x), "x");
klee_assume((x > 0) & (x <
4)); // To
allow valid memory access on
'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_________________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
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
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
