[klee-dev] Query: Klee behavior with pointer de-referencing
Kuchta, Tomasz
t.kuchta12 at imperial.ac.uk
Wed Jan 8 18:10:43 GMT 2014
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/klee-dev@imperial.ac.uk/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 <sdasgup3 at illinois.edu<mailto:sdasgup3 at illinois.edu>>
Date: Wednesday, 8 January 2014 16:58
To: "Kuchta, Tomasz" <t.kuchta12 at imperial.ac.uk<mailto:t.kuchta12 at imperial.ac.uk>>, klee-dev <klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>>
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 <sdasgup3 at illinois.edu<mailto:sdasgup3 at illinois.edu>>
Date: Wednesday, 18 December 2013 20:29
To: "Kuchta, Tomasz" <t.kuchta12 at imperial.ac.uk<mailto:t.kuchta12 at imperial.ac.uk>>, "klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk>" <klee-dev-bounces at imperial.ac.uk<mailto:klee-dev-bounces at imperial.ac.uk>>
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 <sdasgup3 at illinois.edu<mailto:sdasgup3 at illinois.edu>>
Date: Wednesday, 18 December 2013 06:39
To: klee-dev <klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>>
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 27734 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140108/97beaa60/attachment.bin>
More information about the klee-dev
mailing list