RFC: crucible-llvm: Parameterize over memory and pointer types

crucible-llvm/crucible-llvm.cabal

@@ -77,6 +77,7 @@ library
     Lang.Crucible.LLVM.Intrinsics.Libc
     Lang.Crucible.LLVM.Intrinsics.LLVM
     Lang.Crucible.LLVM.MalformedLLVMModule
+    Lang.Crucible.LLVM.Mem
     Lang.Crucible.LLVM.MemModel
     Lang.Crucible.LLVM.MemModel.CallStack
     Lang.Crucible.LLVM.MemModel.CallStack.Internal

crucible-llvm/src/Lang/Crucible/LLVM.hs

@@ -60,22 +60,22 @@ import           What4.ProgramLoc (plSourceLoc)
 --   This will immediately build Crucible CFGs for each function
 --   defined in the module.
 registerModule ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
-   ModuleTranslation arch ->
-   OverrideSim p sym LLVM rtp l a ()
+   ModuleTranslation mem arch ->
+   OverrideSim p sym (LLVM mem) rtp l a ()
 registerModule handleWarning mtrans =
    mapM_ (registerModuleFn handleWarning mtrans) (map (L.decName.fst) (mtrans ^. modTransDefs))
 
 -- | Register a specific named function that is defined in the given
 --   module translation. This will immediately build a Crucible CFG for
 --   the named function.
 registerModuleFn ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
-   ModuleTranslation arch ->
+   ModuleTranslation mem arch ->
    L.Symbol ->
-   OverrideSim p sym LLVM rtp l a ()
+   OverrideSim p sym (LLVM mem) rtp l a ()
 registerModuleFn handleWarning mtrans sym =
   liftIO (getTranslatedCFG mtrans sym) >>= \case
     Nothing ->
@@ -99,10 +99,10 @@ registerModuleFn handleWarning mtrans sym =
 -- | Lazily register all the functions defined in the LLVM module.  See
 --   'registerLazyModuleFn' for a description.
 registerLazyModule ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
-   ModuleTranslation arch ->
-   OverrideSim p sym LLVM rtp l a ()
+   ModuleTranslation mem arch ->
+   OverrideSim p sym (LLVM mem) rtp l a ()
 registerLazyModule handleWarning mtrans =
    mapM_ (registerLazyModuleFn handleWarning mtrans) (map (L.decName.fst) (mtrans ^. modTransDefs))
 
@@ -115,11 +115,11 @@ registerLazyModule handleWarning mtrans =
 --   Note that the callback for printing translation warnings may be called at
 --   a much-later point, when the function in question is actually first invoked.
 registerLazyModuleFn ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling translation warnings -} ->
-   ModuleTranslation arch ->
+   ModuleTranslation mem arch ->
    L.Symbol ->
-   OverrideSim p sym LLVM rtp l a ()
+   OverrideSim p sym (LLVM mem) rtp l a ()
 registerLazyModuleFn handleWarning mtrans sym =
   liftIO (getTranslatedFnHandle mtrans sym) >>= \case
     Nothing -> 
@@ -163,21 +163,21 @@ registerLazyModuleFn handleWarning mtrans sym =
 
 
 llvmGlobalsToCtx
-   :: LLVMContext arch
+   :: mem ~ Mem => LLVMContext mem arch
    -> MemImpl sym
    -> SymGlobalState sym
 llvmGlobalsToCtx = llvmGlobals . llvmMemVar
 
 llvmGlobals
-   :: GlobalVar Mem
+   :: mem ~ Mem => GlobalVar Mem
    -> MemImpl sym
    -> SymGlobalState sym
 llvmGlobals memVar mem = emptyGlobals & insertGlobal memVar mem
 
 llvmExtensionImpl ::
-  (HasLLVMAnn sym) =>
+  (HasLLVMAnn sym, mem ~ Mem) =>
   MemOptions ->
-  ExtensionImpl p sym LLVM
+  ExtensionImpl p sym (LLVM mem)
 llvmExtensionImpl mo =
   let ?memOpts = mo in
   ExtensionImpl

crucible-llvm/src/Lang/Crucible/LLVM/ArraySizeProfile.hs

@@ -175,7 +175,8 @@ argProfiles sym mem as =
 updateProfiles ::
   ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth (C.ArchWidth arch)
   , ?memOpts :: C.MemOptions ) =>
-  C.LLVMContext arch ->
+  mem ~ C.Mem =>
+  C.LLVMContext mem arch ->
   IORef (Map Text [FunctionProfile]) ->
   C.ExecState p sym ext rtp ->
   IO ()
@@ -196,10 +197,10 @@ updateProfiles llvm cell state
   | otherwise = pure ()
 
 arraySizeProfile ::
-  forall sym ext arch p rtp.
+  forall sym ext mem arch p rtp.
   ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth (C.ArchWidth arch)
-  , ?memOpts :: C.MemOptions ) =>
-  C.LLVMContext arch ->
+  , ?memOpts :: C.MemOptions , mem ~ C.Mem) =>
+  C.LLVMContext mem arch ->
   IORef (Map Text [FunctionProfile]) ->
   IO (C.ExecutionFeature p sym ext rtp)
 arraySizeProfile llvm profiles = do

crucible-llvm/src/Lang/Crucible/LLVM/Ctors.hs

@@ -65,6 +65,7 @@ import           Lang.Crucible.CFG.SSAConversion (toSSA)
 import           Lang.Crucible.FunctionHandle (HandleAllocator, mkHandle')
 import           Lang.Crucible.Types (UnitType, TypeRepr(UnitRepr))
 import           Lang.Crucible.LLVM.Extension (LLVM, ArchWidth)
+import qualified Lang.Crucible.LLVM.Mem as Mem
 import           Lang.Crucible.LLVM.Translation.Monad (LLVMContext, _llvmTypeCtx, malformedLLVMModule)
 import           Lang.Crucible.LLVM.Types (HasPtrWidth)
 
@@ -134,9 +135,11 @@ globalCtors mod_ =
 -- ** callCtors
 
 -- | Call some or all of the functions in @llvm.global_ctors@
-callCtors :: (Ctor -> Bool) -- ^ Filter function
+callCtors :: 
+  Mem.Mem mem =>
+ (Ctor -> Bool) -- ^ Filter function
           -> L.Module
-          -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
+          -> LLVMGenerator s mem arch UnitType (Expr (LLVM mem) s UnitType)
 callCtors select mod_ = do
   let err msg = malformedLLVMModule "Error loading @llvm.global_ctors" [fromString msg]
   let ty = L.FunTy (L.PrimType L.Void) [] False
@@ -147,25 +150,25 @@ callCtors select mod_ = do
   return (App EmptyApp)
 
 -- | Call each function in @llvm.global_ctors@ in order of decreasing priority
-callAllCtors :: L.Module -> LLVMGenerator s arch UnitType (Expr LLVM s UnitType)
+callAllCtors :: Mem.Mem mem => L.Module -> LLVMGenerator s mem arch UnitType (Expr (LLVM mem) s UnitType)
 callAllCtors = callCtors (const True)
 
 ----------------------------------------------------------------------
 -- ** callCtorsCFG
 
 -- | Make a 'LLVMGenerator' into a CFG by making it a function with no arguments
 -- that returns unit.
-generatorToCFG :: forall arch wptr ret. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
-               => Text
+generatorToCFG :: forall mem arch wptr ret. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr, Mem.Mem mem)
+  => Text
                -> HandleAllocator
-               -> LLVMContext arch
-               -> (forall s. LLVMGenerator s arch ret (Expr LLVM s ret))
+               -> LLVMContext mem arch
+               -> (forall s. LLVMGenerator s mem arch ret (Expr (LLVM mem) s ret))
                -> TypeRepr ret
-               -> IO (Core.SomeCFG LLVM Core.EmptyCtx ret)
+               -> IO (Core.SomeCFG (LLVM mem) Core.EmptyCtx ret)
 generatorToCFG name halloc llvmctx gen ret = do
   ref <- newIORef []
   let ?lc = _llvmTypeCtx llvmctx
-  let def :: forall args. FunctionDef LLVM (LLVMState arch) args ret IO
+  let def :: forall args. FunctionDef (LLVM mem) (LLVMState mem arch) args ret IO
       def _inputs = (state, gen)
         where state = LLVMState { _identMap     = empty
                                 , _blockInfoMap = empty
@@ -180,11 +183,11 @@ generatorToCFG name halloc llvmctx gen ret = do
   return $! toSSA g
 
 -- | Create a CFG that calls some of the functions in @llvm.global_ctors@.
-callCtorsCFG :: forall arch wptr. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
-             => (Ctor -> Bool) -- ^ Filter function
+callCtorsCFG :: forall mem arch wptr. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr, Mem.Mem mem)
+  => (Ctor -> Bool) -- ^ Filter function
              -> L.Module
              -> HandleAllocator
-             -> LLVMContext arch
-             -> IO (Core.SomeCFG LLVM Core.EmptyCtx UnitType)
+             -> LLVMContext mem arch
+             -> IO (Core.SomeCFG (LLVM mem) Core.EmptyCtx UnitType)
 callCtorsCFG select mod_ halloc llvmctx = do
   generatorToCFG "llvm_global_ctors" halloc llvmctx (callCtors select mod_) UnitRepr

crucible-llvm/src/Lang/Crucible/LLVM/Errors.hs

@@ -62,7 +62,7 @@ import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB
 -- | Combine the three types of bad behaviors
 --
 data BadBehavior sym where
-  BBUndefinedBehavior :: UB.UndefinedBehavior (RegValue' sym) -> BadBehavior sym
+  BBUndefinedBehavior :: UB.UndefinedBehavior mem (RegValue' sym) -> BadBehavior sym
   BBMemoryError       :: ME.MemoryError sym -> BadBehavior sym
  deriving Typeable
 
@@ -93,14 +93,14 @@ data LLVMSafetyAssertion sym =
 -- We expose these rather than the constructors to retain the freedom to
 -- change the internal representation.
 
-undefinedBehavior' :: UB.UndefinedBehavior (RegValue' sym)
+undefinedBehavior' :: UB.UndefinedBehavior mem (RegValue' sym)
                    -> Pred sym
                    -> Text
                    -> LLVMSafetyAssertion sym
 undefinedBehavior' ub pred expl =
   LLVMSafetyAssertion (BBUndefinedBehavior ub) pred (Just expl)
 
-undefinedBehavior :: UB.UndefinedBehavior (RegValue' sym)
+undefinedBehavior :: UB.UndefinedBehavior mem (RegValue' sym)
                   -> Pred sym
                   -> LLVMSafetyAssertion sym
 undefinedBehavior ub pred =
@@ -110,14 +110,14 @@ memoryError :: (1 <= w) => ME.MemoryOp sym w -> ME.MemoryErrorReason -> Pred sym
 memoryError mop rsn pred =
   LLVMSafetyAssertion (BBMemoryError (ME.MemoryError mop rsn)) pred Nothing
 
-poison' :: Poison.Poison (RegValue' sym)
+poison' :: Poison.Poison mem (RegValue' sym)
         -> Pred sym
         -> Text
         -> LLVMSafetyAssertion sym
 poison' poison_ pred expl =
   LLVMSafetyAssertion (BBUndefinedBehavior (UB.PoisonValueCreated poison_)) pred (Just expl)
 
-poison :: Poison.Poison (RegValue' sym)
+poison :: Poison.Poison mem (RegValue' sym)
        -> Pred sym
        -> LLVMSafetyAssertion sym
 poison poison_ pred =