Analysis effects #379

robrix · 2019-11-07T18:13:52Z

This PR replaces the Analysis record type with effects & carriers modelling the environment, heap, and domain.

Depends on Multi component ghcide setup #374.
Fixes Is quasiquotation in Core a good idea? #358.

Doing it in script/ghci-flags means it has to be silent, which is super confusing/surprising. Doing it in script/repl means we can see what it’s up to.

This reverts commit d278a01.

This is goofy as hell but we don’t have maybeM here.

This reverts commit 29e09be.

robrix

Ready for review!

robrix · 2019-12-20T17:46:06Z

.ghci.sample

-:def! no-pretty \ _ -> pure ":set -interactive-print System.IO.print"
-:def! r \_ -> pure ":reload\n:pretty"
+:set -package-id prtty-smpl-3.1.1.0-c89f0500
+:set -interactive-print Text.Pretty.Simple.pPrint


semantic-ast depends on pretty-simple now, which makes it much more challenging to use -package pretty-simple in your ~/.ghci file since ghci “helpfully” ends up loading it twice.

You can avoid that issue by using -package-id, at the cost of having to keep that up to date whenever semantic gets an updated version of it.

I’m not happy with this, but I don’t know a better means of doing this aside from e.g. introducing a new registered package which nothing in semantic depends on just to re-export pretty-simple’s interface, or using a different pretty-printer in semantic than used in the REPL.

Yikes! We should probably submit a bug somewhere to somebody?

robrix · 2019-12-20T17:47:16Z

.stylish-haskell.yaml

@@ -183,7 +183,7 @@ steps:
      #   between actual import and closing bracket.
      #
      # Default: true
-      align: true
+      align: false


This formats LANGUAGE pragmas each on a new line, with the #-} markers unaligned (for diff minimality).

{-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} …

robrix · 2019-12-20T17:48:07Z

script/ghci-flags

-# do a build of dependencies up front to ensure they’re all available
-cabal v2-build -v0 all --only-dependencies
-


This didn’t work out as well as I’d hoped—the silent build means that you can get ghcide and/or script/repl appearing to just hang while it deals with building dependencies.

I’ve moved this to script/repl and removed the -v0.

robrix · 2019-12-20T17:48:50Z

script/ghci-flags

@@ -43,6 +40,7 @@ function flags {
  echo "-isemantic-java/src"
  echo "-isemantic-json/src"
  echo "-isemantic-python/src"
+  echo "-isemantic-python/test"


This lets script/repl find the source files in semantic-python’s tests.

robrix · 2019-12-20T17:49:24Z

script/repl

+# do a build of dependencies up front to ensure they’re all available
+cabal v2-build all --enable-benchmarks --enable-tests --only-dependencies


In addition to moving this back here and removing the -v0 (which silences all output), this now also ensures that the benchmarks’ & tests’ dependencies have been built before loading the repl.

robrix · 2019-12-20T17:49:44Z

semantic-analysis/src/Analysis/Analysis.hs

-module Analysis.Analysis
-( Analysis(..)
-) where


Success: this module no longer exists!

robrix · 2019-12-20T17:51:12Z

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

+module Analysis.Carrier.Heap.Monovariant
+( -- * Heap carrier
+  HeapC(..)
+  -- * Heap effect
+, module Analysis.Effect.Heap
+) where


Factoring this out means that the abstract analyses get to share a lot of code.

robrix · 2019-12-20T17:51:39Z

semantic-analysis/src/Analysis/Concrete.hs

-{-# LANGUAGE DerivingVia, FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns,
-             OverloadedStrings, RankNTypes, RecordWildCards, ScopedTypeVariables, TypeApplications, TypeOperators,
-             UndecidableInstances #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}


An example of the new LANGUAGE pragma style.

Don’t mind this (though I would encourage everyone to turn on automatic execution of stylish-haskell on save, so we can start migrating to this style without murdering history with whitespace changes).

robrix · 2019-12-20T17:53:48Z

semantic-analysis/src/Analysis/Concrete.hs

-data Concrete term name
-  = Closure Path.AbsRelFile Span name (term name) (Env name)
+data Concrete term
+  = Closure Path.AbsRelFile Span (Named (Scope () term Addr))


By holding a scope parameterized by Addr, Closure obviates the need for the Addr parameter it formerly required.

robrix · 2019-12-20T18:03:10Z

semantic-analysis/src/Analysis/Concrete.hs

-  -> File (term name)
-  -> m (File (Either (Path.AbsRelFile, Span, String) (Concrete term name)))
+  -> File (term Addr)
+  -> m (File (Either (Path.AbsRelFile, Span, String) (Concrete term)))


Instead of parameterizing the incoming terms by some arbitrary name type, we parameterize them by the address type for the analysis in question.

In practice this means that we can only analyze closed terms, since you don’t in general have a way to place addresses in the syntax—there’s no way to allocate them from outside the analysis.

My plan is to deal with this by binding free names—names defined in other modules, for example—with existentials, which we will allocate addresses for and can instantiate however we wish. (This is essentially a more principled but otherwise equivalent approach to holes as used in Evaluatable.) Given an input term with existentials, we should ideally produce a result defined modulo the unknown information which we can then supply to resolve the result after the fact. This will allow us to compute partial & incremental analyses of input programs without requiring configuration.

patrickt · 2020-01-08T17:33:19Z

.ghci.sample

-:def! no-pretty \ _ -> pure ":set -interactive-print System.IO.print"
-:def! r \_ -> pure ":reload\n:pretty"
+:set -package-id prtty-smpl-3.1.1.0-c89f0500
+:set -interactive-print Text.Pretty.Simple.pPrint


Yikes! We should probably submit a bug somewhere to somebody?

patrickt · 2020-01-08T19:03:26Z

semantic-analysis/src/Analysis/Concrete.hs

+         )
+      => Algebra (A.Domain term Addr (Concrete term) :+: sig) (DomainC term m) where
+  alg = \case
+    L (L (A.Unit k)) -> k Unit


These L and R pattern matches are a real doozy.

Don’t see what could be done about them, though.

robrix added 30 commits November 1, 2019 14:51

Define a concrete Env carrier.

3aa3cb5

Derive a MonadFail instance for EnvC.

4f44170

Run the env carrier.

f0739bb

Define a carrier for monovariant Env.

ec94b7d

Stub in a module for the Env effect.

131c804

Move Env into its own module.

7809bd2

Run the env effect.

6305e66

Stub in a module for the precise Env carrier.

d8955fd

Move the precise env carrier to its own module.

06ea57e

Use the env effect in the concrete analysis.

e58db3d

Define a module for the monovariant Env carrier.

778f84b

Move the monovariant Env carrier into its own module.

5fef326

Use the Env effect to define the Analysis.

9e472c5

Use the Env effect to define the import graph analysis.

0f7be20

Use the Env effect to define the scope graph analysis.

eb591f9

Evaluate Core using the Env effect.

6e1383d

Reorder the contexts for ease of type application.

d70a169

Reformat the importGraphAnalysis signature.

17da79f

🔥 the Analysis env fields.

961bf62

Stub in a module for the Heap effect.

6359d96

Move the Heap effect to its own module.

d23f34b

Define a smart constructor for Deref.

b1c2f26

Define a smart constructor for Assign.

ab5b566

Section headings.

2502370

Re-export Carrier & run from the effect modules.

e992998

Stub in a module for a precise heap carrier.

05de03e

Re-export the Heap effect.

b2a329c

Stub in a Heap carrier.

5b8364c

HeapC wraps a state effect.

c3327fa

Define a Carrier instance for Heap.

08e1061

robrix and others added 24 commits December 20, 2019 10:30

Declare the dependency on transformers.

7c9c5f0

Move the cabal build call into script/repl.

537f3c3

Doing it in script/ghci-flags means it has to be silent, which is super confusing/surprising. Doing it in script/repl means we can see what it’s up to.

Build the tests’ dependencies.

935fe94

Build the benchmarks’ dependencies.

a45de13

Fix the semantic-python test build.

c04c59d

Fix a couple of instances.

3821557

Add semantic-python’s tests to the load paths.

f305c38

Correct a type signature.

8894d73

Evaluate closed terms.

540b88c

Correct the package id for the sample .ghci.

bfec95a

Remove the CHECK-JQ directive.

f78d90a

🔥 Analysis.ScopeGraph.

f5efb6a

Split up abstraction into separate constructors.

75a63dd

Don’t repeat ourselves.

6612273

Split Domain into multiple effects.

c07324f

Rename the abstract parameter to value.

a167ded

Alignment.

a6fe9b7

Simplify a pattern match.

1a67082

Placate hlint.

d278a01

Revert "Placate hlint."

e34444e

This reverts commit d278a01.

Trick hlint.

29e09be

This is goofy as hell but we don’t have maybeM here.

Revert "Trick hlint."

55e573e

This reverts commit 29e09be.

Ignore hints in assertEvaluatesTo.

f5c8346

Don’t shout about the HLINT pragma.

4022643

robrix commented Jan 6, 2020

View reviewed changes

robrix marked this pull request as ready for review January 6, 2020 22:29

robrix requested a review from a team January 7, 2020 16:03

patrickt approved these changes Jan 8, 2020

View reviewed changes

robrix merged commit 87d526f into master Jan 14, 2020

robrix deleted the analysis-effects branch January 14, 2020 12:27

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Analysis effects #379

Analysis effects #379

robrix commented Nov 7, 2019 •

edited

Loading

robrix left a comment

robrix Dec 20, 2019

patrickt Jan 8, 2020

robrix Dec 20, 2019

robrix Dec 20, 2019

robrix Dec 20, 2019

robrix Dec 20, 2019

robrix Dec 20, 2019

robrix Dec 20, 2019

robrix Dec 20, 2019

patrickt Jan 8, 2020

robrix Dec 20, 2019

robrix Dec 20, 2019

patrickt Jan 8, 2020

patrickt Jan 8, 2020

patrickt Jan 8, 2020

		# do a build of dependencies up front to ensure they’re all available
		cabal v2-build -v0 all --only-dependencies

		# do a build of dependencies up front to ensure they’re all available
		cabal v2-build all --enable-benchmarks --enable-tests --only-dependencies

Analysis effects #379

Analysis effects #379

Conversation

robrix commented Nov 7, 2019 • 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

robrix commented Nov 7, 2019 •

edited

Loading