Hackage :: [Package]

SSTG: STG Symbolic Execution

[ bsd3, library, program, web ] [ Propose Tags ] [ Report a vulnerability ]
Versions [RSS] 0.1.0.1, 0.1.0.2, 0.1.0.3, 0.1.0.4, 0.1.0.5, 0.1.0.6, 0.1.0.7, 0.1.0.8, 0.1.0.9, 0.1.1.0, 0.1.1.1, 0.1.1.2, 0.1.1.3, 0.1.1.4, 0.1.1.5, 0.1.1.6, 0.1.1.7
Dependencies base (>=4.7 && <5), containers (>=0.5 && <0.6), ghc, ghc-paths, SSTG [details]
License BSD-3-Clause
Copyright 2017 Anton Xue
Author Anton Xue
Maintainer anton.xue@yale.edu
Category Web
Home page https://github.com/AntonXue/SSTG#readme
Source repo head: git clone https://github.com/AntonXue/SSTG
Uploaded by AntonXue at 2017-07-26T12:52:32Z
Distributions
Executables SSTG-exe
Downloads 12047 total (18 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2017-07-26 [all 1 reports]

Readme for SSTG-0.1.0.5

[back to package description]

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