KLEE does not maintain a private environment for each state?

[Bowen Zhou]

Hello,

For the sample code below:

#include <stdio.h>
#include <klee/klee.h>

int
main(int argc, char** argv)
{
int c = 1;
klee_make_symbolic(&c, sizeof(c), "c");
FILE* fp = fopen("test", "w");
if (c)
fputs("hello", fp);
fclose(fp);
}

KLEE outputs:

***@orion01:~/llvm/klee$ Release+Asserts/bin/klee --posix-runtime
examples/open/open.bc
KLEE: NOTE: Using model:
/home/min/a/bzhou/llvm/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-12"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: fclose
KLEE: WARNING: undefined reference to function: fopen
KLEE: WARNING: undefined reference to function: fputs
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING ONCE: calling external: syscall(4, 30457376, 30523328)
KLEE: WARNING ONCE: calling external: fopen(26278016, 30437312)
KLEE: WARNING ONCE: calling external: fclose(0)
KLEE: ERROR: failed external call: fclose
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: calling external: fputs(30437776, 0)
Segmentation fault (core dumped)

This leads me to suspect that KLEE does not have a private environment
for each state therefore if one state closes a file, the file would be
closed for all the rest states. This is counter-intuitive to me, or did
I miss anything?

Regards
Bowen Zhou

[Paul Marinescu]

KLEE's model shares file descriptors between states.

However, in your example it seems that fopen fails and fputs crashes because it's called with a NULL pointer. That has nothing to do with KLEE's model.

Paul

Post by Bowen Zhou
Hello,
#include <stdio.h>
#include <klee/klee.h>
int
main(int argc, char** argv)
{
int c = 1;
klee_make_symbolic(&c, sizeof(c), "c");
FILE* fp = fopen("test", "w");
if (c)
fputs("hello", fp);
fclose(fp);
}
KLEE: NOTE: Using model: /home/min/a/bzhou/llvm/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-12"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: fclose
KLEE: WARNING: undefined reference to function: fopen
KLEE: WARNING: undefined reference to function: fputs
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING ONCE: calling external: syscall(4, 30457376, 30523328)
KLEE: WARNING ONCE: calling external: fopen(26278016, 30437312)
KLEE: WARNING ONCE: calling external: fclose(0)
KLEE: ERROR: failed external call: fclose
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: calling external: fputs(30437776, 0)
Segmentation fault (core dumped)
This leads me to suspect that KLEE does not have a private environment for each state therefore if one state closes a file, the file would be closed for all the rest states. This is counter-intuitive to me, or did I miss anything?
Regards
Bowen Zhou
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Cristian Cadar]

Hi, you should also set --libc (e.g, --libc=uclibc).

Cristian

Post by Bowen Zhou
Hello,
#include <stdio.h>
#include <klee/klee.h>
int
main(int argc, char** argv)
{
int c = 1;
klee_make_symbolic(&c, sizeof(c), "c");
FILE* fp = fopen("test", "w");
if (c)
fputs("hello", fp);
fclose(fp);
}
examples/open/open.bc
/home/min/a/bzhou/llvm/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-12"
KLEE: WARNING: undefined reference to function: __errno_location
KLEE: WARNING: undefined reference to function: fclose
KLEE: WARNING: undefined reference to function: fopen
KLEE: WARNING: undefined reference to function: fputs
KLEE: WARNING: undefined reference to function: fwrite
KLEE: WARNING: undefined reference to variable: stderr
KLEE: WARNING ONCE: calling external: syscall(4, 30457376, 30523328)
KLEE: WARNING ONCE: calling external: fopen(26278016, 30437312)
KLEE: WARNING ONCE: calling external: fclose(0)
KLEE: ERROR: failed external call: fclose
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: calling external: fputs(30437776, 0)
Segmentation fault (core dumped)
This leads me to suspect that KLEE does not have a private environment
for each state therefore if one state closes a file, the file would be
closed for all the rest states. This is counter-intuitive to me, or did
I miss anything?
Regards
Bowen Zhou
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev