search

softwarelanguageslab / maf

Static Analysis Framework for Modular Analyses
Other
13 stars 12 forks source link

readme

Modular Analysis Framework (MAF): A Framework for Modular Analysis of Dynamic Languages

Goal

The goal of this artefact is to experiment with abstract machines and language semantics. Currently, the artefact's implementation is focused towards experiments with modular analyses. These are build according to the ModX technique. A comparison on how our ModF analysis compares to a well-known AAM-style analysis is described here.

Additionally, semantics for R5RS Scheme are present. Note that the semantics of our implementation may deviate from the R5RS specification at certain points; these have been described here.

For more information on the incremental analyses that are currently developed using MAF, see here.

Usage

The MAF framework can be used in several ways.

Using the JavaScript visual front-end

The framework includes a JavaScript front-end that can be used to visualise a modular analysis in the browser. Before the visualisation can be run, you have to ensure the code is compiled, by executing the commands fastOptJS ( or fullOptJS) in your sbt repl.

The MAF framework currently provides a standard visualisation for modular analyses, as well as specific visualisations that correspond to several different flavours of the analysis (e.g., adaptive or incremental analyses.)

To run the standard visualisation, open the file standard.html in the web folder with your browser. The visualisation provides information with regard to the work list (coloured in light blue) and currently analysed component (coloured in dark blue). Stepping through the visualisation can be done using the space bar. The other visualisations are also accessible via the web folder.

Analysing a program using command line

The MAF framework is built in a modular style. To run a modular analysis, you need to compose the implementation of a specific machine and an abstract domain.

To analyze a specific program, an instance of the ModF analysis class must be created. The constructor of this class takes a parsed version of the program to be analysed, which can be obtained as follows:

val text = io.Reader.loadFile(path-to-file)
val prog = language.scheme.Schemeparser.parse(text)

Additional preprocessing steps are performed by the modular analysis itself and hence must not be performed manually.

Now, the ModF instance can be created. For example, to analyze prog using a big-step ModF analysis with full argument sensitivity and a type domain:

val analysis = new ModAnalysis(prog) with BigStepSemantics
                                     with StandardSchemeModFSemantics
                                     with FullArgumentSensitivity
                                     with TypePropagationDomain
analysis.analyze()

Method analyze computes the full (and sound) analysis result for the program that ModAnalysis is constructed with. This method does not return the analysis results directly. Rather, after calling analyze, the computed analysis results (e.g., the final store and dependencies) can be accessed through the properties of the analysis object (e.g., through analysis.store and analysis.deps).

Alternatively, one can use the analyzeWithTimeout(<timeout>) method to run the analysis with a given timeout. This timeout is obtained from a Java Duration (using Timeout.start(<duration>)). The method returns when either the analysis has terminated or when the timeout has been reached (approximately, meaning in practice it may run a bit longer than the specified timeout). Extra care should be taken when using this method, as the (partial) analysis results are not guaranteed to be sound when the timeout is triggered. Therefore, when using this method, it is recommended to explicitly check afterwards if the analysis terminated using the finished method.

Running the test suite

This repository is monitored by a CI-system. Upon every push and pull request to this repository, the test suite is run on a specific subset of benchmark programs (MAF tests on action). In addition, the full test suite is run over night (Daily MAF tests).

Current status:

Latest build Nightly tests Daily Incremental MAF tests Incremental MAF tests on action

The full test suite of MAF can easily be run manually using sbt:

maf/test

To allow specific tests to be run, tags have been added to the test suite.

The SlowTest tag currently is only used for some of the soundness tests. When these tests are disabled, only a part of the available benchmark programs will be used.

To run tests with a specific tag, the sbt command maf/testOnly should be used. The -n flag indicates test tags that should be included from testing, whereas the -l flag indicates tags that should be excluded from testing.

For example, to run the parser tests, the following command can be used:

maf/testOnly -- -n ParserTest

(Note the double -- before any possible flags.)
To run all soundness tests, but only on a fast subset of benchmark programs, the command

maf/testOnly -- -n SoundnessTest -l SlowTest

can be executed.

References and Relevant publications

The original idea behind MAF comes from the following work on modular analysis: Effect-Driven Flow Analysis, and A general method for rendering static analyses for diverse concurrency models modular. The MAF framework is presented in the following publication:

MAF is a complete rework of the Scala-AM framework, which was not focused on modular static analysis but was primarily used to experiment with AAM-style analyses. An AAM implementation (inspired by Scala-AM) is provided in MAF for benchmarks comparisons. Scala-AM is described in the following publications:

MAF has been used for evaluating modular static analysis approaches in the following publications:

Scala-AM has been used for evaluating static analysis approaches in the following publications:

Acknowledgements

Many thanks to JProfiler for supporting this open-source project, allowing us to easily identify and resolve performance bottlenecks in our analyses.