B

Benno-Kyle-project

Incremental JavaScript Type Analysis

An incremental (by means of Adapton) type analyzer for JavaScript, built on top of the JSAna analysis framework.

Joint final project for CU Boulder CSCI7135 and CSCI7000 by Kyle Howell and Benno Stein.

As a supplement to the critical path document, refer to our project proposal for 7135.


Critical Path

  1. Identify a motivating example: i.e. write some JavaScript code that is both representative of the problem we're trying to solve and minimally complex.
  2. Implement abstract domains for JavaScript types and operators over domain elements.
  3. Build a non-incremental fixed-point data flow analysis over our abstract domain.
  4. Study the OCaml implementation of Adapton's model of incrementality more deeply and build some small examples of incremental computations to become more familiar with using the library.
  5. Use what we learned in step 4 to incrementalize the data structures used by our data-flow analysis.
  6. Empirically evaluate the effects of using Adapton and incremental computation on the performance of our analysis.

Final Project Submission

Deliverables

Our final paper(pdf,tex) and slides(pdf) are included.

Running Tests

All tests are in the tests/ directory, and the incremental tests used in the benchmarks are named incr_testX_XX.js. For this project, use the following command for running the first series of tests:

./bin/jsana -new-command -run-many "tests/incr_test1_0.\.js"

Other flags for benchmarking include -no-opt-passes and -incremental to disable optimization passes and enable incremental computation respectively.

JSAna Static Analyzer

JSAna is a static analyzer intended to verify modular specifications of JavaScript libraries.

Building JSAna

JSAna has the following build dependencies:

To run the JavaScript frontend for JSAna, a working installation of node.js is required. Once installed, JSAna can be run with the following command:

./bin/jsana

Source Code

The source code consists of two main parts implemented in two distinct modules. Each of these modules is contained in its own subdirectory:

heap: contains the heap abstraction. The domain itself is implemented in Domain with the basic datatype in Type and join and inclusion algorithms in Join and Inclusion. This domain builds significantly upon a pure domain that is implemented as a separate module (so as to be easy to replace).

pure: contains the pure abstraction. The pure abstraction is a domain for sets and values. It uses BDDs to represent sets. Additionally there are other domains used to represent simple facts like cardinality and constants to aid debugging. The top level domain is Domain, but the underlying BDD-based domain is in SetDomain.

Other modules include a top level disjunction domain (in disj), the interpreter (in interpreter), the JavaScript frontend (in frontend), the query program (in query), and the JavaScript preprocessor in bin/jspre.