SSTG: STG Symbolic Execution

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

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

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