From 602e33aa98bc09f2f4f5e5aa061bc511d7b69b5d Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 10:05:59 -0400 Subject: [PATCH 1/8] crucible-llvm: Factor pipe-fitting code into a separate module The goal is to clean it up a bit and export it. --- crucible-llvm/crucible-llvm.cabal | 1 + .../src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 104 ++++++++++++++++++ .../Lang/Crucible/LLVM/Intrinsics/Common.hs | 77 +------------ 3 files changed, 109 insertions(+), 73 deletions(-) create mode 100644 crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 6b3c24b5f..94249f54b 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -98,6 +98,7 @@ library Lang.Crucible.LLVM.Errors.Standards Lang.Crucible.LLVM.Extension.Arch Lang.Crucible.LLVM.Extension.Syntax + Lang.Crucible.LLVM.Intrinsics.Cast Lang.Crucible.LLVM.Intrinsics.Common Lang.Crucible.LLVM.Intrinsics.Libcxx Lang.Crucible.LLVM.Intrinsics.Options diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs new file mode 100644 index 000000000..01ef377b4 --- /dev/null +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -0,0 +1,104 @@ +-- | +-- Module : Lang.Crucible.LLVM.Intrinsics.Cast +-- Description : Cast between bitvectors and pointers in signatuers +-- Copyright : (c) Galois, Inc 2024 +-- License : BSD3 +-- Maintainer : Langston Barrett +-- Stability : provisional +------------------------------------------------------------------------ + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} + +module Lang.Crucible.LLVM.Intrinsics.Cast + ( ArgTransformer(applyArgTransformer) + , ValTransformer(applyValTransformer) + , transformLLVMArgs + , transformLLVMRet + ) where + +import Control.Monad.IO.Class (liftIO) +import Control.Lens +import qualified Data.Text as Text + +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.TraversableFC (fmapFC) + +import Lang.Crucible.Backend +import Lang.Crucible.Panic (panic) +import Lang.Crucible.Simulator.OverrideSim +import Lang.Crucible.Simulator.RegMap +import Lang.Crucible.Types + +import What4.FunctionName + +import Lang.Crucible.LLVM.MemModel + +newtype ArgTransformer p sym ext args args' = + ArgTransformer { applyArgTransformer :: (forall rtp l a. + Ctx.Assignment (RegEntry sym) args -> + OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) } + +newtype ValTransformer p sym ext tp tp' = + ValTransformer { applyValTransformer :: (forall rtp l a. + RegValue sym tp -> + OverrideSim p sym ext rtp l a (RegValue sym tp')) } + +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 ext args args') +transformLLVMArgs _fnName _ Ctx.Empty Ctx.Empty = + return (ArgTransformer (\_ -> return Ctx.Empty)) +transformLLVMArgs fnName bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = do + return (ArgTransformer + (\(xs Ctx.:> x) -> + do (ValTransformer f) <- transformLLVMRet fnName bak tp tp' + (ArgTransformer fs) <- transformLLVMArgs fnName bak rest' rest + xs' <- fs xs + x' <- RegEntry tp' <$> f (regValue x) + pure (xs' Ctx.:> x'))) +transformLLVMArgs fnName _ _ _ = + panic "Intrinsics.transformLLVMArgs" + [ "transformLLVMArgs: argument shape mismatch!" + , "in function: " ++ Text.unpack (functionName fnName) + ] + +transformLLVMRet :: + (IsSymBackend sym bak, Monad m, HasLLVMAnn sym) => + -- | This function name is only used in panic messages. + FunctionName -> + bak -> + TypeRepr ret -> + TypeRepr 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))) +transformLLVMRet _fnName bak (LLVMPointerRepr w) (BVRepr w') + | Just Refl <- testEquality w w' + = return (ValTransformer (liftIO . projectLLVM_bv bak)) +transformLLVMRet fnName bak (VectorRepr tp) (VectorRepr tp') + = do ValTransformer f <- transformLLVMRet fnName bak tp tp' + return (ValTransformer (traverse f)) +transformLLVMRet fnName bak (StructRepr ctx) (StructRepr ctx') + = do ArgTransformer tf <- transformLLVMArgs fnName bak ctx' ctx + return (ValTransformer (\vals -> + let vals' = Ctx.zipWith (\tp (RV v) -> RegEntry tp v) ctx vals in + fmapFC (\x -> RV (regValue x)) <$> tf vals')) + +transformLLVMRet _fnName _bak ret ret' + | Just Refl <- testEquality ret ret' + = return (ValTransformer return) +transformLLVMRet fnName _bak ret ret' + = panic "Intrinsics.transformLLVMRet" + [ "Cannot transform types" + , "*** Source type: " ++ show ret + , "*** Target type: " ++ show ret' + , "in function: " ++ Text.unpack (functionName fnName) + ] + diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs index a5d29a591..cc967035d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -58,13 +58,11 @@ import qualified System.Info as Info import qualified ABI.Itanium as ABI import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(..)) -import Data.Parameterized.TraversableFC (fmapFC) import Lang.Crucible.Backend import Lang.Crucible.CFG.Common (GlobalVar) import Lang.Crucible.Simulator.ExecutionTree (FnState(UseOverride)) import Lang.Crucible.FunctionHandle (FnHandle, mkHandle') -import Lang.Crucible.Panic (panic) import Lang.Crucible.Simulator (stateContext, simHandleAllocator) import Lang.Crucible.Simulator.OverrideSim import Lang.Crucible.Utils.MonadVerbosity (getLogFunction) @@ -78,6 +76,7 @@ import Lang.Crucible.LLVM.Eval (callStackFromMemVar) import Lang.Crucible.LLVM.Globals (registerFunPtr) import Lang.Crucible.LLVM.MemModel import Lang.Crucible.LLVM.MemModel.CallStack (CallStack) +import qualified Lang.Crucible.LLVM.Intrinsics.Cast as Cast import Lang.Crucible.LLVM.Translation.Monad import Lang.Crucible.LLVM.Translation.Types @@ -199,74 +198,6 @@ apply this special case to other override functions (e.g., ------------------------------------------------------------------------ -- ** register_llvm_override -newtype ArgTransformer p sym ext args args' = - ArgTransformer { applyArgTransformer :: (forall rtp l a. - Ctx.Assignment (RegEntry sym) args -> - OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) } - -newtype ValTransformer p sym ext tp tp' = - ValTransformer { applyValTransformer :: (forall rtp l a. - RegValue sym tp -> - OverrideSim p sym ext rtp l a (RegValue sym tp')) } - -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 ext args args') -transformLLVMArgs _fnName _ Ctx.Empty Ctx.Empty = - return (ArgTransformer (\_ -> return Ctx.Empty)) -transformLLVMArgs fnName bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = do - return (ArgTransformer - (\(xs Ctx.:> x) -> - do (ValTransformer f) <- transformLLVMRet fnName bak tp tp' - (ArgTransformer fs) <- transformLLVMArgs fnName bak rest' rest - xs' <- fs xs - x' <- RegEntry tp' <$> f (regValue x) - pure (xs' Ctx.:> x'))) -transformLLVMArgs fnName _ _ _ = - panic "Intrinsics.transformLLVMArgs" - [ "transformLLVMArgs: argument shape mismatch!" - , "in function: " ++ Text.unpack (functionName fnName) - ] - -transformLLVMRet :: - (IsSymBackend sym bak, Monad m, HasLLVMAnn sym) => - -- | This function name is only used in panic messages. - FunctionName -> - bak -> - TypeRepr ret -> - TypeRepr 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))) -transformLLVMRet _fnName bak (LLVMPointerRepr w) (BVRepr w') - | Just Refl <- testEquality w w' - = return (ValTransformer (liftIO . projectLLVM_bv bak)) -transformLLVMRet fnName bak (VectorRepr tp) (VectorRepr tp') - = do ValTransformer f <- transformLLVMRet fnName bak tp tp' - return (ValTransformer (traverse f)) -transformLLVMRet fnName bak (StructRepr ctx) (StructRepr ctx') - = do ArgTransformer tf <- transformLLVMArgs fnName bak ctx' ctx - return (ValTransformer (\vals -> - let vals' = Ctx.zipWith (\tp (RV v) -> RegEntry tp v) ctx vals in - fmapFC (\x -> RV (regValue x)) <$> tf vals')) - -transformLLVMRet _fnName _bak ret ret' - | Just Refl <- testEquality ret ret' - = return (ValTransformer return) -transformLLVMRet fnName _bak ret ret' - = panic "Intrinsics.transformLLVMRet" - [ "Cannot transform types" - , "*** Source type: " ++ show ret - , "*** Target type: " ++ show ret' - , "in function: " ++ Text.unpack (functionName fnName) - ] - -- | Do some pipe-fitting to match a Crucible override function into the shape -- expected by the LLVM calling convention. This basically just coerces -- between values of @BVType w@ and values of @LLVMPointerType w@. @@ -283,11 +214,11 @@ build_llvm_override :: 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' - fret <- transformLLVMRet fnm bak ret ret' + do fargs <- Cast.transformLLVMArgs fnm bak args args' + fret <- Cast.transformLLVMRet fnm bak ret ret' return $ mkOverride' fnm ret' $ do RegMap xs <- getOverrideArgs - applyValTransformer fret =<< llvmOverride =<< applyArgTransformer fargs xs + Cast.applyValTransformer fret =<< llvmOverride =<< Cast.applyArgTransformer fargs xs polymorphic1_llvm_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => From ac879a3f9efd3f1cd6364236e5fda497f632123c Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 10:31:30 -0400 Subject: [PATCH 2/8] crucible-llvm: Clean up and export override pipe-fitting code Make it not panic by default, to make it usable by other clients who may not want to panic. Also, clear up the phase boundary to handle errors (e.g., in the case for structs). --- .../src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 96 ++++++++++--------- .../Lang/Crucible/LLVM/Intrinsics/Common.hs | 17 +++- 2 files changed, 66 insertions(+), 47 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 01ef377b4..4841459ad 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -8,10 +8,14 @@ ------------------------------------------------------------------------ {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} module Lang.Crucible.LLVM.Intrinsics.Cast - ( ArgTransformer(applyArgTransformer) + ( ValCastError + , printValCastError + , ArgTransformer(applyArgTransformer) , ValTransformer(applyValTransformer) , transformLLVMArgs , transformLLVMRet @@ -19,9 +23,12 @@ module Lang.Crucible.LLVM.Intrinsics.Cast import Control.Monad.IO.Class (liftIO) import Control.Lens +import Data.Either.Extra (mapLeft) import qualified Data.Text as Text +import Data.Vector (Vector) import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(Some)) import Data.Parameterized.TraversableFC (fmapFC) import Lang.Crucible.Backend @@ -34,6 +41,20 @@ import What4.FunctionName import Lang.Crucible.LLVM.MemModel +data ValCastError + = MismatchedShape + | ValCastError (Some TypeRepr) (Some TypeRepr) + +printValCastError :: ValCastError -> [String] +printValCastError = + \case + MismatchedShape -> ["argument shape mismatch"] + ValCastError (Some ret) (Some ret') -> + [ "Cannot transform types" + , "*** Source type: " ++ show ret + , "*** Target type: " ++ show ret' + ] + newtype ArgTransformer p sym ext args args' = ArgTransformer { applyArgTransformer :: (forall rtp l a. Ctx.Assignment (RegEntry sym) args -> @@ -44,61 +65,46 @@ newtype ValTransformer p sym ext tp tp' = RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp')) } -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 -> +transformLLVMArgs :: forall p sym ext bak args args'. + (IsSymBackend sym bak, HasLLVMAnn sym) => bak -> CtxRepr args' -> CtxRepr 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 - return (ArgTransformer - (\(xs Ctx.:> x) -> - do (ValTransformer f) <- transformLLVMRet fnName bak tp tp' - (ArgTransformer fs) <- transformLLVMArgs fnName bak rest' rest - xs' <- fs xs - x' <- RegEntry tp' <$> f (regValue x) - pure (xs' Ctx.:> x'))) -transformLLVMArgs fnName _ _ _ = - panic "Intrinsics.transformLLVMArgs" - [ "transformLLVMArgs: argument shape mismatch!" - , "in function: " ++ Text.unpack (functionName fnName) - ] + Either ValCastError (ArgTransformer p sym ext args args') +transformLLVMArgs _ Ctx.Empty Ctx.Empty = + Right (ArgTransformer (\_ -> return Ctx.Empty)) +transformLLVMArgs bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = + do (ValTransformer f) <- transformLLVMRet bak tp tp' + (ArgTransformer fs) <- transformLLVMArgs bak rest' rest + Right (ArgTransformer + (\(xs Ctx.:> x) -> do + xs' <- fs xs + x' <- f (regValue x) + pure (xs' Ctx.:> RegEntry tp' x'))) +transformLLVMArgs _ _ _ = Left MismatchedShape transformLLVMRet :: - (IsSymBackend sym bak, Monad m, HasLLVMAnn sym) => - -- | This function name is only used in panic messages. - FunctionName -> + (IsSymBackend sym bak, HasLLVMAnn sym) => bak -> TypeRepr ret -> TypeRepr ret' -> - m (ValTransformer p sym ext ret ret') -transformLLVMRet _fnName bak (BVRepr w) (LLVMPointerRepr w') + Either ValCastError (ValTransformer p sym ext ret ret') +transformLLVMRet bak (BVRepr w) (LLVMPointerRepr w') | Just Refl <- testEquality w w' - = return (ValTransformer (liftIO . llvmPointer_bv (backendGetSym bak))) -transformLLVMRet _fnName bak (LLVMPointerRepr w) (BVRepr w') + = Right (ValTransformer (liftIO . llvmPointer_bv (backendGetSym bak))) +transformLLVMRet bak (LLVMPointerRepr w) (BVRepr w') | Just Refl <- testEquality w w' - = return (ValTransformer (liftIO . projectLLVM_bv bak)) -transformLLVMRet fnName bak (VectorRepr tp) (VectorRepr tp') - = do ValTransformer f <- transformLLVMRet fnName bak tp tp' - return (ValTransformer (traverse f)) -transformLLVMRet fnName bak (StructRepr ctx) (StructRepr ctx') - = do ArgTransformer tf <- transformLLVMArgs fnName bak ctx' ctx - return (ValTransformer (\vals -> + = Right (ValTransformer (liftIO . projectLLVM_bv bak)) +transformLLVMRet bak (VectorRepr tp) (VectorRepr tp') + = do ValTransformer f <- transformLLVMRet bak tp tp' + Right (ValTransformer (traverse f)) +transformLLVMRet bak (StructRepr ctx) (StructRepr ctx') + = do ArgTransformer tf <- transformLLVMArgs bak ctx' ctx + Right (ValTransformer (\vals -> let vals' = Ctx.zipWith (\tp (RV v) -> RegEntry tp v) ctx vals in fmapFC (\x -> RV (regValue x)) <$> tf vals')) -transformLLVMRet _fnName _bak ret ret' +transformLLVMRet _bak ret ret' | Just Refl <- testEquality ret ret' - = return (ValTransformer return) -transformLLVMRet fnName _bak ret ret' - = panic "Intrinsics.transformLLVMRet" - [ "Cannot transform types" - , "*** Source type: " ++ show ret - , "*** Target type: " ++ show ret' - , "in function: " ++ Text.unpack (functionName fnName) - ] - + = Right (ValTransformer return) +transformLLVMRet _bak ret ret' = Left (ValCastError (Some ret) (Some ret')) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs index cc967035d..dc64162f3 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -63,6 +63,7 @@ import Lang.Crucible.Backend import Lang.Crucible.CFG.Common (GlobalVar) import Lang.Crucible.Simulator.ExecutionTree (FnState(UseOverride)) import Lang.Crucible.FunctionHandle (FnHandle, mkHandle') +import Lang.Crucible.Panic (panic) import Lang.Crucible.Simulator (stateContext, simHandleAllocator) import Lang.Crucible.Simulator.OverrideSim import Lang.Crucible.Utils.MonadVerbosity (getLogFunction) @@ -214,8 +215,20 @@ build_llvm_override :: 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 <- Cast.transformLLVMArgs fnm bak args args' - fret <- Cast.transformLLVMRet fnm bak ret ret' + do fargs <- + case Cast.transformLLVMArgs bak args args' of + Left err -> + panic "Intrinsics.build_llvm_override" + (Cast.printValCastError err ++ + [ "in function: " ++ Text.unpack (functionName fnm) ]) + Right f -> pure f + fret <- + case Cast.transformLLVMRet bak ret ret' of + Left err -> + panic "Intrinsics.build_llvm_override" + (Cast.printValCastError err ++ + [ "in function: " ++ Text.unpack (functionName fnm) ]) + Right f -> pure f return $ mkOverride' fnm ret' $ do RegMap xs <- getOverrideArgs Cast.applyValTransformer fret =<< llvmOverride =<< Cast.applyArgTransformer fargs xs From 9759f9c73b41fb016b9faaaaf552d941ebf115fb Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 11:13:57 -0400 Subject: [PATCH 3/8] crucible-llvm: Rename value "transforming" to "casting" Also remove some unused imports --- .../src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 72 +++++++++---------- .../Lang/Crucible/LLVM/Intrinsics/Common.hs | 6 +- 2 files changed, 36 insertions(+), 42 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 4841459ad..b845d56c2 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -15,30 +15,24 @@ module Lang.Crucible.LLVM.Intrinsics.Cast ( ValCastError , printValCastError - , ArgTransformer(applyArgTransformer) - , ValTransformer(applyValTransformer) - , transformLLVMArgs - , transformLLVMRet + , ArgCast(applyArgCast) + , ValCast(applyValCast) + , castLLVMArgs + , castLLVMRet ) where import Control.Monad.IO.Class (liftIO) import Control.Lens -import Data.Either.Extra (mapLeft) -import qualified Data.Text as Text -import Data.Vector (Vector) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(Some)) import Data.Parameterized.TraversableFC (fmapFC) import Lang.Crucible.Backend -import Lang.Crucible.Panic (panic) import Lang.Crucible.Simulator.OverrideSim import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Types -import What4.FunctionName - import Lang.Crucible.LLVM.MemModel data ValCastError @@ -50,61 +44,61 @@ printValCastError = \case MismatchedShape -> ["argument shape mismatch"] ValCastError (Some ret) (Some ret') -> - [ "Cannot transform types" + [ "Cannot cast types" , "*** Source type: " ++ show ret , "*** Target type: " ++ show ret' ] -newtype ArgTransformer p sym ext args args' = - ArgTransformer { applyArgTransformer :: (forall rtp l a. +newtype ArgCast p sym ext args args' = + ArgCast { applyArgCast :: (forall rtp l a. Ctx.Assignment (RegEntry sym) args -> OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) } -newtype ValTransformer p sym ext tp tp' = - ValTransformer { applyValTransformer :: (forall rtp l a. +newtype ValCast p sym ext tp tp' = + ValCast { applyValCast :: (forall rtp l a. RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp')) } -transformLLVMArgs :: forall p sym ext bak args args'. +castLLVMArgs :: forall p sym ext bak args args'. (IsSymBackend sym bak, HasLLVMAnn sym) => bak -> CtxRepr args' -> CtxRepr args -> - Either ValCastError (ArgTransformer p sym ext args args') -transformLLVMArgs _ Ctx.Empty Ctx.Empty = - Right (ArgTransformer (\_ -> return Ctx.Empty)) -transformLLVMArgs bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = - do (ValTransformer f) <- transformLLVMRet bak tp tp' - (ArgTransformer fs) <- transformLLVMArgs bak rest' rest - Right (ArgTransformer + Either ValCastError (ArgCast p sym ext args args') +castLLVMArgs _ Ctx.Empty Ctx.Empty = + Right (ArgCast (\_ -> return Ctx.Empty)) +castLLVMArgs bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = + do (ValCast f) <- castLLVMRet bak tp tp' + (ArgCast fs) <- castLLVMArgs bak rest' rest + Right (ArgCast (\(xs Ctx.:> x) -> do xs' <- fs xs x' <- f (regValue x) pure (xs' Ctx.:> RegEntry tp' x'))) -transformLLVMArgs _ _ _ = Left MismatchedShape +castLLVMArgs _ _ _ = Left MismatchedShape -transformLLVMRet :: +castLLVMRet :: (IsSymBackend sym bak, HasLLVMAnn sym) => bak -> TypeRepr ret -> TypeRepr ret' -> - Either ValCastError (ValTransformer p sym ext ret ret') -transformLLVMRet bak (BVRepr w) (LLVMPointerRepr w') + Either ValCastError (ValCast p sym ext ret ret') +castLLVMRet bak (BVRepr w) (LLVMPointerRepr w') | Just Refl <- testEquality w w' - = Right (ValTransformer (liftIO . llvmPointer_bv (backendGetSym bak))) -transformLLVMRet bak (LLVMPointerRepr w) (BVRepr w') + = Right (ValCast (liftIO . llvmPointer_bv (backendGetSym bak))) +castLLVMRet bak (LLVMPointerRepr w) (BVRepr w') | Just Refl <- testEquality w w' - = Right (ValTransformer (liftIO . projectLLVM_bv bak)) -transformLLVMRet bak (VectorRepr tp) (VectorRepr tp') - = do ValTransformer f <- transformLLVMRet bak tp tp' - Right (ValTransformer (traverse f)) -transformLLVMRet bak (StructRepr ctx) (StructRepr ctx') - = do ArgTransformer tf <- transformLLVMArgs bak ctx' ctx - Right (ValTransformer (\vals -> + = Right (ValCast (liftIO . projectLLVM_bv bak)) +castLLVMRet bak (VectorRepr tp) (VectorRepr tp') + = do ValCast f <- castLLVMRet bak tp tp' + Right (ValCast (traverse f)) +castLLVMRet bak (StructRepr ctx) (StructRepr ctx') + = do ArgCast tf <- castLLVMArgs bak ctx' ctx + Right (ValCast (\vals -> let vals' = Ctx.zipWith (\tp (RV v) -> RegEntry tp v) ctx vals in fmapFC (\x -> RV (regValue x)) <$> tf vals')) -transformLLVMRet _bak ret ret' +castLLVMRet _bak ret ret' | Just Refl <- testEquality ret ret' - = Right (ValTransformer return) -transformLLVMRet _bak ret ret' = Left (ValCastError (Some ret) (Some ret')) + = Right (ValCast return) +castLLVMRet _bak ret ret' = Left (ValCastError (Some ret) (Some ret')) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs index dc64162f3..07e1eb489 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -216,14 +216,14 @@ build_llvm_override :: build_llvm_override fnm args ret args' ret' llvmOverride = ovrWithBackend $ \bak -> do fargs <- - case Cast.transformLLVMArgs bak args args' of + case Cast.castLLVMArgs bak args args' of Left err -> panic "Intrinsics.build_llvm_override" (Cast.printValCastError err ++ [ "in function: " ++ Text.unpack (functionName fnm) ]) Right f -> pure f fret <- - case Cast.transformLLVMRet bak ret ret' of + case Cast.castLLVMRet bak ret ret' of Left err -> panic "Intrinsics.build_llvm_override" (Cast.printValCastError err ++ @@ -231,7 +231,7 @@ build_llvm_override fnm args ret args' ret' llvmOverride = Right f -> pure f return $ mkOverride' fnm ret' $ do RegMap xs <- getOverrideArgs - Cast.applyValTransformer fret =<< llvmOverride =<< Cast.applyArgTransformer fargs xs + Cast.applyValCast fret =<< llvmOverride =<< Cast.applyArgCast fargs xs polymorphic1_llvm_override :: forall p sym arch wptr l a rtp. (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) => From a618f48202ce4b3dbb3aa6dd2b0cb1a78bd4d5d6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 11:37:11 -0400 Subject: [PATCH 4/8] crucible-llvm: Haddocks for casting --- .../src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index b845d56c2..0a6748c6d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -5,6 +5,12 @@ -- License : BSD3 -- Maintainer : Langston Barrett -- Stability : provisional +-- +-- The built-in overrides in "Lang.Crucible.LLVM.Intrinsics.Libc" and +-- "Lang.Crucible.LLVM.Intrinsics.LLVM" frequently take arguments of type +-- 'Lang.Crucible.Types.BVType', but at runtime everything is represented as an +-- 'Lang.Crucible.LLVM.MemModel.Pointer.LLVMPtr'. This module contains helpers +-- for \"casting\" between pointers and bitvectors. ------------------------------------------------------------------------ {-# LANGUAGE GADTs #-} @@ -36,9 +42,13 @@ import Lang.Crucible.Types import Lang.Crucible.LLVM.MemModel data ValCastError - = MismatchedShape + = -- | Mismatched number of arguments ('castLLVMArgs') or struct fields + -- ('castLLVMRet'). + MismatchedShape + -- | Can\'t cast between these types | ValCastError (Some TypeRepr) (Some TypeRepr) +-- | Turn a 'ValCastError' into a human-readable message (lines). printValCastError :: ValCastError -> [String] printValCastError = \case @@ -49,16 +59,20 @@ printValCastError = , "*** Target type: " ++ show ret' ] +-- | A function to (infallibly) cast between 'Ctx.Assignment's of 'RegEntry's. newtype ArgCast p sym ext args args' = ArgCast { applyArgCast :: (forall rtp l a. Ctx.Assignment (RegEntry sym) args -> OverrideSim p sym ext rtp l a (Ctx.Assignment (RegEntry sym) args')) } +-- | A function to (infallibly) cast a value of types @tp@ to @tp'@. newtype ValCast p sym ext tp tp' = ValCast { applyValCast :: (forall rtp l a. RegValue sym tp -> OverrideSim p sym ext rtp l a (RegValue sym tp')) } +-- | Attempt to construct a function to cast between 'Ctx.Assignment's of +-- 'RegEntry's. castLLVMArgs :: forall p sym ext bak args args'. (IsSymBackend sym bak, HasLLVMAnn sym) => bak -> @@ -77,6 +91,8 @@ castLLVMArgs bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = pure (xs' Ctx.:> RegEntry tp' x'))) castLLVMArgs _ _ _ = Left MismatchedShape +-- | Attempt to construct a function to cast values of type @ret@ to type +-- @ret'@. castLLVMRet :: (IsSymBackend sym bak, HasLLVMAnn sym) => bak -> From b168cb176e2f20f232b5d5834ab9fbb80e0105fa Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 11:37:44 -0400 Subject: [PATCH 5/8] crucible-llvm: Remove unused constraints --- crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 0a6748c6d..979d7e6a2 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -74,7 +74,7 @@ newtype ValCast p sym ext tp tp' = -- | Attempt to construct a function to cast between 'Ctx.Assignment's of -- 'RegEntry's. castLLVMArgs :: forall p sym ext bak args args'. - (IsSymBackend sym bak, HasLLVMAnn sym) => + IsSymBackend sym bak => bak -> CtxRepr args' -> CtxRepr args -> @@ -94,7 +94,7 @@ castLLVMArgs _ _ _ = Left MismatchedShape -- | Attempt to construct a function to cast values of type @ret@ to type -- @ret'@. castLLVMRet :: - (IsSymBackend sym bak, HasLLVMAnn sym) => + IsSymBackend sym bak => bak -> TypeRepr ret -> TypeRepr ret' -> From a7bbd5d907ea85d38677945bb94616e9c681f6a2 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 11:38:08 -0400 Subject: [PATCH 6/8] crucible-llvm: Unnecessary parens --- crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 979d7e6a2..7ebe1305a 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -82,8 +82,8 @@ castLLVMArgs :: forall p sym ext bak args args'. castLLVMArgs _ Ctx.Empty Ctx.Empty = Right (ArgCast (\_ -> return Ctx.Empty)) castLLVMArgs bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = - do (ValCast f) <- castLLVMRet bak tp tp' - (ArgCast fs) <- castLLVMArgs bak rest' rest + do ValCast f <- castLLVMRet bak tp tp' + ArgCast fs <- castLLVMArgs bak rest' rest Right (ArgCast (\(xs Ctx.:> x) -> do xs' <- fs xs From 64030bbd5103e28af9e87299f6f3b20a4db80344 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 11:43:00 -0400 Subject: [PATCH 7/8] crucible-llvm: Export casting module --- crucible-llvm/crucible-llvm.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 94249f54b..528fcfd8a 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -73,6 +73,7 @@ library Lang.Crucible.LLVM.Extension Lang.Crucible.LLVM.Globals Lang.Crucible.LLVM.Intrinsics + Lang.Crucible.LLVM.Intrinsics.Cast Lang.Crucible.LLVM.Intrinsics.Libc Lang.Crucible.LLVM.Intrinsics.LLVM Lang.Crucible.LLVM.MalformedLLVMModule @@ -98,7 +99,6 @@ library Lang.Crucible.LLVM.Errors.Standards Lang.Crucible.LLVM.Extension.Arch Lang.Crucible.LLVM.Extension.Syntax - Lang.Crucible.LLVM.Intrinsics.Cast Lang.Crucible.LLVM.Intrinsics.Common Lang.Crucible.LLVM.Intrinsics.Libcxx Lang.Crucible.LLVM.Intrinsics.Options From 2a8755950445e084a65806a7a533124b5fd70a6f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 27 Mar 2024 13:57:20 -0400 Subject: [PATCH 8/8] Update crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs Co-authored-by: Ryan Scott --- crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 7ebe1305a..4f9f35e7e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -1,6 +1,6 @@ -- | -- Module : Lang.Crucible.LLVM.Intrinsics.Cast --- Description : Cast between bitvectors and pointers in signatuers +-- Description : Cast between bitvectors and pointers in signatures -- Copyright : (c) Galois, Inc 2024 -- License : BSD3 -- Maintainer : Langston Barrett