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}
}
