crucible-llvm: Improve error messages in a few pointer-to-bitvector casts

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs

@@ -29,17 +29,22 @@ 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           Lang.Crucible.Backend
+import           Lang.Crucible.Simulator (SimErrorReason(AssertFailureSimError))
 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
@@ -75,46 +80,54 @@ 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
 
 -- | 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'
+  = 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))
-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'))

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 ++

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

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
@@ -1135,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
@@ -1170,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

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