SSTG-0.1.0.9: README.md

## 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`

## Installation with Cabal
`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 [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 `[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 :: Binding -> String
```

#### Defunctionalization
[Defunctionalization Wikipedia article][defunctionalization]

[defunctionalization]: https://en.wikipedia.org/wiki/Defunctionalization

#### Symbolic Execution
Symbolic execution is done by performin a series of graph reductions on a `State` until we reach some value form, or our `step_count` tick runs out, creating a form of bounded execution exploration.

To load a `State`, two functions can be used:
```
data LoadResult = LoadOkay State | LoadGuess State [Binding] | LoadError String

newtype Program = Program [Binding]

loadState :: Program -> LoadResult

loadStateEntry :: String -> Program -> LoadResult
```
Next we have to fill out the flags for execution:
```
data StepType = BFS | BFSLogged | DFS | DFSLogged

data RunFlags = RunFlags { step_count :: Int
                         , step_type  :: StepType
                         , dump_dir   :: Maybe FilePath }
```
Here `step_count` is the number of steps we may take, the `step_type` is currently only implemented for `BFS` and `BFSLogged`, the latter of which keeps track of every step taken, while `BFS` only returns the very last state. Note that `BFSLogged` is currently unoptimized because it is easy to implement that way :)

Finally, to perform execution, the `execute` function is used:
```
execute :: RunFlags -> State -> [([LiveState], [DeadState])]
```
This yields a list of execution snapshots. The list is a singleton list if `BFS` or `DFS` is used, while multiple snapshots if the `BFSLogged` or `DFSLogged` is done. These can be then printed by using `pprLivesDeadsStr`:
```
pprLivesDeadsStr :: ([LiveState], [DeadState]) -> String
```

#### Constraint Solving
To come.

## TODO List
* Defunctionalization pre-processing
* SMT integration

## Shortcomings
* 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? :)