如何在 klee 中使用 max-time 标签

Question

我正在尝试在 coreutils 的编译字节码版本上运行 klee，这在某种程度上复制了 klee 不久前所做的实验。

我在弄清楚如何使用 --max-time 标志时遇到了一些麻烦。

当我运行这个命令时，它需要大约 3 分钟，尽管最大时间是 10 秒：

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

当我运行这个命令时，大约需要 3 秒。该命令是相同的，除了文件名和 --max-time 标志被切换。

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

最后，当我在没有 --max-time 标志的情况下运行它时

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

至少需要 30 分钟，此时我放弃并杀死了它。

显然，文件名前后的标志都在做某事，但我不确定是什么。根据文档， --max-time 的标准用法将其放在文件名之前。谁能帮助我了解发生了什么？

Answer 1

KLEE 使用 llvm 的命令行参数预处理器 there 的实现。由于InputFile 选项是一个位置参数，所有后面的都被忽略。 但是--sym-args、--sym-files、--sym-stdin等选项在POSIX runtime中是独立处理的。