Lang.LamIf.Monads

Documentation

newtype InjectLamIf val a

Constructors

InjectLamIf

Fields

runInjectLamIf :: (a, LamIfState val)

Instances

Inject * (InjectLamIf val) (PathSensitiveΣᵇ val)

Inject * (InjectLamIf val) (FlowInsensitiveΣᵇ val)

Inject * (InjectLamIf val) (FlowSensitiveΣᵇ val)

(Ord val, POrd val, JoinLattice val, Val val) => ExecutionLamIf val (InjectLamIf val) (PathSensitiveΣᵇ val) (PathSensitiveM val)

(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val)

(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowSensitiveΣᵇ val) (FlowSensitiveM val)

isoInjectLamIf :: InjectLamIf val a ⇄ (a, LamIfState val)

newtype PathSensitiveΣᵇ val a

Constructors

PathSensitiveΣᵇ

Fields

runPathSensitiveΣᵇ :: PolyStateΠ (LamIfState val) (NondetJoinΠ ID) a

Instances

Inject * (InjectLamIf val) (PathSensitiveΣᵇ val)

(Ord val, POrd val, JoinLattice val, Val val) => ExecutionLamIf val (InjectLamIf val) (PathSensitiveΣᵇ val) (PathSensitiveM val)

GaloisTransformer (PathSensitiveΣᵇ val) (PathSensitiveM val)

isoPathSensitiveΣᵇ :: PathSensitiveΣᵇ val a ⇄ PolyStateΠ (LamIfState val) (NondetJoinΠ ID) a

isoPathSensitiveΣᵇ2 :: PathSensitiveΣᵇ val ↝⇄ PolyStateΠ (LamIfState val) (NondetJoinΠ ID)

newtype PathSensitiveΣ val a

Constructors

PathSensitiveΣ

Fields

runPathSensitiveΣ :: 𝒫 (a, LamIfState val)

Instances

JoinLattice (PathSensitiveΣ val a)

Difference (PathSensitiveΣ val a)

Join (PathSensitiveΣ val a)

Bot (PathSensitiveΣ val a)

POrd (PathSensitiveΣ val a)

(Pretty val, Pretty a) => Pretty (PathSensitiveΣ val a)

isoPathSensitiveΣ :: (Ord val, Ord a) => PathSensitiveΣ val a ⇄ PathSensitiveΣᵇ val a

newtype PathSensitiveM val a

Constructors

PathSensitiveM

Fields

runPathSensitiveM :: PolyStateT (LamIfState val) (NondetJoinT ID) a

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (PathSensitiveM val)

(Ord val, POrd val, JoinLattice val, Val val) => ExecutionLamIf val (InjectLamIf val) (PathSensitiveΣᵇ val) (PathSensitiveM val)

Monad (PathSensitiveM val)

Functor (PathSensitiveM val)

MonadJoinLattice (PathSensitiveM val)

MonadJoin (PathSensitiveM val)

MonadBot (PathSensitiveM val)

MonadState (LamIfState val) (PathSensitiveM val)

GaloisTransformer (PathSensitiveΣᵇ val) (PathSensitiveM val)

isoPathSensitiveM :: PathSensitiveM val a ⇄ PolyStateT (LamIfState val) (NondetJoinT ID) a

isoPathSensitiveM2 :: PathSensitiveM val ↝⇄ PolyStateT (LamIfState val) (NondetJoinT ID)

data LamIfContext val

Constructors

LamIfContext

Fields

ctxEnv :: Env

ctxΚAddr :: Maybe ExpAddr

ctxTime :: Time

Instances

Eq (LamIfContext k val)

Ord (LamIfContext k val)

(Pretty Env, Pretty (Maybe ExpAddr), Pretty Time) => Pretty (LamIfContext k val)

data LamIfStores val

Constructors

LamIfStores

Fields

storesStore :: Store val

storesΚStore :: KStore val

Instances

Eq val => Eq (LamIfStores val)

Ord val => Ord (LamIfStores val)

Join val => JoinLattice (LamIfStores val)

Difference val => Difference (LamIfStores val)

Join val => Join (LamIfStores val)

Bot (LamIfStores val)

POrd val => POrd (LamIfStores val)

(Pretty (Store val0), Pretty (KStore val0)) => Pretty (LamIfStores val)

splitLamIfState :: LamIfState val -> (LamIfContext val, LamIfStores val)

combineLamIfState :: (LamIfContext val, LamIfStores val) -> LamIfState val

isoSplitLamIfState :: LamIfState val ⇄ (LamIfContext val, LamIfStores val)

isoCombineLamIfState :: (a, LamIfState val) ⇄ ((a, LamIfContext val), LamIfStores val)

newtype FlowSensitiveΣᵇ val a

Constructors

FlowSensitiveΣᵇ

Fields

runFlowSensitiveΣᵇ :: PolyStateΠ (LamIfContext val) (FlowJoinΠ (LamIfStores val) ID) a

Instances

Inject * (InjectLamIf val) (FlowSensitiveΣᵇ val)

(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowSensitiveΣᵇ val) (FlowSensitiveM val)

Join val => GaloisTransformer (FlowSensitiveΣᵇ val) (FlowSensitiveM val)

isoFlowSensitiveΣᵇ :: FlowSensitiveΣᵇ val a ⇄ PolyStateΠ (LamIfContext val) (FlowJoinΠ (LamIfStores val) ID) a

isoFlowSensitiveΣ2ᵇ :: FlowSensitiveΣᵇ val ↝⇄ PolyStateΠ (LamIfContext val) (FlowJoinΠ (LamIfStores val) ID)

newtype FlowSensitiveΣ val a

Constructors

FlowSensitiveΣ

Fields

runFlowSensitiveΣ :: (a, LamIfContext val) ⇰ LamIfStores val

Instances

Join val => JoinLattice (FlowSensitiveΣ val a)

Difference val => Difference (FlowSensitiveΣ val a)

Join val => Join (FlowSensitiveΣ val a)

Bot (FlowSensitiveΣ val a)

POrd val => POrd (FlowSensitiveΣ val a)

(Pretty val, Pretty a) => Pretty (FlowSensitiveΣ val a)

isoFlowSensitiveΣ :: (Ord a, Join val) => FlowSensitiveΣ val a ⇄ FlowSensitiveΣᵇ val a

newtype FlowSensitiveM val a

Constructors

FlowSensitiveM

Fields

runFlowSensitiveM :: PolyStateT (LamIfContext val) (FlowJoinT (LamIfStores val) ID) a

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (FlowSensitiveM val)

(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowSensitiveΣᵇ val) (FlowSensitiveM val)

Join val => Monad (FlowSensitiveM val)

Functor (FlowSensitiveM val)

Join val => MonadJoinLattice (FlowSensitiveM val)

Join val => MonadJoin (FlowSensitiveM val)

Join val => MonadBot (FlowSensitiveM val)

Join val => MonadState (LamIfState val) (FlowSensitiveM val)

Join val => GaloisTransformer (FlowSensitiveΣᵇ val) (FlowSensitiveM val)

isoFlowSensitiveM :: FlowSensitiveM val a ⇄ PolyStateT (LamIfContext val) (FlowJoinT (LamIfStores val) ID) a

isoFlowSensitiveM2 :: FlowSensitiveM val ↝⇄ PolyStateT (LamIfContext val) (FlowJoinT (LamIfStores val) ID)

newtype FlowInsensitiveΣᵇ val a

Constructors

FlowInsensitiveΣᵇ

Fields

runFlowInsensitiveΣᵇ :: PolyStateΠ (LamIfContext val) (NondetJoinΠ (StateΠ (LamIfStores val) ID)) a

Instances

Inject * (InjectLamIf val) (FlowInsensitiveΣᵇ val)

(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val)

Join val => GaloisTransformer (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val)

isoFlowInsensitiveΣᵇ :: FlowInsensitiveΣᵇ val a ⇄ PolyStateΠ (LamIfContext val) (NondetJoinΠ (StateΠ (LamIfStores val) ID)) a

isoFlowInsensitiveΣᵇ2 :: FlowInsensitiveΣᵇ val ↝⇄ PolyStateΠ (LamIfContext val) (NondetJoinΠ (StateΠ (LamIfStores val) ID))

newtype FlowInsensitiveΣ val a

Constructors

FlowInsensitiveΣ

Fields

runFlowInsensitiveΣ :: (𝒫 (a, LamIfContext val), LamIfStores val)

Instances

Join val => JoinLattice (FlowInsensitiveΣ val a)

Difference val => Difference (FlowInsensitiveΣ val a)

Join val => Join (FlowInsensitiveΣ val a)

Bot (FlowInsensitiveΣ val a)

POrd val => POrd (FlowInsensitiveΣ val a)

(Pretty val, Pretty a) => Pretty (FlowInsensitiveΣ val a)

isoFlowInsensitiveΣ :: Ord a => FlowInsensitiveΣ val a ⇄ FlowInsensitiveΣᵇ val a

newtype FlowInsensitiveM val a

Constructors

FlowInsensitiveM

Fields

runFlowInsensitiveM :: PolyStateT (LamIfContext val) (NondetJoinT (StateT (LamIfStores val) ID)) a

Instances

(POrd val, JoinLattice val, Val val) => MonadLamIf val (FlowInsensitiveM val)

(Ord val, POrd val, JoinLattice val, Difference val, Val val, Pretty val) => ExecutionLamIf val (InjectLamIf val) (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val)

Join val => Monad (FlowInsensitiveM val)

Functor (FlowInsensitiveM val)

Join val => MonadJoinLattice (FlowInsensitiveM val)

Join val => MonadJoin (FlowInsensitiveM val)

Join val => MonadBot (FlowInsensitiveM val)

Join val => MonadState (LamIfState val) (FlowInsensitiveM val)

Join val => GaloisTransformer (FlowInsensitiveΣᵇ val) (FlowInsensitiveM val)

isoFlowInsensitiveM :: FlowInsensitiveM val a ⇄ PolyStateT (LamIfContext val) (NondetJoinT (StateT (LamIfStores val) ID)) a

isoFlowInsensitiveM2 :: FlowInsensitiveM val ↝⇄ PolyStateT (LamIfContext val) (NondetJoinT (StateT (LamIfStores val) ID))

data MonadParam where

Constructors

MonadParam :: forall val ς' ς m. P m -> (ς Exp ⇄ ς' Exp) -> (ς Exp -> Doc) -> W (ExecutionLamIf val (InjectLamIf val) ς' m, LFPLamIf ς) -> MonadParam

pathSensitive :: DomainParam -> MonadParam

flowSensitive :: DomainParam -> MonadParam

flowInsensitive :: DomainParam -> MonadParam