Commit aec47aec authored by Katharina Brandl's avatar Katharina Brandl
Browse files

Updated tutoral language to work with new version of sturdy.

parent b8560f72
......@@ -14,4 +14,5 @@ scheme/*.csv
scheme/graph_files/*.png
scheme/graph_files/gabriel/*.png
scheme/graph_files/scala-am/*.png
node_modules/
\ No newline at end of file
node_modules/
*.yaml.lock
......@@ -30,6 +30,10 @@ instance Show Label where
instance Pretty Label where
pretty (Label l) = "#" <> pretty l
instance Enum Label where
toEnum = Label
fromEnum = labelVal
instance PreOrd Label where
() = (==)
......@@ -44,7 +48,25 @@ fresh :: MonadState Label m => m Label
fresh = state (\l -> (l,l+1))
generate :: State Label x -> x
generate m = evalState m 0
generate = generateFrom 0
generateState :: State Label x -> (x, Label)
generateState = generateStateFrom 0
generateFrom :: Label -> State Label x -> x
generateFrom i m = evalState m i
generateStateFrom :: Label -> State Label x -> (x, Label)
generateStateFrom i m = runState m i
generate' :: Monad m => StateT Label m x -> m x
generate' m = evalStateT m 0
generate' = generateFrom' 0
generateState' :: StateT Label m x -> m (x, Label)
generateState' = generateStateFrom' 0
generateFrom' :: Monad m => Label -> StateT Label m x -> m x
generateFrom' i m = evalStateT m i
generateStateFrom' :: Label -> StateT Label m x -> m (x, Label)
generateStateFrom' i m = runStateT m i
......@@ -9,7 +9,7 @@ packages:
- 'while'
# - 'stratego'
- 'jimple'
# - 'tutorial'
- 'tutorial'
allow-newer: true
extra-deps:
- git: https://github.com/svenkeidel/dump-core/
......
name: sturdy-tutorial
version: 0.2.0.0
version: 0.3.0.0
license: BSD3
maintainer: Sven Keidel <svenkeidel@gmail.com>
category: Language
......@@ -9,7 +9,9 @@ dependencies:
- hashable
- mtl
- profunctors
- prettyprinter
- sturdy-lib
- sturdy-arrows
- random
- text
- transformers
......
......@@ -9,6 +9,7 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ImplicitParams #-}
{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-}
-- | This file instantiates the generic interpreter with abstract
-- values to implement the abstract interpreter. All we have to do is
......@@ -16,136 +17,188 @@
-- by the sturdy standard library.
module SturdyStyle.AbstractInterpreter where
import Prelude hiding (Bool(..),lookup,and,fail)
import Prelude hiding (Bool(..),Bounded(..),(/),fail,(.),filter,id)
import qualified Prelude as P
import Syntax
import SturdyStyle.GenericInterpreter(IsValue, ArrowAlloc)
import qualified SturdyStyle.GenericInterpreter as Generic
import Control.Category
import Control.Arrow
import Control.Arrow.Fail as Fail
import Control.Arrow.Fix
import Control.Arrow.Environment
import Control.Arrow.Store
import Control.Arrow.Fail
import Control.Arrow.Alloc
import Control.Arrow.Abstract.Join
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Fix.CallCount(unroll)
import Control.Arrow.Fix.Chaotic(innermost)
import Control.Arrow.Order
import qualified Control.Arrow.Trans as Trans
import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Abstract.Environment
import Control.Arrow.Transformer.Abstract.Error
import Control.Arrow.Transformer.Abstract.Fix
import Control.Arrow.Transformer.Abstract.Fix.CallCount
import Control.Arrow.Transformer.Abstract.Fix.Component
import Control.Arrow.Transformer.Abstract.Fix.Context as Ctx
import Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable
import Control.Arrow.Transformer.Abstract.Fix.Stack
import Control.Arrow.Transformer.Abstract.Store
import Control.Arrow.Transformer.Abstract.Terminating
import Control.Arrow.Transformer.Abstract.Fix
import Data.Abstract.FreeCompletion (FreeCompletion)
import Data.Abstract.Error (Error)
import qualified Data.Abstract.Error as E
import Data.Abstract.Terminating (Terminating)
import qualified Data.Abstract.StrongMap as SM
import qualified Data.Abstract.Map as M
import Data.Profunctor
import Data.Label
import qualified Data.Boolean as B
import Data.Hashable
import Data.Abstract.DiscretePowerset(Pow)
import qualified Data.Lens as L
import Data.Order
import Data.Abstract.Widening(Widening)
import qualified Data.Abstract.Widening as W
import Data.Label
import qualified Data.Lens as L
import Data.Text.Prettyprint.Doc
import Data.Abstract.Boolean (Bool)
import qualified Data.Abstract.Boolean as B
import Data.Abstract.DiscretePowerset (Pow)
import Data.Abstract.Error (Error(..))
import qualified Data.Abstract.Error as E
import Data.Abstract.FreeCompletion(FreeCompletion(..))
import Data.Abstract.InfiniteNumbers
import Data.Abstract.Interval (Interval)
import qualified Data.Abstract.Interval as I
import Data.Abstract.Map (Map)
import qualified Data.Abstract.Map as M
import qualified Data.Abstract.Ordering as O
import qualified Data.Abstract.StrongMap as SM
import Data.Abstract.Terminating (Terminating)
import qualified Data.Abstract.Terminating as T
import qualified Data.Abstract.StackWidening as S
import Data.Abstract.There(There(..))
import Data.Abstract.Stable
import Data.Abstract.Widening (Widening)
import qualified Data.Abstract.Widening as W
import GHC.Exts
import GHC.Exts(IsString(..))
import GHC.Generics
import SturdyStyle.GenericInterpreter(IsValue(..))
import qualified SturdyStyle.GenericInterpreter as Generic
import Syntax
type Addr = FreeCompletion Label
data AbsVal = BoolVal AbsBool | NumVal Interval | TopVal deriving (Show, Eq,Generic)
data AbsBool = True | False | TopBool deriving (Show,Eq,Generic)
data Interval = Interval Int Int deriving (Show,Eq,Generic)
data AbsVal = BoolVal Bool | NumVal IV | TopVal deriving (Show, Eq,Generic)
type IV = Interval (InfiniteNumber Integer)
type Env = SM.Map String Addr
type Store = Map Addr AbsVal
type Errors = Pow String
type In = ((Env,[Statement]),Store)
type Out = Terminating (Error Errors (Store, ()))
instance (IsString e, ArrowChoice c, ArrowJoin c, ArrowFail e c) => IsValue AbsVal (AbstractT c) where
numLit = arr $ \n -> NumVal (Interval n n)
instance (IsString e, ArrowChoice c, ArrowFail e c, Fail.Join AbsVal c,
ArrowComplete AbsVal c)
=> IsValue AbsVal (ValueT AbsVal c) where
type JoinVal z (ValueT AbsVal c) =
(ArrowComplete z (ValueT AbsVal c), Fail.Join z c)
numLit = proc x -> returnA -< NumVal (I.Interval (Number $ toInteger x) (Number $ toInteger x))
add = proc (v1,v2) -> case (v1,v2) of
-- When adding all numbers within two intervals, the smallest
-- number that can occur is the addition of the lower interval
-- bounds and the largest number that can occur is the addition of
-- the upper interval bounds.
(NumVal (Interval x1 y1),NumVal (Interval x2 y2)) -> returnA -< NumVal (Interval (x1 + x2) (y1 + y2))
_ -> fail -< "Expected two numbers as arguments for 'add'"
(NumVal n1,NumVal n2) ->
returnA -< NumVal (n1 + n2)
lt = proc (v1,v2) -> case (v1,v2) of
(NumVal (Interval x1 y1),NumVal (Interval x2 y2))
-- When the largest number in the first interval is smaller than
-- the smallest number in the second interval, then the `<`
-- check succeeds.
| y1 <= x2 -> returnA -< BoolVal True
(TopVal, TopVal) ->
(returnA -< NumVal top)
<> (fail -< "Expected two numbers as arguments for 'add'")
(TopVal, NumVal _) ->
(returnA -< NumVal top)
<> (fail -< "Expected two numbers as arguments for 'add'")
-- When the largest number in the second interval is smaller than
-- the smallest number in the first interval, then the `<`
-- check fails.
| y2 < x1 -> returnA -< BoolVal False
(NumVal _, TopVal) ->
(returnA -< NumVal top)
<> (fail -< "Expected two numbers as arguments for 'add'")
-- When the intervals overlap, we don't know if the `<` check succeeds or fails.
| otherwise -> returnA -< BoolVal TopBool
(TopVal,TopVal) -> (returnA -< BoolVal TopBool) <> (fail -< "Expected two numbers as arguments for 'lt'")
_ -> fail -< "Expected two numbers as arguments for 'lt'"
_ ->
fail -< "Expected two numbers as arguments for 'add'"
lt = proc (v1,v2) -> case (v1,v2) of
(NumVal n1, NumVal n2) -> returnA -< BoolVal (n1 O.< n2)
(TopVal,TopVal) -> (returnA -< BoolVal top) <> (fail -< "Expected two numbers as arguments for 'lt'")
(TopVal, NumVal _) -> (returnA -< BoolVal top) <> (fail -< "Expected two numbers as arguments for 'lt'")
(NumVal _, TopVal) -> (returnA -< BoolVal top) <> (fail -< "Expected two numbers as arguments for 'lt'")
_ -> fail -< "Expected two numbers as arguments for 'lt'"
boolLit = arr $ \b -> case b of
P.True -> BoolVal True
P.False -> BoolVal False
P.True -> BoolVal B.True
P.False -> BoolVal B.False
and = proc (v1,v2) -> case (v1,v2) of
(BoolVal b1,BoolVal b2) -> case b1 of
False -> returnA -< BoolVal False
True -> returnA -< BoolVal b2
TopBool -> returnA -< BoolVal (False b2)
(TopVal,TopVal) -> (returnA -< BoolVal TopBool) <> (fail -< "Expected two booleans as arguments for 'and'")
(BoolVal b1,BoolVal b2) -> returnA -< BoolVal (b1 `B.and` b2)
(TopVal, TopVal) -> (returnA -< BoolVal top) <> (fail -< "Expected two booleans as arguments for 'and'")
(TopVal, BoolVal _) -> (returnA -< BoolVal top) <> (fail -< "Expected two booleans as arguments for 'and'")
(BoolVal _, TopVal) -> (returnA -< BoolVal top) <> (fail -< "Expected two booleans as arguments for 'and'")
_ -> fail -< "Expected two booleans as arguments for 'and'"
if_ f g = proc (cond,s1,s2) -> case cond of
BoolVal True -> f -< s1
BoolVal False -> g -< s2
if_ f g = proc (cond,(s1,s2)) -> case cond of
BoolVal B.True -> f -< s1
BoolVal B.False -> g -< s2
-- If the condition could evaluate to true or false, we have to
-- evaluate both branches and join the results.
BoolVal TopBool -> (f -< s1) <> (g -< s2)
BoolVal B.Top -> (f -< s1) <> (g -< s2)
NumVal _ -> fail -< "Expected a boolean expression as condition for an if"
TopVal -> (f -< s1) <> (g -< s2) <> (fail -< "Expected a boolean expression as condition for an if")
instance (Profunctor c, Arrow c) => ArrowAlloc (String, AbsVal, Label) Addr (AbstractT c) where
instance (Profunctor c, ArrowChoice c) => ArrowAlloc Addr (ValueT AbsVal c) where
alloc = proc (_,_,l) -> returnA -< return l
run :: [LStatement] -> Terminating (Error (Pow String) (M.Map Addr AbsVal))
run stmts = fmap fst <$>
runFixT stackWiden widenResult
(runTerminatingT
(runErrorT
(runStoreT
(runEnvT
(runAbstractT
(Generic.run ::
Fix [Statement] ()
(AbstractT
(EnvT String Addr
(StoreT Addr AbsVal
(ErrorT (Pow String)
(TerminatingT
(FixT _ () () (->))))))) [Statement] ()))))))
(M.empty,(SM.empty,generate (sequence stmts)))
-- | The interval analysis instantiates the generic interpreter
-- 'Generic.run' with the components for fixpoint computation
-- ('FixT'), termination ('TerminatingT'), failure ('ErrorT'), store
-- ('StoreT'), environments ('EnvT'), and values ('IntervalT').
run :: (?bound :: IV) => Int -> Env -> Store -> [Statement] -> Terminating (Error (Pow String) Store)
run k initEnv initStore prog =
let ?contextWidening = M.widening widenVal in
let ?cacheWidening = widenResult in
let ?fixpointAlgorithm =
transform (L.iso' (\(store,(env,stmts)) -> ((env,stmts),store))
(\((env,stmts),store) -> (store,(env,stmts))))
(L.iso' id id) $
fixpointAlgorithm $
filter isWhileLoop
-- $ callsiteSensitive' k (\((_,stmts),_) -> case stmts of (stmt:_) -> Just (label stmt); [] -> Nothing)
$ unroll k (\((_,stmts),_) -> case stmts of (stmt:_) -> label stmt; [] -> -1)
. innermost
in
fmap (fmap fst) <$> snd $
Trans.run
(Generic.run ::
(ValueT AbsVal
(EnvT Env
(StoreT Store
(ErrorT Errors
(TerminatingT
(FixT
(ComponentT Component In
(StackT Stack In
(CacheT Cache In Out
(CallCountT Label
(ContextT (Ctx.Second Context) Label In
(->)))))))))))) [Statement] ())
(initStore,(initEnv, prog))
where
widenVal = widening (I.bounded ?bound)
widenResult = T.widening $ E.widening W.finite (M.widening widenVal W.** W.finite)
stackWiden = S.filter' (L.second (L.second whileLoops))
$ S.groupBy (L.iso (\(store,(ev,stmt)) -> (stmt,(ev,store))) (\(stmt,(ev,store)) -> (store,(ev,stmt))))
$ S.stack
$ S.maxSize 1
$ S.reuseFirst
$ S.fromWidening (SM.widening W.finite W.** M.widening widenVal)
runWithInitVals :: (?bound :: IV) => Int -> [(String,AbsVal)] -> [LStatement]
-> (Terminating (Error (Pow String) Store), Env)
runWithInitVals k initVals stmts =
(run k initEnv initStore prog, initEnv)
where
(prog, start) = generateState (sequence stmts)
labels = map Lower [start..]
(strings,vals) = unzip initVals
initEnv = SM.fromList $ zipWith (,) strings labels
initStore = M.fromThereList $ zipWith (,) labels (map (\v -> (Must, v)) vals)
-- Orderings ------------------------------------------------------------
......@@ -157,53 +210,33 @@ instance PreOrd AbsVal where
_ TopVal = P.True
_ _ = P.False
instance PreOrd Interval where
Interval x1 y1 Interval x2 y2 = x2 <= x1 && y1 <= y2
instance PreOrd AbsBool where
True True = P.True
False False = P.True
_ TopBool= P.True
_ _ = P.False
-- The least upper bound v1 ⊔ v2 calculates the smallest value that is
-- greater than v1 and v2.
instance Complete AbsVal where
NumVal i1 NumVal i2 = NumVal (i1 i2)
BoolVal b1 BoolVal b2 = BoolVal (b1 b2)
_ _ = TopVal
instance Complete Interval where
Interval x1 y1 Interval x2 y2 = Interval (min x1 y1) (max x2 y2)
instance Complete AbsBool where
b1 b2 = if b1 == b2 then b1 else TopBool
-- Widening also calculates an upper bound of two values, however, it
-- additionally ensures that an infinite ascending chain of values
-- becomes finite.
widenVal :: Widening AbsVal
widenVal (NumVal (Interval x1 y1)) (NumVal (Interval x2 y2))
| x2 < x1 || y1 < y2 = (W.Instable,TopVal)
| otherwise = (W.Stable,NumVal (Interval x2 y2))
widenVal (BoolVal b1) (BoolVal b2) = if b1 == b2 then (W.Stable,BoolVal b1) else (W.Instable,BoolVal TopBool)
widenVal v1 v2
| v1 == v2 = (W.Stable,v1)
| otherwise = (W.Instable,TopVal)
-- Arrow Instances ------------------------------------------------------
newtype AbstractT c x y = AbstractT { runAbstractT :: c x y }
deriving (Category,Profunctor,Arrow,ArrowChoice,ArrowJoin,ArrowFail e,ArrowEnv var addr env,ArrowStore addr val)
deriving instance ArrowFix x y c => ArrowFix x y (AbstractT c)
type instance Fix x y (AbstractT c) = AbstractT (Fix x y c)
instance Complete AbsVal where
() = W.toJoin1 widening ()
-- NumVal i1 ⊔ NumVal i2 = NumVal (i1 ⊔ i2)
-- BoolVal b1 ⊔ BoolVal b2 = BoolVal (b1 ⊔ b2)
-- _ ⊔ _ = TopVal
widening :: Widening IV -> Widening AbsVal
widening w v1 v2 = case (v1,v2) of
(BoolVal b1,BoolVal b2) -> second BoolVal (B.widening b1 b2)
(NumVal n1,NumVal n2) -> second NumVal (n1 `w` n2)
(NumVal _,BoolVal _) -> (Unstable, TopVal)
(BoolVal _,NumVal _) -> (Unstable, TopVal)
(TopVal,TopVal) -> (Stable,TopVal)
(_,TopVal) -> (Unstable,TopVal)
(TopVal,_) -> (Unstable,TopVal)
-- Arrow Instances ------------------------------------------------------
deriving instance ArrowComplete () c => ArrowComplete () (ValueT AbsVal c)
deriving instance ArrowComplete AbsVal c => ArrowComplete AbsVal (ValueT AbsVal c)
instance Hashable AbsVal
instance Hashable AbsBool
instance Hashable Interval
instance Pretty AbsVal where
pretty = viaShow
whileLoops :: L.Prism' [Statement] ((Expr,[Statement],Label),[Statement])
whileLoops = L.prism' (\((c,b,l),ss) -> While c b l:ss)
......
......@@ -6,6 +6,7 @@
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ImplicitParams #-}
-- | This file instantiates the generic interpreter with concrete
-- values to implement the concrete interpreter. All we have to do is
-- to implement the `IsValue` interface, everything else is provided
......@@ -14,13 +15,10 @@ module SturdyStyle.ConcreteInterpreter where
import Prelude hiding (lookup,and,fail)
import Control.Category
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Environment
import Control.Arrow.Store
import Control.Arrow.Fail
import Control.Arrow.Alloc
import Control.Arrow.Fail as Fail
import qualified Control.Arrow.Trans as Trans
import Control.Arrow.Transformer.Value
import Control.Arrow.Transformer.Concrete.Failure
import Control.Arrow.Transformer.Concrete.Environment
import Control.Arrow.Transformer.Concrete.Store
......@@ -30,16 +28,21 @@ import Data.HashMap.Lazy(HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Profunctor
import Data.Label
import qualified Data.Function as Function
import SturdyStyle.GenericInterpreter(IsValue(..))
import SturdyStyle.GenericInterpreter(IsValue,ArrowAlloc)
import qualified SturdyStyle.GenericInterpreter as Generic
import Syntax
data Val = BoolVal Bool | NumVal Int deriving (Eq,Show)
data Val = BoolVal Bool | NumVal Integer deriving (Eq,Show)
type Addr = Label
type Env = HashMap String Addr
type Store = HashMap Addr Val
instance (ArrowChoice c, ArrowFail String c) => IsValue Val (ConcreteT c) where
numLit = proc n -> returnA -< NumVal n
instance (ArrowChoice c, ArrowFail String c, Fail.Join Val c) => IsValue Val (ValueT Val c) where
type JoinVal y (ValueT Val c) = (Fail.Join y c)
numLit = proc n -> returnA -< NumVal $ toInteger n
add = proc (v1,v2) -> case (v1,v2) of
(NumVal n1, NumVal n2) -> returnA -< NumVal (n1 + n2)
(_,_) -> fail -< "Expected two numbers as arguments for +"
......@@ -54,30 +57,35 @@ instance (ArrowChoice c, ArrowFail String c) => IsValue Val (ConcreteT c) where
(BoolVal b1, BoolVal b2) -> returnA -< BoolVal (b1 && b2)
(_,_) -> fail -< "Expected two booleans as arguments for &&"
if_ f g = proc (v,x,y) -> case v of
if_ f g = proc (v,(x,y)) -> case v of
BoolVal True -> f -< x
BoolVal False -> g -< y
_ -> fail -< "Expected a boolean expression as condition for an if"
instance (Profunctor c, Arrow c) => ArrowAlloc (String, Val, Label) Label (ConcreteT c) where
instance (ArrowChoice c, Profunctor c) => ArrowAlloc Addr (ValueT Val c) where
alloc = proc (_,_,l) -> returnA -< l
run :: [LStatement] -> Error String (HashMap Addr Val)
run stmts = fst <$>
runFailureT
(runStoreT
(runEnvT
(runConcreteT
(Generic.run ::
ConcreteT
(EnvT String Addr
(StoreT Addr Val
(FailureT String
(->)))) [Statement] ()))))
(M.empty,(M.empty,generate (sequence stmts)))
run :: Env -> Store -> [Statement] -> Error String (HashMap Addr Val)
run initEnv initStore prog =
let ?fixpointAlgorithm = Function.fix in
fst <$>
Trans.run
(Generic.run ::
ValueT Val
(EnvT Env
(StoreT Store
(FailureT String
(->)))) [Statement] ())
(initStore,(initEnv,prog))
newtype ConcreteT c x y = ConcreteT { runConcreteT :: c x y }
deriving (Category,Profunctor,Arrow,ArrowChoice,ArrowFail e,ArrowEnv var addr env,ArrowStore addr val)
deriving instance ArrowFix x y c => ArrowFix x y (ConcreteT c)
type instance Fix x y (ConcreteT c) = ConcreteT (Fix x y c)
runWithInitVals :: [(String,Val)] -> [LStatement]
-> (Error String (HashMap Addr Val), Env)
runWithInitVals initVals stmts =
(run initEnv initStore prog, initEnv)
where
(prog, start) = generateState (sequence stmts)
labels = [start..]
(strings,vals) = unzip initVals
initEnv = M.fromList $ zipWith (,) strings labels
initStore = M.fromList $ zipWith (,) labels vals
......@@ -2,6 +2,8 @@
{-# LANGUAGE Arrows #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeFamilies #-}
-- | To show that an abstract interpreter produces correct results, we
-- have to prove that it soundly approximates the concrete interpreter.
-- However, with the previous styles, it is not explicit which parts
......@@ -19,12 +21,12 @@ import Prelude hiding (lookup,and,fail)
import Control.Arrow
import Control.Arrow.Fix
import Control.Arrow.Environment
import Control.Arrow.Environment(ArrowEnv)
import qualified Control.Arrow.Environment as Env
import Control.Arrow.Store
import qualified Control.Arrow.Store as Store
import Control.Arrow.Fail
import Control.Arrow.Alloc
import Control.Arrow.Fail as Fail
import Data.Label
......@@ -33,24 +35,28 @@ import GHC.Exts
-- | This interface abstracts over the values of the language.
class Arrow c => IsValue val c | c -> val where
type family JoinVal x (c :: * -> * -> *) :: Constraint
numLit :: c Int val
boolLit :: c Bool val
add :: c (val,val) val
and :: c (val,val) val
lt :: c (val,val) val
if_ :: c x () -> c y () -> c (val,x,y) ()
if_ :: JoinVal z c => c x z -> c y z -> c (val, (x,y)) z
class ArrowAlloc addr c where
alloc :: c (String,val,Label) addr
-- | The generic interpreter uses other language-independent
-- interfaces for environments, stores, failure and fixpoints from the