Home

This project is an experimental implementation of a generic library to construct control-flow analyses for abstract collecting semantics on top of different abstract machines.

The constructed analyses can feature Abstract Garbage Collection, counting, shared or per-state store, different variants of context-sensitivity depending on a used underlying monad and particular implementation of analysis-specific type-classes.

Prerequisites to run the examples

We assume Glasgow Haskell Compiler (GHC) version 7.2 or newer is installed in the system.

Examples

The following commands should be executed from the project root.

ex is usually an implicitly imported simple program to test the analyses in the appropriate calculus, unless it is said otherwise.

The actual code is self-explanatory and can be found in the appropriate example files and companion utility modules.

Concrete collecting semantics for CPS

1. ghci CFA/CPS/Examples/Concrete.hs
2. concreteResult ex

Abstract collecting semantics for CPS with per-state store and Garbage Collection

1. ghci CFA/CPS/Examples/AbstractNonShared.hs
2. nonSharedResultC ex

Abstract collecting semantics for CPS with per-state store, Garbage Collection and counting

1. ghci CFA/CPS/Examples/AbstractNonSharedCount.hs
2. abstractResultC ex

Abstract collecting semantics for CPS with shared store

1. ghci CFA/CPS/Examples/AbstractShared.hs
2. abstractResultSSC ex

Abstract collecting semantics for CPS with shared store and counting

1. ghci CFA/CPS/Examples/AbstractSharedCount.hs
2. abstractResultSSC ex

Concrete collecting semantics for Lambda-CESK

1. ghci CFA/CESK/Examples/Concrete.hs
2. concreteResult ex

Abstract collecting semantics for Lambda-CESK with per-state store

1. ghci CFA/CESK/Examples/AbstractNonShared.hs
2. abstractResult ex

Abstract collecting semantics for ANF Featherweight Java with per-state store

1. ghci CFA/AFJ/Examples/AbstractNonShared.hs
2. abstractResult ctable mainVars mainStmts

Building

To build the library, make sure that the Glasgow Haskell Compiler is installed in your system.

To build the whole project, execute from the project root:

make all

To remove generated binaries:

make clean

Warning

Last time this code was tested, the examples above worked fine only if the code hasn't been built before via make (otherwise some symbols are reported missing at the runtime).

If you intend to run the examples in the interactive mode, make sure you have run make clean before. We hope to fix this minor issue soon.

License

The sources are released under CRAPL license.

If you have questions or concerns about the CRAPL, or you need more information about this license, please contact Prof. Matthew Might.