Skip to content

Commit

Permalink
Merge pull request #1185 from langston-barrett/lb/llvm-ov-pass-bak
Browse files Browse the repository at this point in the history
crucible-llvm: Don't pass around the symbolic backend explicitly
  • Loading branch information
langston-barrett committed Mar 26, 2024
2 parents 0d26eb4 + f3d828a commit ddbf276
Show file tree
Hide file tree
Showing 11 changed files with 895 additions and 880 deletions.
3 changes: 3 additions & 0 deletions crucible-llvm/CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@

* `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`
argument. To retrieve the current symbolic backend, use
`Lang.Crucible.Simulator.OverrideSim.ovrWithBackend`.

# 0.6 -- 2024-02-05

Expand Down
20 changes: 8 additions & 12 deletions crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs
Original file line number Diff line number Diff line change
Expand Up @@ -93,13 +93,11 @@ data LLVMOverride p sym ext args ret =
, llvmOverride_args :: CtxRepr args -- ^ A representation of the argument types
, llvmOverride_ret :: TypeRepr ret -- ^ A representation of the return type
, llvmOverride_def ::
forall bak.
IsSymBackend sym bak =>
GlobalVar Mem ->
bak ->
Ctx.Assignment (RegEntry sym) args ->
forall rtp args' ret'.
OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
IsSymInterface sym =>
GlobalVar Mem ->
Ctx.Assignment (RegEntry sym) args ->
forall rtp args' ret'.
OverrideSim p sym ext rtp args' ret' (RegValue sym ret)
-- ^ The implementation of the intrinsic in the simulator monad
-- (@OverrideSim@).
}
Expand Down Expand Up @@ -279,8 +277,7 @@ build_llvm_override ::
TypeRepr ret ->
CtxRepr args' ->
TypeRepr ret' ->
(forall bak rtp' l' a'. IsSymBackend sym bak =>
bak ->
(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')
Expand All @@ -290,8 +287,7 @@ build_llvm_override fnm args ret args' ret' llvmOverride =
fret <- transformLLVMRet fnm bak ret ret'
return $ mkOverride' fnm ret' $
do RegMap xs <- getOverrideArgs
ovrWithBackend $ \bak' ->
applyValTransformer fret =<< llvmOverride bak' =<< applyArgTransformer fargs xs
applyValTransformer fret =<< llvmOverride =<< applyArgTransformer fargs xs

polymorphic1_llvm_override :: forall p sym arch wptr l a rtp.
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
Expand Down Expand Up @@ -452,7 +448,7 @@ do_register_llvm_override llvmctx llvmOverride = do

llvmDeclToFunHandleRepr' decl $ \args ret -> do
o <- build_llvm_override fnm overrideArgs overrideRet args ret
(\bak asgn -> llvmOverride_def llvmOverride mvar bak asgn)
(\asgn -> llvmOverride_def llvmOverride mvar asgn)
bind_llvm_func llvmctx (L.decName decl) args ret (UseOverride o)

-- | Create an allocation for an override and register it.
Expand Down
Loading

0 comments on commit ddbf276

Please sign in to comment.