From 7db2d17f130cee3bf5e28d1cb95c322c808259c4 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 26 Apr 2024 11:15:15 -0400 Subject: [PATCH] llvm: Return the list of overrides that were applied This is useful for some downstream consumers, e.g., if you want to allow forward-declarations in Crucible-LLVM S-expression syntax programs that eventually resolve to overrides. Also, improve documentation for all these functions. --- crucible-llvm/CHANGELOG.md | 2 + .../src/Lang/Crucible/LLVM/Intrinsics.hs | 75 ++++++++++++++----- uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs | 4 +- 3 files changed, 60 insertions(+), 21 deletions(-) diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md index f5233fc0d..f5ac274c1 100644 --- a/crucible-llvm/CHANGELOG.md +++ b/crucible-llvm/CHANGELOG.md @@ -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` diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs index 2d9d5489b..5abcda08f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs @@ -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 @@ -63,7 +64,9 @@ 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 ) => @@ -71,10 +74,12 @@ register_llvm_overrides :: [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, @@ -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) $ diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs index 34ebc8002..9667ae711 100644 --- a/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs +++ b/uc-crux-llvm/src/UCCrux/LLVM/Run/Simulate.hs @@ -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)) @@ -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"