Hi Sandeep, I’ve checked the program with added #include <assert.h> on the latest KLEE.
This is the result that I get: klee test.bc KLEE: output directory = "klee-out-5" KLEE: done: total instructions = 102 KLEE: done: completed paths = 3 KLEE: done: generated tests = 3 This time 3 test cases were created: ktest-tool --write-ints test000001.ktest ktest file : 'test000001.ktest' args : ['test.bc'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 1 ktest file : 'test000002.ktest' args : ['test.bc'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 2 ktest-tool --write-ints test000003.ktest ktest file : 'test000003.ktest' args : ['test.bc'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 3 Please find the source file that I’ve used attached. I am definitely not an expert, but taking the archive thread mentioned by Cristian (http://www.mail-archive.com/[email protected]/msg00891.html) as a hint, I can guess that this behaviour might be caused by the object resolution. The variable “x” is symbolic and it is constrained to be 1,2 or 3. We create the “temp” pointer by offsetting the array pointer by the symbolic offset “x”. Since “x” is symbolic, now “temp” can point to one of three different memory objects: array[1], array[2] or array[3]. I guess this is the reason why we do get 3 executions here. You may want to take a look at Executor::executeMemoryOperation. To make a quick test I’ve added a printout in this part of the function: ExecutionState *unbound = &state; for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) { klee_message(“resolution list”); // <<<< added by me And when I executed the program once more, I got: klee test.bc KLEE: output directory = "klee-out-7" KLEE: resolution list KLEE: resolution list KLEE: resolution list KLEE: done: total instructions = 102 KLEE: done: completed paths = 3 KLEE: done: generated tests = 3 The added message is appearing thee times, which means that we have three possible objects that the pointer can point at. In the code just below the mentioned fragment, we have a line calling “fork” function, which essentially means creating an alternative execution path. I might be wrong, but my guess would be that we have three test cases here, because the pointer that we create using the constrained symbolic value ‘x’ can be pointing at three different memory objects. Hope that helps. Tomek From: Sandeep <[email protected]<mailto:[email protected]>> Date: Wednesday, 8 January 2014 16:58 To: "Kuchta, Tomasz" <[email protected]<mailto:[email protected]>>, klee-dev <[email protected]<mailto:[email protected]>> Subject: Re: [klee-dev] Query: Klee behavior with pointer de-referencing Hello Tomasz, Thanks a lot for the try. As you said the test case that you are getting is for failed external assert call. But what is expected in this case is one testcase for the path (*temp > 0) (as all values of the symbolic variable x will suggest that path only). Can you please add #include<assert.h> and run it again. (I am also getting the same behavior if I omit #include<assert.h> ). Thanks Sandeep On 12/18/2013 3:53 PM, Kuchta, Tomasz wrote: Hi Sandeep, For foo (x, 10, 20, 30, 40) the result is the following: tk2512:/data/temp$ /data/temp/klee/Release+Asserts/bin/klee test.bc KLEE: output directory = "klee-out-4" KLEE: WARNING: undefined reference to function: assert KLEE: WARNING ONCE: calling external: assert(1) KLEE: ERROR: /data/temp/test.c:13: failed external call: assert KLEE: NOTE: now ignoring this error at this location KLEE: done: total instructions = 69 KLEE: done: completed paths = 3 KLEE: done: generated tests = 1 1 test file is generated (this is for failed external call assert and x == 1): ktest-tool --write-ints test000001.ktest ktest file : 'test000001.ktest' args : ['test.bc'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 1 Best regards, Tomek From: Sandeep <[email protected]<mailto:[email protected]>> Date: Wednesday, 18 December 2013 20:29 To: "Kuchta, Tomasz" <[email protected]<mailto:[email protected]>>, "[email protected]<mailto:[email protected]>" <[email protected]<mailto:[email protected]>> Subject: Re: [klee-dev] Query: Klee behavior with pointer de-referencing Thanks a lot Tomasz. I two believe that only two paths should get reported. But I am getting 3 (with one abort) Can you please confirm the number of paths that you are getting with the following call to foo return foo(x,10,20,30,40); I believe it is just 1 in your case. Thanks Sandeep On 12/18/2013 01:41 AM, Kuchta, Tomasz wrote: Hello Sandeep, It seems to me that both paths are possible here. We first constraint x to be 1, 2 or 3 by doing klee_assume((x > 0) & (x < 4)). Then we will have the following values for the corresponding indices in the “array”, if we call foo() with arguments x1 = 10, x2 = 20, x3 = 30, x4 = -1: array[1] == 20 array[2] == 30 array[3] == -1 Both: array[1] and array[2] will exercise the path leading to assert(1), because their values are greater than 0. On the other hand, array[3] will exercise the path leading to assert(0), because its value is –1. I’ve run the test on the current latest version of KLEE and two *.ktest files were created: ktest-tool --write-ints test000001.ktest ktest file : 'test000001.ktest' args : ['test.bc'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 1 ktest-tool --write-ints test000002.ktest ktest file : 'test000002.ktest' args : ['test.bc'] num objects: 1 object 0: name: 'x' object 0: size: 4 object 0: data: 3 The first file corresponds to the path exercised by value 20 of array[1] (x == 1, which transforms to array[1]). The second file corresponds to the path exercised by value –1 of array[3] (x == 3, which transforms to array[3]). Hope that helps, Best regards Tomek From: Sandeep <[email protected]<mailto:[email protected]>> Date: Wednesday, 18 December 2013 06:39 To: klee-dev <[email protected]<mailto:[email protected]>> Subject: [klee-dev] Query: Klee behavior with pointer de-referencing 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 -- With Thanks and Regards, Sandeep Dasgupta Graduate ( PhD ) in Computer Science Room : 1218 Siebel Center for Computer Science -- With Thanks and Regards, Sandeep Dasgupta Graduate ( PhD ) in Computer Science Room : 1218 Siebel Center for Computer Science
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
