浮点支持是可能的。我认为不常见的原因有两个：

• 二进制 IL 的大多数应用程序不适用于浮点。例如，大多数 SMT 求解器仅支持整数算术运算。如果不能对行为进行推理，建模行为就不是很有用。

• 没有多少成熟的任意精度浮点代码库可以很容易地引入这些项目。

最近有一项出色的工作将浮点指令转换为 LLVM bitcode 语言，该项目称为McSema，由TrailOfBits的人员管理。

一位开发人员承诺，一旦代码达到良好状态，就会将其开源。

编辑：我刚刚看到埃德麦克曼的答案。我完全同意他的观点，即缺乏处理此类问题的工具使得很难集成到二进制程序分析框架中。但是，这已经是问题的结果，而不是原因。

其实，以我的拙见，使这个问题变得极其繁琐的原因在于它的本质。您必须处理连续问题（浮点数逻辑）并将其转换为离散问题（命题逻辑）。

这两种模型的混合使得处理变得非常困难，因为输入的微小差异可能最终导致截然不同的输出（位向量大小也可能对输出产生很大影响）。这种行为与您在加密散列函数中遇到的非常接近，其中对输入的微小修改将导致输出完全改变。

而且，输出的这种高度可变性并不能帮助工具将所有行为包装成一个有意义的逻辑公式，该公式可以与其他逻辑公式一起用命题逻辑表达。

如果 SMT 求解器开始考虑混合常用QF_AUFBV逻辑（通常用于程序模拟）和浮点逻辑（QF_LRA和QF_NRA），那么可能会有一些希望。