From 9a8756db08b5c8d676cc0660d88d91f77596a1ea Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Mon, 9 Jul 2018 13:31:15 -0400 Subject: [PATCH 1/6] Define a gensym operation, producing fresh names. Co-Authored-By: Patrick Thomson --- src/Data/Abstract/Name.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Data/Abstract/Name.hs b/src/Data/Abstract/Name.hs index 2abd5a127..abb3d87d6 100644 --- a/src/Data/Abstract/Name.hs +++ b/src/Data/Abstract/Name.hs @@ -2,11 +2,14 @@ module Data.Abstract.Name ( Name -- * Constructors +, gensym , name , nameI , formatName ) where +import Control.Monad.Effect +import Control.Monad.Effect.Fresh import Data.Aeson import qualified Data.Char as Char import Data.Text (Text) @@ -33,6 +36,9 @@ instance Primitive Name where decodePrimitive = Name . LT.toStrict <$> Decode.text <|> I <$> Decode.int primType _ = Bytes +gensym :: (Functor (m effs), Member Fresh effs, Effectful m) => m effs Name +gensym = I <$> fresh + -- | Construct a 'Name' from a 'Text'. name :: Text -> Name name = Name From 2f8f4e367e9c9f904f260298f226c65d4c9baea7 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Mon, 9 Jul 2018 13:31:46 -0400 Subject: [PATCH 2/6] Gensym the names of boxed values. Co-Authored-By: Patrick Thomson --- src/Control/Abstract/Heap.hs | 7 +++++-- src/Control/Abstract/Value.hs | 4 +++- src/Data/Abstract/Evaluatable.hs | 7 +++++-- src/Data/Abstract/Value/Abstract.hs | 2 ++ 4 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/Control/Abstract/Heap.hs b/src/Control/Abstract/Heap.hs index 6f996d811..16cfcab93 100644 --- a/src/Control/Abstract/Heap.hs +++ b/src/Control/Abstract/Heap.hs @@ -53,11 +53,14 @@ putHeap = put modifyHeap :: Member (State (Heap address (Cell address) value)) effects => (Heap address (Cell address) value -> Heap address (Cell address) value) -> Evaluator address value effects () modifyHeap = modify' -box :: Member (Allocator address value) effects +box :: ( Member (Allocator address value) effects + , Member Fresh effects + ) => value -> Evaluator address value effects address box val = do - addr <- alloc "" + name <- gensym + addr <- alloc name assign addr val pure addr diff --git a/src/Control/Abstract/Value.hs b/src/Control/Abstract/Value.hs index c23894a3e..7a713df4d 100644 --- a/src/Control/Abstract/Value.hs +++ b/src/Control/Abstract/Value.hs @@ -254,7 +254,9 @@ subtermAddress :: ( AbstractValue address value effects subtermAddress = address <=< subtermRef -- | Convenience function for boxing a raw value and wrapping it in an Rval -rvalBox :: Member (Allocator address value) effects +rvalBox :: ( Member (Allocator address value) effects + , Member Fresh effects + ) => value -> Evaluator address value effects (ValueRef address) rvalBox val = Rval <$> box val diff --git a/src/Data/Abstract/Evaluatable.hs b/src/Data/Abstract/Evaluatable.hs index e93cfa0f9..7c8640cb0 100644 --- a/src/Data/Abstract/Evaluatable.hs +++ b/src/Data/Abstract/Evaluatable.hs @@ -50,6 +50,7 @@ class (Show1 constr, Foldable constr) => Evaluatable constr where , Member (Env address) effects , Member (Exc (LoopControl address)) effects , Member (Exc (Return address)) effects + , Member Fresh effects , Member (Modules address) effects , Member (Reader ModuleInfo) effects , Member (Reader PackageInfo) effects @@ -149,9 +150,11 @@ instance HasPrelude 'PHP builtInPrint :: ( AbstractIntro value , AbstractFunction address value effects - , Member (Resumable (EnvironmentError address)) effects + , Member (Allocator address value) effects , Member (Env address) effects - , Member (Allocator address value) effects) + , Member Fresh effects + , Member (Resumable (EnvironmentError address)) effects + ) => Name -> Evaluator address value effects address builtInPrint v = do diff --git a/src/Data/Abstract/Value/Abstract.hs b/src/Data/Abstract/Value/Abstract.hs index e678af802..aa4580e0b 100644 --- a/src/Data/Abstract/Value/Abstract.hs +++ b/src/Data/Abstract/Value/Abstract.hs @@ -30,6 +30,7 @@ instance AbstractIntro Abstract where instance ( Member (Allocator address Abstract) effects , Member (Env address) effects , Member (Exc (Return address)) effects + , Member Fresh effects ) => AbstractFunction address Abstract effects where closure names _ body = do @@ -47,6 +48,7 @@ instance ( Member (Allocator address Abstract) effects instance ( Member (Allocator address Abstract) effects , Member (Env address) effects , Member (Exc (Return address)) effects + , Member Fresh effects , Member NonDet effects ) => AbstractValue address Abstract effects where From a86688d9ad1bb5ee237242825dee2e99710fba81 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Mon, 9 Jul 2018 13:34:35 -0400 Subject: [PATCH 3/6] (Re-)define a putEnv operation. Co-Authored-By: Patrick Thomson --- src/Control/Abstract/Environment.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Control/Abstract/Environment.hs b/src/Control/Abstract/Environment.hs index d67a9fe36..5ffcb4be3 100644 --- a/src/Control/Abstract/Environment.hs +++ b/src/Control/Abstract/Environment.hs @@ -3,6 +3,7 @@ module Control.Abstract.Environment ( Environment , Exports , getEnv +, putEnv , export , lookupEnv , bind @@ -29,6 +30,10 @@ import Prologue getEnv :: Member (Env address) effects => Evaluator address value effects (Environment address) getEnv = send GetEnv +-- | Replace the environment. +putEnv :: Member (Env address) effects => (Environment address) -> Evaluator address value effects () +putEnv = send . PutEnv + -- | Add an export to the global export state. export :: Member (Env address) effects => Name -> Name -> Maybe address -> Evaluator address value effects () export name alias addr = send (Export name alias addr) @@ -62,6 +67,7 @@ data Env address m return where Close :: Set Name -> Env address m (Environment address) Locally :: m a -> Env address m a GetEnv :: Env address m (Environment address) + PutEnv :: Environment address -> Env address m () Export :: Name -> Name -> Maybe address -> Env address m () instance Effect (Env address) where @@ -70,6 +76,7 @@ instance Effect (Env address) where handleState c dist (Request (Close names) k) = Request (Close names) (dist . (<$ c) . k) handleState c dist (Request (Locally action) k) = Request (Locally (dist (action <$ c))) (dist . fmap k) handleState c dist (Request GetEnv k) = Request GetEnv (dist . (<$ c) . k) + handleState c dist (Request (PutEnv e) k) = Request (PutEnv e) (dist . (<$ c) . k) handleState c dist (Request (Export name alias addr) k) = Request (Export name alias addr) (dist . (<$ c) . k) runEnv :: Effects effects @@ -94,6 +101,7 @@ handleEnv = \case a <- reinterpret2 handleEnv (raiseEff action) a <$ modify' (Env.pop @address) GetEnv -> get + PutEnv e -> put e Export name alias addr -> modify (Exports.insert name alias addr) -- | Errors involving the environment. From 5d433205d57e9baa1ab0bd107ff1104fab7fd46f Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Mon, 9 Jul 2018 13:36:27 -0400 Subject: [PATCH 4/6] Put the environment instead of running locally. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This fixes an error where caching always looked up a configuration that hadn’t been cached due to `locally` initiating a fresh scope. Co-Authored-By: Patrick Thomson --- src/Analysis/Abstract/Caching.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Analysis/Abstract/Caching.hs b/src/Analysis/Abstract/Caching.hs index 8c0beeca7..b7a83ac3d 100644 --- a/src/Analysis/Abstract/Caching.hs +++ b/src/Analysis/Abstract/Caching.hs @@ -92,8 +92,9 @@ convergingModules :: ( AbstractValue address value effects convergingModules recur m = do c <- getConfiguration (subterm (moduleBody m)) -- Convergence here is predicated upon an Eq instance, not α-equivalence - cache <- converge lowerBound (\ prevCache -> isolateCache . raiseHandler locally $ do + cache <- converge lowerBound (\ prevCache -> isolateCache $ do TermEvaluator (putHeap (configurationHeap c)) + TermEvaluator (putEnv (configurationEnvironment c)) -- We need to reset fresh generation so that this invocation converges. resetFresh 0 $ -- This is subtle: though the calling context supports nondeterminism, we want From 7e450aa14ba9e26a61cdcf87eecbf7669d1dcada Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Mon, 9 Jul 2018 13:47:22 -0400 Subject: [PATCH 5/6] Use gensym in the definition of lambda. Co-Authored-By: Patrick Thomson --- src/Control/Abstract/Primitive.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Control/Abstract/Primitive.hs b/src/Control/Abstract/Primitive.hs index 45d3b3cdf..268850a6e 100644 --- a/src/Control/Abstract/Primitive.hs +++ b/src/Control/Abstract/Primitive.hs @@ -61,7 +61,7 @@ lambda :: (AbstractFunction address value effects, Member Fresh effects) => (Name -> Evaluator address value effects address) -> Evaluator address value effects value lambda body = do - var <- nameI <$> fresh + var <- gensym closure [var] lowerBound (body var) defineBuiltins :: ( AbstractValue address value effects From 37d67801adda44004655c17ada382d1244637d05 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Mon, 9 Jul 2018 13:48:27 -0400 Subject: [PATCH 6/6] :memo: gensym. Co-Authored-By: Patrick Thomson --- src/Data/Abstract/Name.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Data/Abstract/Name.hs b/src/Data/Abstract/Name.hs index abb3d87d6..8c68b1dee 100644 --- a/src/Data/Abstract/Name.hs +++ b/src/Data/Abstract/Name.hs @@ -36,6 +36,7 @@ instance Primitive Name where decodePrimitive = Name . LT.toStrict <$> Decode.text <|> I <$> Decode.int primType _ = Bytes +-- | Generate a fresh (unused) name for use in synthesized variables/closures/etc. gensym :: (Functor (m effs), Member Fresh effs, Effectful m) => m effs Name gensym = I <$> fresh