Skip to content

Commit

Permalink
Merge pull request #1199 from langston-barrett/lb/matched-ovs
Browse files Browse the repository at this point in the history
llvm: Return the list of overrides that were applied
  • Loading branch information
langston-barrett authored Apr 26, 2024
2 parents a42279a + 7db2d17 commit 63f7c86
Show file tree
Hide file tree
Showing 3 changed files with 60 additions and 21 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

* `register_llvm_overrides{,_}` now returns the list of overrides that were
applied.
* The `doMallocHandle` function was removed.
* The `RegOverrideM` monad was replaced by the `MakeOverride` function newtype.
* Several type parameters were removed from `OverrideTemplate`, and the `ext`
Expand Down
75 changes: 56 additions & 19 deletions crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,8 @@ module Lang.Crucible.LLVM.Intrinsics
) where

import Control.Lens hiding (op, (:>), Empty)
import Control.Monad (forM_)
import Control.Monad (forM)
import Data.Maybe (catMaybes)
import qualified Text.LLVM.AST as L

import qualified ABI.Itanium as ABI
Expand Down Expand Up @@ -63,18 +64,22 @@ llvmIntrinsicTypes =
MapF.insert (knownSymbol :: SymbolRepr "LLVM_pointer") IntrinsicMuxFn $
MapF.empty

-- | Register all declare and define overrides
-- | Match two sets of 'OverrideTemplate's against the @declare@s and @define@s
-- in a 'L.Module', registering all the overrides that apply and returning them
-- as a list.
register_llvm_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
L.Module ->
[OverrideTemplate p sym LLVM arch] {- ^ Additional \"define\" overrides -} ->
[OverrideTemplate p sym LLVM arch] {- ^ Additional \"declare\" overrides -} ->
LLVMContext arch ->
OverrideSim p sym LLVM rtp l a ()
-- | Applied (@define@ overrides, @declare@ overrides)
OverrideSim p sym LLVM rtp l a ([SomeLLVMOverride p sym LLVM], [SomeLLVMOverride p sym LLVM])
register_llvm_overrides llvmModule defineOvrs declareOvrs llvmctx =
do register_llvm_define_overrides llvmModule defineOvrs llvmctx
register_llvm_declare_overrides llvmModule declareOvrs llvmctx
do defOvs <- register_llvm_define_overrides llvmModule defineOvrs llvmctx
declOvs <- register_llvm_declare_overrides llvmModule declareOvrs llvmctx
pure (defOvs, declOvs)

-- | Filter the initial list of templates to only those that could
-- possibly match the given declaration based on straightforward,
Expand All @@ -90,43 +95,75 @@ filterTemplates ::
filterTemplates ts decl = filter (matches nm . overrideTemplateMatcher) ts
where L.Symbol nm = L.decName decl

-- | Helper function for registering overrides
-- | Match a set of 'OverrideTemplate's against a single 'L.Declare',
-- registering all the overrides that apply and returning them as a list.
match_llvm_overrides ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch ->
-- | Overrides to attempt to match against this declaration
[OverrideTemplate p sym ext arch] ->
-- | Declaration of the function that might get overridden
L.Declare ->
OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
match_llvm_overrides llvmctx acts decl =
llvmPtrWidth llvmctx $ \wptr -> withPtrWidth wptr $ do
let acts' = filterTemplates acts decl
let L.Symbol nm = L.decName decl
let declnm = either (const Nothing) Just $ ABI.demangleName nm
mbOvs <-
forM (map overrideTemplateAction acts') $ \(MakeOverride act) ->
case act decl declnm llvmctx of
Nothing -> pure Nothing
Just sov@(SomeLLVMOverride ov) -> do
register_llvm_override ov decl llvmctx
pure (Just sov)
pure (catMaybes mbOvs)

-- | Match a set of 'OverrideTemplate's against a set of 'L.Declare's,
-- registering all the overrides that apply and returning them as a list.
register_llvm_overrides_ ::
(IsSymInterface sym, HasLLVMAnn sym) =>
LLVMContext arch ->
-- | Overrides to attempt to match against these declarations
[OverrideTemplate p sym ext arch] ->
-- | Declarations of the functions that might get overridden
[L.Declare] ->
OverrideSim p sym ext rtp l a ()
OverrideSim p sym ext rtp l a [SomeLLVMOverride p sym ext]
register_llvm_overrides_ llvmctx acts decls =
llvmPtrWidth llvmctx $ \wptr -> withPtrWidth wptr $
forM_ decls $ \decl ->
do let acts' = filterTemplates acts decl
let L.Symbol nm = L.decName decl
let declnm = either (const Nothing) Just $ ABI.demangleName nm
forM_ (map overrideTemplateAction acts') $ \(MakeOverride act) ->
case act decl declnm llvmctx of
Nothing -> pure ()
Just (SomeLLVMOverride ov) ->
register_llvm_override ov decl llvmctx
concat <$> forM decls (\decl -> match_llvm_overrides llvmctx acts decl)

-- | Match a set of 'OverrideTemplate's against all the @declare@s and @define@s
-- in a 'L.Module', registering all the overrides that apply and returning them
-- as a list.
--
-- Registers a default set of overrides, in addition to the ones passed as an
-- argument.
register_llvm_define_overrides ::
(IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
L.Module ->
-- | Additional (non-default) @define@ overrides
[OverrideTemplate p sym LLVM arch] ->
LLVMContext arch ->
OverrideSim p sym LLVM rtp l a ()
OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_define_overrides llvmModule addlOvrs llvmctx =
let ?lc = llvmctx^.llvmTypeCtx in
register_llvm_overrides_ llvmctx (addlOvrs ++ define_overrides) $
(allModuleDeclares llvmModule)

-- | Match a set of 'OverrideTemplate's against all the @declare@s in a
-- 'L.Module', registering all the overrides that apply and returning them as
-- a list.
--
-- Registers a default set of overrides, in addition to the ones passed as an
-- argument.
register_llvm_declare_overrides ::
( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
L.Module ->
-- | Additional (non-default) @declare@ overrides
[OverrideTemplate p sym LLVM arch] ->
LLVMContext arch ->
OverrideSim p sym LLVM rtp l a ()
OverrideSim p sym LLVM rtp l a [SomeLLVMOverride p sym LLVM]
register_llvm_declare_overrides llvmModule addlOvrs llvmctx =
let ?lc = llvmctx^.llvmTypeCtx
in register_llvm_overrides_ llvmctx (addlOvrs ++ declare_overrides) $
Expand Down
4 changes: 2 additions & 2 deletions uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -324,7 +324,7 @@ registerOverrides appCtx modCtx kind overrides =
Text.unwords
["Registering", kind, "override for", describeOverride override]

LLVMIntrinsics.register_llvm_overrides_
void $ LLVMIntrinsics.register_llvm_overrides_
(modCtx ^. moduleTranslation . transContext)
overrides
(allModuleDeclares (modCtx ^. llvmModule . to getModule))
Expand Down Expand Up @@ -488,7 +488,7 @@ mkCallbacks appCtx modCtx funCtx halloc callbacks constraints cfg llvmOpts specs
--
-- Stuff like LLVM intrinsics, `free`, `malloc`
let llMod = modCtx ^. llvmModule . to getModule
LLVMIntrinsics.register_llvm_overrides llMod [] [] llvmCtxt
void $ LLVMIntrinsics.register_llvm_overrides llMod [] [] llvmCtxt

-- These are aligned for easy reading in the logs
let sCruxLLVM = "crux-llvm"
Expand Down

0 comments on commit 63f7c86

Please sign in to comment.