prepack
prepack copied to clipboard
facebookarchive
Hook up Z3.
When Prepack comes across conditional control-flow during its interpretation of the initialization code, e.g. if (require("NativeModules").UIManager.screen.width > 1000) { ... } else { ... } then it explores both branches, and merges the resulting states.
However, if a branch is actually infeasible, this results in a sub-optimal bloated residual program. Consider the following example, where the then-branch is in fact infeasible. let screen = require("NativeModules").UIManager.screen; if (screen.width > 1000 && screen.width < 0) { ... } else { ... } (There is no actual code with such a trivial infeasible branch, but this can arise when Prepack stitches together more complicated control flows.)
In order to reason about feasibility of path conditions, we should hook up Prepack to an SMT solver, e.g. Z3 (https://github.com/Z3Prover/z3).
- Look at src/evaluators/IfStatement.js for where we fork control flow in the presence of an AbstractValue. Check here if both branches are feasible, and skip one side if not.
- There are different ways to hook up Z3 to Prepack. Unfortunately, there is no JavaScript binding for Z3. Alternative, you could use the C/C++ binding, and write a Node.JS C/C++ AddOn https://nodejs.org/api/addons.html to communicate with Z3.
Refactoring how we create values (#597) is a prerequisite for this work.
https://github.com/ExpoSEJS/z3javascript seems to provide an npm package that gives JS bindings for Z3.
