I am testing out a simple program, where I am creating a file, and
reading in some data from the file into a buffer.
The size of the buffer is small, and so I should get a possible memory
error. Here is the source code:
#include <fcntl.h>
#include <stdio.h>
#include <string.h>
#include <assert.h>
int main(int argc, char **argv)
{
char buffer[3];
char name[10];
klee_make_symbolic(&name, sizeof(name), "fname");
klee_assume(name[9] == '\0');
klee_assume(name[0] != '\0');
int fd, bytes;
fd = open(name, O_RDWR);
if(fd < 0) {
printf("Could not open..\n");
return -1;
}
bytes = read(fd, buffer, 20);
printf("bytes = %d\n", bytes);
return 0;
}
So I test this using the following command:
klee --libc=uclibc --posix-runtime file.o --sym-files 1 40
And as expected, I get a test case which says that there is a memory
error and there is a chance for "buffer" to be overrun.
Now, if I want to replay this test case and see that I am possibly
running into a segmentation fault because the return address of main
is getting corrupted, I would want that a file is actually created,
and the contents of that file match the contents in the corresponding
ktest file that is generated for the memory error. Is there any way to
accomplish this or will have to write a whole bunch of code to make
this happen?
The bigger picture:::
I am extending klee to support sockets, and reads/writes from the
network. So, what I am doing is redirecting socket, recv, send calls
etc so that reads and writes take place through symbolic files. This
way I will be able to test out
network servers/clients through klee.
So now, I have a server, which just opens a socket, waits for a
connection, and then reads data when a client connects to it. The
socket descriptor that I am returning to the server, is nothing but a
file descriptor that i have obtained from opening a symbolic file
instead. This time I am again reading in the data, from the socket
into a buffer. The size of the buffer is small and thus klee should
report that there is a possible memory error.
Klee does this successfully, creates a corresponding test case, which
contains the data that is required in the symbolic file that is
created during the socket call which is required to overrun the
buffer.
I want to replay this test case, and during runtime I would want to
actually create a file from which the server reads out the required
data to overrun the buffer.
This raises another question. While replaying the test case, is there
a way, That I can get the program to use the stubs defined in
runtime/POSIX intead of the actual system calls?
Sorry for the long email, I hope I was clear enough to explain my problem..
-Lokesh
--
Lokesh Agarwal
MSISTM, Carnegie Mellon University
412 - 877 - 9131
