## SSTG
Haskell Symbolic Execution with STG Semantics

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

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

[paper]: http://community.haskell.org/~simonmar/papers/evalapplyjfp06.pdf

## 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][stgsyn] as a near one-to-one translation of an internal language called [SSTG Lang][sstglang].

[stgsyn]: https://downloads.haskell.org/~ghc/8.0.1/docs/html/libraries/ghc-8.0.1/StgSyn.html
[sstglang]: https://github.com/AntonXue/SSTG/blob/master/src/SSTG/Core/Syntax/Language.hs

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? :)