Modular abstract interpretation #668

robrix · 2022-02-25T18:19:47Z

This PR:

Brings in the modular abstract interpretation mechanisms (e.g. the linking code) that I forgot to bring over following Parametric modular interpretation #659.
Extends the Exception domain to support modular abstract interpretation.
Depends on Exception tracking #666.
Depends on Move & rename the analyses to group them together #667.
Depends on Support ghc 9.2 tclem/lingo-haskell#14 (sort of).

robrix

I intend to fix the export problem in a follow-up PR; this is, therefore, ready for review.

robrix · 2022-04-04T19:10:36Z

semantic-analysis/.ghci.repl

+-- 9.2+
+:seti -Wno-missing-kind-signatures
+:seti -Wno-missing-signatures


We now support 9.2, but only for semantic-analysis (for now).

robrix · 2022-04-04T19:11:31Z

semantic-analysis/python.tsg

+(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


This lets us import imports 😊

robrix · 2022-04-04T19:13:09Z

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

+     => (term -> m ExcSet)
+     -> (term -> m ExcSet) )
+  -> File term
+  -> m (File (Module ExcSet))


Note that this is the first of our analyses to return a Module (and thus to support modular analysis). Unfortunately, because we don't yet track exports, we can't do linking properly.

robrix · 2022-04-04T19:14:16Z

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

+runStatement :: ([Message] -> a -> m r) -> StatementC m a -> m r
+runStatement k (StatementC m) = runState (k . reverse) [] m


Statement effects just track sequential, imperative directives, currently limited to imports. This collects them into Messages which are then returned via this handler.

robrix · 2022-04-04T19:15:29Z

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

+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


This convenience wraps up a pattern common among the (0-CFA) analyses into a convenient bundle. It's also a great example of exposing effects while hiding carriers, the essence of abstraction.

robrix · 2022-04-04T19:16:20Z

semantic-analysis/src/Analysis/Module.hs

+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 b' (imports m Set.\\ Map.keysSet ms) (exports m) u' where
+  (u', b') = foldl' (\ (u, b) -> resolve u b . exports) (unknown m, body m) (Map.restrictKeys ms (imports m))
+  resolve u b e = (u Set.\\ Map.keysSet e, b . mappend (Map.restrictKeys e u))


Brought in verbatim from membrane. I intend to tidy this up in a future PR, as it's somewhat unreadable as-is.

Yeah, it’s a bit dense. Would you mind taking a run at it now? Even pulling out and naming the fold function would help a bit.

robrix · 2022-04-04T19:17:41Z

semantic-analysis/src/Analysis/Syntax.hs

+data Term
+  = Var Name
+  | Noop
+  | Iff Term Term Term
+  | Bool Bool
+  | String Text
+  | Throw Term
+  | Let Name Term Term
+  | Import (NonEmpty Text)
+  deriving (Eq, Ord, Show)


The tagless final class, and the Print and Interpret instantiations of it are gone, because defining an Ord instance for Interpret would have been agonizing. Instead, we parse into a first-order, initial encoding: plain old data.

Plain old data is (usually) my favorite kind of data!

It's just, it was so nice! But too clever by half.

robrix · 2022-04-04T19:18:27Z

semantic-analysis/src/Analysis/Syntax.hs

@@ -134,48 +106,66 @@ let' n v m = do

 -- Parsing

-parseFile :: Syntax rep => FilePath -> IO (Either (A.JSONPath, String) (Maybe rep))
+parseFile :: (Has (Throw String) sig m, MonadIO m) => FilePath -> m (File Term)


We also parse into a File, which is convenient since we use those for analysis (so that we can service file/line/etc directives).

robrix · 2022-04-04T19:20:36Z

semantic-analysis/src/Analysis/Syntax.hs

    pure (index, node, node <$ guard (ty == "module")))
+
+parseType :: A.Object -> [A.Value] -> String -> A.Parser (IntMap.IntMap Term -> Term)


I pulled this and the rest of parseNode's where clause to the top level, mostly to make it tidier and give them type signatures. The only real change otherwise is using Term constructors in parseType here instead of Syntax methods.

robrix · 2022-04-04T19:21:12Z

semantic-source/CHANGELOG.md

+# 0.1.0.2
+
+- Support ghc 9.2.
+


I bumped semantic-source, which turned out to be rather confusing, but eh, it's out there now.

patrickt · 2022-04-08T19:36:59Z

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

+
+-- Messages
+
+data Message


newtype here?

Expectation is that there'll be other message types, but in the meantime, yeah, good call.

patrickt · 2022-04-08T19:38:54Z

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

+import Data.List.NonEmpty (NonEmpty)
+import Data.Text
+
+-- Statement effect


Can you expand a little on this? Where is this intended to be used, etc?

patrickt · 2022-04-08T19:39:06Z

semantic-analysis/src/Analysis/Module.hs

+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 b' (imports m Set.\\ Map.keysSet ms) (exports m) u' where
+  (u', b') = foldl' (\ (u, b) -> resolve u b . exports) (unknown m, body m) (Map.restrictKeys ms (imports m))
+  resolve u b e = (u Set.\\ Map.keysSet e, b . mappend (Map.restrictKeys e u))


Yeah, it’s a bit dense. Would you mind taking a run at it now? Even pulling out and naming the fold function would help a bit.

patrickt · 2022-04-08T19:42:33Z

semantic-analysis/src/Analysis/Syntax.hs

+data Term
+  = Var Name
+  | Noop
+  | Iff Term Term Term
+  | Bool Bool
+  | String Text
+  | Throw Term
+  | Let Name Term Term
+  | Import (NonEmpty Text)
+  deriving (Eq, Ord, Show)


Plain old data is (usually) my favorite kind of data!

patrickt · 2022-04-08T19:43:40Z

semantic-analysis/src/Analysis/Syntax.hs

-    let' n v' (eval (b (Interpret (pure (pure v'))))))
+evalModule :: (Has (Env addr) sig m, HasLabelled Store (Store addr val) sig m, Has (Dom val) sig m) => (Term -> S.StatementC m val) -> (Term -> m (Module val))
+evalModule f i = S.runStatement mk (eval f i) where
+  mk msgs b = pure (Module (const b) (Set.fromList (map (\ (S.Import cs) -> name (Text.intercalate (pack ".") (toList cs))) msgs)) mempty mempty)


Some let-bindings here would go a long way.

I think I'm going to 🔥 them instead, as there's no way to provide the body, unknowns, and exports independent of the domain type anyway.

patrickt · 2022-04-08T19:44:02Z

semantic-analysis/src/Analysis/Syntax.hs

+    -- FIXME: this should get the path to the source file, not the path to the JSON.
+    -- FIXME: this should use the span of the source file, not an empty span.


Do you want to fix these now or later?

Later, definitely.

robrix · 2022-04-11T15:24:04Z

by Allie Brosh, Hyperbole and a Half

robrix added 2 commits February 25, 2022 13:16

Blank commit so I can open a PR early.

4d5a121

Add a module for modular modules.

cfd3a09

Base automatically changed from rhea-range to master March 1, 2022 17:34

robrix added 27 commits March 1, 2022 12:35

Ignore some warnings.

52fea09

Merge branch 'master' into modular-mechanics

5515fc5

Tweak bounds so semantic-source builds.

90c5d14

Disable CUSK warnings.

aa5c305

Tested with 9.2.1.

22ce94a

Bump the semantic-source version.

d2b4841

Changelog.

da58814

Loosen bounds.

c526457

Use Aeson's Key API instead of packing Text explicitly.

b551323

Update the set of modules to load.

b640cb1

Ignore some warnings in the REPL.

0a4544c

🔥 warnings we don't care about.

ccb964e

Succeed.

59fab3d

Define a Module type.

be067de

Add imports to modules.

2b0308e

Add exports to modules.

862ee70

Add unknown symbols.

8d74085

Define module sets.

9498d1c

Define linking.

51e9f06

Define a Semigroup instance for ModuleSet.

551a1c2

Ignore some files.

67c6371

Add imports to the JSON.

3d4c10a

Bind everything in a where clause.

96876c6

Close over the edges.

da672d9

Add a signature for parseType.

2a1a4d6

Parse imports from the JSON.

e2c620f

Give identifiers a type.

3460f99

robrix added 14 commits April 1, 2022 14:14

🔥 Print.

eca9c56

Evaluate terms.

50e7046

Switch the entry points over to Term.

dc2b0cc

🔥 Interpret.

8886693

🔥 the Syntax class.

88bea16

Compat. with older aesons.

5875760

Support the full range of interpretation for ExcSet.

3e6b09e

Derive some instances for Message.

6acd6be

Merge exception sets.

fc6e4f5

Extract a function producing the results of a run.

9613961

Construct modules.

37a66ad

Define a generalized running helper.

454a2b1

Provide state for the store.

e8e01cf

Use runFiles for exception tracing.

4e07d54

robrix marked this pull request as ready for review April 4, 2022 19:09

robrix requested a review from a team as a code owner April 4, 2022 19:09

robrix commented Apr 4, 2022

View reviewed changes

robrix mentioned this pull request Apr 4, 2022

Track exports in exception tracing modules #675

Merged

4 tasks

patrickt reviewed Apr 8, 2022

View reviewed changes

robrix added 7 commits April 8, 2022 16:01

newtype.

004e22f

📝 the Statement effect module.

5f3221a

Rename variables.

c00f666

Unpack exports in resolve.

69ecdc4

🔥 a pointless shared binding.

99b82b2

Rename resolve.

ef559e0

🔥 evalModule.

128aebc

patrickt approved these changes Apr 11, 2022

View reviewed changes

robrix merged commit 4cfe7cc into master Apr 11, 2022

robrix deleted the modular-mechanics branch April 11, 2022 15:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Modular abstract interpretation #668

Modular abstract interpretation #668

robrix commented Feb 25, 2022 •

edited

Loading

robrix left a comment

robrix Apr 4, 2022

robrix Apr 4, 2022

robrix Apr 4, 2022

robrix Apr 4, 2022

robrix Apr 4, 2022

robrix Apr 4, 2022

patrickt Apr 8, 2022

robrix Apr 4, 2022

patrickt Apr 8, 2022

robrix Apr 8, 2022

robrix Apr 4, 2022

robrix Apr 4, 2022

robrix Apr 4, 2022

patrickt Apr 8, 2022

robrix Apr 8, 2022

patrickt Apr 8, 2022

robrix Apr 8, 2022

patrickt Apr 8, 2022

patrickt Apr 8, 2022

patrickt Apr 8, 2022

robrix Apr 8, 2022

patrickt Apr 8, 2022

robrix Apr 8, 2022

robrix commented Apr 11, 2022 •

edited

Loading

		runStatement :: ([Message] -> a -> m r) -> StatementC m a -> m r
		runStatement k (StatementC m) = runState (k . reverse) [] m

		pure (index, node, node <$ guard (ty == "module")))

		parseType :: A.Object -> [A.Value] -> String -> A.Parser (IntMap.IntMap Term -> Term)

		-- FIXME: this should get the path to the source file, not the path to the JSON.
		-- FIXME: this should use the span of the source file, not an empty span.

Modular abstract interpretation #668

Modular abstract interpretation #668

Conversation

robrix commented Feb 25, 2022 • edited Loading

robrix left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robrix commented Apr 11, 2022 • edited Loading

robrix commented Feb 25, 2022 •

edited

Loading

robrix commented Apr 11, 2022 •

edited

Loading