Skip to content

Commit

Permalink
crucible-llvm: Generalize pipe-fitting code to any language extension (
Browse files Browse the repository at this point in the history
…#1188)

This will be helpful for e.g. Macaw.
  • Loading branch information
langston-barrett committed Mar 26, 2024
1 parent 1c6e59e commit 1b0bd47
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 9 deletions.
2 changes: 2 additions & 0 deletions crucible-llvm/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
# next

* `build_llvm_override` is now generic over the `ext` type parameter. This
should be a backwards-compatible change.
* `LLVMOverride` now has an additional `ext` type parameter. See the Haddocks
for `LLVMOverride` for details and motivation.
* The `llvmOverride_def` field of `LLVMOverride` no longer takes a `bak`
Expand Down
18 changes: 9 additions & 9 deletions crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs
Original file line number Diff line number Diff line change
Expand Up @@ -199,24 +199,24 @@ apply this special case to other override functions (e.g.,
------------------------------------------------------------------------
-- ** register_llvm_override

newtype ArgTransformer p sym args args' =
newtype ArgTransformer p sym ext args args' =
ArgTransformer { applyArgTransformer :: (forall rtp l a.
Ctx.Assignment (RegEntry sym) args ->
OverrideSim p sym LLVM rtp l a (Ctx.Assignment (RegEntry sym) args')) }
OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) }

newtype ValTransformer p sym tp tp' =
newtype ValTransformer p sym ext tp tp' =
ValTransformer { applyValTransformer :: (forall rtp l a.
RegValue sym tp ->
OverrideSim p sym LLVM rtp l a (RegValue sym tp')) }
OverrideSim p sym ext rtp l a (RegValue sym tp')) }

transformLLVMArgs :: forall m p sym bak args args'.
transformLLVMArgs :: forall m p sym ext bak args args'.
(IsSymBackend sym bak, Monad m, HasLLVMAnn sym) =>
-- | This function name is only used in panic messages.
FunctionName ->
bak ->
CtxRepr args' ->
CtxRepr args ->
m (ArgTransformer p sym args args')
m (ArgTransformer p sym ext args args')
transformLLVMArgs _fnName _ Ctx.Empty Ctx.Empty =
return (ArgTransformer (\_ -> return Ctx.Empty))
transformLLVMArgs fnName bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = do
Expand All @@ -240,7 +240,7 @@ transformLLVMRet ::
bak ->
TypeRepr ret ->
TypeRepr ret' ->
m (ValTransformer p sym ret ret')
m (ValTransformer p sym ext ret ret')
transformLLVMRet _fnName bak (BVRepr w) (LLVMPointerRepr w')
| Just Refl <- testEquality w w'
= return (ValTransformer (liftIO . llvmPointer_bv (backendGetSym bak)))
Expand Down Expand Up @@ -279,8 +279,8 @@ build_llvm_override ::
TypeRepr ret' ->
(forall rtp' l' a'. IsSymInterface sym =>
Ctx.Assignment (RegEntry sym) args ->
OverrideSim p sym LLVM rtp' l' a' (RegValue sym ret)) ->
OverrideSim p sym LLVM rtp l a (Override p sym LLVM args' ret')
OverrideSim p sym ext rtp' l' a' (RegValue sym ret)) ->
OverrideSim p sym ext rtp l a (Override p sym ext args' ret')
build_llvm_override fnm args ret args' ret' llvmOverride =
ovrWithBackend $ \bak ->
do fargs <- transformLLVMArgs fnm bak args args'
Expand Down

0 comments on commit 1b0bd47

Please sign in to comment.