From fb996ef15a20d78ff733696926bbff2d794259d6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 14:16:37 -0400 Subject: [PATCH 1/6] Improve error message in pointer-to-bitvector cast for overrides --- .../src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 55 ++++++++++++++----- .../Lang/Crucible/LLVM/Intrinsics/Common.hs | 4 +- 2 files changed, 43 insertions(+), 16 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 4f9f35e7e..2360a79b3 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -29,12 +29,18 @@ module Lang.Crucible.LLVM.Intrinsics.Cast 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.Some (Some(Some)) import Data.Parameterized.TraversableFC (fmapFC) +import What4.FunctionName (FunctionName (functionName)) +import What4.Interface (SymBV) +import qualified What4.Interface as W4 + import Lang.Crucible.Backend +import Lang.Crucible.Simulator (SimErrorReason(AssertFailureSimError)) import Lang.Crucible.Simulator.OverrideSim import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Types @@ -75,46 +81,67 @@ newtype ValCast p sym ext tp tp' = -- 'RegEntry's. castLLVMArgs :: forall p sym ext bak args args'. IsSymBackend sym bak => + -- | Only used in error messages + FunctionName -> bak -> CtxRepr args' -> CtxRepr args -> Either ValCastError (ArgCast p sym ext args args') -castLLVMArgs _ Ctx.Empty Ctx.Empty = +castLLVMArgs _fnm _ 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 +castLLVMArgs fnm bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = + do ValCast f <- castLLVMRet fnm bak tp tp' + ArgCast fs <- castLLVMArgs fnm bak rest' rest Right (ArgCast (\(xs Ctx.:> x) -> do xs' <- fs xs x' <- f (regValue x) pure (xs' Ctx.:> RegEntry tp' x'))) -castLLVMArgs _ _ _ = Left MismatchedShape +castLLVMArgs _ _ _ _ = Left MismatchedShape + +-- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value. +ptrToBv :: + IsSymBackend sym bak => + -- | Only used in error messages + FunctionName -> + bak -> + LLVMPtr sym w -> + IO (SymBV sym w) +ptrToBv fnm bak (LLVMPointer blk bv) = + do let sym = backendGetSym bak + p <- W4.natEq sym blk =<< W4.natLit sym 0 + assert bak p $ + AssertFailureSimError + "Found a pointer where a bitvector was expected" + ("In the arguments or return value of" ++ Text.unpack (functionName fnm)) + return bv -- | Attempt to construct a function to cast values of type @ret@ to type -- @ret'@. castLLVMRet :: IsSymBackend sym bak => + -- | Only used in error messages + FunctionName -> bak -> TypeRepr ret -> TypeRepr ret' -> Either ValCastError (ValCast p sym ext ret ret') -castLLVMRet bak (BVRepr w) (LLVMPointerRepr w') +castLLVMRet _fnm bak (BVRepr w) (LLVMPointerRepr w') | Just Refl <- testEquality w w' = Right (ValCast (liftIO . llvmPointer_bv (backendGetSym bak))) -castLLVMRet bak (LLVMPointerRepr w) (BVRepr w') +castLLVMRet fnm bak (LLVMPointerRepr w) (BVRepr w') | Just Refl <- testEquality w w' - = Right (ValCast (liftIO . projectLLVM_bv bak)) -castLLVMRet bak (VectorRepr tp) (VectorRepr tp') - = do ValCast f <- castLLVMRet bak tp tp' + = Right (ValCast (liftIO . ptrToBv fnm bak)) +castLLVMRet fnm bak (VectorRepr tp) (VectorRepr tp') + = do ValCast f <- castLLVMRet fnm bak tp tp' Right (ValCast (traverse f)) -castLLVMRet bak (StructRepr ctx) (StructRepr ctx') - = do ArgCast tf <- castLLVMArgs bak ctx' ctx +castLLVMRet fnm bak (StructRepr ctx) (StructRepr ctx') + = do ArgCast tf <- castLLVMArgs fnm 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')) -castLLVMRet _bak ret ret' +castLLVMRet _fnm _bak ret ret' | Just Refl <- testEquality ret ret' = Right (ValCast return) -castLLVMRet _bak ret ret' = Left (ValCastError (Some ret) (Some ret')) +castLLVMRet _fnm _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 98c6ac66d..c9975dd4e 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs @@ -155,14 +155,14 @@ build_llvm_override :: build_llvm_override fnm args ret args' ret' llvmOverride = ovrWithBackend $ \bak -> do fargs <- - case Cast.castLLVMArgs bak args args' of + case Cast.castLLVMArgs fnm 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.castLLVMRet bak ret ret' of + case Cast.castLLVMRet fnm bak ret ret' of Left err -> panic "Intrinsics.build_llvm_override" (Cast.printValCastError err ++ From 02ade5420149ff7d6d4a8893caa038ee4a3ad465 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 14:19:08 -0400 Subject: [PATCH 2/6] Improve error message in pointer-to-bitvector cast for `printf` --- crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs index 955ef889e..20d862071 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs @@ -689,8 +689,12 @@ printfOps bak valist = , printfGetInteger = \i sgn _len -> case valist V.!? (i-1) of - Just (AnyValue (LLVMPointerRepr w) x) -> - do bv <- liftIO (projectLLVM_bv bak x) + Just (AnyValue (LLVMPointerRepr w) (LLVMPointer blk bv)) -> + do isBv <- liftIO (natEq sym blk =<< natLit sym 0) + liftIO $ assert bak isBv $ + AssertFailureSimError + "Passed a pointer to printf where a bitvector was expected" + "" if sgn then return $ BV.asSigned w <$> asBV bv else From cebf1ca654cda460df529f836c99ff29197d6b01 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 14:21:29 -0400 Subject: [PATCH 3/6] Improve haddocks for `ptrToBv` --- crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 4 +++- 1 file changed, 3 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 2360a79b3..405c9eef3 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -99,7 +99,9 @@ castLLVMArgs fnm bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = pure (xs' Ctx.:> RegEntry tp' x'))) castLLVMArgs _ _ _ _ = Left MismatchedShape --- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value. +-- | Assert that a pointer is actually a raw bitvector and extract its value. +-- +-- Like 'projectLLVM_bv', but with a more specific error message. ptrToBv :: IsSymBackend sym bak => -- | Only used in error messages From fd07476ce6bfadd5a882ed386c23c3f257d5b878 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 14:27:29 -0400 Subject: [PATCH 4/6] Provide `ptrToBv`, an alternative to `projectLLVM_bv` --- .../src/Lang/Crucible/LLVM/Intrinsics/Cast.hs | 30 +++++-------------- .../src/Lang/Crucible/LLVM/MemModel.hs | 1 + .../Lang/Crucible/LLVM/MemModel/Partial.hs | 27 +++++++++++++---- 3 files changed, 30 insertions(+), 28 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs index 405c9eef3..f634717eb 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs @@ -36,8 +36,6 @@ import Data.Parameterized.Some (Some(Some)) import Data.Parameterized.TraversableFC (fmapFC) import What4.FunctionName (FunctionName (functionName)) -import What4.Interface (SymBV) -import qualified What4.Interface as W4 import Lang.Crucible.Backend import Lang.Crucible.Simulator (SimErrorReason(AssertFailureSimError)) @@ -45,7 +43,8 @@ import Lang.Crucible.Simulator.OverrideSim import Lang.Crucible.Simulator.RegMap import Lang.Crucible.Types -import Lang.Crucible.LLVM.MemModel +import Lang.Crucible.LLVM.MemModel.Partial (ptrToBv) +import Lang.Crucible.LLVM.MemModel.Pointer data ValCastError = -- | Mismatched number of arguments ('castLLVMArgs') or struct fields @@ -99,25 +98,6 @@ castLLVMArgs fnm bak (rest' Ctx.:> tp') (rest Ctx.:> tp) = pure (xs' Ctx.:> RegEntry tp' x'))) castLLVMArgs _ _ _ _ = Left MismatchedShape --- | Assert that a pointer is actually a raw bitvector and extract its value. --- --- Like 'projectLLVM_bv', but with a more specific error message. -ptrToBv :: - IsSymBackend sym bak => - -- | Only used in error messages - FunctionName -> - bak -> - LLVMPtr sym w -> - IO (SymBV sym w) -ptrToBv fnm bak (LLVMPointer blk bv) = - do let sym = backendGetSym bak - p <- W4.natEq sym blk =<< W4.natLit sym 0 - assert bak p $ - AssertFailureSimError - "Found a pointer where a bitvector was expected" - ("In the arguments or return value of" ++ Text.unpack (functionName fnm)) - return bv - -- | Attempt to construct a function to cast values of type @ret@ to type -- @ret'@. castLLVMRet :: @@ -133,7 +113,11 @@ castLLVMRet _fnm bak (BVRepr w) (LLVMPointerRepr w') = Right (ValCast (liftIO . llvmPointer_bv (backendGetSym bak))) castLLVMRet fnm bak (LLVMPointerRepr w) (BVRepr w') | Just Refl <- testEquality w w' - = Right (ValCast (liftIO . ptrToBv fnm bak)) + = let err = + AssertFailureSimError + "Found a pointer where a bitvector was expected" + ("In the arguments or return value of" ++ Text.unpack (functionName fnm)) in + Right (ValCast (liftIO . ptrToBv bak err)) castLLVMRet fnm bak (VectorRepr tp) (VectorRepr tp') = do ValCast f <- castLLVMRet fnm bak tp tp' Right (ValCast (traverse f)) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index 88fc1db63..5962b6c43 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -59,6 +59,7 @@ module Lang.Crucible.LLVM.MemModel , G.ppPtr , G.ppTermExpr , llvmPointer_bv + , Partial.ptrToBv , Partial.projectLLVM_bv -- * Memory operations diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs index ebe3e768e..0a39fda2f 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs @@ -46,6 +46,7 @@ module Lang.Crucible.LLVM.MemModel.Partial , BoolAnn(..) , annotateME , annotateUB + , ptrToBv , projectLLVM_bv , floatToBV @@ -262,16 +263,32 @@ annotateME sym mop rsn p = (BBMemoryError (MemoryError mop rsn)) return p' --- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value. -projectLLVM_bv :: +-- | Assert that the given LLVM pointer value is actually a raw bitvector and +-- extract its value. +ptrToBv :: IsSymBackend sym bak => - bak -> LLVMPtr sym w -> IO (SymBV sym w) -projectLLVM_bv bak (LLVMPointer blk bv) = + bak -> + -- | Error to report if casting the pointer to a bitvector fails + SimErrorReason -> + LLVMPtr sym w -> + IO (SymBV sym w) +ptrToBv bak err (LLVMPointer blk bv) = do let sym = backendGetSym bak p <- natEq sym blk =<< natLit sym 0 - assert bak p $ AssertFailureSimError "Pointer value coerced to bitvector" "" + assert bak p err return bv +-- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value. +-- +-- Note that this assertion has a very generic message, which can be unhelpful +-- to users when it fails. Consider using 'ptrToBv' instead. +projectLLVM_bv :: + IsSymBackend sym bak => + bak -> LLVMPtr sym w -> IO (SymBV sym w) +projectLLVM_bv bak ptr = + let err = AssertFailureSimError "Pointer value coerced to bitvector" "" in + ptrToBv bak err ptr + ------------------------------------------------------------------------ -- ** PartLLVMVal From 6af2c59616a1ddedee704debf1858d6477b7bdfc Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 15:37:49 -0400 Subject: [PATCH 5/6] Improve error message when pointers are found in strings --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index 5962b6c43..5cb01608d 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -1136,7 +1136,8 @@ strLen bak mem = go (BV.zero PtrWidth) (truePred sym) do ast <- impliesPred sym cond loadok assert bak ast $ AssertFailureSimError "Error during memory load: strlen" "" v <- unpackMemValue sym (LLVMPointerRepr (knownNat @8)) llvmval - test <- bvIsNonzero sym =<< Partial.projectLLVM_bv bak v + let err = AssertFailureSimError "Found pointer in string passed to `strlen`" "" + test <- bvIsNonzero sym =<< Partial.ptrToBv bak err v iteM bvIte sym test (do cond' <- andPred sym cond test @@ -1171,7 +1172,8 @@ loadString bak mem = go id go f _ (Just 0) = return $ f [] go f p maxChars = do v <- doLoad bak mem p (bitvectorType 1) (LLVMPointerRepr (knownNat :: NatRepr 8)) noAlignment - x <- Partial.projectLLVM_bv bak v + let err = AssertFailureSimError "Found pointer when loading string" "" + x <- Partial.ptrToBv bak err v case BV.asUnsigned <$> asBV x of Just 0 -> return $ f [] Just c -> do From a3241a4267f58fa42f58ce8524026801160778db Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 12 Jul 2024 16:02:01 -0400 Subject: [PATCH 6/6] Improve error messages in pointer-to-bitvector casts in string operations Co-authored-by: Ryan Scott --- crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs index 5cb01608d..226fa93e9 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs @@ -1136,7 +1136,7 @@ strLen bak mem = go (BV.zero PtrWidth) (truePred sym) do ast <- impliesPred sym cond loadok assert bak ast $ AssertFailureSimError "Error during memory load: strlen" "" v <- unpackMemValue sym (LLVMPointerRepr (knownNat @8)) llvmval - let err = AssertFailureSimError "Found pointer in string passed to `strlen`" "" + let err = AssertFailureSimError "Found pointer instead of byte in string passed to `strlen`" "" test <- bvIsNonzero sym =<< Partial.ptrToBv bak err v iteM bvIte sym test @@ -1172,7 +1172,7 @@ loadString bak mem = go id go f _ (Just 0) = return $ f [] go f p maxChars = do v <- doLoad bak mem p (bitvectorType 1) (LLVMPointerRepr (knownNat :: NatRepr 8)) noAlignment - let err = AssertFailureSimError "Found pointer when loading string" "" + let err = AssertFailureSimError "Found pointer instead of byte when loading string" "" x <- Partial.ptrToBv bak err v case BV.asUnsigned <$> asBV x of Just 0 -> return $ f []