Goal

Monarch is the successor of MAF a framework for experimenting with modular static analyses that are based on abstract interpretation. This iteration of the framework focusses on monadic implementations of the so-called "Abstracting Definitional Interpreters" (Darais et al., 2017) technique to static analysis.

MAF focussed on static analyses developed according to the ModX technique. While this current iteration of the framwork still includes an implementation of the algorithms used in this ModX technique, its analyses are not structured in this way. Rather, ModX is viewed as an intelligent worklist algorithm provided as a parameter to the analysis' implementation.

Usage

This section is a work in progress

The framework can be used in a standalone mode by interacting with it through a command line interface. This command line interface currently offers some basic analyses for Scheme and some utilities for testing parsing of Python programs. This CLI is offered by the maf2-analysis package, and can be executed by running cabal run in this package.

Alternatively, the repository can be used as a set of libraries. This usage is illustrated by this package, which implements a simple analysis for the extended lambda calculus. It also contains a suitable cabal configuration to load our set of libraries from this repository through Github's infrastructure.

Structure

The project is structured as a monorepository containing several indepent libraries. The idea behind this structure is to enable re-use of each of the components in our framework, allowing them to be easily used in smaller experiments. The libraries that make up our framework are as follows:

• maf2-domains: this library contains some core abstract domains that are used in our analyses. These abstract domains are underpinned by abstract interpretation theory and are formulated in terms of mathematical lattices.
• maf2-syntax: this library contains syntax parsing and preprocessing facilities for all targets of our analyses. Our analyses currently target Scheme and Python.
• maf2-analysis: this library contains our analyses.

Each library contains additional documentation about their structure and usage in third-party libraries/applications.

References and Relevant publications

The original idea behind ModX 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 previous iteration of the MAF framework is presented in the following publication:

• MAF: A Framework for Modular Static Analysis of Higher-Order Languages. SCAM 2020. pdf. See release: SCAM 2020

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:

• Scala-AM: A Modular Static Analysis Framework. SCAM 2016. pdf , doi.
• Building a Modular Static Analysis Framework in Scala. Scala@SPLASH 2016. pdf , doi.

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

• A Parallel Worklist Algorithm and Its Exploration Heuristics for Static Modular Analyses. Journal of Systems and Software, Volume 181. 2021. pdf, doi.
• A Parallel Worklist Algorithm for Modular Analyses. SCAM 2020. pdf. See release: SCAM 2020
• Incremental Flow Analysis through Computational Dependency Reification. SCAM 2020. pdf. _See release: SCAM 2020
• Summary-Based Compositional Analysis for Soft Contract Verification. SCAM 2022. preprint pdf. git. artifact .

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

• Garbage-Free Abstract Interpretation through Abstract Reference Counting. ECOOP 2019. pdf.
• A general method for rendering static analyses for diverse concurrency models modular. Journal of Systems and Software, Volume 149. 2019. pdf, doi.
• Mailbox Abstractions for Static Analysis of Actor Programs. ECOOP 2017. pdf, doi.
• Employing Run-time Static Analysis to Improve Concolic Execution. BENEVOL 2017. pdf.
• Incrementalizing Abstract Interpretation. BENEVOL 2017. pdf.
• Static taint analysis of event-driven scheme programs. ELS 2017. pdf.
• Improving trace-based JIT optimisation using whole-program information. VMIL@SPLASH 2016. pdf, doi.
• STRAF: A Scala Framework for Experiments in Trace-Based JIT Compilation. GTTSE 2015. pdf, doi.

License

All code in this repository is licensed according to the license provided in the LICENSE file.