Skip to content

Commit

Permalink
various fixes + wip infinite loop
Browse files Browse the repository at this point in the history
  • Loading branch information
bramvdbogaerde committed Nov 6, 2023
1 parent d19c3eb commit f7d8d00
Show file tree
Hide file tree
Showing 5 changed files with 97 additions and 43 deletions.
12 changes: 6 additions & 6 deletions maf2-analysis/maf2-hs.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,9 @@ source-repository head

library
exposed-modules:
Analysis.Scheme.Simple
Interpreter.Scheme
other-modules:
Analysis.Actors.Mailbox
Analysis.Actors.Monad
Analysis.Actors.Semantics
Expand All @@ -42,7 +45,6 @@ library
Analysis.Scheme.Monad
Analysis.Scheme.Primitives
Analysis.Scheme.Semantics
Analysis.Scheme.Simple
Analysis.Semantics
Analysis.Store
Benchmark.Programs
Expand All @@ -54,14 +56,12 @@ library
Data.LabeledProduct
Data.ListExtra
Data.SetExtra
Interpreter.Scheme
Interpreter.Scheme.Eval
Interpreter.Scheme.Monad
Interpreter.Scheme.Primitives
Interpreter.Scheme.Semantics
Interpreter.Scheme.Values
Lib
other-modules:
Paths_maf2_hs
hs-source-dirs:
src
Expand All @@ -81,7 +81,7 @@ library
MultiParamTypeClasses
FunctionalDependencies
GeneralizedNewtypeDeriving
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -fno-warn-type-defaults -O0 -fprint-potential-instances
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -fno-warn-type-defaults -O0 -fprint-potential-instances -fprof-auto -fprof-cafs
build-depends:
HUnit
, IfElse
Expand Down Expand Up @@ -131,7 +131,7 @@ executable maf2-hs-exe
MultiParamTypeClasses
FunctionalDependencies
GeneralizedNewtypeDeriving
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -fno-warn-type-defaults -O0 -fprint-potential-instances -threaded -rtsopts -with-rtsopts=-N
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -fno-warn-type-defaults -O0 -fprint-potential-instances -fprof-auto -fprof-cafs -threaded -rtsopts -with-rtsopts=-N
build-depends:
HUnit
, IfElse
Expand Down Expand Up @@ -182,7 +182,7 @@ test-suite maf2-hs-test
MultiParamTypeClasses
FunctionalDependencies
GeneralizedNewtypeDeriving
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -fno-warn-type-defaults -O0 -fprint-potential-instances -threaded -rtsopts -with-rtsopts=-N
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -fno-warn-type-defaults -O0 -fprint-potential-instances -fprof-auto -fprof-cafs -threaded -rtsopts -with-rtsopts=-N
build-depends:
HUnit
, IfElse
Expand Down
5 changes: 5 additions & 0 deletions maf2-analysis/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -71,9 +71,14 @@ ghc-options:
- -fno-warn-type-defaults
- -O0
- -fprint-potential-instances
- -fprof-auto
- -fprof-cafs

library:
source-dirs: src
exposed-modules:
- Analysis.Scheme.Simple
- Interpreter.Scheme

executables:
maf2-hs-exe:
Expand Down
15 changes: 4 additions & 11 deletions maf2-analysis/src/Analysis/Monad.hs
Original file line number Diff line number Diff line change
@@ -1,19 +1,14 @@
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances, AllowAmbiguousTypes, PolyKinds #-}
{-# LANGUAGE FunctionalDependencies, ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

{-# OPTIONS_GHC -Wno-redundant-constraints #-}
-- | This module provides monadic operations shared between many analyses.
--
-- To make instantiations for combinations of these typeclasses easier, this module also provides an abstraction based on Monad **layers**.
-- These layers corresponds to monads in a monad transformer stack. However, since `MonadTrans` lacks a method for peeling away a single layer
-- from the monad transformer stack, the `MonadLayer` typeclass is used instead.
--
-- We combine these layers with the `Cap` monad which collects the capabilities of the monad stack into a typelevel list and combines them
-- with monad stack itself. The advantage of this is that we do need to create additional `newtype`s for each element in the monad stack.
-- Instead, we pair the element in the monad stack with a capbility which can be used to distinguish multiple monads of the same type from each-other.
--
-- To ensure that layers and capabilities remain paired, each layer should correspond to exactly one capability in the list of capabilities.
--
module Analysis.Monad(
-- Typeclass interfaces
StoreM(..),
Expand Down Expand Up @@ -42,15 +37,13 @@ import qualified Data.Set as Set
import Data.TypeLevel.List
import Data.DMap
import Data.Kind
import Data.Functor.Identity
import Domain
import Analysis.Store hiding (lookupSto, extendSto, updateSto)
import qualified Analysis.Store as Store
import Control.Monad.Layer
import Control.Monad.Trans.Maybe
import Control.Monad.Writer hiding (mzero)
import Control.Monad.Error
import GHC.TypeError

----------------------------------------------------------------------------------------------------
-- Typeclasses for monadic analysis functionality
Expand Down Expand Up @@ -142,7 +135,7 @@ runEnv initialEnv (EnvT m) = runReaderT m initialEnv

---

newtype CtxT ctx m a = CtxT { getContextReader :: (ReaderT ctx m a) } deriving (MonadReader ctx, Monad, Applicative, MonadLayer, Functor)
newtype CtxT ctx m a = CtxT { getContextReader :: ReaderT ctx m a } deriving (MonadReader ctx, Monad, Applicative, MonadLayer, Functor)
instance {-# OVERLAPPING #-} Monad m => CtxM (CtxT ctx m) ctx where
getCtx = ask
withCtx = local
Expand Down Expand Up @@ -204,7 +197,7 @@ instance (Monad t, Address adr, StoreM (Lower t) adr, MonadLayer t) => StoreM t
updateAdr adr = upperM . updateAdr adr
lookupAdr = upperM . lookupAdr

runSto :: forall ks l m a . DMap ks -> (StateT (DMap ks) m) a -> m (a, DMap ks)
runSto :: forall ks m a . DMap ks -> (StateT (DMap ks) m) a -> m (a, DMap ks)
runSto = flip runStateT

--
Expand Down Expand Up @@ -238,5 +231,5 @@ runAlloc allocator (AllocT m) = runReaderT m allocator
-- CallM
--

instance (Monad m, CallM (Lower m) env v, MonadLayer m) => CallM m env v where
instance (Monad m, CallM (Lower m) env v, MonadLayer m) => CallM m env v where
call = upperM . call
84 changes: 67 additions & 17 deletions maf2-analysis/src/Analysis/Scheme.hs
Original file line number Diff line number Diff line change
@@ -1,10 +1,12 @@
{-# LANGUAGE UndecidableInstances, FlexibleInstances, ConstraintKinds #-}
{-# OPTIONS_GHC -Wall #-}
module Analysis.Scheme where

import Prelude hiding (exp, lookup)

import Debug.Trace

import Analysis.Scheme.Primitives
import Analysis.Environment
import qualified Analysis.Scheme.Semantics as Semantics
import Analysis.Scheme.Monad (SchemeM)
import Analysis.Monad hiding (getEnv)
Expand All @@ -14,9 +16,10 @@ import Control.Monad.Trans.Class
import Control.Monad.Join
import Control.Monad.Layer
import Control.Monad.Error (MonadError)
import Control.Monad.Cond (unlessM)

import Syntax.Scheme
import Domain (Address, Vlu)
import Domain (Vlu, subsumes, JoinLattice, bottom)
import Domain.Scheme hiding (Exp, Env)

import Data.DMap (DMap, fromMap, Hashable)
Expand All @@ -25,8 +28,7 @@ import Data.Function ((&))
import Data.Dynamic
import Data.Functor.Identity
import Data.TypeLevel.Ghost

import GHC.Generics (Generic)
import Data.Functor ((<&>))

-----------------------------------------
-- Shorthands
Expand Down Expand Up @@ -83,11 +85,11 @@ instance (SchemeAnalysisConstraints var v ctx dep) => ModX (ModF var v ctx dep)
type Dep (ModF var v ctx dep) = dep
-- | The analysis of a single component runs the Scheme semantics
-- on the body of that component
analyze (exp, env, ctx, _) store =
let (((_, error), (spawns, triggers, registers)), sto) = (Semantics.eval exp >>= writeAdr (retAdr (exp, env, ctx, Ghost)))
analyze (exp, env, ctx, _) store =
let (((_, error), (spawns, triggers, registers)), sto) = trace (show exp) $ (Semantics.eval exp >>= writeAdr (retAdr (exp, env, ctx, Ghost)))
& runEvalT
& runErr
& runCallT @v @ctx
& runCallT' @v @ctx
& runSto store
& runEnv env
& runAlloc @PaAdr (allocPai @ctx)
Expand All @@ -102,7 +104,12 @@ instance (SchemeAnalysisConstraints var v ctx dep) => ModX (ModF var v ctx dep)
-- Open recursion for evaluation
-----------------------------------------

newtype BaseSchemeEvalT v m a = BaseSchemeEvalT (m a) deriving (Monad, Functor, Applicative, MonadLayer)
newtype BaseSchemeEvalT v m a = BaseSchemeEvalT (m a) deriving (Monad, Functor, Applicative)

instance (Monad m) => MonadLayer (BaseSchemeEvalT v m) where
type Lower (BaseSchemeEvalT v m) = m
upperM = BaseSchemeEvalT
lowerM f (BaseSchemeEvalT m) = BaseSchemeEvalT (f m)

instance (MonadJoin m) => MonadJoin (BaseSchemeEvalT v m) where
mzero = BaseSchemeEvalT mzero
Expand All @@ -111,8 +118,8 @@ instance (MonadJoin m) => MonadJoin (BaseSchemeEvalT v m) where
instance MonadTrans (BaseSchemeEvalT v) where
lift = BaseSchemeEvalT

instance (MonadError m, SchemeM (BaseSchemeEvalT v m) v, MonadLayer m, SchemeAnalysisConstraints var v ctx dep) => (Analysis.Monad.EvalM (BaseSchemeEvalT v m) v Exp) where
eval = Semantics.eval
instance (MonadError m, SchemeM (BaseSchemeEvalT v m) v, SchemeAnalysisConstraints var v ctx dep) => (Analysis.Monad.EvalM (BaseSchemeEvalT v m) v Exp) where
eval = trace "eval" Semantics.eval


runEvalT :: BaseSchemeEvalT v m a -> m a
Expand All @@ -129,29 +136,67 @@ class (Ord dep, Hashable dep) => Dependency adr dep | adr -> dep where
-- CallM & StoreM implementation
-----------------------------------------

newtype CallT' var v ctx dep m a = CallT' (m a) deriving (Monad, Functor, Applicative)
instance {-# OVERLAPPING #-} (Monad m,
SchemeAnalysisConstraints var v ctx dep,
JoinLattice v
) => CallM (CallT' var v ctx dep m) (Env var v ctx dep) v where
call = const $ return bottom

instance (Monad m) => MonadLayer (CallT' var v ctx dep m) where
type (Lower (CallT' var v ctx dep m)) = m
upperM = CallT'
lowerM f (CallT' m) = CallT' (f m)

instance (MonadJoin m) => MonadJoin (CallT' var v ctx dep m) where
mzero = CallT' mzero
mjoin (CallT' ma) (CallT' mb) = CallT' $ mjoin ma mb

runCallT' :: forall v ctx m a c dep var . (Monad m, c ~ ModF var v ctx dep)
=> CallT' var v ctx dep m a
-> m (a, ([Component c], [Dep c], [Dep c]))
runCallT' (CallT' m) = m <&> (, ([], [], []))




newtype CallT var v ctx dep m a = CallT (ModxT (ModF var v ctx dep) m a) deriving (Monad, Functor, Applicative, MonadLayer)

instance (Ord (Component (ModF var v ctx dep)), Ord (Dep (ModF var v ctx dep)), MonadJoin m) => MonadJoin (CallT var v ctx dep m) where
mzero = CallT mzero
mjoin (CallT ma) (CallT mb) = CallT $ mjoin ma mb

needsUpdate :: forall m adr v . (JoinLattice v, Show v, Vlu adr ~ v, StoreM m adr) => adr -> v -> m Bool
needsUpdate adr vlu' = trace (show vlu') $ do
_ <- trace "lookup before" $ return ()
vlu <- lookupAdr adr
if subsumes vlu' vlu then
return False
else
return True

-- | When a store update occurs, registers that update as a write effect,
-- when a store read occurs, registers that read as a read effect
instance {-# OVERLAPPING #-} (
Dependency adr dep,
StoreM m adr,
JoinLattice (Vlu adr),
Show (Vlu adr),
SchemeAnalysisConstraints var v ctx dep
) => StoreM (CallT var v ctx dep m) adr where

writeAdr adr vlu = CallT @var @v @ctx $ do
writeAdr adr vlu = trace ("writeAdr " ++ show vlu) $ CallT @var @v @ctx $ do
-- TODO: it is rather strange that type inference
-- cannot figure out that `c` must equal `ModF v ctx`
-- hence the explicit type annotations
_ <- trigger @_ @(ModF var v ctx dep) (dep adr)
unlessM (lift $ needsUpdate adr vlu) $ do
trigger @_ @(ModF var v ctx dep) (dep adr)

lift $ writeAdr adr vlu

updateAdr adr vlu = CallT $ do
_ <- trigger @_ @(ModF var v ctx dep) (dep adr)
unlessM (lift $ needsUpdate adr vlu) $ do
trigger @_ @(ModF var v ctx dep) (dep adr)
lift $ updateAdr adr vlu

lookupAdr adr = CallT $ do
Expand All @@ -162,16 +207,17 @@ instance {-# OVERLAPPING #-} (
-- | This instances spawns the called function as a component,
-- and reads the return value from the store.
instance {-# OVERLAPPING #-} (CtxM m ctx,
StoreM m var,
Monad m,
StoreM (CallT var v ctx dep m) var,
SchemeAnalysisConstraints var v ctx dep
) => CallM (CallT var v ctx dep m) (Env var v ctx dep) v where
call (e, env) = CallT @var @v @ctx $ do
call (e, env) = do
-- get the current context
ctx <- lift getCtx
ctx <- CallT $ lift getCtx
-- create a new component from this context
let comp = (e, env, ctx, Ghost)
-- spawn the new component
_ <- spawn comp
_ <- CallT $ spawn comp
-- lookup the return value of the component
lookupAdr (retAdr comp)

Expand All @@ -189,6 +235,10 @@ runCallT (CallT m) = runModxT @c m
-- TODO: too many constraints, makes it more difficult to parse the program
-- as written, try to simplify
type SchemeAnalysisConstraints var v ctx dep = (
Show v,
Show (Vlu (PAdr v)),
Show (Vlu (SAdr v)),
Show (Vlu (VAdr v)),
SchemeDomain v,
SchemeConstraints v Exp var (Env var v ctx dep),
StoreDefinedFor v,
Expand Down
24 changes: 15 additions & 9 deletions maf2-analysis/src/Control/SVar/ModX.hs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ instance WorkList [a] a where
add = (:)
remove (e:wl) = (e, wl)
isEmpty [] = True
isEmpty _ = False

--------------------------------------------------
-- State Variables
Expand Down Expand Up @@ -242,7 +243,7 @@ data ModXState c = ModXState {
emptyModxState :: ModXState c
emptyModxState = ModXState Set.empty Set.empty Set.empty

instance (Ord (Component c), Ord (Dep c)) => Joinable (ModXState c) where
instance (Ord (Component c), Ord (Dep c)) => Joinable (ModXState c) where
join s1 s2 = ModXState {
spawns = spawns s1 `Set.union` spawns s2,
triggers = triggers s1 `Set.union` triggers s2,
Expand All @@ -252,14 +253,19 @@ instance (Ord (Component c), Ord (Dep c)) => Joinable (ModXState c) where
instance (Ord (Component c), Ord (Dep c)) => JoinLattice (ModXState c) where
bottom = emptyModxState
subsumes s1 s2 =
subsumes (spawns s1) (spawns s2) &&
subsumes (spawns s1) (spawns s2) &&
subsumes (triggers s1) (triggers s2) &&
subsumes (registers s1) (registers s2)
subsumes (registers s1) (registers s2)


-- | A monad that keeps track of the set of spawned
-- components
newtype ModxT c m a = ModxT (StateT (ModXState c) m a) deriving (Monad, MonadLayer, Applicative, Functor)
newtype ModxT c m a = ModxT { innerModxT :: StateT (ModXState c) m a } deriving (MonadLayer, Applicative, Functor)

instance (Monad m) => Monad (ModxT c m) where
(ModxT m) >>= f = ModxT $ m >>= (innerModxT . f)
return = pure


instance MonadTrans (ModxT c) where
lift = ModxT . lift
Expand All @@ -276,8 +282,8 @@ instance (Monad m, ModX c) => MonadModX (ModxT c m) c where

runModxT :: forall c m a . Monad m => ModxT c m a -> m (a, ([Component c], [Dep c], [Dep c]))
runModxT (ModxT m) = do
(a, state) <- runStateT m emptyModxState
return $ let ModXState { .. } = state
(a, state) <- runStateT m emptyModxState
return $ let ModXState { .. } = state
in (a, (Set.toList spawns, Set.toList triggers, Set.toList registers))

integrate :: (WorkList wl (Component c), ModX c)
Expand All @@ -296,7 +302,7 @@ integrate loopState wl st' spawns' r' w' = (loopState', wl'')
(Map.fromList (map (,Set.singleton cmp) r'))
(dependents loopState)
toReanal = Set.unions $ map (fromMaybe Set.empty . flip Map.lookup dependents') w'
wl'' = addAll (Set.toList toReanal) wl'
wl'' = addAll (Set.toList $ toSpawn `Set.union` toReanal) wl'
loopState' = ModxLoop {
seen = seen',
dependents = dependents',
Expand All @@ -322,8 +328,8 @@ loop :: ( ModX c,
WorkList wl (Component c))
=> ModxLoop c
-> wl
-> (State c)
loop loopState@ModxLoop { .. } wl = if isEmpty wl then state
-> State c
loop loopState@ModxLoop { .. } wl = trace "loop" $ if isEmpty wl then state
else
let (state, spawns, r, w) = analyze cmp state
in uncurry loop $ integrate loopState wl state spawns r w
Expand Down

0 comments on commit f7d8d00

Please sign in to comment.