-
Notifications
You must be signed in to change notification settings - Fork 459
Generalize analyses over the term type #209
Changes from all commits
fcf6540
56984fa
7b6b6a4
05fa90e
fdc20a4
c82623d
104bdac
465319b
9acaaae
65e2184
54430ac
3387eac
e022b47
7e7f33c
99d9a8d
2666f6c
5c67ea0
6652520
97ae6e9
813cde3
e287557
8b8a330
b926114
4553d59
fde2a44
2559f58
2dde200
1192971
c3cf286
ea174b2
021350b
a549039
bd8f0ca
d817530
da0d780
15e5731
2c28e53
e9853c1
0b86f91
bd5aea6
8ad510d
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,4 +1,4 @@ | ||
| {-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} | ||
| {-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RankNTypes, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} | ||
| module Analysis.Concrete | ||
| ( Concrete(..) | ||
| , concrete | ||
|
|
@@ -20,7 +20,6 @@ import Control.Effect.NonDet | |
| import Control.Effect.Reader hiding (Local) | ||
| import Control.Effect.State | ||
| import Control.Monad ((<=<), guard) | ||
| import qualified Data.Core as Core | ||
| import Data.File | ||
| import Data.Function (fix) | ||
| import qualified Data.IntMap as IntMap | ||
|
|
@@ -30,7 +29,6 @@ import qualified Data.Map as Map | |
| import Data.Name | ||
| import Data.Semigroup (Last (..)) | ||
| import qualified Data.Set as Set | ||
| import Data.Term | ||
| import Data.Text (Text, pack) | ||
| import Data.Traversable (for) | ||
| import Prelude hiding (fail) | ||
|
|
@@ -41,17 +39,17 @@ type Env = Map.Map User Precise | |
| newtype FrameId = FrameId { unFrameId :: Precise } | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
| data Concrete | ||
| = Closure Loc User (Term (Core.Ann :+: Core.Core) User) Env | ||
| data Concrete term | ||
| = Closure Loc User term Env | ||
| | Unit | ||
| | Bool Bool | ||
| | String Text | ||
| | Record Env | ||
| deriving (Eq, Ord, Show) | ||
| -- NB: We derive the 'Semigroup' instance for 'Concrete' to take the second argument. This is equivalent to stating that the return value of an imperative sequence of statements is the value of its final statement. | ||
| deriving Semigroup via Last Concrete | ||
| deriving Semigroup via Last (Concrete term) | ||
|
|
||
| recordFrame :: Concrete -> Maybe Env | ||
| recordFrame :: Concrete term -> Maybe Env | ||
| recordFrame (Record frame) = Just frame | ||
| recordFrame _ = Nothing | ||
|
|
||
|
|
@@ -60,44 +58,64 @@ newtype Frame = Frame | |
| } | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
| type Heap = IntMap.IntMap Concrete | ||
| type Heap term = IntMap.IntMap (Concrete term) | ||
|
|
||
| data Edge = Lexical | Import | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
|
|
||
| -- | Concrete evaluation of a term to a value. | ||
| -- | ||
| -- >>> map fileBody (snd (concrete [File (Loc "bool" emptySpan) (Core.bool True)])) | ||
| -- >>> map fileBody (snd (concrete eval [File (Loc "bool" emptySpan) (Core.bool True)])) | ||
| -- [Right (Bool True)] | ||
| concrete :: [File (Term (Core.Ann :+: Core.Core) User)] -> (Heap, [File (Either (Loc, String) Concrete)]) | ||
| concrete | ||
| :: (Foldable term, Show (term User)) | ||
| => (forall sig m | ||
| . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Abstracting this evaluator over any This list of constraints will eventually grow as we factor bits of |
||
| => Analysis (term User) Precise (Concrete (term User)) m | ||
| -> (term User -> m (Concrete (term User))) | ||
| -> (term User -> m (Concrete (term User))) | ||
| ) | ||
| -> [File (term User)] | ||
| -> (Heap (term User), [File (Either (Loc, String) (Concrete (term User)))]) | ||
| concrete eval | ||
| = run | ||
| . runFresh | ||
| . runHeap | ||
| . traverse runFile | ||
|
|
||
| runFile :: ( Carrier sig m | ||
| , Effect sig | ||
| , Member Fresh sig | ||
| , Member (State Heap) sig | ||
| ) | ||
| => File (Term (Core.Ann :+: Core.Core) User) | ||
| -> m (File (Either (Loc, String) Concrete)) | ||
| runFile file = traverse run file | ||
| . traverse (runFile eval) | ||
|
|
||
| runFile | ||
| :: ( Carrier sig m | ||
| , Effect sig | ||
| , Foldable term | ||
| , Member Fresh sig | ||
| , Member (State (Heap (term User))) sig | ||
| , Show (term User) | ||
| ) | ||
| => (forall sig m | ||
| . (Carrier sig m, Member (Reader Loc) sig, MonadFail m) | ||
| => Analysis (term User) Precise (Concrete (term User)) m | ||
| -> (term User -> m (Concrete (term User))) | ||
| -> (term User -> m (Concrete (term User))) | ||
| ) | ||
| -> File (term User) | ||
| -> m (File (Either (Loc, String) (Concrete (term User)))) | ||
| runFile eval file = traverse run file | ||
| where run = runReader (fileLoc file) | ||
| . runFailWithLoc | ||
| . runReader @Env mempty | ||
| . fix (eval concreteAnalysis) | ||
|
|
||
| concreteAnalysis :: ( Carrier sig m | ||
| , Foldable term | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We need |
||
| , Member Fresh sig | ||
| , Member (Reader Env) sig | ||
| , Member (Reader Loc) sig | ||
| , Member (State Heap) sig | ||
| , Member (State (Heap (term User))) sig | ||
| , MonadFail m | ||
| , Show (term User) | ||
| ) | ||
| => Analysis Precise Concrete m | ||
| => Analysis (term User) Precise (Concrete (term User)) m | ||
| concreteAnalysis = Analysis{..} | ||
| where alloc _ = fresh | ||
| bind name addr m = local (Map.insert name addr) m | ||
|
|
@@ -133,7 +151,7 @@ concreteAnalysis = Analysis{..} | |
| pure (val >>= lookupConcrete heap n) | ||
|
|
||
|
|
||
| lookupConcrete :: Heap -> User -> Concrete -> Maybe Precise | ||
| lookupConcrete :: Heap term -> User -> Concrete term -> Maybe Precise | ||
| lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete | ||
| where -- look up the name in a concrete value | ||
| inConcrete = inFrame <=< maybeA . recordFrame | ||
|
|
@@ -150,7 +168,7 @@ lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete | |
| maybeA = maybe empty pure | ||
|
|
||
|
|
||
| runHeap :: StateC Heap m a -> m (Heap, a) | ||
| runHeap :: StateC (Heap term) m a -> m (Heap term, a) | ||
| runHeap = runState mempty | ||
|
|
||
|
|
||
|
|
@@ -159,7 +177,7 @@ runHeap = runState mempty | |
| -- > λ let (heap, res) = concrete [ruby] | ||
| -- > λ writeFile "/Users/rob/Desktop/heap.dot" (export (addressStyle heap) (heapAddressGraph heap)) | ||
| -- > λ :!dot -Tsvg < ~/Desktop/heap.dot > ~/Desktop/heap.svg | ||
| heapGraph :: (Precise -> Concrete -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a | ||
| heapGraph :: (Precise -> Concrete term -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap term -> G.Graph a | ||
| heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h) | ||
| where graph k v rest = (G.vertex (vertex k v) `G.connect` outgoing v) `G.overlay` rest | ||
| outgoing = \case | ||
|
|
@@ -169,14 +187,14 @@ heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h) | |
| Closure _ _ _ env -> foldr (G.overlay . edge (Left Lexical)) G.empty env | ||
| Record frame -> Map.foldrWithKey (\ k -> G.overlay . edge (Right k)) G.empty frame | ||
|
|
||
| heapValueGraph :: Heap -> G.Graph Concrete | ||
| heapValueGraph :: Heap term -> G.Graph (Concrete term) | ||
| heapValueGraph h = heapGraph (const id) (const fromAddr) h | ||
| where fromAddr addr = maybe G.empty G.vertex (IntMap.lookup addr h) | ||
|
|
||
| heapAddressGraph :: Heap -> G.Graph (EdgeType, Precise) | ||
| heapAddressGraph :: Heap term -> G.Graph (EdgeType term, Precise) | ||
| heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G.vertex . (,) . either Edge Slot) | ||
|
|
||
| addressStyle :: Heap -> G.Style (EdgeType, Precise) Text | ||
| addressStyle :: Heap term -> G.Style (EdgeType term, Precise) Text | ||
| addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes } | ||
| where vertex (_, addr) = pack (show addr) <> " = " <> maybe "?" fromConcrete (IntMap.lookup addr heap) | ||
| edgeAttributes _ (Slot name, _) = ["label" G.:= name] | ||
|
|
@@ -191,12 +209,13 @@ addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes } | |
| Record _ -> "{}" | ||
| showPos (Pos l c) = pack (show l) <> ":" <> pack (show c) | ||
|
|
||
| data EdgeType | ||
| data EdgeType term | ||
| = Edge Edge | ||
| | Slot User | ||
| | Value Concrete | ||
| | Value (Concrete term) | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
|
|
||
| -- $setup | ||
| -- >>> :seti -XOverloadedStrings | ||
| -- >>> import qualified Data.Core as Core | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -33,7 +33,7 @@ eval :: ( Carrier sig m | |
| , MonadFail m | ||
| , Semigroup value | ||
| ) | ||
| => Analysis address value m | ||
| => Analysis (Term (Ann :+: Core) User) address value m | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
| -> (Term (Ann :+: Core) User -> m value) | ||
| -> (Term (Ann :+: Core) User -> m value) | ||
| eval Analysis{..} eval = \case | ||
|
|
@@ -214,14 +214,14 @@ ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' stateme | |
| __semantic_truthy = "__semantic_truthy" | ||
|
|
||
|
|
||
| data Analysis address value m = Analysis | ||
| data Analysis term address value m = Analysis | ||
| { alloc :: User -> m address | ||
| , bind :: forall a . User -> address -> m a -> m a | ||
| , lookupEnv :: User -> m (Maybe address) | ||
| , deref :: address -> m (Maybe value) | ||
| , assign :: address -> value -> m () | ||
| , abstract :: (Term (Ann :+: Core) User -> m value) -> User -> Term (Ann :+: Core) User -> m value | ||
| , apply :: (Term (Ann :+: Core) User -> m value) -> value -> value -> m value | ||
| , abstract :: (term -> m value) -> User -> term -> m value | ||
| , apply :: (term -> m value) -> value -> value -> m value | ||
| , unit :: m value | ||
| , bool :: Bool -> m value | ||
| , asBool :: value -> m Bool | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -13,60 +13,62 @@ import Control.Effect.Fresh | |
| import Control.Effect.NonDet | ||
| import Control.Effect.Reader | ||
| import Control.Effect.State | ||
| import qualified Data.Core as Core | ||
| import qualified Data.Map as Map | ||
| import Data.Maybe (fromMaybe) | ||
| import Data.Monoid (Alt(..)) | ||
| import qualified Data.Set as Set | ||
| import Data.Term (Term) | ||
|
|
||
| type Cache name a = Map.Map (Term (Core.Ann :+: Core.Core) name) (Set.Set a) | ||
| type Heap name a = Map.Map name (Set.Set a) | ||
| newtype Cache term a = Cache { unCache :: Map.Map term (Set.Set a) } | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Without the |
||
| deriving (Eq, Ord, Show) | ||
|
|
||
| type Heap address a = Map.Map address (Set.Set a) | ||
|
|
||
| newtype FrameId name = FrameId { unFrameId :: name } | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
|
|
||
| convergeTerm :: forall m sig a name | ||
| convergeTerm :: forall m sig a term address proxy | ||
| . ( Carrier sig m | ||
| , Effect sig | ||
| , Eq address | ||
| , Member Fresh sig | ||
| , Member (State (Heap name a)) sig | ||
| , Member (State (Heap address a)) sig | ||
| , Ord a | ||
| , Ord name | ||
| , Ord term | ||
| ) | ||
| => (Term (Core.Ann :+: Core.Core) name -> NonDetC (ReaderC (Cache name a) (StateC (Cache name a) m)) a) | ||
| -> Term (Core.Ann :+: Core.Core) name | ||
| => proxy address | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We didn’t mention the address type anywhere else, so we needed a dummy parameter to keep it unambiguous. (We could also have used
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. +1 on avoiding |
||
| -> (term -> NonDetC (ReaderC (Cache term a) (StateC (Cache term a) m)) a) | ||
| -> term | ||
| -> m (Set.Set a) | ||
| convergeTerm eval body = do | ||
| convergeTerm _ eval body = do | ||
| heap <- get | ||
| (cache, _) <- converge (Map.empty :: Cache name a, heap :: Heap name a) $ \ (prevCache, _) -> runState Map.empty . runReader prevCache $ do | ||
| (cache, _) <- converge (Cache Map.empty :: Cache term a, heap :: Heap address a) $ \ (prevCache, _) -> runState (Cache Map.empty) . runReader prevCache $ do | ||
| _ <- resetFresh . runNonDetM Set.singleton $ eval body | ||
| get | ||
| pure (fromMaybe mempty (Map.lookup body cache)) | ||
| pure (fromMaybe mempty (Map.lookup body (unCache cache))) | ||
|
|
||
| cacheTerm :: forall m sig a name | ||
| cacheTerm :: forall m sig a term | ||
| . ( Alternative m | ||
| , Carrier sig m | ||
| , Member (Reader (Cache name a)) sig | ||
| , Member (State (Cache name a)) sig | ||
| , Member (Reader (Cache term a)) sig | ||
| , Member (State (Cache term a)) sig | ||
| , Ord a | ||
| , Ord name | ||
| , Ord term | ||
| ) | ||
| => (Term (Core.Ann :+: Core.Core) name -> m a) | ||
| -> (Term (Core.Ann :+: Core.Core) name -> m a) | ||
| => (term -> m a) | ||
| -> (term -> m a) | ||
| cacheTerm eval term = do | ||
| cached <- gets (Map.lookup term) | ||
| cached <- gets (Map.lookup term . unCache) | ||
| case cached :: Maybe (Set.Set a) of | ||
| Just results -> foldMapA pure results | ||
| Nothing -> do | ||
| results <- asks (fromMaybe mempty . Map.lookup term) | ||
| modify (Map.insert term (results :: Set.Set a)) | ||
| results <- asks (fromMaybe mempty . Map.lookup term . unCache) | ||
| modify (Cache . Map.insert term (results :: Set.Set a) . unCache) | ||
| result <- eval term | ||
| result <$ modify (Map.insertWith (<>) term (Set.singleton (result :: a))) | ||
| result <$ modify (Cache . Map.insertWith (<>) term (Set.singleton (result :: a)) . unCache) | ||
|
|
||
| runHeap :: name -> ReaderC (FrameId name) (StateC (Heap name a) m) b -> m (Heap name a, b) | ||
| runHeap addr m = runState (Map.singleton addr Set.empty) (runReader (FrameId addr) m) | ||
| runHeap :: StateC (Heap address a) m b -> m (Heap address a, b) | ||
| runHeap m = runState (Map.empty) m | ||
|
|
||
| -- | Fold a collection by mapping each element onto an 'Alternative' action. | ||
| foldMapA :: (Alternative m, Foldable t) => (b -> m a) -> t b -> m a | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We no longer rely directly on imports of
Data.Coreor any other syntax. We do still rely onAnalysis.Evalfor theAnalysisrecord, but it could easily be moved elsewhere (and will eventually be factored into effects anyway).This means that we could in principle split the analyses off into a new package, which is a good sign that we’ve got the right separation of concerns going.