crucible-llvm-syntax: Parse addition and subtraction of pointers

crucible-llvm-syntax/README.md

@@ -27,9 +27,11 @@ statements:
 If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral,
 
 - `ptr : Nat -> Bitvector n -> Ptr n`: construct a pointer from a block and offset
+- `ptr-add-offset : Ptr w -> Bitvector w -> Ptr w`: add an offset to a pointer
 - `ptr-block : Ptr n -> Nat`: get the block number of a pointer
 - `ptr-offset : Ptr n -> Bitvector n`: get the offset of a pointer
 - `ptr-ite : Bool -> Ptr n -> Ptr n -> Ptr n`: if-then-else for pointers
+- `ptr-sub : Ptr w -> Ptr w -> Ptr w`: subtract two pointers
 - `alloca : Alignment -> Bitvector w -> Ptr w`: allocate space on the stack
 - `load : Alignment -> LLVMType -> Ptr w -> T`: load a value from memory, where the type `T` is determined by the `LLVMType`
 - `load-handle : Type -> [Type] -> Ptr w -> T`: load a function handle from memory, where the type `T` is determined by the given return and argument types

crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs

@@ -121,6 +121,14 @@ llvmAtomParser mvar =
           ptrAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
           return (Some ptrAtom)
 
+      Atom.AtomName "ptr-add-offset" -> Parse.describe "LLVM ptr-add-offset arguments" $ do
+        loc <- Parse.position
+        assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth Ctx.:> BVRepr ?ptrWidth)
+        let (rest, bv) = Ctx.decompose assign
+        let (Ctx.Empty, ptr) = Ctx.decompose rest
+        let stmt = Ext.LLVM_PtrAddOffset ?ptrWidth mvar ptr bv
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       Atom.AtomName "ptr-block" -> Parse.describe "LLVM ptr-block arguments" $ do
         loc <- Parse.position
         Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
@@ -147,6 +155,14 @@ llvmAtomParser mvar =
           let expr = Ext.LLVM_PointerIte w b p1 p2
           Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
 
+      Atom.AtomName "ptr-sub" -> Parse.describe "LLVM ptr-sub arguments" $ do
+        loc <- Parse.position
+        assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth Ctx.:> LLVMPointerRepr ?ptrWidth)
+        let (rest, subtrahend) = Ctx.decompose assign
+        let (Ctx.Empty, minuend) = Ctx.decompose rest
+        let stmt = Ext.LLVM_PtrSubtract ?ptrWidth mvar minuend subtrahend
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       Atom.AtomName "alloca" -> Parse.describe "LLVM alloca arguments" $ do
         loc <- Parse.position
         (align, assign) <-

crucible-llvm-syntax/test-data/ptr.cbl

@@ -11,6 +11,9 @@
 
     (let sz (bv 64 1))
     (let a (alloca none sz))
+    (let b (ptr-add-offset a sz))
+    (let c (ptr-sub b a))
+
     (let vblk0 (the Nat 0))
     (let voff0 (bv 8 255))
     (let v0 (ptr 8 vblk0 voff0))

crucible-llvm-syntax/test-data/ptr.out.good

@@ -10,6 +10,8 @@
       (assert! (equal? off0 off) "offsets equal")
       (let sz (bv 64 1))
       (let a (alloca none sz))
+      (let b (ptr-add-offset a sz))
+      (let c (ptr-sub b a))
       (let vblk0 (the Nat 0))
       (let voff0 (bv 8 255))
       (let v0 (ptr 8 vblk0 voff0))
@@ -55,34 +57,38 @@ test-ptr
   $11 = bVLit(64, BV 1)
   % 13:12
   $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12
-  % 15:16
-  $13 = bVLit(8, BV 255)
-  % 16:13
-  $14 = extensionApp(pointerExpr $0 $13)
-  % 17:5
-  $15 = store crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0 $14
-  % 18:12
-  $16 = load crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0
-  % 19:15
-  $17 = extensionApp(pointerBlock $16)
-  % 20:15
-  $18 = extensionApp(pointerOffset $16)
-  % 21:14
-  $19 = natEq($0, $17)
-  % 21:34
-  $20 = stringLit("stored block numbers equal")
-  % 21:5
-  assert($19, $20)
-  % 22:14
-  $21 = baseIsEq(BaseBVRepr 8, $13, $18)
-  % 22:34
-  $22 = stringLit("stored offsets equal")
-  % 22:5
+  % 14:12
+  $13 = ptrAddOffset crucible-llvm-syntax-test-memory $12 $11
+  % 15:12
+  $14 = ptrSubtract crucible-llvm-syntax-test-memory $13 $12
+  % 18:16
+  $15 = bVLit(8, BV 255)
+  % 19:13
+  $16 = extensionApp(pointerExpr $0 $15)
+  % 20:5
+  $17 = store crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0 $16
+  % 21:12
+  $18 = load crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0
+  % 22:15
+  $19 = extensionApp(pointerBlock $18)
+  % 23:15
+  $20 = extensionApp(pointerOffset $18)
+  % 24:14
+  $21 = natEq($0, $19)
+  % 24:34
+  $22 = stringLit("stored block numbers equal")
+  % 24:5
   assert($21, $22)
-  % 24:12
-  $23 = resolveGlobal crucible-llvm-syntax-test-memory "malloc"
-  % 25:12
-  $24 = loadFunctionHandle crucible-llvm-syntax-test-memory $23 as Nothing
-  % 27:5
+  % 25:14
+  $23 = baseIsEq(BaseBVRepr 8, $15, $20)
+  % 25:34
+  $24 = stringLit("stored offsets equal")
+  % 25:5
+  assert($23, $24)
+  % 27:12
+  $25 = resolveGlobal crucible-llvm-syntax-test-memory "malloc"
+  % 28:12
+  $26 = loadFunctionHandle crucible-llvm-syntax-test-memory $25 as Nothing
+  % 30:5
   return $4
   % no postdom