Merge pull request #1239 from GaloisInc/lb/cli-ext-impl-io

cli: Allow client libraries to use `IO` to create `ExtensionImpl`
GaloisInc · Aug 20, 2024 · 93bfa7f · 93bfa7f
2 parents 7514e90 + e068194
commit 93bfa7f
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 10 deletions.
diff --git a/crucible-cli/app/Main.hs b/crucible-cli/app/Main.hs
@@ -13,7 +13,7 @@ import qualified Lang.Crucible.CLI.Options as Opts
 main :: IO ()
 main =
   do let ?parserHooks = defaultParserHooks
-     Opts.main "crucible" (\_ -> emptyExtensionImpl) simulationHooks
+     Opts.main "crucible" (\_ -> pure emptyExtensionImpl) simulationHooks
   where
         simulationHooks =
           defaultSimulateProgramHooks

diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -114,7 +114,8 @@ defaultSimulateProgramHooks = SimulateProgramHooks
 
 simulateProgramWithExtension
    :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)
-   => (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext)
+   => (forall sym bak t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) =>
+        bak -> IO (ExtensionImpl () sym ext))
    -> FilePath -- ^ The name of the input (appears in source locations)
    -> Text     -- ^ The contents of the input
    -> Handle   -- ^ A handle that will receive the output
@@ -159,7 +160,7 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                                                   (UseCFG ssa (postdomInfo ssa))
                                                   m)
                                         fwdDecFnBindings cs
-                       let ext = mkExt sym
+                       ext <- mkExt bak
                        let simCtx = initSimContext bak emptyIntrinsicTypes ha outh fns ext ()
                        let simSt  = InitialState simCtx gst defaultAbortHandler retType $
                                       runOverrideSim retType $
@@ -215,7 +216,7 @@ simulateProgram
    -> IO ()
 simulateProgram fn theInput outh profh opts hooks = do
   let ?parserHooks = defaultParserHooks
-  let ext = const emptyExtensionImpl
+  let ext = const (pure emptyExtensionImpl)
   simulateProgramWithExtension ext fn theInput outh profh opts hooks
 
 repl :: 
@@ -257,7 +258,8 @@ data Command
 -- line), and this function takes care of the rest.
 execCommand :: 
   (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) =>
-  (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) ->
+  (forall sym bak t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) =>
+    bak -> IO (ExtensionImpl () sym ext)) ->
   SimulateProgramHooks ext ->
   Command ->
   IO ()

diff --git a/crucible-cli/src/Lang/Crucible/CLI/Options.hs b/crucible-cli/src/Lang/Crucible/CLI/Options.hs
@@ -1,9 +1,10 @@
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Lang.Crucible.CLI.Options (main) where
 
-import Lang.Crucible.Backend (IsSymInterface)
+import Lang.Crucible.Backend (IsSymBackend)
 import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import Lang.Crucible.Simulator.ExecutionTree (ExtensionImpl)
 
@@ -14,6 +15,8 @@ import           Options.Applicative ( (<**>) )
 
 import           Lang.Crucible.CLI
 
+import What4.Expr (ExprBuilder)
+
 file :: String -> Opt.Parser FilePath
 file which = Opt.strArgument (Opt.metavar "FILE" <> Opt.help ("The " <> which <> " file"))
 
@@ -53,7 +56,7 @@ parseCheck =
 main ::
   (?parserHooks :: ParserHooks ext, IsSyntaxExtension ext) =>
   String ->
-  (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) ->
+  (forall sym bak t st fs. (IsSymBackend sym bak, sym ~ ExprBuilder t st fs) => bak -> IO (ExtensionImpl () sym ext)) ->
   SimulateProgramHooks ext ->
   IO ()
 main name ext simulationHooks =

diff --git a/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs b/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs
@@ -15,7 +15,7 @@ import qualified Data.Map as Map
 
 import Data.Parameterized.NatRepr (knownNat)
 
-import Lang.Crucible.Backend (IsSymInterface)
+import Lang.Crucible.Backend (IsSymBackend)
 import Lang.Crucible.FunctionHandle (newHandleAllocator)
 import Lang.Crucible.Simulator.ExecutionTree (ExtensionImpl)
 import Lang.Crucible.Simulator.OverrideSim (writeGlobal)
@@ -43,7 +43,7 @@ import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTyp
 withLlvmHooks ::
   (forall w.
     (HasPtrWidth w, ?parserHooks :: ParserHooks LLVM) =>
-    (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym LLVM) ->
+    (forall sym bak. IsSymBackend sym bak => bak -> IO (ExtensionImpl () sym LLVM)) ->
     SimulateProgramHooks LLVM ->
     IO a) ->
   IO a
@@ -80,5 +80,5 @@ withLlvmHooks k = do
           , setupOverridesHook = setupOverrides
           }
   let ext _ = let ?recordLLVMAnnotation = \_ _ _ -> pure ()
-              in llvmExtensionImpl Mem.defaultMemOptions
+              in pure (llvmExtensionImpl Mem.defaultMemOptions)
   k ext simulationHooks