llvm: Introduce predicate-building helpers ptrSameAlloc and ptrIsBv

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

@@ -64,6 +64,7 @@ import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack)
 import qualified Lang.Crucible.LLVM.MemModel.Type as G
 import qualified Lang.Crucible.LLVM.MemModel.Generic as G
 import           Lang.Crucible.LLVM.MemModel.Partial
+import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr
 import           Lang.Crucible.LLVM.Printf
 import           Lang.Crucible.LLVM.QQ( llvmOvr )
 import           Lang.Crucible.LLVM.TypeContext
@@ -689,8 +690,8 @@ printfOps bak valist =
 
   , printfGetInteger = \i sgn _len ->
      case valist V.!? (i-1) of
-       Just (AnyValue (LLVMPointerRepr w) (LLVMPointer blk bv)) ->
-         do isBv <- liftIO (natEq sym blk =<< natLit sym 0)
+       Just (AnyValue (LLVMPointerRepr w) p@(LLVMPointer _blk bv)) ->
+         do isBv <- liftIO (Ptr.ptrIsBv sym p)
             liftIO $ assert bak isBv $
               AssertFailureSimError
                "Passed a pointer to printf where a bitvector was expected"

crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs

@@ -1023,9 +1023,9 @@ doPtrAddOffset ::
   LLVMPtr sym wptr {- ^ base pointer -} ->
   SymBV sym wptr   {- ^ offset       -} ->
   IO (LLVMPtr sym wptr)
-doPtrAddOffset bak m x@(LLVMPointer blk _) off = do
+doPtrAddOffset bak m x off = do
   let sym = backendGetSym bak
-  isBV <- natEq sym blk =<< natLit sym 0
+  isBV <- ptrIsBv sym x
   x' <- ptrAdd sym PtrWidth x off
   v <- case asConstantPred isBV of
          Just True  -> return isBV
@@ -1652,13 +1652,13 @@ buildDisjointRegionsAssertion ::
   SymBV sym w      {- ^ length of region 2  -} ->
   IO (Pred sym)
 buildDisjointRegionsAssertion sym w dest dlen src slen = do
-  let LLVMPointer dblk doff = dest
-  let LLVMPointer sblk soff = src
+  let LLVMPointer _dblk doff = dest
+  let LLVMPointer _sblk soff = src
 
   dend <- bvAdd sym doff =<< sextendBVTo sym w PtrWidth dlen
   send <- bvAdd sym soff =<< sextendBVTo sym w PtrWidth slen
 
-  diffBlk   <- notPred sym =<< natEq sym dblk sblk
+  diffBlk   <- notPred sym =<< ptrSameAlloc sym dest src
   destfirst <- bvSle sym dend soff
   srcfirst  <- bvSle sym send doff
 
@@ -1678,15 +1678,15 @@ buildDisjointRegionsAssertionWithSub ::
   SymBV sym wptr   {- ^ length of region 2  -} ->
   IO (Pred sym)
 buildDisjointRegionsAssertionWithSub sym dest dlen src slen = do
-  let LLVMPointer dblk doff = dest
-  let LLVMPointer sblk soff = src
+  let LLVMPointer _dblk doff = dest
+  let LLVMPointer _sblk soff = src
 
   dend <- bvAdd sym doff dlen
   send <- bvAdd sym soff slen
 
   zero_bv <- bvZero sym PtrWidth
 
-  diffBlk <- notPred sym =<< natEq sym dblk sblk
+  diffBlk <- notPred sym =<< ptrSameAlloc sym dest src
 
   allPos <- andAllOf sym folded =<< mapM (bvSle sym zero_bv) [doff, dend, soff, send]
   destfirst <- bvSle sym zero_bv =<< bvSub sym soff dend

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs

@@ -92,7 +92,7 @@ import           Lang.Crucible.LLVM.Bytes (Bytes)
 import qualified Lang.Crucible.LLVM.Bytes as Bytes
 import           Lang.Crucible.LLVM.MemModel.MemLog (memState)
 import           Lang.Crucible.LLVM.MemModel.CallStack (CallStack, getCallStack)
-import           Lang.Crucible.LLVM.MemModel.Pointer ( pattern LLVMPointer, LLVMPtr )
+import           Lang.Crucible.LLVM.MemModel.Pointer ( pattern LLVMPointer, LLVMPtr, ptrIsBv )
 import           Lang.Crucible.LLVM.MemModel.Type (StorageType(..), StorageTypeF(..), Field(..))
 import qualified Lang.Crucible.LLVM.MemModel.Type as Type
 import           Lang.Crucible.LLVM.MemModel.Value (LLVMVal(..))
@@ -272,10 +272,10 @@ ptrToBv ::
   SimErrorReason ->
   LLVMPtr sym w ->
   IO (SymBV sym w)
-ptrToBv bak err (LLVMPointer blk bv) =
+ptrToBv bak err p@(LLVMPointer _blk bv) =
   do let sym = backendGetSym bak
-     p <- natEq sym blk =<< natLit sym 0
-     assert bak p err
+     isBv <- ptrIsBv sym p
+     assert bak isBv err
      return bv
 
 -- | Assert that the given LLVM pointer value is actually a raw bitvector and extract its value.

crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs

@@ -65,11 +65,13 @@ module Lang.Crucible.LLVM.MemModel.Pointer
 
     -- * Operations on valid pointers
   , constOffset
+  , ptrSameAlloc
   , ptrEq
   , ptrLe
   , ptrAdd
   , ptrDiff
   , ptrSub
+  , ptrIsBv
   , ptrIsNull
   , isGlobalPointer
   , isGlobalPointer'
@@ -121,9 +123,15 @@ data LLVMPointer sym w =
 
 deriving instance (Show (SymNat sym), Show (SymBV sym w)) => Show (LLVMPointer sym w)
 
+-- | Retrieve this pointer\'s block number.
+--
+-- Use of this function is discouraged, as it is abstraction-breaking.
 llvmPointerBlock :: LLVMPtr sym w -> SymNat sym
 llvmPointerBlock (LLVMPointer blk _) = blk
 
+-- | Retrieve this pointer\'s offset.
+--
+-- Use of this function is discouraged, as it is abstraction-breaking.
 llvmPointerOffset :: LLVMPtr sym w -> SymBV sym w
 llvmPointerOffset (LLVMPointer _ off) = off
 
@@ -299,6 +307,22 @@ instance TestEquality FloatSize where
 constOffset :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> G.Addr -> IO (SymBV sym w)
 constOffset sym w x = bvLit sym w (G.bytesToBV w x)
 
+-- | Test whether two pointers point to the same allocation (i.e., have the same
+-- block number).
+--
+-- Using this function is preferred to pattern matching on 'LLVMPointer' or
+-- 'llvmPointerBlock', because it operates at a higher level of abstraction
+-- (i.e., if the representation of pointers were changed, it could continue to
+-- work as intended).
+ptrSameAlloc ::
+  (1 <= w, IsSymInterface sym) =>
+  sym ->
+  LLVMPtr sym w ->
+  LLVMPtr sym w ->
+  IO (Pred sym)
+ptrSameAlloc sym (LLVMPointer base1 _off1) (LLVMPointer base2 _off2) =
+  natEq sym base1 base2
+
 -- | Test whether two pointers are equal.
 ptrEq :: (1 <= w, IsSymInterface sym)
       => sym
@@ -368,6 +392,20 @@ ptrSub sym _w (LLVMPointer base off1) off2 =
   do diff <- bvSub sym off1 off2
      return (LLVMPointer base diff)
 
+-- | Test if a pointer value is a bitvector (i.e., has a block number of 0)
+--
+-- Using this function is preferred to pattern matching on 'LLVMPointer' or
+-- 'llvmPointerBlock', because it operates at a higher level of abstraction
+-- (i.e., if the representation of pointers were changed, it could continue to
+-- work as intended).
+ptrIsBv ::
+  IsSymInterface sym =>
+  sym ->
+  LLVMPtr sym w ->
+  IO (Pred sym)
+ptrIsBv sym (LLVMPointer blk _off) =
+  natEq sym blk =<< natLit sym 0
+
 -- | Test if a pointer value is the null pointer.
 ptrIsNull :: (1 <= w, IsSymInterface sym)
           => sym

crucible-llvm/src/Lang/Crucible/LLVM/SimpleLoopInvariant.hs

@@ -518,7 +518,7 @@ safeBVLoad sym mem ptr st def align =
        C.Err _ -> return def
        C.NoErr p v ->
          do v' <- C.unpackMemValue sym (C.LLVMPointerRepr w) v
-            p0 <- W4.natEq sym (C.llvmPointerBlock v') =<< W4.natLit sym 0
+            p0 <- C.ptrIsBv sym v'
             p' <- W4.andPred sym p p0
             W4.bvIte sym p' (C.llvmPointerOffset v') def