-
Notifications
You must be signed in to change notification settings - Fork 459
Records #203
Changes from all commits
0115512
ebafd64
de51991
83cd925
218c8f3
00beb2d
e259bc0
f373ca4
1398c99
2606e1e
3459b3b
972a52d
79f5737
cbf9f43
8c06d7b
a10cdc9
15a125b
6f5e578
e809a29
38efb33
ef24642
bff499e
f24ef8b
b5a0624
db448e6
1d50aec
2a5c181
c175bc3
c9b328e
94546f7
c495b4b
85c1815
5e8a2c2
b851621
8373e3a
d5afd84
2c13ed8
fb318fa
4cc6520
cd3f73a
c613b0c
b0bc2cf
5f21602
8bc79bd
fea81ee
6c5240b
d41d775
384c221
9b6f7dd
958d32f
1abddf4
9ffd3f8
77cb532
2a60039
d299288
a1f41e1
900bdbe
acfcee1
3f7ac5e
37caa4d
0c80fd2
69b2151
325dc9d
45a3d6f
9522662
ed94f7e
a25d971
724ae17
0797316
1ce4153
b8bcad0
a39e773
a77ecdb
f9eea38
52da8b7
043d308
b43bdbb
539f8db
45723e7
344b5bd
a5ac6f3
0cb3f18
f851b2b
09fdb30
024d2d4
200bf17
5c033ab
77acb91
f1c4d8a
390b25a
50f9b82
9b3164a
ed0231c
4e98c04
b0ee9ee
aa7f1fc
1caf99b
a63e7c3
16413e1
6050b95
fa9c991
6aa85af
1e43157
0045283
7b29063
6b250c7
b119712
a96eadb
47b43cf
453b898
3da182d
9612762
56d40da
edbea69
99668a3
5b68260
76eb3e2
b58ddb4
b700740
d1671a6
59af553
08878f1
9ccd11e
068941e
e03236d
308066f
8e5c216
4bd2129
0d530dc
e4470bc
3b67414
ac3f487
3d65ae9
f10cbb2
0254bc9
15430ba
41a31d1
7c24672
a0bf65f
339585f
93eba20
7b0a415
ab07e5a
e2ec37e
eb2ede6
7c686d1
0d2f05a
dd6d9a0
28404ae
b80dd53
78bd32e
372ed98
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 FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeOperators, UndecidableInstances #-} | ||
| {-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-} | ||
| module Analysis.Concrete | ||
| ( Concrete(..) | ||
| , concrete | ||
|
|
@@ -27,10 +27,11 @@ import qualified Data.IntMap as IntMap | |
| import qualified Data.IntSet as IntSet | ||
| import Data.Loc | ||
| import qualified Data.Map as Map | ||
| import Data.Monoid (Alt(..)) | ||
| import Data.Name | ||
| import qualified Data.Set as Set | ||
| import Data.Term | ||
| import Data.Text (Text, pack) | ||
| import Data.Traversable (for) | ||
| import Prelude hiding (fail) | ||
|
|
||
| type Precise = Int | ||
|
|
@@ -40,25 +41,27 @@ newtype FrameId = FrameId { unFrameId :: Precise } | |
| deriving (Eq, Ord, Show) | ||
|
|
||
| data Concrete | ||
| = Closure Loc User (Term Core.Core User) Precise | ||
| = Closure Loc User (Term Core.Core User) Env | ||
| | Unit | ||
| | Bool Bool | ||
| | String Text | ||
| | Obj Frame | ||
| | Record Env | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
| objectFrame :: Concrete -> Maybe Frame | ||
| objectFrame (Obj frame) = Just frame | ||
| objectFrame _ = Nothing | ||
| recordFrame :: Concrete -> Maybe Env | ||
| recordFrame (Record frame) = Just frame | ||
| recordFrame _ = Nothing | ||
|
|
||
| data Frame = Frame | ||
| { frameEdges :: [(Core.Edge, Precise)] | ||
| , frameSlots :: Env | ||
| newtype Frame = Frame | ||
| { frameSlots :: Env | ||
| } | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
| type Heap = IntMap.IntMap Concrete | ||
|
|
||
| data Edge = Lexical | Import | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
|
|
||
| -- | Concrete evaluation of a term to a value. | ||
| -- | ||
|
|
@@ -74,46 +77,39 @@ concrete | |
| runFile :: ( Carrier sig m | ||
| , Effect sig | ||
| , Member Fresh sig | ||
| , Member (Reader FrameId) sig | ||
| , Member (State Heap) sig | ||
| ) | ||
| => File (Term Core.Core User) | ||
| -> m (File (Either (Loc, String) Concrete)) | ||
| runFile file = traverse run file | ||
| where run = runReader (fileLoc file) | ||
| . runFailWithLoc | ||
| . runReader @Env mempty | ||
| . fix (eval concreteAnalysis) | ||
|
|
||
| concreteAnalysis :: ( Carrier sig m | ||
| , Member Fresh sig | ||
| , Member (Reader Env) sig | ||
|
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. Rather than modelling the local environment explicitly in the heap, we resume using an |
||
| , Member (Reader Loc) sig | ||
| , Member (Reader FrameId) sig | ||
| , Member (State Heap) sig | ||
| , MonadFail m | ||
| ) | ||
| => Analysis Precise Concrete m | ||
| concreteAnalysis = Analysis{..} | ||
| where alloc _ = fresh | ||
| bind name addr = modifyCurrentFrame (updateFrameSlots (Map.insert name addr)) | ||
| lookupEnv n = do | ||
| FrameId frameAddr <- ask | ||
| val <- deref frameAddr | ||
| heap <- get | ||
| pure (val >>= lookupConcrete heap n) | ||
| bind name addr m = local (Map.insert name addr) m | ||
| lookupEnv n = asks (Map.lookup n) | ||
|
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. Wow, way way way way better. |
||
| deref = gets . IntMap.lookup | ||
| assign addr value = modify (IntMap.insert addr value) | ||
| abstract _ name body = do | ||
| loc <- ask | ||
| FrameId parentAddr <- ask | ||
| pure (Closure loc name body parentAddr) | ||
| apply eval (Closure loc name body parentAddr) a = do | ||
| frameAddr <- fresh | ||
| assign frameAddr (Obj (Frame [(Core.Lexical, parentAddr)] mempty)) | ||
| local (const loc) . (frameAddr ...) $ do | ||
| env <- asks (flip Map.restrictKeys (Set.delete name (foldMap Set.singleton body))) | ||
| pure (Closure loc name body env) | ||
| apply eval (Closure loc name body env) a = do | ||
| local (const loc) $ do | ||
| addr <- alloc name | ||
| assign addr a | ||
| bind name addr | ||
| eval body | ||
| local (const (Map.insert name addr env)) (eval body) | ||
| apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function" | ||
| unit = pure Unit | ||
| bool b = pure (Bool b) | ||
|
|
@@ -122,30 +118,24 @@ concreteAnalysis = Analysis{..} | |
| string s = pure (String s) | ||
| asString (String s) = pure s | ||
| asString v = fail $ "Cannot coerce " <> show v <> " to String" | ||
| -- FIXME: differential inheritance (reference fields instead of copying) | ||
| -- FIXME: copy non-lexical parents deeply? | ||
| frame = do | ||
| lexical <- asks unFrameId | ||
| pure (Obj (Frame [(Core.Lexical, lexical)] mempty)) | ||
| -- FIXME: throw an error | ||
| -- FIXME: support dynamic imports | ||
| edge e addr = modifyCurrentFrame (\ (Frame ps fs) -> Frame ((e, addr) : ps) fs) | ||
| addr ... m = local (const (FrameId addr)) m | ||
|
|
||
| updateFrameSlots f frame = frame { frameSlots = f (frameSlots frame) } | ||
|
|
||
| modifyCurrentFrame f = do | ||
| addr <- asks unFrameId | ||
| Just (Obj frame) <- deref addr | ||
| assign addr (Obj (f frame)) | ||
| record fields = do | ||
| fields' <- for fields $ \ (name, value) -> do | ||
| addr <- alloc name | ||
| assign addr value | ||
| pure (name, addr) | ||
| pure (Record (Map.fromList fields')) | ||
| addr ... n = do | ||
| val <- deref addr | ||
| heap <- get | ||
| pure (val >>= lookupConcrete heap n) | ||
|
|
||
|
|
||
| lookupConcrete :: Heap -> User -> Concrete -> Maybe Precise | ||
| lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete | ||
| where -- look up the name in a concrete value | ||
| inConcrete = inFrame <=< maybeA . objectFrame | ||
| inConcrete = inFrame <=< maybeA . recordFrame | ||
| -- look up the name in a specific 'Frame', with slots taking precedence over parents | ||
| inFrame (Frame ps fs) = maybeA (Map.lookup name fs) <|> getAlt (foldMap (Alt . inAddress . snd) ps) | ||
| inFrame fs = maybeA (Map.lookup name fs) <|> (maybeA (Map.lookup "__semantic_super" fs) >>= inAddress) | ||
|
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. We have a top-level define for
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. It’s not top-level, and I’m actually pretty sure that I don’t want this to live in here long-term; it should be encoded in the compilers, so that different languages can specify their own lookup strategies. This will be important for e.g. |
||
| -- look up the name in the value an address points to, if we haven’t already visited it | ||
| inAddress addr = do | ||
| visited <- get | ||
|
|
@@ -157,27 +147,24 @@ lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete | |
| maybeA = maybe empty pure | ||
|
|
||
|
|
||
| runHeap :: (Carrier sig m, Member Fresh sig) => ReaderC FrameId (StateC Heap m) a -> m (Heap, a) | ||
| runHeap m = do | ||
| addr <- fresh | ||
| runState (IntMap.singleton addr (Obj (Frame [] mempty))) (runReader (FrameId addr) m) | ||
| runHeap :: StateC Heap m a -> m (Heap, a) | ||
| runHeap = runState mempty | ||
|
|
||
|
|
||
| -- | 'heapGraph', 'heapValueGraph', and 'heapAddressGraph' allow us to conveniently export SVGs of the heap: | ||
| -- | ||
| -- > λ 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 Core.Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a | ||
| heapGraph :: (Precise -> Concrete -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap -> 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 | ||
| Unit -> G.empty | ||
| Bool _ -> G.empty | ||
| String _ -> G.empty | ||
| Closure _ _ _ parentAddr -> edge (Left Core.Lexical) parentAddr | ||
| Obj frame -> fromFrame frame | ||
| fromFrame (Frame es ss) = foldr (G.overlay . uncurry (edge . Left)) (foldr (G.overlay . uncurry (edge . Right)) G.empty (Map.toList ss)) es | ||
| 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 h = heapGraph (const id) (const fromAddr) h | ||
|
|
@@ -189,20 +176,20 @@ heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G.vertex . (,) | |
| addressStyle :: Heap -> G.Style (EdgeType, 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] | ||
| edgeAttributes _ (Edge Core.Import, _) = ["color" G.:= "blue"] | ||
| edgeAttributes _ (Edge Core.Lexical, _) = ["color" G.:= "green"] | ||
| edgeAttributes _ _ = [] | ||
| edgeAttributes _ (Slot name, _) = ["label" G.:= name] | ||
| edgeAttributes _ (Edge Import, _) = ["color" G.:= "blue"] | ||
| edgeAttributes _ (Edge Lexical, _) = ["color" G.:= "green"] | ||
| edgeAttributes _ _ = [] | ||
| fromConcrete = \case | ||
| Unit -> "()" | ||
| Bool b -> pack $ show b | ||
| String s -> pack $ show s | ||
| Closure (Loc p (Span s e)) n _ _ -> "\\\\ " <> n <> " [" <> p <> ":" <> showPos s <> "-" <> showPos e <> "]" | ||
| Obj _ -> "{}" | ||
| Record _ -> "{}" | ||
| showPos (Pos l c) = pack (show l) <> ":" <> pack (show c) | ||
|
|
||
| data EdgeType | ||
| = Edge Core.Edge | ||
| = Edge Edge | ||
| | Slot User | ||
| | Value Concrete | ||
| deriving (Eq, Ord, Show) | ||
|
|
||
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.
I wonder whether strict maps are preferable? Probably something we should file an issue about.
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.
I’m not particularly interested in the performance of the concrete analysis at the moment given that we’re only intending to use it for validation, but we can revisit that later, for sure.