store structure as a constraint in Scheme domain

maf2-analysis/src/Analysis/Monad.hs

@@ -41,7 +41,7 @@ import Control.Monad.State hiding (mzero)
 import Syntax.Scheme.AST
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.TypeLevel.List 
+import Data.TypeLevel.List
 import Data.DMap
 import Domain
 import Analysis.Store hiding (lookupSto, extendSto, updateSto)
@@ -117,7 +117,11 @@ class (Monad m) => EvalM m v e  | m -> v where
 -- Instances
 ----------------------------------------------------------------------------------------------------
 
-newtype EnvT env m a = EnvT (ReaderT env m a) deriving (MonadReader env, Monad, Applicative, MonadLayer, Functor)
+newtype EnvT env m a = EnvT { getEnvReader ::  ReaderT env m a } deriving (MonadReader env, Monad, Applicative, MonadLayer, Functor)
+
+instance (Monad m, MonadJoin m) => MonadJoin (EnvT env m) where
+   mjoin (EnvT ma) = EnvT . mjoin ma . getEnvReader
+   mzero = EnvT mzero
 
 instance {-# OVERLAPPING #-} (Environment env adr, Monad m) => EnvM (EnvT env m) adr env where
    lookupEnv nam = asks (Analysis.Environment.lookup nam)
@@ -137,14 +141,18 @@ runEnv initialEnv (EnvT m) = runReaderT m initialEnv
 
 ---
 
-newtype CtxT ctx m a = CtxT (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
 instance (MonadLayer t, CtxM (Lower t) ctx) => CtxM t ctx where
    getCtx =  upperM getCtx
    withCtx f = lowerM (withCtx f)
 
+instance (MonadJoin m) => MonadJoin (CtxT ctx m) where
+   mjoin (CtxT ma) = CtxT . mjoin ma . getContextReader
+   mzero = CtxT mzero
+
 runCtx :: ctx -> (CtxT ctx m) a -> m a
 runCtx initialCtx (CtxT m) = runReaderT m initialCtx
 
@@ -206,7 +214,11 @@ runSto =  flip runStateT
 type Allocator from ctx to = (from -> ctx -> to)
 
 -- Allocator that turns a function into an allocator of the suiteable type
-newtype AllocT from ctx to m a = AllocT (ReaderT (Allocator from ctx to) m a) deriving (MonadReader (Allocator from ctx to), Monad, Applicative, Functor, MonadLayer)
+newtype AllocT from ctx to m a = AllocT { getAllocReader :: ReaderT (Allocator from ctx to) m a } deriving (MonadReader (Allocator from ctx to), Monad, Applicative, Functor, MonadLayer)
+
+instance (MonadJoin m) => MonadJoin (AllocT from ctx to m) where
+   mjoin (AllocT ma) = AllocT . mjoin ma . getAllocReader
+   mzero = AllocT mzero
 
 instance {-# OVERLAPPING #-} (Monad m, CtxM m ctx) => AllocM (AllocT from ctx to m) from to where
    alloc from = do

maf2-analysis/src/Analysis/Scheme.hs

@@ -11,7 +11,7 @@ import Analysis.Monad hiding (eval, getEnv)
 import Control.SVar.ModX
 import Syntax.Scheme
 import Domain (Address, Vlu)
-import Domain.Scheme (SchemeDomain, SchemeConstraints, SchemeAdrs, SAdr, PAdr, VAdr)
+import Domain.Scheme (SchemeDomain, SchemeConstraints, SchemeAdrs, SAdr, PAdr, VAdr, StoreDefinedFor)
 import qualified Domain.Scheme
 
 import Data.DMap (DMap, (:->), fromMap, Hashable)
@@ -104,7 +104,7 @@ class SchemeAlloc ctx v | ctx -> v where
   allocVar :: Ide -> ctx -> VarAdr v ctx 
   allocCtx :: ctx -> ctx
 
-instance (SchemeDomain v, SchemeConstraints v Exp (VarAdr v ctx) (Env v ctx), Typeable v, Typeable ctx, SchemeAlloc ctx v, Hashable v, Hashable ctx, Eq ctx, Ord ctx) => ModX (ModF v ctx) where 
+instance (SchemeDomain v, StoreDefinedFor v, SchemeConstraints v Exp (VarAdr v ctx) (Env v ctx), Typeable v, Typeable ctx, SchemeAlloc ctx v, Hashable v, Hashable ctx, Eq ctx, Ord ctx) => ModX (ModF v ctx) where 
   -- A component is a closure + a context
   type Component (ModF v ctx)  = (Exp, Env v ctx, ctx)
   -- | Global store
@@ -136,7 +136,7 @@ newtype AnalysisResult v ctx = AnalysisResult (State (ModF v ctx))
 -- result. It uses the default initial environment
 -- as specified in `Analysis.Scheme.Primitives`
 analyzeProgram :: forall v ctx wl . 
-                  (WorkList wl (Component (ModF v ctx)), SchemeDomain v, SchemeConstraints v Exp (VarAdr v ctx) (Env v ctx), Ord ctx, Ord v, Hashable ctx, Hashable v, Typeable ctx, Typeable v, SchemeAlloc ctx v) 
+                  (WorkList wl (Component (ModF v ctx)), SchemeDomain v, SchemeConstraints v Exp (VarAdr v ctx) (Env v ctx), StoreDefinedFor v,  Ord ctx, Ord v, Hashable ctx, Hashable v, Typeable ctx, Typeable v, SchemeAlloc ctx v) 
                => Program  -- ^ the program analyse
                -> wl       -- ^ the initial contents of the worklist, can be empty. This function will add the initial component to it. 
                -> (Exp -> ctx) -- ^ context allocation function for a given expression (usually associated with a function call)

maf2-domains/maf2-domains.cabal

@@ -46,6 +46,7 @@ library
       Domain.Python.DataFrame
       Domain.Scheme.Class
       Domain.Scheme.Modular
+      Domain.Scheme.Store
       Paths_maf2_domains
   hs-source-dirs:
       src

maf2-domains/src/Domain/Scheme.hs

@@ -1,48 +1,13 @@
 {-# LANGUAGE FlexibleContexts, UndecidableInstances, PatternSynonyms, FlexibleInstances, ConstraintKinds #-}
 {-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-missing-fields -fno-warn-missing-pattern-synonym-signatures -fno-warn-incomplete-patterns #-}
-module Domain.Scheme (SchemeAdrs, Address(..),  module Domain.Scheme.Class, module Domain.Scheme.Modular) where
+module Domain.Scheme (
+   module Domain.Scheme.Class, 
+   module Domain.Scheme.Modular,
+   module Domain.Scheme.Store
+) where
 
-import Data.Coerce hiding (coerce)
-import qualified Data.Coerce as Coerce
-import Control.Applicative (Applicative(liftA2))
-import Data.Kind
-import Data.Set (Set)
-import Data.Default
-import qualified Data.Set as Set
-import Control.Monad ((>=>), (<=<))
-import qualified Control.Monad as M
-
-import Prelude hiding (null)
-import Data.List hiding (null)
-import Control.Monad.Join
-import Data.Maybe (isJust)
-import Data.DMap ((:->))
-import Data.Kind
-import Data.Hashable
-import Data.Typeable
-
-import Domain
 import Domain.Scheme.Class
 import Domain.Scheme.Modular
+import Domain.Scheme.Store
 
 
-
-----------------------------------------------
--- Store interactions
-----------------------------------------------
-
--- | A mapping from Scheme addresses
--- to their corresponding values.
--- 
--- For a given `v` for which an instance of 
--- `SchemeDomain` exists, it computes an association list
--- mapping addresses to the heap allocated-values of the domain.
--- 
--- This can be used as the basis for a `Data.DMap`. 
-type SchemeAdrs v = '[
-   Adr  v :-> Vlu (Adr v),
-   PAdr v :-> Vlu (PAdr v),
-   VAdr v :-> Vlu (VAdr v),
-   SAdr v :-> Vlu (SAdr v) 
-   ]
-

maf2-domains/src/Domain/Scheme/Store.hs

@@ -0,0 +1,49 @@
+{-# LANGUAGE ConstraintKinds, FlexibleContexts #-}
+-- | Memory model for analyses that use the abstract domain for Scheme.
+--
+-- It specifies the notion of a "store" which is an abstraction of  the actual program memory as a function from a finite set of addresses to an abstract value.
+--
+-- The memory of a Scheme program is divided into multiple disjoint regions:
+--
+-- * A region to store the values of variables 
+-- * A region to store strings
+-- * A region to store vectors
+-- * A region to store pairs
+--
+-- All other values are entirely immutable and therefore do not have to be allocated in a store.
+--
+-- The Domain.Scheme.Class defines the type for each of these addresses. This module exposes a type level association list that defines a mapping between these addresses and their corresponding abstract values. Furthermore, this module contains a constraint generator that creates `Has` constraints for each address in the Scheme domain.
+module Domain.Scheme.Store(SchemeAdrs, StoreDefinedFor) where
+
+import Domain
+import Domain.Scheme.Class
+
+import Data.Kind
+import Data.DMap
+import Data.TypeLevel.List
+
+-- | A mapping from Scheme addresses
+-- to their corresponding values.
+-- 
+-- For a given `v` for which an instance of 
+-- `SchemeDomain` exists, it computes an association list
+-- mapping addresses to the heap allocated-values of the domain.
+-- 
+-- This can be used as the basis for a `Data.DMap`. 
+type SchemeAdrs v = '[
+   Adr  v :-> Vlu (Adr v),
+   PAdr v :-> Vlu (PAdr v),
+   VAdr v :-> Vlu (VAdr v),
+   SAdr v :-> Vlu (SAdr v) 
+   ]
+
+
+-- | Generate a set of inclusion constraints for the `SchemeAdrs` 
+-- association list.
+type family GenerateInclusion xs ks :: Constraint where 
+   GenerateInclusion '[]                ks = ()
+   GenerateInclusion (KV adr vlu ': xs) ks = (Has ks (KV adr vlu), GenerateInclusion xs ks)
+
+-- Set of inclusion constraints for `SchemeAdrs`
+type StoreDefinedFor v = 
+   (GenerateInclusion (SchemeAdrs v) (SchemeAdrs v), NoDuplicates (SchemeAdrs v))

maf2-typelevel/src/Data/TypeLevel/List.hs

@@ -1,11 +1,17 @@
-{-# LANGUAGE UndecidableInstances, PolyKinds, FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances, PolyKinds, FlexibleInstances, FlexibleContexts #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
-module Data.TypeLevel.List(Has) where
+module Data.TypeLevel.List(Has, NoDuplicates) where
 
 import GHC.TypeError
 
+
+-- | Class that has an instance when the given type level list `l`
+--  contains the given value `v`
 class Has (l :: [k]) (v :: k)
 instance {-# OVERLAPPABLE #-} (Has xs x) => Has (y ': xs) x
 instance {-# OVERLAPPING #-} Has (x ': xs) x
 instance TypeError (Text "value not in list") => Has '[] v
 
+-- | Predicate that is satisfied when the gien list does not contain duplicates
+class NoDuplicates (l :: [k]) 
+instance NoDuplicates l -- TODO: implement