maam

Monadic Abstracting Abstract Machines (MAAM) built on Galois Transformers.

Monadic Abstracting Abstract Machines (MAAM) built on Galois Transformers. See "Galois Transformers and Modular Abstract Interpreters" by Darais, Might and Van Horn.

Building and Running

I recommend building with a cabal sandbox. To initialize a cabal sandbox (that will live in the current directory) and install needed dependencies, run:

make sandbox

I have not included dependency bounds in my cabal file. Should you have trouble finding appropriate bounds, here are the versions of ghc and cabal packages that I am using.

base=4.8.1.0
containers=0.5.6.2
template-haskell=2.10.0.0
text=1.2.1.3
vector=0.11.0.0

Running

To run the project, displaying three different sets of analysis results for a small example, run:

cabal run

Example output is included at the end of this README.

Source Code

All code is in src/.

DISCLAIMERS:

• The analyses implemented in Lang.LamIf are not optimized for efficiency but their performance is reasonable. However, the pretty printing of results can be very expensive due to a naive pretty printing algorithm that I'm using.
• The prelude replacement that I'm using is non-standard, and also uses lots of unicode. I plan on writting an ASCII compatibility layer at some point.

FP

FP is a core functional programming library which replaces the standard Prelude. FP includes more batteries for things like functors, monads, monad transformers, lenses, pretty printing, parsing, deriving, and more. On the downside, it is non-idiomatic at parts and isn't as mature (i.e. debugged and stable).

MAAM

MAAM is a semantics-independent library for building abstract interpreters, while also making it easy to change the path and flow sensitivity of the interpreter.

MAAM only contains types and definitions which are specific to analysis in general. Because the monad transformers that capture path and flow sensitivity are fully general purpose, they are defined in FP.Prelude.Monads and FP.Prelude.Effects, not here. The same goes for lattice structures, which are mostly all defined in FP.Prelude.Lattice. If I were to port MAAM to use the standard Prelude, I would need to rip out maybe 50% of FP.Prelude to be packaged alongside it.

The only code that ends up being specific to analysis is the mapping from monadic actions to state space transition systems, which is defined in MAAM.GaloisTransformer.

LamIf

Lang.LamIf implements the following for a small applied lambda calculus with booleans and if-statements:

• Syntax syntax (Lang.LamIf.Syntax)
• Parsing (Lang.LamIf.Parser)
• Syntax annotations (Lang.LamIf.Stamp)
• Semantic values (Lang.LamIf.Values)
• Abstract time (Lang.LamIf.Time)
• Monadic semantics (Lang.LamIf.Semantics)
• Concrete and abstract value domains (Lang.LamIf.Domains)
• Instantiations of language-independent monads from MAAM (Lang.LamIf.Monads)
• Execution of analyses (Lang.LamIf.Execution)
• Example analyses (Lang.LamIf.Examples)

Example Output

If you execute the project it will compute three different abstract interpretations of a very small program. The variations in path and flow sensitivity are implemented by rearranging the monad transformers used to construct the analysis monad.

program
  0: let x := (1 + 1) - 1 in
  1: let n := (if0 x then x else 1) in
  2: let m := (if0 x then x else 1) in
  3: let r := (if0 x then n + m else 0) in r
zcfa flow insensitive
{ x ↦ {AInt 0,ANotZero,AAnyInt,ABot}
, n ↦ {AInt 0,AInt 1,ANotZero,AAnyInt,ABot}
, m ↦ {AInt 0,AInt 1,ANotZero,AAnyInt,ABot}
, r ↦ {AInt 0,APos,AZero,ANotZero,AAnyInt,ABot}
}
zcfa flow sensitive
{ x ↦ {AInt 0,ANotZero,AAnyInt}
, n ↦ {AInt 0,AInt 1}
, m ↦ {AInt 0}
, r ↦ {APos,AZero}
}
zcfa path sensitive
{ x ↦ {AInt 0,ANotZero,AAnyInt}
, n ↦ {AInt 0,AInt 1}
, m ↦ {AInt 0}
, r ↦ {AZero}
}