If you are new to the project, and want to pick up some background knowledge, here are some pointers.
JavaScript code processing
Prepack uses Babel to parse and generator JavaScript code. The Prepack's interpreter is directly interpreting the Babel AST.
JavaScript semantics
At the core of Prepack is an almost ECMAScript 5 compatible interpreter — implemented in JavaScript! The interpreter closely follows the ECMAScript 2016 Language Specification, with a focus on correctness and spec conformance. You can think of the interpreter in Prepack as a clean reference implementation of JavaScript.
Symbolic execution
Prepack's interpreter has the ability to operate on abstract values which typically arise from environment interactions. For example, Date.now can return an abstract value. You can also manually inject abstract values via auxiliary helper functions such as __abstract(). Prepack tracks all operations that are performed over abstract values. When branching over abstract values, Prepack will fork execution and explore all possibilities. Thus, Prepack implements a Symbolic Execution engine for JavaScript. To deal with the state exploration problem, Prepack may join variables and heap properties, resulting in conditional abstract values.
- Symbolic execution on Wikipedia
- Original paper on symbolic execution: Symbolic execution and program testing
- Prepack keeps track of effects in branches via transaction logs.
- Prepack performs state merging at control-flow joint points, see State joining and splitting for the symbolic execution of binaries and Using state merging and state pruning to address the path explosion problem faced by symbolic execution for an overview of the problem area.
Partial evaluation
In its main mode of operation, Prepack achieves similar effects to partial evaluation, but it doesn't do so using the traditional partial evaluation approach. In any case, here are some references:
- Partial evaluation on Wikipedia
- Nice online book on partial evaluation: Partial Evaluation and Automatic Program Generation
Abstract interpretation
At this time, Prepack only makes limited use of abstract interpretation, in particular around tracking type and value domains, and to compute limited loop and recursion fixed points.
- Abstract interpretation on Wikipedia
- Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation (program trace semantics)
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
Code generation
After interpretation has computed all relevant effects of the code, in the form of a final heap, the effects are being serialized as another JavaScript program.
- Thanks to the interpreter, Prepack performs loop unrolling and constant folding.
- lambda lifting is applied to all residual functions that are referenced from the final heap.
- For any residual computations outside of residual functions, Prepack also performs common subexpression elimination.