Commit 627882f3 authored by Sven Keidel's avatar Sven Keidel

switch from cabal files to hpack

parent 9637f00d
......@@ -5,5 +5,6 @@
/.idea
.DS_Store
cabal.config
*.cabal
cabal.project.local
.ghc.environment.*
name: sturdy-lib
version: 0.1.0.0
synopsis: A library for creating sound static analyses
maintainer: Sven Keidel <svenkeidel@gmail.com>
license: BSD3
github: svenkeidel/sturdy
category: Language
dependencies:
- base
- containers
- hashable
- mtl
- random
- text
- unordered-containers
flags:
trace:
description: Enable tracing of the abstract intepreter
default: False
manual: True
library:
ghc-options: -Wall
source-dirs:
- src
when:
- condition: flag(trace)
cpp-options: -DTRACE
tests:
spec:
main: Spec.hs
source-dirs:
- test
dependencies:
- hspec
- sturdy-lib
......@@ -36,8 +36,6 @@ import qualified Data.Abstract.Widening as W
import Data.Abstract.StackWidening (StackWidening)
import qualified Data.Abstract.StackWidening as SW
#define TRACE
#ifdef TRACE
import Debug.Trace
import Text.Printf
......@@ -124,7 +122,7 @@ memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,inCache), o
(x',stack') = runState (stackWidening x) stack
(outCache'',y) <- f (stackWidening,widening) -< (((stack',inCache), outCache'),x')
let outCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y outCache''
let y' = outCache''' M.! x'
y' = fromJust (M.unsafeLookup x' outCache''')
returnA -< (outCache''',y')
#else
......@@ -150,7 +148,7 @@ memoize (FixT f) = FixT $ \(stackWidening,widening) -> proc (((stack,inCache), o
(x',stack') = runState (stackWidening x) stack
(outCache'',y) <- f (stackWidening,widening) -< trace (printf "CALL: %s" (show x')) (((stack',inCache), outCache'),x')
let outCache''' = M.unsafeInsertWith (flip (T.widening widening)) x' y outCache''
y' = fromMaybe (error "x not in cache") (M.unsafeLookup x outCache''')
y' = fromJust (M.unsafeLookup x' outCache''')
returnA -< trace (printf "CACHE: %s := (%s -> %s)\n" (show x) (show y) (show y') ++
printf "RET: %s -> %s" (show x') (show y'))
(M.unsafeInsertWith (flip (T.widening widening)) x y outCache'',y')
......
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveGeneric #-}
module Control.Arrow.Transformer.Abstract.LiveVariables where
import Prelude hiding (id,(.),read)
import Control.Category
import Control.Arrow
import Control.Arrow.Alloc
import Control.Arrow.Conditional
import Control.Arrow.Environment
import Control.Arrow.Except
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Lift
import Control.Arrow.Random
import Control.Arrow.Reader
import Control.Arrow.Store
import Control.Arrow.Writer
import Control.Arrow.Transformer.Writer
import Data.Identifiable
import Data.Hashable
import Data.Order
import Data.Semigroup
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Abstract.DiscretePowerset as P
-- | Transition function for live variables
newtype LiveVars v = LiveVars (Pow v -> Pow v)
vars :: LiveVars v -> Pow v
vars (LiveVars f) = f P.empty
instance Show v => Show (LiveVars v) where
show = show . vars
instance Hashable v => Hashable (LiveVars v) where
hashWithSalt salt = hashWithSalt salt . vars
instance Eq v => Eq (LiveVars v) where
lv1 == lv2 = vars lv1 == vars lv2
instance Identifiable v => PreOrd (LiveVars v) where
lv1 lv2 = vars lv1 vars lv2
instance Identifiable v => Complete (LiveVars v) where
LiveVars f LiveVars g = LiveVars (\lv -> f lv g lv)
live :: Identifiable v => v -> LiveVars v
live x = LiveVars $ P.insert x
dead :: Identifiable v => v -> LiveVars v
dead x = LiveVars $ P.delete x
-- | Composing two transition functions
instance Semigroup (LiveVars v) where
(<>) = mappend
instance Monoid (LiveVars v) where
mempty = LiveVars id
mappend (LiveVars f) (LiveVars g) = LiveVars (f . g)
-- | An arrow transformer that tracks the live variables.
newtype LiveVariables v c x y = LiveVariables (Writer (LiveVars v) c x y)
runLiveVariables :: LiveVariables v c x y -> c x (LiveVars v,y)
runLiveVariables (LiveVariables f) = runWriter f
instance (Identifiable var, ArrowRead (var,lab) val x (LiveVars var,y) c)
=> ArrowRead (var,lab) val x y (LiveVariables var c) where
read (LiveVariables f) (LiveVariables g) = LiveVariables $ proc ((var,lab),x) -> do
tell -< live var
read f g -< ((var,lab),x)
instance (Identifiable var, ArrowWrite (var,lab) val c) => ArrowWrite (var,lab) val (LiveVariables var c) where
write = LiveVariables $ proc ((var,lab),val) -> do
tell -< dead var
write -< ((var,lab),val)
type instance Fix x y (LiveVariables v c) = LiveVariables v (Fix x (LiveVars v,y) c)
deriving instance (ArrowFix x (LiveVars v,y) c) => ArrowFix x y (LiveVariables v c)
deriving instance ArrowLift (LiveVariables v)
instance (ArrowApply c) => ArrowApply (LiveVariables v c) where
app = LiveVariables ((\(LiveVariables f,x) -> (f,x)) ^>> app)
deriving instance (Arrow c) => Category (LiveVariables v c)
deriving instance (Arrow c) => Arrow (LiveVariables v c)
deriving instance (ArrowChoice c) => ArrowChoice (LiveVariables v c)
deriving instance (ArrowReader r c) => ArrowReader r (LiveVariables v c)
deriving instance (ArrowFail e c) => ArrowFail e (LiveVariables v c)
deriving instance (ArrowExcept x (LiveVars v,y) e c) => ArrowExcept x y e (LiveVariables v c)
-- deriving instance (ArrowState s c) => ArrowState s (LiveVariables v c)
deriving instance ArrowAlloc x y c => ArrowAlloc x y (LiveVariables v c)
deriving instance ArrowRand r c => ArrowRand r (LiveVariables v c)
deriving instance ArrowCond val x y (LiveVars v,z) c => ArrowCond val x y z (LiveVariables v c)
deriving instance ArrowEnv x y env c => ArrowEnv x y env (LiveVariables v c)
deriving instance PreOrd (c x (LiveVars v,y)) => PreOrd (LiveVariables v c x y)
deriving instance LowerBounded (c x (LiveVars v,y)) => LowerBounded (LiveVariables v c x y)
deriving instance Complete (c x (LiveVars v,y)) => Complete (LiveVariables v c x y)
deriving instance CoComplete (c x (LiveVars v,y)) => CoComplete (LiveVariables v c x y)
deriving instance UpperBounded (c x (LiveVars v,y)) => UpperBounded (LiveVariables v c x y)
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Arrow.Transformer.Compose where
import Control.Category
import Control.Arrow
import Control.Arrow.Trans
import Control.Arrow.Fix
import Data.Order
newtype IdentityT c x y = IdentityT {runIdentityT :: c x y}
deriving (Category,Arrow,ArrowChoice,PreOrd,Complete)
instance ArrowTrans IdentityT where
type Dom1 IdentityT x y = x
type Cod1 IdentityT x y = y
lift = IdentityT
unlift = runIdentityT
instance ArrowApply c => ArrowApply (IdentityT c) where
app = lift $ first unlift ^>> app
instance ArrowFix x y c => ArrowFix x y (IdentityT c) where
fix = liftFix
newtype ComposeT
(s :: (* -> * -> *) -> (* -> * -> *))
(t :: (* -> * -> *) -> (* -> * -> *))
(c :: * -> * -> *) (x :: *) (y :: *)
= ComposeT { runComposeT :: (s (t c)) x y }
type (:*:) = ComposeT
instance (ArrowTrans s,ArrowTrans t) => ArrowTrans (ComposeT s t) where
type Dom1 (ComposeT s t) x y = Dom1 t (Dom1 s x y) (Cod1 s x y)
type Cod1 (ComposeT s t) x y = Cod1 t (Dom1 s x y) (Cod1 s x y)
lift = undefined
unlift = undefined
(*:) :: ComposeT s t c x y -> s (t c) x y
(*:) = runComposeT
name: sturdy-lib
version: 0.1.0.0
-- synopsis:
description: A library for abstract interpretation
license: BSD3
license-file: LICENSE
author: Sven Keidel
maintainer: svenkeidel@gmail.com
-- copyright:
category: Language
build-type: Simple
extra-source-files:
cabal-version: >=1.10
flag trace
Description: Enable tracing
Default: False
library
ghc-options: -Wall
if flag(trace) {
cpp-options: -DTRACE
}
exposed-modules:
Data.Boolean,
Data.Monoidal,
Data.GaloisConnection,
Data.Identifiable,
Data.Label,
Data.Numeric,
Data.Order,
Data.Utils,
Data.CallString,
Data.Concrete.Boolean,
Data.Concrete.Error,
Data.Concrete.Failure,
Data.Concrete.Powerset,
Data.Abstract.Either,
Data.Abstract.Equality,
Data.Abstract.Ordering,
Data.Abstract.Boolean,
Data.Abstract.Failure,
Data.Abstract.Error,
Data.Abstract.InfiniteNumbers,
Data.Abstract.FiniteMap,
Data.Abstract.FreeCompletion,
Data.Abstract.Interval,
Data.Abstract.Maybe,
Data.Abstract.Powerset,
Data.Abstract.DiscretePowerset,
Data.Abstract.Sign,
Data.Abstract.Map,
Data.Abstract.Terminating,
Data.Abstract.There,
Data.Abstract.Widening,
Data.Abstract.StackWidening,
Control.Arrow.Alloc,
Control.Arrow.Const,
Control.Arrow.Conditional,
Control.Arrow.Deduplicate,
Control.Arrow.Environment,
Control.Arrow.Fail,
Control.Arrow.Except,
Control.Arrow.Fix,
Control.Arrow.Random,
Control.Arrow.Reader,
Control.Arrow.State,
Control.Arrow.Store,
Control.Arrow.Trans,
Control.Arrow.Writer,
Control.Arrow.Utils,
Control.Arrow.Abstract.Join,
Control.Arrow.Transformer.Reader,
Control.Arrow.Transformer.State,
Control.Arrow.Transformer.Writer,
Control.Arrow.Transformer.Cont,
Control.Arrow.Transformer.Const,
Control.Arrow.Transformer.Static,
Control.Arrow.Transformer.Concrete.Environment,
Control.Arrow.Transformer.Concrete.Except,
Control.Arrow.Transformer.Concrete.Failure,
Control.Arrow.Transformer.Concrete.Fixpoint,
Control.Arrow.Transformer.Concrete.Store,
Control.Arrow.Transformer.Concrete.Random,
Control.Arrow.Transformer.Concrete.Trace,
Control.Arrow.Transformer.Abstract.Completion,
Control.Arrow.Transformer.Abstract.Environment,
Control.Arrow.Transformer.Abstract.Contour,
Control.Arrow.Transformer.Abstract.BoundedEnvironment,
Control.Arrow.Transformer.Abstract.Failure,
Control.Arrow.Transformer.Abstract.Except,
-- Control.Arrow.Transformer.Abstract.GreatestFixPoint,
Control.Arrow.Transformer.Abstract.Fixpoint,
Control.Arrow.Transformer.Abstract.Powerset,
Control.Arrow.Transformer.Abstract.Store,
Control.Arrow.Transformer.Abstract.ReachingDefinitions
-- Control.Arrow.Transformer.Abstract.LiveVariables
build-depends: base,
containers,
hashable,
mtl,
random,
text,
unordered-containers
hs-source-dirs: src/
default-language: Haskell2010
test-suite specs
type: exitcode-stdio-1.0
ghc-options: -Wall
hs-source-dirs: test
main-is: Spec.hs
build-depends: base,
hspec,
sturdy-lib,
hashable,
unordered-containers,
text
other-modules: FiniteMapSpec,
FixSpec,
MapSpec,
TraceSpec
default-language: Haskell2010
name: sturdy-pcf
version: 0.1.0.0
license: BSD3
maintainer: Sven Keidel <svenkeidel@gmail.com>
category: Language
dependencies:
- base
- hashable
- mtl
- sturdy-lib
- text
- transformers
- unordered-containers
library:
source-dirs:
- src
ghc-options: -Wall
tests:
spec:
main: Spec.hs
source-dirs:
- test
ghc-options: -Wall
dependencies:
- sturdy-pcf
- hspec
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveGeneric #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module SignAnalysis where
import Prelude hiding (id)
import Control.Category
import Control.Arrow
import Control.Arrow.Fail
import Control.Arrow.Fix
import Control.Arrow.Environment
import Data.Error
import Data.Foldable (toList)
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Hashable
import Data.Order
import Data.Powerset
import qualified Data.Sign as Sign
import Data.Sign hiding (Bot,Top)
import Data.Text (Text)
import Data.Store (Store)
import GHC.Generics
import PCF (Expr)
import Shared
data Closure = Closure Text Expr Env deriving (Eq,Show,Generic)
data Val = Bot | NumVal Sign | ClosureVal (Pow Closure) | Top deriving (Eq,Show,Generic)
type Env = M.HashMap Text Addr
type Addr = Text
type Interp = BoundedEnv Text Addr Val (ErrorArrow String (CacheArrow (HashMap Text Addr, Store Addr Val, Expr) (Error String (Store Addr Val, Val))))
instance LowerBounded String where
bottom = "Program might not terminate"
evalSign :: HashMap Text Val -> Expr -> Error String Val
evalSign env e = runCacheArrow (runErrorArrow (runBoundedEnv eval)) (alloc,env,e)
where alloc = id
instance IsVal Val Interp where
succ = proc s -> case s of
NumVal n -> returnA -< NumVal (n+1)
_ -> failA -< "Expected a number as argument for 'succ'"
pred = proc s -> case s of
NumVal n -> returnA -< NumVal (n-1)
_ -> failA -< "Expected a number as argument for 'pred'"
zero = arr $ const (NumVal 0)
ifZero f g = proc (v1, (x, y)) -> case v1 of
NumVal Zero -> f -< x
NumVal Sign.Top -> (f -< x) (g -< y)
NumVal _ -> g -< y
_ -> failA -< "Expected a number as condition for 'ifZero'"
instance IsClosure Val Env Interp where
closure = arr $ \(x, e, env) -> ClosureVal (return (Closure x e env))
applyClosure f = proc (fun, arg) -> case fun of
ClosureVal cls -> lubA (proc (Closure x body env) -> do
env' <- extendEnv -< (x,arg,env)
localEnv f -< (env', body))
-<< toList cls
_ -> failA -< "Expected a closure"
instance PreOrd Val where
Bot _ = True
_ Top = True
NumVal n1 NumVal n2 = n1 n2
ClosureVal c1 ClosureVal c2 = c1 c2
_ _ = False
instance LowerBounded Val where
bottom = Bot
instance Complete Val where
Bot y = y
x Bot = x
Top _ = Top
_ Top = Top
NumVal x NumVal y = NumVal (x y)
ClosureVal x ClosureVal y = ClosureVal (x y)
_ _ = Top
instance Hashable Closure
instance Hashable Val
name: sturdy-pcf
version: 0.1.0.0
license: BSD3
license-file: LICENSE
author: Sven Keidel
maintainer: s.keidel@tudelft.nl
category: Language
build-type: Simple
extra-source-files:
cabal-version: >=1.10
library
ghc-options: -Wall
exposed-modules: Syntax,
GenericInterpreter,
ConcreteInterpreter,
IntervalAnalysis
-- SignAnalysis
build-depends: base,
hashable,
mtl,
sturdy-lib,
text,
transformers,
unordered-containers
hs-source-dirs: src
default-language: Haskell2010
test-suite specs
type: exitcode-stdio-1.0
ghc-options: -Wall
hs-source-dirs: test
main-is: Spec.hs
other-modules: ConcreteSpec,
IntervalAnalysisSpec,
SignAnalysisSpec,
SharedSpecs
build-depends: base,
hspec,
mtl,
sturdy-lib,
sturdy-pcf,
unordered-containers,
text
default-language: Haskell2010
......@@ -15,8 +15,8 @@ import Pretty.Results
import Paths_sturdy_stratego
import qualified Criterion.Measurement as CM
import qualified Criterion.Types as CT
import qualified Criterion as CM
import qualified Criterion as CT
import Data.ATerm
import Data.Abstract.Error
......@@ -35,7 +35,6 @@ import Text.Printf
-- | Runs the case studies.
main :: IO ()
main = do
CM.initializeTime
prettyPrint H.ppHaskell =<< caseStudy (W.eval 5) "arrows" "desugar_arrow_0_0"
prettyPrint H.ppHaskell =<< caseStudy (W.eval 5) "cca" "norm_0_0"
prettyPrint P.ppPCF =<< caseStudy (W.eval 5) "arith" "eval_0_0"
......@@ -51,11 +50,6 @@ prettyPrint pprint res =
then print $ ppResults pprint (toList res)
else printf "Output ommited because the result set contains %d elements\n" (H.size res)
measure :: String -> IO () -> IO ()
measure analysisName action = do
(m,_) <- CM.measure (CT.nfIO action) 1
printf "- %s: %s\n" analysisName (CM.secs (CT.measCpuTime m))
-- | Runs the given semantics on the given function within the given
-- case study.
caseStudy :: (Strat -> StratEnv -> W.TermEnv -> W.Term -> Terminating (W.Pow (F.Failure String (Error () (W.TermEnv,W.Term))))) -> String -> String -> IO (HashSet W.Term)
......@@ -68,7 +62,7 @@ caseStudy eval name function = do
let res = fromTerminating (error "non-terminating wildcard semantics") $ eval (Call (fromString function) [] []) (stratEnv module_) S.empty W.Wildcard
let terms = H.fromList $ toList $ filterResults (toList res)
_ <- CM.measure (CT.nfIO (return terms)) 1
CT.benchmark (CT.nfIO (return terms))
return terms
where
filterResults = fmap (\r -> case r of Success (_,t) -> t; SuccessOrFail _ (_,t) -> t; Fail _ -> error "")
......
name: sturdy-stratego
version: 0.1.0.0
license: BSD3
maintainer: Sven Keidel <svenkeidel@gmail.com>
category: Language
dependencies:
- base
- attoparsec
- containers
- deepseq
- fgl
- hashable
- mtl
- sturdy-lib
- text
- transformers
- tree-automata
- unordered-containers
- QuickCheck
library:
source-dirs:
- src
ghc-options: -Wall -O2 -fprof-auto
executables:
case-studies:
source-dirs:
- case-studies
main: Main.hs
dependencies:
- sturdy-stratego
- pretty
- vector
- criterion
tests:
spec:
main: Spec.hs
source-dirs:
- test
dependencies:
- hspec
- sturdy-stratego
{-# LANGUAGE Arrows #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
module AbstractTypedSemantics where
import Prelude hiding (fail)
import InterpreterArrow
import WildcardSemantics hiding (Term(..),TermEnv)
import Sort
import Signature
import qualified Signature as Sig
import Syntax(Strat,StratEnv,Module,signature,stratEnv)
import Utils
import Control.Arrow hiding ((<+>))
import Control.Arrow.Append
import Control.Arrow.Try
import Data.Constructor
import Data.Hashable
import Data.Order hiding (lub)
import Data.PowersetResult
import qualified Data.Term as T
import Data.Term(HasTerm(..),TermF)
import Data.TermEnv
import Data.Text(Text,pack)
import Data.TypedResult(TypeError(..))
import Data.Complete (Complete)
import qualified Data.Complete as C
import Text.Printf
data Term
= Cons Constructor [Term] Sort
| StringLiteral Text
| NumberLiteral Int
| Wildcard Sort
deriving (Eq)
type TermEnv = AbstractTermEnv Term
evalModule :: Int -> Module -> Strat -> (Term,TermEnv) -> PowersetResult (Term,TermEnv)
evalModule i module_ = eval i (signature module_) (stratEnv module_)
eval :: Int -> Signature -> StratEnv -> Strat -> (Term,TermEnv) -> PowersetResult (Term,TermEnv)
eval i sig senv s = runInterp (eval' i s) (sig, senv)
instance HasTerm Term (Interp (Signature,senv) s PowersetResult) where
matchTerm = proc t -> case t of
Cons c ts _ -> returnA -< T.Cons c ts
StringLiteral s -> returnA -< T.StringLiteral s
NumberLiteral n -> returnA -< T.NumberLiteral n
Wildcard _ -> returnA -< T.Wildcard
matchTermRefine = proc t -> case t of
Wildcard Top -> returnA -< T.Wildcard
Wildcard (Option s) ->
alternatives -< [T.Cons "None" [], T.Cons "Some" [Wildcard s]]
Wildcard (List s) ->
alternatives -< [T.Cons "Nil" [], T.Cons "Cons" [Wildcard s