Merge pull request #1150 from langston-barrett/lb/crucible-syntax-acfg

crucible-syntax: Remove `ACFG` in favor of `AnyCFG`

crucible-cli/src/Lang/Crucible/CLI.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Lang.Crucible.CLI
   ( simulateProgramWithExtension
@@ -36,6 +37,7 @@ import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.Some (Some(Some))
 
 import qualified Lang.Crucible.CFG.Core as C
+import qualified Lang.Crucible.CFG.Reg as C.Reg
 import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import Lang.Crucible.CFG.Reg
 import Lang.Crucible.CFG.SSAConversion
@@ -141,11 +143,12 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                                   , parsedProgForwardDecs = fds
                                   }) -> do
                 case find isMain cs of
-                  Just (ACFG Ctx.Empty retType mn) ->
-                    do gst <- resolveExternsHook hooks sym externs emptyGlobals
+                  Just (AnyCFG mn@(C.Reg.cfgArgTypes -> Ctx.Empty)) ->
+                    do let retType = C.Reg.cfgReturnType mn
+                       gst <- resolveExternsHook hooks sym externs emptyGlobals
                        fwdDecFnBindings <- resolveForwardDeclarationsHook hooks fds
                        let mainHdl = cfgHandle mn
-                       let fns = foldl' (\(FnBindings m) (ACFG _ _ g) ->
+                       let fns = foldl' (\(FnBindings m) (AnyCFG g) ->
                                           case toSSA g of
                                             C.SomeCFG ssa ->
                                               FnBindings $
@@ -194,7 +197,7 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                   _ -> hPutStrLn outh "No suitable main function found"
 
   where
-  isMain (ACFG _ _ g) = handleName (cfgHandle g) == fromString "main"
+  isMain (AnyCFG g) = handleName (cfgHandle g) == fromString "main"
 
 simulateProgram
    :: FilePath -- ^ The name of the input (appears in source locations)

crucible-concurrency/src/Cruces/CrucesMain.hs

@@ -94,15 +94,17 @@ cruciblesConfig = Crux.Config
       ]
   }
 
-findMain :: FunctionName -> [ACFG ()] -> FnVal sym Ctx.EmptyCtx C.UnitType
+findMain :: FunctionName -> [AnyCFG ()] -> FnVal sym Ctx.EmptyCtx C.UnitType
 findMain mainName cs =
   case find (isFn mainName) cs of
-    Just (ACFG Ctx.Empty C.UnitRepr m) ->
-      HandleFnVal (cfgHandle m)
+    Just (AnyCFG m) ->
+      case (cfgArgTypes m, cfgReturnType m) of
+        (Ctx.Empty, C.UnitRepr) -> HandleFnVal (cfgHandle m)
+        _ -> undefined
     _ ->
       undefined
   where
-    isFn x (ACFG _ _ g) = handleName (cfgHandle g) == x
+    isFn x (AnyCFG g) = handleName (cfgHandle g) == x
 
 run :: Crux.Logs Crux.CruxLogMessage
     => (Crux.CruxOptions, CrucesOptions)
@@ -155,7 +157,7 @@ run (cruxOpts, opts) =
                                           [ case toSSA g of
                                               C.SomeCFG ssa ->
                                                 FnBinding (cfgHandle g) (UseCFG ssa (postdomInfo ssa))
-                                          | ACFG _ _ g <- cs
+                                          | AnyCFG g <- cs
                                           ] ++ exploreBuiltins
                                 )
             res <- Crux.runSimulator cruxOpts { Crux.solver = "yices"

crucible-syntax/CHANGELOG.md

@@ -1,3 +1,10 @@
+# next
+
+* The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`,
+  which serves a similar purpose (hiding the argument and return types). The
+  CFG argument and return types can be recovered via
+  `Lang.Crucible.CFG.Reg.{cfgArgTypes,cfgReturnType}`.
+
 # 0.3
 
 * The return type of `prog`:

crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs

@@ -28,7 +28,6 @@ module Lang.Crucible.Syntax.Concrete
   ( -- * Errors
     ExprErr(..)
   -- * Parsing and Results
-  , ACFG(..)
   , ParserHooks(..)
   , ParsedProgram(..)
   , defaultParserHooks
@@ -89,7 +88,6 @@ import qualified Data.Text as T
 import qualified Data.Vector as V
 import Numeric.Natural
 
-import qualified Lang.Crucible.CFG.Extension as LCCE
 import Lang.Crucible.Syntax.ExprParse hiding (SyntaxError)
 import qualified Lang.Crucible.Syntax.ExprParse as SP
 import Lang.Crucible.Syntax.Monad
@@ -199,7 +197,7 @@ data ParsedProgram ext = ParsedProgram
     -- ^ For each parsed @extern@, map its name to its global variable. It is
     --   the responsibility of the caller to insert each global variable into
     --   the 'SymGlobalState' alongside an appropriate 'RegValue'.
-  , parsedProgCFGs :: [ACFG ext]
+  , parsedProgCFGs :: [AnyCFG ext]
     -- ^ The CFGs for each parsed @defun@.
   , parsedProgForwardDecs :: Map FunctionName SomeHandle
     -- ^ For each parsed @declare@, map its name to its function handle. It is
@@ -1924,16 +1922,6 @@ data Rand ext s t = Rand (AST s) (E ext s t)
 
 --------------------------------------------------------------------------
 
--- | Any CFG, regardless of its arguments and return type, with its helpers
-data ACFG ext :: Type where
-  ACFG :: forall (s :: Type) (init :: Ctx CrucibleType) (ret :: CrucibleType) ext .
-          ( LCCE.IsSyntaxExtension ext ) =>
-          CtxRepr init -> TypeRepr ret ->
-          CFG ext s init ret ->
-          ACFG ext
-
-deriving instance Show (ACFG ext)
-
 data Arg t = Arg AtomName Position (TypeRepr t)
 
 someAssign ::
@@ -2228,7 +2216,7 @@ initParser (FunctionHeader _ (funArgs :: Ctx.Assignment Arg init) _ _ _) (Functi
 cfgs :: ( IsSyntaxExtension ext
         , ?parserHooks :: ParserHooks ext )
      => [AST s]
-     -> TopParser s [ACFG ext]
+     -> TopParser s [AnyCFG ext]
 cfgs = fmap parsedProgCFGs <$> prog
 
 prog :: ( TraverseExt ext
@@ -2240,8 +2228,7 @@ prog defuns =
   do headers <- catMaybes <$> traverse topLevel defuns
      cs <- forM headers $
        \(hdr@(FunctionHeader _ funArgs ret handle _), src@(FunctionSource _ body)) ->
-         do let types = argTypes funArgs
-            initParser hdr src
+         do initParser hdr src
             args <- toList <$> use stxAtoms
             let ?returnType = ret
             st <- get
@@ -2255,7 +2242,7 @@ prog defuns =
                                  LabelID lbl -> lbl
                                  LambdaID {} -> error "initial block is lambda"
                        e' = mkBlock (blockID e) vs (blockStmts e) (blockTerm e)
-                   return $ ACFG types ret $ CFG handle entry (e' : rest)
+                   return $ AnyCFG (CFG handle entry (e' : rest))
      gs <- use stxGlobals
      externs <- use stxExterns
      fds <- uses stxForwardDecs $ fmap $

crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs

@@ -95,7 +95,7 @@ doParseCheck fn theInput pprint outh =
                 assertNoExterns externs
                 assertNoForwardDecs fds
                 forM_ ok $
-                 \(ACFG _ _ theCfg) ->
+                 \(AnyCFG theCfg) ->
                    do C.SomeCFG ssa <- return $ toSSA theCfg
                       hPutStrLn outh $ show $ cfgHandle theCfg
                       hPutStrLn outh $ show $ C.ppCFG' True (postdomInfo ssa) ssa

crucible/src/Lang/Crucible/CFG/Core.hs

@@ -823,7 +823,7 @@ instance PrettyExt ext => Show (SomeCFG ext i r)
   where show cfg = case cfg of SomeCFG c -> show c
 
 -- | Control flow graph.  This data type closes existentially
---   over all the type parameters.
+--   over all the type parameters except @ext@.
 data AnyCFG ext where
   AnyCFG :: CFG ext blocks init ret
          -> AnyCFG ext

crucible/src/Lang/Crucible/CFG/Generator.hs

@@ -134,7 +134,7 @@ import           What4.Symbol
 import           Lang.Crucible.CFG.Core (AnyCFG(..))
 import           Lang.Crucible.CFG.Expr(App(..))
 import           Lang.Crucible.CFG.Extension
-import           Lang.Crucible.CFG.Reg
+import           Lang.Crucible.CFG.Reg hiding (AnyCFG)
 import           Lang.Crucible.CFG.EarlyMergeLoops (earlyMergeLoops)
 import           Lang.Crucible.FunctionHandle
 import           Lang.Crucible.Types

crucible/src/Lang/Crucible/CFG/Reg.hs

@@ -34,9 +34,11 @@ module Lang.Crucible.CFG.Reg
     CFG(..)
   , cfgEntryBlock
   , cfgInputTypes
+  , cfgArgTypes
   , cfgReturnType
   , substCFG
   , SomeCFG(..)
+  , AnyCFG(..)
   , Label(..)
   , substLabel
   , LambdaLabel(..)
@@ -924,7 +926,11 @@ cfgEntryBlock g =
     (Fold.find (\b -> blockID b == LabelID (cfgEntryLabel g)) (cfgBlocks g))
 
 cfgInputTypes :: CFG ext s init ret -> CtxRepr init
-cfgInputTypes g = handleArgTypes (cfgHandle g)
+cfgInputTypes = cfgArgTypes
+{-# DEPRECATED cfgInputTypes "Use cfgArgTypes instead" #-}
+
+cfgArgTypes :: CFG ext s init ret -> CtxRepr init
+cfgArgTypes g = handleArgTypes (cfgHandle g)
 
 cfgReturnType :: CFG ext s init ret -> TypeRepr ret
 cfgReturnType g = handleReturnType (cfgHandle g)
@@ -1007,7 +1013,16 @@ instance PrettyExt ext => Pretty (CFG ext s init ret) where
          , vcat (pretty <$> cfgBlocks g) ]
 
 ------------------------------------------------------------------------
--- SomeCFG
+-- SomeCFG, AnyCFG
 
 -- | 'SomeCFG' is a CFG with an arbitrary parameter 's'.
 data SomeCFG ext init ret = forall s . SomeCFG !(CFG ext s init ret)
+
+-- | Control flow graph.  This data type closes existentially
+--   over all the type parameters except @ext@.
+data AnyCFG ext where
+  AnyCFG :: CFG ext blocks init ret
+         -> AnyCFG ext
+
+instance PrettyExt ext => Show (AnyCFG ext) where
+  show cfg = case cfg of AnyCFG c -> show c

crucible/src/Lang/Crucible/CFG/SSAConversion.hs

@@ -966,7 +966,7 @@ toSSA :: C.IsSyntaxExtension ext
       -> C.SomeCFG ext init ret
 toSSA g = do
   let h = cfgHandle g
-  let initTypes = cfgInputTypes g
+  let initTypes = cfgArgTypes g
   let entry = cfgEntryLabel g
   let blocks = cfgBlocks g
   case resolveBlockMap (handleName h) entry blocks of