Klee与stp vs. Klee和其他坐着的解算器

Klee uses STP as its constraint solver, but theoretically it is possible to change its solver. STP does not allow floating point operations. If we decide to replace STP with another constraint solver, say z3, would klee be able to generate floating point constraints?

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

The flow is: C code -> llvm bitcode -> klee -> stp clauses -> klee -> output

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

If klee gets floating point llvm instructions, is it able to interpret them? Does it generate fp constraints in smt language, that stp is not able to handle them, or it doesn't generate fp constraints at all?

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

Any reference for your answer would be appreciated.

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

1 个解决方案

#1

This link contains a fork of KLEE with floating point support. No idea how mature is it, though.

此链接包含具有浮点支持的KLEE分支。但不知道它有多成熟。