连接 Z3。

当 Prepack 在解释初始化代码时遇到条件控制流时,例如 if (require("NativeModules").UIManager.screen.width > 1000) { ... } else { ... } 则会探索两个分支,并合并结果状态。 但是,如果某个分支实际上是不可行的,则会导致一个不理想的臃肿的剩余程序。 请看以下示例,其中 then 分支实际上是不可行的。 let screen = require("NativeModules").UIManager.screen; if (screen.width > 1000 && screen.width < 0) { ... } else { ... } (没有实际代码具有如此简单的不可行分支,但 Prepack 将更复杂的控制流拼接在一起时可能会出现这种情况。) 为了推理路径条件的可行性,我们应该将 Prepack 连接到一个 SMT 解算器,例如 Z3 (https://GitHub.com/Z3Prover/z3)。 - 请查看 src/evaluators/IfStatement.js,了解我们在存在 AbstractValue 时如何分支控制流。检查这里,确保两个分支都可行,如果不,则跳过其中一条。 - 有多种方法可以将 Z3 连接到 Prepack。不幸的是,没有 JavaScript 绑定用于 Z3。另一种选择是使用 C/C++ 绑定,并编写一个 Node.js C/C++ AddOn https://nodejs.org/api/addons.html 来与 Z3 通信。