Annotated core nodes

daedalus-core/daedalus-core.cabal

@@ -45,6 +45,7 @@ library
     Daedalus.Core.TH.Ops,
     Daedalus.Core.ShrinkBiasedOr,
     Daedalus.Core.InlineCase,
+    Daedalus.Core.CFG,    
     Daedalus.Core.Semantics.Parser,
     Daedalus.Core.Semantics.Env,
     Daedalus.Core.Semantics.Expr,

daedalus-core/src/Daedalus/Core/Basics.hs

@@ -72,6 +72,7 @@ data Annot =
     SrcAnnot Text
   | SrcRange SourceRange  -- ^ Reference to something in the original source
   | NoFail                -- ^ The grammar is known to not fail
+  | NodeID GUID
   deriving (Generic,NFData,Show)
 
 type Label = Text
@@ -231,7 +232,7 @@ instance PP Annot where
       SrcAnnot t -> pp t
       SrcRange r -> pp r
       NoFail     -> "NoFail"
-
+      NodeID g   -> "id:" <> pp g
 
 instance PP Type where
   ppPrec n ty =

daedalus-core/src/Daedalus/Core/CFG.hs

@@ -0,0 +1,207 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- This module exports two closely related APIs: a pass to annotate a
+-- (un-annotated) module with GUIDs, one for each node; and a pass to
+-- turn those annotations into a CFG.
+
+-- Construct a control flow graph and an associated annotated Module
+
+module Daedalus.Core.CFG
+  ( addNodeIDs
+  , pattern WithNodeID
+  , cfg
+  , NodeID
+  , CFGModule(..)
+  , CFG
+  , CFGFun(..)
+  , CFGSimpleNode(..)
+  , CFGNode(..)
+  , cfgFunToDot
+  ) where
+
+import           Data.Functor   (($>))
+import           Data.List      (partition)
+import           Data.Map       (Map)
+import qualified Data.Map       as Map
+import           GHC.Generics   (Generic)
+import           MonadLib       (WriterT, put, runWriterT)
+
+import           Daedalus.Core
+import           Daedalus.GUID  (GUID, HasGUID, getNextGUID)
+import           Daedalus.Panic (panic)
+import           Daedalus.PP
+
+{-# COMPLETE WithNodeID #-}
+pattern WithNodeID :: NodeID -> [Annot] -> Grammar -> Grammar
+pattern WithNodeID n anns g <- (getNodeIDPat -> (n, anns, g))
+
+getNodeIDPat :: Grammar -> (NodeID, [Annot], Grammar)
+getNodeIDPat (skipGetAnnot -> (anns', g))
+  | ([NodeID n], anns) <- partition isNodeID anns' = (n, anns, g)
+  | otherwise = panic "Missing NodeID annotation" []
+  where
+    isNodeID (NodeID {}) = True
+    isNodeID _           = False
+
+-- ----------------------------------------------------------------------------------------
+-- Decorating grammar nodes
+
+addNodeIDs :: HasGUID m => Module -> m Module
+addNodeIDs mo = do
+  gfs <- traverse (traverse addNodeIDsG) (mGFuns mo)
+  pure mo { mGFuns = gfs }
+
+addNodeIDsG :: HasGUID m => Grammar -> m Grammar
+addNodeIDsG (Annot a g) = Annot a <$> addNodeIDsG g
+addNodeIDsG g = do
+  nid <- freshNodeID
+  Annot (NodeID nid) <$> gebChildrenG addNodeIDsG pure pure g
+
+-- ----------------------------------------------------------------------------------------
+-- Construct CFG
+
+-- Entry
+cfg :: HasGUID m => Module -> m CFGModule
+cfg m = do
+  m_cfgfuns <- traverse cfgGFun (mGFuns m)
+  let cfgfuns = Map.fromList [ (cfgfunName f, f) | Just f <- m_cfgfuns ]
+  pure (CFGModule cfgfuns)
+
+-- ----------------------------------------------------------------------------------------
+-- CFG datatype
+
+type NodeID = GUID
+
+data CFGModule = CFGModule
+  { cfgFuns  :: Map FName CFGFun
+  } deriving (Generic)
+
+type CFG = Map NodeID CFGNode  
+
+data CFGFun = CFGFun
+  { cfgfunEntry :: !NodeID
+  , cfgfunExit  :: !NodeID
+  , cfgfunName  :: !FName
+  , cfgfunCFG   :: !CFG
+  -- , cfgfunGrammars :: Map NodeID Grammar
+  } deriving (Generic)
+
+-- We ignore Annot
+data CFGSimpleNode =
+  CPure Expr
+  | CGetStream
+  | CSetStream Expr
+  | CMatch Sem Match
+  | CCall FName [Expr]
+
+-- Basically Grammar without Do/Let
+data CFGNode =
+  CSimple (Maybe Name) CFGSimpleNode NodeID
+  | CFail
+  | COr Bool NodeID NodeID
+  | CCase (Case NodeID)
+  | CLoop (Maybe Name) (LoopClass' Expr NodeID) NodeID
+
+-- ----------------------------------------------------------------------------------------
+-- Workers
+
+freshNodeID :: HasGUID m => m NodeID
+freshNodeID = getNextGUID
+
+cfgGFun :: HasGUID m => Fun Grammar -> m (Maybe CFGFun)
+cfgGFun fu =
+  case fDef fu of
+    Def b -> do
+      exitN <- freshNodeID
+      (inN, nodes) <- runWriterT (cfgG Nothing exitN b)
+      let cfgfun = CFGFun
+            { cfgfunEntry = inN
+            , cfgfunExit  = exitN
+            , cfgfunName  = fName fu
+            , cfgfunCFG   = nodes
+            }
+      pure (Just cfgfun)
+    External -> pure Nothing
+
+cfgG :: HasGUID m => Maybe Name -> NodeID -> Grammar -> WriterT CFG m NodeID
+cfgG m_x exitN (WithNodeID inN _anns g) =
+  case g of
+    Pure e -> simple (CPure e)
+    GetStream    -> simple CGetStream
+    SetStream e  -> simple (CSetStream e)
+    Match s m    -> simple (CMatch s m)
+    Fail {}      -> emitNode CFail
+
+    Do_ lhs rhs   -> goDo Nothing lhs rhs
+    Do  n lhs rhs -> goDo (Just n) lhs rhs
+    Let n e rhs   -> do
+      rhsN <- cfgG (Just n) exitN rhs
+      emitNode (CSimple m_x (CPure e) rhsN)
+
+    OrBiased lhs rhs   -> goOr True lhs rhs
+    OrUnbiased lhs rhs -> goOr False lhs rhs
+    Call fn es -> simple (CCall fn es)
+    Annot _a _g' -> panic "Unexpected Annot" []    
+    GCase cs   -> do
+      cs' <- traverse (cfgG m_x exitN) cs
+      emitNode (CCase cs')
+    Loop lc -> do
+      lc' <- traverse (cfgG m_x inN) lc -- loop back here
+      emitNode (CLoop m_x lc' exitN)
+  where
+    goDo m_y lhs rhs = do
+      rhsN <- cfgG m_x exitN rhs
+      cfgG m_y rhsN lhs
+
+    goOr biased lhs rhs = do
+      lN <- cfgG m_x exitN lhs
+      rN <- cfgG m_x exitN rhs
+      emitNode (COr biased lN rN) $> lN -- Ignore id of Do, use the id of the first non-do in the AST.
+
+    simple n = emitNode (CSimple m_x n exitN)
+    emitNode node = tell (Map.singleton inN node) $> inN
+
+    tell = put -- to be consistent with mtl
+
+-- ----------------------------------------------------------------------------------------
+-- Pretty printing
+
+cfgFunToDot :: CFGFun -> Doc
+cfgFunToDot f =
+  ("digraph " <> pp (cfgfunName f) <> " " <> lbrace)
+  $+$ nest 2 (vcat (prelude ++ nodes))
+  $+$ rbrace
+  where
+    prelude = [ "init -> " <> pp (cfgfunEntry f) <> semi
+              , "init [style = invis];"
+              , pp (cfgfunExit f) <> " [style = invis];"
+              ]
+    nodes   = concat [ mkNode k n |  (k, n) <- Map.toList (cfgfunCFG f) ]
+    mkNode nid n =
+      let (lbl, edges) =
+            case n of
+              CSimple m_x sn nxtN -> (mkSimple m_x sn, [(nid, nxtN, Nothing)])
+              CFail -> ("Fail", [])
+              COr b l r -> ("Or" <> if b then " (biased) " else "", [(nid, l, Nothing), (nid, r, Nothing)])
+              CCase (Case n' pats) -> ("Case " <> pp n', [ (nid, l, Just (pp pat)) | (pat, l) <- pats ])
+              CLoop m_x lc nxtN -> ( maybe empty (\x -> pp x <> " = ") m_x <> "Loop"
+                                   , [ (nid, loopClassBody lc, Just "loop"), (nid, nxtN, Just "exit") ])
+          edges' = [ pp l1 <> " -> " <> pp l2 <> maybe empty (brackets . (<>) "label = ". doubleQuotes) m_lbl <> semi
+                   | (l1, l2, m_lbl) <- edges ]
+      in ( pp nid <> " " <> brackets ("label = " <> doubleQuotes lbl) <> semi ) : edges'
+
+    mkSimple m_x sn =
+      let pfx = maybe empty (\x -> pp x <> " = ") m_x
+      in pfx <> case sn of
+        CPure e -> pp e
+        CGetStream -> "GetStream"
+        CSetStream e -> "SetStream " <> pp e
+        CMatch s m  -> ppMatch s m
+        CCall fn es  -> pp fn <> hsep (map pp es)
+
+
+
+

src/Daedalus/Driver.hs

@@ -45,13 +45,15 @@ module Daedalus.Driver
   , passConstFold
   , passDeterminize
   , passNorm
+  , passAddNodeIDs
   , passMayFail
   , passShrinkBiasedOr
   , passInlineCase
   , passWarnFork
   , passVM
   , ddlRunPass
 
+
     -- * State
   , State(..)
   , ddlState
@@ -134,6 +136,7 @@ import qualified Daedalus.Core.Determinize as Core
 import qualified Daedalus.Core.Effect as Core
 import qualified Daedalus.Core.ShrinkBiasedOr as Core
 import qualified Daedalus.Core.InlineCase as Core
+import qualified Daedalus.Core.CFG as Core
 import qualified Daedalus.DDL2Core as Core
 import qualified Daedalus.VM   as VM
 import qualified Daedalus.VM.Compile.Decl as VM
@@ -831,6 +834,9 @@ passConstFold = coreToCore "specialise types" Core.constFold
 passDeterminize :: ModuleName -> Daedalus ()
 passDeterminize = coreToCore "determinize" (pure . Core.determinizeModule)
 
+passAddNodeIDs :: ModuleName -> Daedalus ()
+passAddNodeIDs = coreToCore "add node IDs" Core.addNodeIDs
+
 passNorm :: ModuleName -> Daedalus ()
 passNorm = coreToCore "norm" (pure . Core.normM)
 

talos/app/CommandLine.hs

@@ -9,7 +9,7 @@ import Options.Applicative
 
 data Outfile = AllOutput FilePath | PatOutput FilePath
 
-data Mode = SynthesisMode | SummaryMode | DumpCoreMode
+data Mode = SynthesisMode | SummaryMode | DumpCoreMode | CFGDotMode
 
 data Options =
   Options { optSolver    :: FilePath
@@ -139,8 +139,9 @@ patOutputOpt = strOption
 modeOpt :: Parser Mode
 modeOpt = flag' SummaryMode ( long "summary" <> help "Print out analysis results")
           <|> flag' DumpCoreMode ( long "dump-core" <> help "Print out intermediate core")
+          <|> flag' CFGDotMode ( long "cfg-dot" <> help "Print out the control flow graph(s)")
           <|> pure SynthesisMode -- defaultx
-          
+
 entryOpt :: Parser String
 entryOpt = strOption
     ( long "entry"

talos/app/Main.hs

@@ -13,11 +13,13 @@ import qualified Streaming.Prelude     as S
 import           System.Console.ANSI
 import           System.IO             (IOMode (..), hFlush, openFile, stdout)
 
+import           Daedalus.Core.CFG (cfg, cfgFunToDot, cfgFuns)
 import           Daedalus.PP
 import           Talos
 
 import           CommandLine
-
+import Daedalus.GUID (runFresh)
+import Data.Foldable (traverse_)
 
 -- debugging
 -- import qualified SimpleSMT as S
@@ -36,13 +38,19 @@ main = do
     SynthesisMode -> doSynthesis opts
     SummaryMode   -> doSummary opts
     DumpCoreMode  -> doDumpCore opts
-
+    CFGDotMode    -> doCFGDot opts
 
 doDumpCore :: Options -> IO ()
 doDumpCore opts = do
   (_mainRule, md, _nguid) <- runDaedalus (optDDLInput opts) (optInvFile opts) (optDDLEntry opts) (optNoLoops opts)
   print (pp md)
 
+doCFGDot :: Options -> IO ()
+doCFGDot opts = do
+  (_mainRule, md, nguid) <- runDaedalus (optDDLInput opts) (optInvFile opts) (optDDLEntry opts) (optNoLoops opts)
+  let (cfgm, _nguid') = runFresh (cfg md) nguid
+  traverse_ (print . pp . cfgFunToDot) (cfgFuns cfgm)
+
 doSummary :: Options -> IO ()
 doSummary opts = do
   putStrLn "Summarising ..."

talos/src/Talos.hs

@@ -227,7 +227,7 @@ runDaedalus inFile m_invFile m_entry noLoops = daedalus $ do
   passConstFold specMod
 
   entry <- ddlGetFName mm entryName
-
+  
   md    <- ddlGetAST specMod astCore >>= ddlRunPass . allPassesM entry
 
   nguid <- ddlRunPass getNextGUID

talos/src/Talos/Passes.hs

@@ -7,6 +7,8 @@ import Daedalus.GUID
 import Daedalus.Core
 import Daedalus.Core.Type
 import Daedalus.Core.Normalize
+import Daedalus.Core.CFG (addNodeIDs)
+
 -- import Daedalus.Core.Inline
 import qualified Data.Text as Text
 import Daedalus.PP (showPP)
@@ -15,13 +17,15 @@ import Control.Monad (zipWithM)
 import Talos.Passes.LiftExpr (liftExprM)
 import Talos.Passes.NoBytesPatterns (noBytesPatternsM)
 
+
 allPassesM :: (Monad m, HasGUID m) => FName -> Module -> m Module
 allPassesM _entry m = noBytesPatternsM m >>=
                       pure . removeUnitsM >>=
                       liftExprM >>=
                       nameBoundExprM >>=
                       nameMatchResultsM >>=
-                      pure . normM
+                      pure . normM >>=
+                      addNodeIDs
 
 -- ----------------------------------------------------------------------------------------
 -- Name non-variable bound expressions

talos/talos.cabal

@@ -106,6 +106,7 @@ executable talos
                      , daedalus
                      , daedalus-value
                      , daedalus-utils
+                     , daedalus-core                     
                      , optparse-applicative
                      , bytestring
                      , streaming