llvm - 带有 stp 的 Klee 与带有其他 sat 求解器的 Klee

Question

Klee 使用 STP 作为其约束求解器，但理论上可以更改其求解器。STP 不允许浮点运算。如果我们决定用另一个约束求解器（比如 z3）替换 STP，klee 是否能够生成浮点约束？

流程是：C 代码 -> llvm bitcode -> klee -> stp 子句 -> klee -> 输出

如果 klee 获得浮点 llvm 指令，它是否能够解释它们？它是在 smt 语言中生成 fp 约束，stp 无法处理它们，还是根本不生成 fp 约束？

任何参考您的答案将不胜感激。

Answer 1

这个链接包含一个支持浮点的 KLEE 分支。不过，不知道它有多成熟。