I'm trying to run klee on a compiled bytecode version of the coreutils, somewhat replicating the experiment that klee did a while back.
I'm having some trouble figuring out how to use the --max-time flag.
When I run this command, it takes around 3 minutes, despite the max-time being 10 seconds:
klee --optimize --libc=uclibc --posix-runtime --max-time 10s ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
When I run this command, it takes around 3 seconds. The command is identical, except for the fact that the filename and the --max-time flag are switched.
klee --optimize --libc=uclibc --posix-runtime --max-time 10s ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
Finally, when I run it without the --max-time flag
klee --optimize --libc=uclibc --posix-runtime ./echo.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdin 8 --sym-stdout
it takes at least 30 minutes, at which point I gave up and killed it.
Clearly, the flag before and after the filename are both doing something, but I'm not sure what. The standard usage for --max-time puts it before the filename according to the documentation. Can anyone help me understand what's happening?
KLEE uses llvm's implementation of command line argument preprocessor there . And since
InputFile
option is a positional argument, all following ones are ignored. However, such options as--sym-args
,--sym-files
,--sym-stdin
are processed in POSIX runtime independently.