Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
If you are new to the project, and want to pick up some background knowledge, here are some pointers.
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
- 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.
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
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