stubs-common: Stop using projectLLVM_bv to zero-extend/truncate pointers

Doing so is actively harmful when adjusting the size of pointers, as
`projectLLVM_bv` will throw an assertion failure if this happens. We now adjust
pointer sizes in an alternative, non-assertion-failure–throwing fashion.

After doing this, some functions in `Stubs.Override` (e.g., `bvToPtr`) no
longer serve a useful purpose, so I went ahead and removed them.

Fixes #41.

stubs-common/src/Stubs/FunctionOverride/AArch32/Linux.hs

@@ -88,7 +88,7 @@ aarch32LinuxIntegerArguments bak archVals argTypes regFile mem = do
   -- NB: `regArgList` below only has four elements, so the cost of using (++)
   -- below (which is O(n) in the size of the first list n) is negligible.
   let argList = regArgList ++ stackArgList
-  AO.buildArgumentAssignment bak argTypes argList
+  AO.buildArgumentAssignment (LCB.backendGetSym bak) argTypes argList
   where
     ptrWidth = PN.knownNat @32
     regArgList = map (pure . lookupReg) aarch32LinuxIntegerArgumentRegisters
@@ -166,9 +166,7 @@ aarch32LinuxIntegerReturnRegisters bak _archVals ovTy result initRegs =
       :: (1 WI.<= srcW, DMT.KnownNat srcW)
       => LCLM.LLVMPtr sym srcW
       -> IO (LCLM.LLVMPtr sym 32)
-    extendResult res = do
-      asBv <- LCLM.projectLLVM_bv bak res
-      AO.bvToPtr sym asBv (PN.knownNat @32)
+    extendResult res = AO.adjustPointerSize sym res (PN.knownNat @32)
 
     updateRegs ::
          LCS.RegValue sym (DMS.ArchRegStruct DMA.ARM)

stubs-common/src/Stubs/FunctionOverride/ForwardDeclarations.hs

@@ -53,6 +53,7 @@ mkForwardDeclarationOverride bak
   (SF.SomeFunctionOverride resolvedFnOv NEL.:| parents) fwdDecName fwdDecHandle =
     LCS.mkOverride' fwdDecName (LCF.handleReturnType fwdDecHandle) ovSim
   where
+    sym = LCB.backendGetSym bak
     fwdDecRetType = SFA.promoteBVToPtr $ LCF.handleReturnType fwdDecHandle
 
     ovSim ::
@@ -72,7 +73,7 @@ mkForwardDeclarationOverride bak
       let resEntry0 = LCS.RegEntry (SF.functionReturnType resolvedFnOv) resValue
       -- Step (4)
       resEntry1 <- liftIO $
-        SO.narrowPointerType bak fwdDecRetType resEntry0
+        SO.narrowPointerType sym fwdDecRetType resEntry0
       -- Step (5)
       resEntry2 <- liftIO $
         SFA.convertBitvector bak (LCF.handleReturnType fwdDecHandle) resEntry1
@@ -100,7 +101,7 @@ mkForwardDeclarationOverride bak
               IO (Ctx.Assignment (LCS.RegEntry sym) regTps')
         go Ctx.Empty Ctx.Empty = pure Ctx.Empty
         go (regTypeReprs Ctx.:> regTypeRepr) (narrowEntries Ctx.:> narrowEntry) = do
-          regEntry <- SO.extendPointerType bak regTypeRepr narrowEntry
+          regEntry <- SO.extendPointerType sym regTypeRepr narrowEntry
           regEntries <- go regTypeReprs narrowEntries
           pure (regEntries Ctx.:> regEntry)
         go _ _ = CMC.throwM $ SE.ForwardDeclarationArgumentNumberMismatch

stubs-common/src/Stubs/FunctionOverride/PPC/Linux.hs

@@ -87,7 +87,7 @@ ppcLinuxIntegerArguments bak archVals argTypes regs mem = do
   -- NB: `regArgList` below only has eight elements, so the cost of using (++)
   -- below (which is O(n) in the size of the first list n) is negligible.
   let argList = regArgList ++ stackArgList
-  AO.buildArgumentAssignment bak argTypes argList
+  AO.buildArgumentAssignment (LCB.backendGetSym bak) argTypes argList
   where
     regArgList = map (pure . DMS.lookupReg archVals (LCS.RegEntry LCT.knownRepr regs))
                      ppcLinuxIntegerArgumentRegisters
@@ -162,9 +162,8 @@ ppcLinuxIntegerReturnRegisters bak archVals ovTy result initRegs =
       :: (1 WI.<= srcW, DMT.KnownNat srcW)
       => LCLM.LLVMPtr sym srcW
       -> IO (LCLM.LLVMPtr sym (SAP.AddrWidth v))
-    extendOrTruncResult res = do
-      asBv <- LCLM.projectLLVM_bv bak res
-      AO.bvToPtr sym asBv (SAP.addrWidth (DMP.knownVariant @v))
+    extendOrTruncResult res =
+      AO.adjustPointerSize sym res (SAP.addrWidth (DMP.knownVariant @v))
 
     updateRegs ::
          LCS.RegValue sym (DMS.ArchRegStruct (DMP.AnyPPC v))

stubs-common/src/Stubs/FunctionOverride/X86_64/Linux.hs

@@ -90,7 +90,7 @@ x86_64LinuxIntegerArguments bak archVals argTypes regs mem = do
   -- NB: `regArgList` below only has six elements, so the cost of using (++)
   -- below (which is O(n) in the size of the first list n) is negligible.
   let argList = regArgList ++ stackArgList
-  AO.buildArgumentAssignment bak argTypes argList
+  AO.buildArgumentAssignment (LCB.backendGetSym bak) argTypes argList
   where
     ptrWidth = WI.knownNat @64
     regArgList = map (pure . DMS.lookupReg archVals (LCS.RegEntry LCT.knownRepr regs)) DMX.x86ArgumentRegs
@@ -142,15 +142,15 @@ x86_64LinuxIntegerReturnRegisters bak archVals ovTyp result initRegs =
           pure $ updateRegs allRegs [(reg, val)]
         LCLM.LLVMPointerRepr w
           | Just WI.Refl <- WI.testEquality w (WI.knownNat @8) -> do
-          extVal <- bvZextResult val
+          extVal <- liftIO $ bvZextResult val
           pure $ updateRegs allRegs [(reg, extVal)]
         LCLM.LLVMPointerRepr w
           | Just WI.Refl <- WI.testEquality w (WI.knownNat @16) -> do
-          extVal <- bvZextResult val
+          extVal <- liftIO $ bvZextResult val
           pure $ updateRegs allRegs [(reg, extVal)]
         LCLM.LLVMPointerRepr w
           | Just WI.Refl <- WI.testEquality w (WI.knownNat @32) -> do
-          extVal <- bvZextResult val
+          extVal <- liftIO $ bvZextResult val
           pure $ updateRegs allRegs [(reg, extVal)]
         _ -> AP.panic AP.FunctionOverride
                       "x86_64LinuxIntegerReturnRegisters"
@@ -163,10 +163,8 @@ x86_64LinuxIntegerReturnRegisters bak archVals ovTyp result initRegs =
     bvZextResult
       :: (1 <= srcW, KnownNat srcW)
       => LCLM.LLVMPtr sym srcW
-      -> LCS.OverrideSim p sym ext r args rtp (LCLM.LLVMPtr sym 64)
-    bvZextResult res = do
-      asBv <- liftIO $ LCLM.projectLLVM_bv bak res
-      liftIO $ AO.bvToPtr sym asBv (WI.knownNat @64)
+      -> IO (LCLM.LLVMPtr sym 64)
+    bvZextResult res = liftIO $ AO.adjustPointerSize sym res (PN.knownNat @64)
 
     updateRegs :: LCS.RegValue sym (DMS.ArchRegStruct DMX.X86_64)
                -> [( DMC.ArchReg DMX.X86_64 (DMT.BVType 64)

stubs-common/src/Stubs/Override.hs

@@ -8,17 +8,15 @@ module Stubs.Override
   ( buildArgumentAssignment
   , narrowPointerType
   , extendPointerType
-  , bvToPtr
-  , ptrToBv8
-  , ptrToBv32
+  , adjustPointerSize
   , overrideMemOptions
   ) where
 
 import qualified Control.Monad.Catch as CMC
 import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.NatRepr as PN
-import           GHC.TypeNats ( type (<=), KnownNat )
+import           GHC.TypeNats ( type (<=) )
 
 import qualified Lang.Crucible.Backend as LCB
 import qualified Lang.Crucible.Simulator as LCS
@@ -45,16 +43,16 @@ import qualified Stubs.Panic as AP
 -- list is monadic because of the possible need to load a value from memory.
 -- See @Note [Passing arguments to functions]@ in "Ambient.FunctionOverride".
 buildArgumentAssignment
-  :: forall w args sym bak
-   . (1 <= w, LCB.IsSymBackend sym bak)
-  => bak
+  :: forall w args sym
+   . (1 <= w, LCB.IsSymInterface sym)
+  => sym
   -> LCT.CtxRepr args
   -- ^ Types of arguments
   -> [IO (LCS.RegEntry sym (LCLM.LLVMPointerType w))]
   -- ^ List of potential argument values
   -> IO (Ctx.Assignment (LCS.RegEntry sym) args, AF.GetVarArg sym)
   -- ^ The argument values and a callback for retrieving variadic arguments
-buildArgumentAssignment bak argTyps argEntries = do
+buildArgumentAssignment sym argTyps argEntries = do
   (knownArgs, variadicArgs) <- buildAssignment argTyps argEntries
   pure ( knownArgs
        , AF.GetVarArg $ \tp -> getVarArg tp variadicArgs
@@ -113,7 +111,7 @@ buildArgumentAssignment bak argTyps argEntries = do
                            ]
             mkArg : args' -> do
               arg <- mkArg
-              arg' <- narrowPointerType bak trep arg
+              arg' <- narrowPointerType sym trep arg
               rest <- go typs' args'
               return (rest Ctx.:> arg')
 
@@ -126,13 +124,13 @@ newtype BvNarrowing sym w tp where
 -- 'LCLM.LLVMPointerType's, truncate the wider type to the narrow type.
 -- Otherwise, require the types to be the same.
 narrowPointerType ::
-  forall sym bak wideTp narrowTp.
-  LCB.IsSymBackend sym bak =>
-  bak ->
+  forall sym wideTp narrowTp.
+  LCB.IsSymInterface sym =>
+  sym ->
   LCT.TypeRepr narrowTp ->
   LCS.RegEntry sym wideTp ->
   IO (LCS.RegEntry sym narrowTp)
-narrowPointerType bak narrowTypeRepr wideEntry
+narrowPointerType sym narrowTypeRepr wideEntry
   | LCLM.LLVMPointerRepr widePtrW <- LCS.regType wideEntry
   = case MapF.lookup narrowTypeRepr (conversions widePtrW) of
       Nothing -> CMC.throwM $ AE.FunctionTypeBvNarrowingError widePtrW
@@ -164,7 +162,7 @@ narrowPointerType bak narrowTypeRepr wideEntry
             => PN.NatRepr narrowPtrW
             -> LCS.RegEntry sym (LCLM.LLVMPointerType widePtrW)
             -> IO (LCS.RegEntry sym (LCLM.LLVMPointerType narrowPtrW))
-    bvTrunc bvW ptr = adjustPtrEntrySize bak ptr bvW
+    bvTrunc bvW ptr = adjustPointerEntrySize sym ptr bvW
 
 -- | Bitvector conversion from a narrow type to a wider width.
 -- Like 'BvConversion', except with the argument and result types in the
@@ -177,13 +175,13 @@ newtype BvExtension sym w tp where
 -- 'LCLM.LLVMPointerType's, zero-extend the narrow type to the wider type.
 -- Otherwise, require the types to be the same.
 extendPointerType ::
-  forall sym bak narrowTp wideTp.
-  LCB.IsSymBackend sym bak =>
-  bak ->
+  forall sym narrowTp wideTp.
+  LCB.IsSymInterface sym =>
+  sym ->
   LCT.TypeRepr wideTp ->
   LCS.RegEntry sym narrowTp ->
   IO (LCS.RegEntry sym wideTp)
-extendPointerType bak wideTypeRepr narrowEntry
+extendPointerType sym wideTypeRepr narrowEntry
   | LCLM.LLVMPointerRepr widePtrW <- wideTypeRepr
   = case MapF.lookup narrowTypeRepr (conversions widePtrW) of
       Nothing -> CMC.throwM $ AE.FunctionTypeBvExtensionError widePtrW
@@ -217,80 +215,60 @@ extendPointerType bak wideTypeRepr narrowEntry
             => PN.NatRepr widePtrW
             -> LCS.RegEntry sym (LCLM.LLVMPointerType narrowPtrW)
             -> IO (LCS.RegEntry sym (LCLM.LLVMPointerType widePtrW))
-    bvZext bvW ptr = adjustPtrEntrySize bak ptr bvW
+    bvZext bvW ptr = adjustPointerEntrySize sym ptr bvW
 
--- | Zero extend or truncate bitvector to an LLVMPointer
-bvToPtr :: forall sym srcW ptrW
-         . ( LCB.IsSymInterface sym
-           , 1 <= srcW
-           , 1 <= ptrW
-           )
-           => sym
-           -> WI.SymExpr sym (WI.BaseBVType srcW)
-           -> PN.NatRepr ptrW
-           -> IO (LCS.RegValue sym (LCLM.LLVMPointerType ptrW))
-bvToPtr sym bv ptrW =
-  case PN.compareNat srcW ptrW of
-    PN.NatEQ -> LCLM.llvmPointer_bv sym bv
-    PN.NatLT _w -> WI.bvZext sym ptrW bv >>= LCLM.llvmPointer_bv sym
-    PN.NatGT _w -> WI.bvTrunc sym ptrW bv >>= LCLM.llvmPointer_bv sym
+-- | Zero-extend or truncate a @'WI.SymBV' sym srcW@ to be of size @dstW@.
+adjustBvSize ::
+  forall sym srcW dstW.
+  ( LCB.IsSymInterface sym
+  , 1 <= srcW
+  , 1 <= dstW
+  ) =>
+  sym ->
+  WI.SymBV sym srcW ->
+  PN.NatRepr dstW ->
+  IO (WI.SymBV sym dstW)
+adjustBvSize sym bv dstW =
+  case PN.compareNat srcW dstW of
+    PN.NatEQ -> pure bv
+    PN.NatLT _w -> WI.bvZext sym dstW bv
+    PN.NatGT _w -> WI.bvTrunc sym dstW bv
   where
     srcW :: PN.NatRepr srcW
     srcW = case WI.exprType bv of
              WI.BaseBVRepr w -> w
 
--- | Zero extend or truncate an 'LCLM.LLVMPointer' 'LCS.RegEntry'.
-adjustPtrEntrySize ::
-  forall sym bak srcW dstW.
-  ( LCB.IsSymBackend sym bak
+-- | Zero-extend or truncate an @'LCLM.LLVMPtr' sym srcW@ to be of size @dstW@.
+adjustPointerSize ::
+  forall sym srcW dstW.
+  ( LCB.IsSymInterface sym
+  , 1 <= srcW
+  , 1 <= dstW
+  ) =>
+  sym ->
+  LCLM.LLVMPtr sym srcW ->
+  PN.NatRepr dstW ->
+  IO (LCLM.LLVMPtr sym dstW)
+adjustPointerSize sym srcPtr dstW = do
+  let LCLM.LLVMPointer srcBase srcOffset = srcPtr
+  dstOffset <- adjustBvSize sym srcOffset dstW
+  pure $ LCLM.LLVMPointer srcBase dstOffset
+
+-- | Zero-extend or truncate an @'LCLM.LLVMPtr' sym srcW@ 'LCS.RegEntry' to be of
+-- size @dstW@.
+adjustPointerEntrySize ::
+  forall sym srcW dstW.
+  ( LCB.IsSymInterface sym
   , 1 <= srcW
   , 1 <= dstW
   ) =>
-  bak ->
+  sym ->
   LCS.RegEntry sym (LCLM.LLVMPointerType srcW) ->
   PN.NatRepr dstW ->
   IO (LCS.RegEntry sym (LCLM.LLVMPointerType dstW))
-adjustPtrEntrySize bak srcPtr dstW = do
-  let sym = LCB.backendGetSym bak
-  bv <- LCLM.projectLLVM_bv bak $ LCS.regValue srcPtr
-  rv <- bvToPtr sym bv dstW
-  pure $ LCS.RegEntry (LCLM.LLVMPointerRepr dstW) rv
-
--- | Convert an 'LCLM.LLVMPtr' to an 8-bit vector by dropping the upper bits.
-ptrToBv8 :: ( LCB.IsSymBackend sym bak )
-          => bak
-          -> PN.NatRepr w
-          -> LCS.RegEntry sym (LCLM.LLVMPointerType w)
-          -> IO (LCS.RegEntry sym (LCT.BVType 8))
-ptrToBv8 = ptrToBv
-
--- | Convert an 'LCLM.LLVMPtr' to a 32-bit vector by dropping the upper bits.
-ptrToBv32 :: ( LCB.IsSymBackend sym bak )
-          => bak
-          -> PN.NatRepr w
-          -> LCS.RegEntry sym (LCLM.LLVMPointerType w)
-          -> IO (LCS.RegEntry sym (LCT.BVType 32))
-ptrToBv32 = ptrToBv
-
--- | Convert an 'LCLM.LLVMPtr' to a bitvector by dropping the upper bits.
-ptrToBv :: forall sym bak ptrW destW
-         . ( LCB.IsSymBackend sym bak
-           , KnownNat destW
-           , 1 <= destW
-           )
-        => bak
-        -> PN.NatRepr ptrW
-        -> LCS.RegEntry sym (LCLM.LLVMPointerType ptrW)
-        -> IO (LCS.RegEntry sym (LCT.BVType destW))
-ptrToBv bak nr ptr = do
-  let sym = LCB.backendGetSym bak
-  bvW <- LCLM.projectLLVM_bv bak (LCS.regValue ptr)
-  case PN.compareNat nr (WI.knownNat @destW) of
-    PN.NatLT _ -> AP.panic AP.Override "ptrToBv32" ["Pointer too small to truncate to 32 bits: " ++ show nr]
-    PN.NatEQ -> return $! LCS.RegEntry LCT.knownRepr bvW
-    PN.NatGT _w -> do
-      lower <- WI.bvTrunc sym (WI.knownNat @destW) bvW
-      return $! LCS.RegEntry LCT.knownRepr lower
+adjustPointerEntrySize sym ptrEntry dstW =
+  LCS.RegEntry (LCLM.LLVMPointerRepr dstW) <$>
+  adjustPointerSize sym (LCS.regValue ptrEntry) dstW
 
 -- | The memory options used to configure the memory model for system call and
 -- function overrides.

stubs-common/src/Stubs/Syscall/AArch32/Linux.hs

@@ -130,7 +130,7 @@ aarch32LinuxSyscallArgumentRegisters bak regTypes regs syscallTypes
           -- No syscalls make use of variadic arguments (see Note [Varargs] in
           -- Ambient.FunctionOverride), so we do not make use of the GetVarArg
           -- callback.
-          (regAssn, _getVarArg) <- AO.buildArgumentAssignment bak syscallTypes regEntries
+          (regAssn, _getVarArg) <- AO.buildArgumentAssignment (LCB.backendGetSym bak) syscallTypes regEntries
           pure regAssn
   | otherwise = AP.panic AP.Syscall "aarch32LinuxSyscallArgumentRegisters" [ "Unexpected argument register shape: " ++ show regTypes ]
   where

stubs-common/src/Stubs/Syscall/PPC/Linux.hs

@@ -154,7 +154,7 @@ ppcLinuxSyscallArgumentRegisters variantRepr bak regTypes regs syscallTypes
           -- No syscalls make use of variadic arguments (see Note [Varargs] in
           -- Ambient.FunctionOverride), so we do not make use of the GetVarArg
           -- callback.
-          (regAssn, _getVarArg) <- AO.buildArgumentAssignment bak syscallTypes regEntries
+          (regAssn, _getVarArg) <- AO.buildArgumentAssignment (LCB.backendGetSym bak) syscallTypes regEntries
           pure regAssn
   | otherwise = AP.panic AP.Syscall "ppcLinuxSyscallArgumentRegisters" [ "Unexpected argument register shape: " ++ show regTypes ]
   where

stubs-common/src/Stubs/Syscall/X86_64/Linux.hs

@@ -84,7 +84,7 @@ x86_64LinuxSyscallArgumentRegisters bak regTyps regs syscallTyps
         -- Extract argument registers and put in list.
         let regEntries = map (pure . toRegEntry) [rdi, rsi, rdx, r10, r8, r9]
         -- Build an assignment from 'regEntries'
-        (regAssn, _) <- AO.buildArgumentAssignment bak syscallTyps regEntries
+        (regAssn, _) <- AO.buildArgumentAssignment (LCB.backendGetSym bak) syscallTyps regEntries
         -- No syscalls make use of variadic arguments (see Note [Varargs] in
         -- Ambient.FunctionOverride), so we do not make use of the GetVarArg
         -- callback.