Repository files navigation

Copyright 2009-2020 Aarhus University

TAJS is a dataflow analysis for JavaScript that infers type information and call graphs.

The current version of the analysis contains a model of ECMAScript 3rd edition, including the standard library, and partial models of the ECMAScript 5 and its standard library, the HTML DOM, and the browser API.In some cases where ECMAScript has introduced incompatibilities with prior editions, including some changes made in ECMAScript 6, the analysis models the most recent language design.Other recent ECMAScript language features are partially supported viaBabel. The browser API is modeled after Chrome.

For research publications and other information about this tool seehttp://www.brics.dk/TAJS.

Make sure you clone not only the TAJS repository but also the submodules, for example by running

git submodule update --init --recursive

To build TAJS, you must first installJava,Ant, andNode.js.

The simplest way to build TAJS is to run Ant:

ant

This will build two jar files:dist/tajs.jar (contains only TAJS itself) anddist/tajs-all.jar (includes the relevant extra libraries).

The jar files are also available for download athttp://www.brics.dk/TAJS/dist/.

(To see all available ant targets, runant -p.)

You can now run the analysis as, for example:

java -jar dist/tajs-all.jar test-resources/src/google/richards.js

or

java -jar dist/tajs-all.jar test-resources/src/chromeexperiments/3ddemo.html

By default, TAJS outputs some information about its progress and eventually a list of type warnings and other messages.

Some of the available options (run TAJS without arguments to see the full list):

• -inspector - startTAJS Inspector after analysis (seebelow)

• -callgraph - output call graph as text and in a fileout/callgraph.dot (process withGraphviz dot)

• -show-variable-info - output type and line information about all variables

• -debug - output extensive internal information during the analysis

• -flowgraph - output the initial and final flow graphs (TAJS's intermediate representation) as text and toout/flowgraphs/ (in Graphviz dot format, with a file for each function and for the complete program)

• -low-severity - enable many more type warnings

• -quiet - only print results, not information about analysis progress

• -states - output intermediate abstract states during the analysis

• -statistics - output various statistics about the analysis results

• -uneval - enable the Unevalizer for on-the-fly translation ofeval calls, as described in'Remedying the Eval that Men Do', ISSTA 2012

• -determinacy - enable the techniques described in'Determinacy in Static Analysis of jQuery', OOPSLA 2014

• -test-soundness - test soundness using concrete execution as described in'Systematic Approaches for Increasing Soundness and Precision of Static Analyzers', SOAP 2017 (seebelow)

• -blended-analysis - use concrete execution as described in'Systematic Approaches for Increasing Soundness and Precision of Static Analyzers', SOAP 2017 for increasing precision (seebelow)

• -unsound X - enable unsound assumption X, e.g.-ignore-unlikely-property-reads causes some unlikely properties to be ignored during dynamic property read operations, and-show-unsoundness-usage outputs usage of unsound assumptions

• -babel - enable preprocessing using Babel to support recent ECMAScript features

• -type-filtering - enable type filtering using TypeScript declaration files for npm packages (seebelow)

Note that the analysis produces lots of addition information that is not output by default. If you want full access to the abstract states and call graphs, as a starting point see the source code fordk.brics.tajs.Main.The javadoc for TAJS is available athttp://www.brics.dk/TAJS/doc/.

TAJS Inspector (enabled using option-inspector) is a web-based interface to the analysis results.It is primarily intended as a development tool for investigating information collected during analysis.This includes abstract values of variables and properties, call graphs, and type warnings, but also internal analysisinformation, such as, number of times each primitive instruction is processed, number of contexts for each function,and "imprecision suspiciousness" of abstract states.

TAJS recognizes a few special built-in functions to support debugging and testing of the tool.For example, callingTAJS_dumpState() in the JavaScript program being analyzed will report the abstract state at the program point of the call.The full list of functions is documented inTAJS-functions.md.

The analysis models of the HTML DOM, the browser API, and the ECMAScript native library are not 100% complete.For a list of other known sources of unsoundness, seehttps://github.com/cs-au-dk/TAJS/issues?q=is%3Aopen+is%3Aissue+label%3Asoundiness.

It is possible to test that the analysis fixpoint over-approximates concrete behaviors.This requires a log file of concrete behaviors to be provided to TAJS.Sample log files are located intest-resources/logs.

Soundness testing using an existing log file can be performed like this:

java -jar dist/tajs-all.jar -test-soundness -log-file test-resources/logs/google/richards.js.log.gz test-resources/src/google/richards.js

This will produce the usual output, with the following line appended:

...Soundness testing succeeded for 1884 checks (with 0 expected failures)

Expected mismatches can be registered inKnownUnsoundnesses.java.

New log files can be generated by running the analyzed program concretely and monitoring its behavior usingjalangilogger (seebelow).

Soundness testing with a freshly generated log file can be performed like this:

java -jar dist/tajs-all.jar -test-soundness -generate-log -log-file my-log-file.log test-resources/src/google/richards.js

If DOM modeling is enabled (e.g. if the given file is an HTML file) then a browser is spawned and user input is processed (until stopped or timeout).If analyzing a stand-alone JavaScript file, the log file is generated with Node.js instead of using a browser.

Changes to the source code of the analyzed program requires a new log file to be created.

It is possible to artificially increase precision of the analysis by filtering abstract values based on values observed concretely. This optionrequires a log file as described forsoundness testing.

Blended analysis using an existing log file can be performed like this:

java -jar dist/tajs-all.jar -blended-analysis -log-file test-resources/logs/google/richards.js.log.gz test-resources/src/google/richards.js

The output is as usual, but probably with fewer warnings due to the analysis being more precise.

A variant of blended analysis is to tell the analysis to ignore code that is unreached according to the given log file:

java -jar dist/tajs-all.jar -ignore-unreached -log-file test-resources/logs/google/richards.js.log.gz test-resources/src/google/richards.js

Blended analysis with a freshly generated log file can be performed like this:

java -jar dist/tajs-all.jar -blended-analysis -generate-log -log-file my-log-file.log test-resources/src/google/richards.js

Another way to increase precision istype filtering, which filters dataflow according to types obtained from TypeScript declaration files for npm modules.

Example:

java -jar dist/tajs-all.jar -nodejs -type-filtering test-resources/src/tsspecs/myapp/myapp.js

The soundness of this mechanism relies on the assumption that the TypeScript declaration files are correct with respect to the module implementations.

The scriptresources/tsspecs/install-types.js can be used for quickly installing TypeScript declaration files fromDefinitelyTyped for all modules in thenode_modules sub-directory of the current directory.

Some advanced features of TAJS require additional environment configuration which can be defined in a tajs.propertiesproperties file.These features will automatically look for a tajs.properties file in the working directory and its ancestor directories.

To generate log files for soundness testing,Node.js andjalangilogger must be installed.

Individual external dependencies can be registered in tajs.properties like this:

jalangilogger = /home/tajs-user/tajs/extras/jalangiloggerbabel = /home/tajs-user/tajs/extras/babel

Alternatively, register the location of the TAJS installation:

tajs = /home/tajs-user/tajs

For generation of log files for soundness testing, TAJS needs to know the locations ofgraalVmNode,node orjjs:

graalVmNode = /usr/graalvm/bin/nodenode = /usr/bin/nodejsjjs = /usr/bin/jjs

(On Windows, the paths are something likeC:/Program Files/nodejs/node.exe andC:/Program Files/Java/jdk1.8.0_131/bin/jjs.exe.)

IfgraalVmNode is defined, the log file will be generated using NodeProf. Otherwisenode needs to be defined and it will then be used with Jalangi to generate the log file.

jjs is only needed if using Nashorn as generator environment instead of Node.js, which can be set programmatically in the soundness tester options.

The directorytest contains a collection of tests that can be executed by runningdk.brics.tajs.test.RunFast with JUnit from Eclipse/IntelliJ or withant test-fast from the command-line.(A more thorough but slower test located indk.brics.tajs.test.RunAll can be run withant test-all.)

See thejsdelta package for how to usejsdelta with TAJS.

This software includes components from:

• Google Closure Compiler (https://closure-compiler.github.io//)
• Jericho HTML Parser (http://jericho.htmlparser.net/)
• Log4j (http://logging.apache.org/log4j)
• args4j (http://args4j.kohsuke.org/)
• Gson (https://github.com/google/gson)
• JUnit (http://junit.org/) (for development only)
• Jetty (http://www.eclipse.org/jetty/) (forTAJS Inspector only)

This diagram shows the main package source code dependencies:

dk.brics.tajs.test.PackageDependencyTest can be used for checking the package dependencies.

The following people have contributed to the source code:

• Anders Møller
• Esben Andreasen
• Simon Holm Jensen
• Peter Thiemann
• Magnus Madsen
• Matthias Diehn Ingesman
• Peter Jonsson
• Benjamin Barslev Nielsen
• Christoffer Quist Adamsen
• Gianluca Mezzetti
• Martin Torp
• Simon Gregersen
• Oskar Haarklou Veileborg