Merge pull request #1184 from langston-barrett/lb/crucible-llvm-overr…

…ide-ext

crucible-llvm: Generalize `LLVMOverride`'s `ext` parameter

crucible-llvm/CHANGELOG.md

@@ -1,3 +1,8 @@
+# next
+
+* `LLVMOverride` now has an additional `ext` type parameter. See the Haddocks
+  for `LLVMOverride` for details and motivation.
+
 # 0.6 -- 2024-02-05
 
 * `bindLLVMFunPtr` now accepts an `Text.LLVM.AST.Symbol` rather than a whole `Declare`.

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

@@ -83,7 +83,11 @@ import           Lang.Crucible.LLVM.Translation.Types
 
 -- | This type represents an implementation of an LLVM intrinsic function in
 -- Crucible.
-data LLVMOverride p sym args ret =
+--
+-- This is parameterized over @ext@ so that 'LLVMOverride's can more easily be
+-- reused in the context of other language extensions that are also based on the
+-- LLVM memory model, such as Macaw.
+data LLVMOverride p sym ext args ret =
   LLVMOverride
   { llvmOverride_declare :: L.Declare    -- ^ An LLVM name and signature for this intrinsic
   , llvmOverride_args    :: CtxRepr args -- ^ A representation of the argument types
@@ -95,13 +99,13 @@ data LLVMOverride p sym args ret =
          bak ->
          Ctx.Assignment (RegEntry sym) args ->
          forall rtp args' ret'.
-         OverrideSim p sym LLVM rtp args' ret' (RegValue sym ret)
+         OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
     -- ^ The implementation of the intrinsic in the simulator monad
     -- (@OverrideSim@).
   }
 
-data SomeLLVMOverride p sym =
-  forall args ret. SomeLLVMOverride (LLVMOverride p sym args ret)
+data SomeLLVMOverride p sym ext =
+  forall args ret. SomeLLVMOverride (LLVMOverride p sym ext args ret)
 
 -- | Convenient LLVM representation of the @size_t@ type.
 llvmSizeT :: HasPtrWidth wptr => L.Type
@@ -292,15 +296,15 @@ build_llvm_override fnm args ret args' ret' llvmOverride =
 polymorphic1_llvm_override :: forall p sym arch wptr l a rtp.
   (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
   String ->
-  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym) ->
+  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym LLVM) ->
   OverrideTemplate p sym arch rtp l a
 polymorphic1_llvm_override prefix fn =
   OverrideTemplate (PrefixMatch prefix) (register_1arg_polymorphic_override prefix fn)
 
 register_1arg_polymorphic_override :: forall p sym arch wptr l a rtp.
   (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
   String ->
-  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym) ->
+  (forall w. (1 <= w) => NatRepr w -> SomeLLVMOverride p sym LLVM) ->
   RegOverrideM p sym arch rtp l a ()
 register_1arg_polymorphic_override prefix overrideFn =
   do (L.Declare{ L.decName = L.Symbol nm },_,_) <- ask
@@ -313,7 +317,7 @@ register_1arg_polymorphic_override prefix overrideFn =
 
 basic_llvm_override :: forall p args ret sym arch wptr l a rtp.
   (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
-  LLVMOverride p sym args ret ->
+  LLVMOverride p sym LLVM args ret ->
   OverrideTemplate p sym arch rtp l a
 basic_llvm_override ovr = OverrideTemplate matcher regOvr
   where
@@ -367,7 +371,7 @@ isMatchingDeclaration requested provided = and
 
 register_llvm_override :: forall p args ret sym arch wptr l a rtp.
   (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
-  LLVMOverride p sym args ret ->
+  LLVMOverride p sym LLVM args ret ->
   RegOverrideM p sym arch rtp l a ()
 register_llvm_override llvmOverride = do
   (requestedDecl,_,llvmctx) <- ask
@@ -433,7 +437,7 @@ bind_llvm_func llvmCtx nm args ret impl = do
 do_register_llvm_override :: forall p args ret sym arch wptr l a rtp.
   (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
   LLVMContext arch ->
-  LLVMOverride p sym args ret ->
+  LLVMOverride p sym LLVM args ret ->
   OverrideSim p sym LLVM rtp l a ()
 do_register_llvm_override llvmctx llvmOverride = do
   let decl = llvmOverride_declare llvmOverride
@@ -463,7 +467,7 @@ alloc_and_register_override ::
   (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) =>
   bak ->
   LLVMContext arch ->
-  LLVMOverride p sym args ret ->
+  LLVMOverride p sym LLVM args ret ->
   -- | Aliases
   [L.Symbol] ->
   OverrideSim p sym LLVM rtp l a ()