@hackage SSTG0.1.0.6

SSTG

Haskell Symbolic Execution with STG Semantics

Based on the paper: Making a Fast Curry: Push/Enter vs. Eval/Apply for Higher-order Languages

Hackage Page: https://hackage.haskell.org/package/SSTG

Dependencies

• ghc >= 8.0.1

Install

cabal install SSTG

As an API

SSTG is designed for use as an API to perform extraction and symbolic execution of models extracted from Haskell source, curated by hand, or derived from other sources.

import SSTG

Program Model Extraction

SSTG represents GHC StgSyn as a near one-to-one translation of an internal language called SSTG Lang.

This can be extracted from Haskell source by performing a call to the function:

mkTargetBindings :: FilePath -> FilePath -> IO [SSTG.Binding]
mkTargetBinding proj src = ...

Here proj denotes the project directory, while src respresents the source file. This enables compilation of multiple Haskell files simultaneously, as GHC requires reference paths to a common project directory for compilation accuracy.

In a given file structure as follows:

path/to/stuff/
  +-- project/
        +-- folder-one/
              +-- source.hs

The corresponding proj and src would be equivalent to:

proj = path/to/stuff
src  = path/to/stuff/folder-one/source.hs

The extracted [SSTG.Binding], like almost everything in SSTG, is endowed with Show, Equal, Read. However, it is advised to use the pretty-print functions defined in SSTG.Utils.Printing. For instance:

pprBindingStr :: SSTG.Binding -> String

Defunctionalizatoin

Symbolic Execution

Constraint Solving

To come.

TODO List

• Defunctionalization pre-processing
• SMT integration

Shortcommings

• Uninterpreted function evaluations are abstracted as symbolic computations. This includes all functions defined in Prelude and those not defined in the scope of the target programs.
• There might be bugs, who knows? :)