From efd654f334d4c228d057b0ee983ff092f54c7d89 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 16 Aug 2024 16:03:03 -0400 Subject: [PATCH 1/3] cli: Allow client libraries to use `IO` to create `ExtensionImpl` This is needed in Macaw. --- crucible-cli/app/Main.hs | 2 +- crucible-cli/src/Lang/Crucible/CLI.hs | 8 ++++---- crucible-cli/src/Lang/Crucible/CLI/Options.hs | 2 +- crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/crucible-cli/app/Main.hs b/crucible-cli/app/Main.hs index d2a47b423..7ac7a9fe1 100644 --- 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 index 3ad8171c5..85bb985c5 100644 --- a/crucible-cli/src/Lang/Crucible/CLI.hs +++ b/crucible-cli/src/Lang/Crucible/CLI.hs @@ -114,7 +114,7 @@ defaultSimulateProgramHooks = SimulateProgramHooks simulateProgramWithExtension :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) - => (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) + => (forall sym. IsSymInterface sym => sym -> 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 +159,7 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = (UseCFG ssa (postdomInfo ssa)) m) fwdDecFnBindings cs - let ext = mkExt sym + ext <- mkExt sym let simCtx = initSimContext bak emptyIntrinsicTypes ha outh fns ext () let simSt = InitialState simCtx gst defaultAbortHandler retType $ runOverrideSim retType $ @@ -215,7 +215,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 +257,7 @@ 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. IsSymInterface sym => sym -> 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 index e178b3b01..8079e62b4 100644 --- a/crucible-cli/src/Lang/Crucible/CLI/Options.hs +++ b/crucible-cli/src/Lang/Crucible/CLI/Options.hs @@ -53,7 +53,7 @@ parseCheck = main :: (?parserHooks :: ParserHooks ext, IsSyntaxExtension ext) => String -> - (forall sym. IsSymInterface sym => sym -> ExtensionImpl () sym ext) -> + (forall sym. IsSymInterface sym => sym -> 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 index 675b8556b..106e37acb 100644 --- a/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs +++ b/crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs @@ -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. IsSymInterface sym => sym -> 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 \ No newline at end of file From 7d1ed447f7dfcd87ae2062cee9a9f3e0a9052e25 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 16 Aug 2024 16:19:26 -0400 Subject: [PATCH 2/3] cli: Allow client libraries to use `bak` to create `ExtensionImpl` --- crucible-cli/src/Lang/Crucible/CLI.hs | 6 +++--- crucible-cli/src/Lang/Crucible/CLI/Options.hs | 4 ++-- crucible-llvm-cli/src/Lang/Crucible/LLVM/CLI.hs | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs index 85bb985c5..b4ec6e1f1 100644 --- a/crucible-cli/src/Lang/Crucible/CLI.hs +++ b/crucible-cli/src/Lang/Crucible/CLI.hs @@ -114,7 +114,7 @@ defaultSimulateProgramHooks = SimulateProgramHooks simulateProgramWithExtension :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) - => (forall sym. IsSymInterface sym => sym -> IO (ExtensionImpl () sym ext)) + => (forall sym bak. IsSymBackend sym bak => 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 +159,7 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks = (UseCFG ssa (postdomInfo ssa)) m) fwdDecFnBindings cs - ext <- mkExt sym + ext <- mkExt bak let simCtx = initSimContext bak emptyIntrinsicTypes ha outh fns ext () let simSt = InitialState simCtx gst defaultAbortHandler retType $ runOverrideSim retType $ @@ -257,7 +257,7 @@ data Command -- line), and this function takes care of the rest. execCommand :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => - (forall sym. IsSymInterface sym => sym -> IO (ExtensionImpl () sym ext)) -> + (forall sym bak. IsSymBackend sym bak => 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 index 8079e62b4..f50f6b4ef 100644 --- a/crucible-cli/src/Lang/Crucible/CLI/Options.hs +++ b/crucible-cli/src/Lang/Crucible/CLI/Options.hs @@ -3,7 +3,7 @@ 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) @@ -53,7 +53,7 @@ parseCheck = main :: (?parserHooks :: ParserHooks ext, IsSyntaxExtension ext) => String -> - (forall sym. IsSymInterface sym => sym -> IO (ExtensionImpl () sym ext)) -> + (forall sym bak. IsSymBackend sym bak => 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 index 106e37acb..5006903ab 100644 --- 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 -> IO (ExtensionImpl () sym LLVM)) -> + (forall sym bak. IsSymBackend sym bak => bak -> IO (ExtensionImpl () sym LLVM)) -> SimulateProgramHooks LLVM -> IO a) -> IO a From e068194188b38cbcf3b10aa52f0574a4480418bb Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 16 Aug 2024 16:43:28 -0400 Subject: [PATCH 3/3] cli: Allow clients to know `sym ~ ExprBuilder` for `ExtensionImpl` --- crucible-cli/src/Lang/Crucible/CLI.hs | 6 ++++-- crucible-cli/src/Lang/Crucible/CLI/Options.hs | 5 ++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs index b4ec6e1f1..13fde1727 100644 --- 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 bak. IsSymBackend sym bak => bak -> IO (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 @@ -257,7 +258,8 @@ data Command -- line), and this function takes care of the rest. execCommand :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext) => - (forall sym bak. IsSymBackend sym bak => bak -> IO (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 index f50f6b4ef..2d688f4b1 100644 --- a/crucible-cli/src/Lang/Crucible/CLI/Options.hs +++ b/crucible-cli/src/Lang/Crucible/CLI/Options.hs @@ -1,5 +1,6 @@ {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} module Lang.Crucible.CLI.Options (main) where @@ -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 bak. IsSymBackend sym bak => bak -> IO (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 =