Merge pull request #668 from github/modular-mechanics

Modular abstract interpretation

semantic-analysis/.ghci.repl

@@ -32,9 +32,12 @@
 -- 8.10+
 :seti -Wno-missing-safe-haskell-mode
 :seti -Wno-prepositive-qualified-module
+-- 9.2+
+:seti -Wno-missing-kind-signatures
+:seti -Wno-missing-signatures
 
 -- We have this one on in the project but not in the REPL to reduce noise
 :seti -Wno-type-defaults
 :set -Wno-unused-packages
 
-:load Analysis.Concrete Analysis.Exception Analysis.Syntax Analysis.Typecheck
+:load Analysis.Analysis.Concrete Analysis.Analysis.Exception Analysis.Syntax Analysis.Analysis.Typecheck

semantic-analysis/.gitignore

@@ -0,0 +1,2 @@
+test.json
+test.py

semantic-analysis/python.tsg

@@ -6,9 +6,26 @@
   attr (@this.node) type = "module"
 }
 
-(identifier) @id
+(identifier) @this
 {
-  node @id.node
+  node @this.node
+  attr (@this.node) type = "identifier"
+  var @this.text = (source-text @this)
+  attr (@this.node) text = (source-text @this)
+}
+
+(import_statement) @this
+{
+  node @this.node
+  attr (@this.node) type = "import"
+}
+
+(import_statement name: (dotted_name (identifier) @id)) @this
+{
+  edge @this.node -> @id.node
+  attr (@id.node) role = "module-name-fragment"
+  attr (@this.node -> @id.node) index = (named-child-index @id)
+  attr (@this.node -> @id.node) text = @id.text
 }
 
 (string) @this

semantic-analysis/script/ghci-flags

@@ -64,8 +64,9 @@ function flags {
   echo "-Wno-name-shadowing"
   echo "-Wno-safe"
   echo "-Wno-unsafe"
-  [[ "$ghc_version" = 8.8.* ]] || [[ "$ghc_version" = 8.10.* ]] && echo "-Wno-missing-deriving-strategies" || true
-  [[ "$ghc_version" = 8.10.* ]] && echo "-Wno-missing-safe-haskell-mode" && echo "-Wno-prepositive-qualified-module" && echo "-Wno-unused-packages"
+  [[ "$ghc_version" = 8.8.* ]] || [[ "$ghc_version" = 8.10.* ]] || [[ "$ghc_version" = 9.2.* ]] && echo "-Wno-missing-deriving-strategies" || true
+  [[ "$ghc_version" = 8.10.* ]] || [[ "$ghc_version" = 9.2.* ]] && echo "-Wno-missing-safe-haskell-mode" && echo "-Wno-prepositive-qualified-module" && echo "-Wno-unused-packages" || true
+  [[ "$ghc_version" = 9.2.* ]] && echo "-Wno-missing-kind-signatures" || true
 }
 
 flags > "$output_file"

semantic-analysis/semantic-analysis.cabal

@@ -39,6 +39,9 @@ common common
     ghc-options:
       -Wno-missing-safe-haskell-mode
       -Wno-prepositive-qualified-module
+  if (impl(ghc >= 9.2))
+    ghc-options:
+      -Wno-missing-kind-signatures
 
 library
   import: common
@@ -49,23 +52,26 @@ library
     Analysis.Analysis.Typecheck
     Analysis.Blob
     Analysis.Carrier.Fail.WithLoc
+    Analysis.Carrier.Statement.State
     Analysis.Carrier.Store.Monovariant
     Analysis.Carrier.Store.Precise
     Analysis.Data.Snoc
     Analysis.Effect.Domain
     Analysis.Effect.Env
+    Analysis.Effect.Statement
     Analysis.Effect.Store
     Analysis.File
     Analysis.FlowInsensitive
     Analysis.Functor.Named
+    Analysis.Module
     Analysis.Name
     Analysis.Project
     Analysis.Reference
     Analysis.Syntax
   build-depends:
-    , aeson                       ^>= 1.4
+    , aeson                        >= 1.4 && < 3
     , base                         >= 4.13 && < 5
-    , bytestring                  ^>= 0.10.8.2
+    , bytestring                   >= 0.10.8.2 && < 0.13
     , containers                  ^>= 0.6
     , fused-effects               ^>= 1.1
     , hashable

semantic-analysis/src/Analysis/Analysis/Exception.hs

@@ -1,25 +1,40 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Analysis.Analysis.Exception
 ( Exception(..)
 , ExcSet(..)
+, exceptionTracing
 , fromExceptions
 , var
 , exc
   -- * Exception tracing analysis
 , ExcC(..)
 ) where
 
+import qualified Analysis.Carrier.Statement.State as A
+import qualified Analysis.Carrier.Store.Monovariant as A
 import           Analysis.Effect.Domain
+import           Analysis.Effect.Env (Env)
+import           Analysis.Effect.Store
+import           Analysis.File
+import           Analysis.FlowInsensitive (cacheTerm, convergeTerm)
+import           Analysis.Module
 import           Analysis.Name
 import           Control.Algebra
 import           Control.Applicative (Alternative (..))
+import           Control.Effect.Labelled
+import           Control.Effect.State
 import qualified Data.Foldable as Foldable
+import           Data.Function (fix)
 import qualified Data.Set as Set
+import qualified Data.Text as Text
 
 -- | Names of exceptions thrown in the guest language and recorded by this analysis.
 --
@@ -47,6 +62,35 @@ exc :: Exception -> ExcSet
 exc e = ExcSet mempty (Set.singleton e)
 
 
+exceptionTracing
+  :: Ord term
+  => ( forall sig m
+     .  (Has (Env A.MAddr) sig m, HasLabelled Store (Store A.MAddr ExcSet) sig m, Has (Dom ExcSet) sig m, Has A.Statement sig m)
+     => (term -> m ExcSet)
+     -> (term -> m ExcSet) )
+  -> [File term]
+  -> (A.MStore ExcSet, [File (Module ExcSet)])
+exceptionTracing eval = A.runFiles (runFile eval)
+
+runFile
+  :: ( Has (State (A.MStore ExcSet)) sig m
+     , Ord term )
+  => ( forall sig m
+     .  (Has (Env A.MAddr) sig m, HasLabelled Store (Store A.MAddr ExcSet) sig m, Has (Dom ExcSet) sig m, Has A.Statement sig m)
+     => (term -> m ExcSet)
+     -> (term -> m ExcSet) )
+  -> File term
+  -> m (File (Module ExcSet))
+runFile eval = traverse run where
+  run
+    = A.runStatement result
+    . A.runEnv @ExcSet
+    . convergeTerm (A.runStore @ExcSet . runExcC . fix (cacheTerm . eval))
+  result msgs sets = do
+    let set = Foldable.fold sets
+        imports = Set.fromList (map (\ (A.Import components) -> name (Text.intercalate (Text.pack ".") (Foldable.toList components))) msgs)
+    pure (Module (const set) imports mempty (freeVariables set))
+
 newtype ExcC m a = ExcC { runExcC :: m a }
   deriving (Alternative, Applicative, Functor, Monad)
 

semantic-analysis/src/Analysis/Carrier/Statement/State.hs

@@ -0,0 +1,43 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Analysis.Carrier.Statement.State
+( -- * Messages
+  Message(..)
+  -- * Statement carrier
+, runStatement
+, StatementC(..)
+  -- * Statement effect
+, module Analysis.Effect.Statement
+) where
+
+import           Analysis.Effect.Statement hiding (Import)
+import qualified Analysis.Effect.Statement as S
+import           Control.Algebra
+import           Control.Carrier.State.Church
+import           Control.Monad.Fail as Fail
+import           Data.List.NonEmpty (NonEmpty)
+import           Data.Text (Text)
+
+-- Messages
+
+newtype Message
+  = Import (NonEmpty Text)
+  deriving (Eq, Ord, Show)
+
+
+-- Statement carrier
+
+runStatement :: ([Message] -> a -> m r) -> StatementC m a -> m r
+runStatement k (StatementC m) = runState (k . reverse) [] m
+
+newtype StatementC m a = StatementC { runStatementC :: StateC [Message] m a }
+  deriving (Applicative, Functor, Monad, Fail.MonadFail)
+
+instance Algebra sig m => Algebra (S.Statement :+: sig) (StatementC m) where
+  alg hdl sig ctx = case sig of
+    L (S.Import ns) -> StatementC ((<$ ctx) <$> modify (Import ns:))
+    R other         -> StatementC (alg (runStatementC . hdl) (R other) ctx)

semantic-analysis/src/Analysis/Carrier/Store/Monovariant.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
@@ -19,10 +20,13 @@ module Analysis.Carrier.Store.Monovariant
 , EnvC(..)
   -- * Env effect
 , module Analysis.Effect.Env
+  -- * Running
+, runFiles
 ) where
 
 import Analysis.Effect.Env
 import Analysis.Effect.Store
+import Analysis.File (File)
 import Analysis.Name
 import Control.Algebra
 import Control.Carrier.State.Church
@@ -83,3 +87,15 @@ instance Has (State (MStore value)) sig m
         pure (MAddr n <$ Map.lookup (MAddr n) store <$ ctx)
 
     R other -> EnvC (alg (runEnv . hdl) other ctx)
+
+
+-- Running
+
+runFiles
+  :: (forall sig m . Has (State (MStore  value)) sig m => File term -> m (File result))
+  -> [File term]
+  -> (MStore value, [File result])
+runFiles runFile
+  = run
+  . runStoreState
+  . traverse runFile

semantic-analysis/src/Analysis/Effect/Statement.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{- |
+The @'Statement'@ effect is designed to provide instrumentation for source-level interactions we need visibility into which are nevertheless not (currently) modelled by expressions: e.g. statements, declarations, certain directives, etc.
+
+Currently this is limited to imports, where the value-level semantics are (for many languages) essentially the unit value, but where the effect of bringing an environment and entire subset of the store into scope are essential to track for modular interpretation.
+-}
+module Analysis.Effect.Statement
+( -- * Statement effect
+  simport
+, Statement(..)
+) where
+
+import Control.Algebra
+import Data.Kind as K
+import Data.List.NonEmpty (NonEmpty)
+import Data.Text
+
+-- Statement effect
+
+simport :: Has Statement sig m => NonEmpty Text -> m ()
+simport ns = send (Import ns)
+
+data Statement (m :: K.Type -> K.Type) k where
+  Import :: NonEmpty Text -> Statement m ()

semantic-analysis/src/Analysis/Module.hs

@@ -0,0 +1,27 @@
+module Analysis.Module
+( Module(..)
+, ModuleSet(..)
+, link
+) where
+
+import           Analysis.Name
+import           Data.Foldable (foldl')
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+
+data Module a = Module
+  { body    :: Map.Map Name a -> a
+  , imports :: Set.Set Name
+  , exports :: Map.Map Name a
+  , unknown :: Set.Set Name
+  }
+
+newtype ModuleSet a = ModuleSet { getModuleSet :: Map.Map Name (Module a) }
+
+instance Semigroup (ModuleSet a) where
+  m1 <> m2 = ModuleSet ((link m2 <$> getModuleSet m1) <> (link m1 <$> getModuleSet m2))
+
+link :: ModuleSet a -> Module a -> Module a
+link (ModuleSet ms) m = Module body' (imports m Set.\\ Map.keysSet ms) (exports m) unknown' where
+  (unknown', body') = foldl' (uncurry resolveSymbolsInModule) (unknown m, body m) (Map.restrictKeys ms (imports m))
+  resolveSymbolsInModule unknown body m = (unknown Set.\\ Map.keysSet (exports m), body . mappend (Map.restrictKeys (exports m) unknown))