macaw-symbolic-syntax: Add concrete syntax for BitsToPtr and PtrToBits

Checks off two boxes in #346.
GaloisInc · Dec 2, 2024 · 4e2aa62 · 4e2aa62
1 parent 4bf0334
commit 4e2aa62
Show file tree

Hide file tree

Showing 5 changed files with 105 additions and 47 deletions.
diff --git a/symbolic-syntax/README.md b/symbolic-syntax/README.md
@@ -23,6 +23,8 @@ The extra operations are:
 - `pointer-diff :: Pointer -> Pointer -> Bitvector w` where `w` is the number of bits in a pointer (usually 32 or 64).
 - `pointer-sub :: Pointer -> Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64).
 - `pointer-eq :: Pointer -> Pointer -> Bool`.
+- `bits-to-pointer :: Bitvector w -> Pointer` where `w` is the number of bits in a pointer (usually 32 or 64). This returns a pointer with a block number of 0 and an offset equal to the bitvector argument.
+- `pointer-to-bits :: Pointer -> Bitvector w` where `w` is the number of bits in a pointer (usually 32 or 64). This returns a bitvector equal to the offset of the pointer argument. By default, this requires that the pointer argument have a block number of 0, and supplying a pointer with a non-zero block number will result in an assertion failure.
 - `pointer-read :: forall (t :: Type) -> Endianness -> Pointer -> t` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)` (for some positive number `w`) or one of the type aliases listed above.
 - `pointer-write :: forall (t :: Type) -> Endianness -> Pointer -> t -> Unit` where the first argument is the type of the value to read and the second argument is `le` or `be`. `Type` must either be `Bitvector (8 * w)` (for some positive number `w`) or one of the type aliases listed above.
 

diff --git a/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs b/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
@@ -366,6 +366,50 @@ wrapMakeNull = ExtensionWrapper
       let nullptr = DMS.MacawNullPtr (DMC.addrWidthRepr WI.knownNat) in
       return (LCCR.EvalApp (LCE.ExtensionApp nullptr)) }
 
+-- | Wrapper for the 'DMS.BitsToPtr' syntax extension that enables users to
+-- convert a bitvector to a pointer.
+--
+-- > bits-to-pointer bv
+wrapBitsToPointer
+  :: ( w ~ DMC.ArchAddrWidth arch
+     , 1 <= w
+     , KnownNat w
+     , DMC.MemWidth w )
+  => ExtensionWrapper arch
+                      (Ctx.EmptyCtx Ctx.::> LCT.BVType w)
+                      (LCLM.LLVMPointerType w)
+wrapBitsToPointer = ExtensionWrapper
+  { extName = LCSA.AtomName "bits-to-pointer"
+  , extArgTypes = Ctx.empty Ctx.:> LCT.BVRepr LCT.knownNat
+  , extWrapper = \args ->
+      let bitsToPointer =
+            LCCR.EvalApp .
+            LCE.ExtensionApp .
+            DMS.BitsToPtr WI.knownNat in
+      Ctx.uncurryAssignment (pure . bitsToPointer) args }
+
+-- | Wrapper for the 'DMS.PtrToBits' syntax extension that enables users to
+-- convert a pointer to a bitvector by extracting the pointer offset.
+--
+-- > pointer-to-bits bv
+wrapPointerToBits
+  :: ( w ~ DMC.ArchAddrWidth arch
+     , 1 <= w
+     , KnownNat w
+     , DMC.MemWidth w )
+  => ExtensionWrapper arch
+                      (Ctx.EmptyCtx Ctx.::> LCLM.LLVMPointerType w)
+                      (LCT.BVType w)
+wrapPointerToBits = ExtensionWrapper
+  { extName = LCSA.AtomName "pointer-to-bits"
+  , extArgTypes = Ctx.empty Ctx.:> LCLM.LLVMPointerRepr LCT.knownNat
+  , extWrapper = \args ->
+      let pointerToBits =
+            LCCR.EvalApp .
+            LCE.ExtensionApp .
+            DMS.PtrToBits WI.knownNat in
+      Ctx.uncurryAssignment (pure . pointerToBits) args }
+
 -- | Wrapper for the 'DMS.PtrEq' syntax extension that enables users to test
 -- the equality of two pointers.
 --
@@ -516,6 +560,8 @@ extensionWrappers = Map.fromList
   , (LCSA.AtomName "pointer-sub", SomeExtensionWrapper wrapPointerSub)
   , (LCSA.AtomName "pointer-eq", SomeExtensionWrapper wrapPointerEq)
   , (LCSA.AtomName "pointer-make-null", SomeExtensionWrapper wrapMakeNull)
+  , (LCSA.AtomName "pointer-to-bits", SomeExtensionWrapper wrapPointerToBits)
+  , (LCSA.AtomName "bits-to-pointer", SomeExtensionWrapper wrapBitsToPointer)
   ]
 
 ptrTypeParser :: LCSM.MonadSyntax LCSA.Atomic m => m (Some LCT.TypeRepr)

diff --git a/symbolic-syntax/test-data/ops.cbl b/symbolic-syntax/test-data/ops.cbl
@@ -2,11 +2,13 @@
 (defun @ops ((p Pointer) (q Pointer)) Unit
   (start start:
     (let b (bv-typed-literal SizeT 42))
+    (let bp (bits-to-pointer b))
+    (let pb (pointer-to-bits bp))
     (let n (pointer-make-null))
     (let d (pointer-diff p q))
     (let r (pointer-add p d))
 	(let s (pointer-sub r d))
 	(let e (pointer-eq s p))
     (let t (pointer-read Int le s))
     (pointer-write SizeT le s b)
-    (return ())))
+    (return ())))
diff --git a/symbolic-syntax/test-data/ops.out b/symbolic-syntax/test-data/ops.out
@@ -1,6 +1,8 @@
 (defun @ops ((p Pointer) (q Pointer)) Unit
    (start start:
       (let b (bv-typed-literal SizeT 42))
+      (let bp (bits-to-pointer b))
+      (let pb (pointer-to-bits bp))
       (let n (pointer-make-null))
       (let d (pointer-diff p q))
       (let r (pointer-add p d))
@@ -16,30 +18,32 @@ ops
   $2 = intLit(42)
   % 4:12
   $3 = integerToBV(64, $2)
-  % 5:12
-  $4 = extensionApp(null_ptr)
-  % internal
-  $5 = (ptr_sub $0 $1)
-  % 6:12
-  $6 = extensionApp((ptr_to_bits_64 $5))
-  % internal
-  $7 = extensionApp((bits_to_ptr_64 $6))
+  % 5:13
+  $4 = extensionApp((bits_to_ptr_64 $3))
+  % 6:13
+  $5 = extensionApp((ptr_to_bits_64 $4))
   % 7:12
-  $8 = (ptr_add $0 $7)
-  % 8:16
-  $9 = (ptr_sub $8 $7)
-  % 9:16
-  $10 = (ptr_eq $9 $0)
+  $6 = extensionApp(null_ptr)
+  % internal
+  $7 = (ptr_sub $0 $1)
+  % 8:12
+  $8 = extensionApp((ptr_to_bits_64 $7))
   % internal
-  $11 = (macawReadMem bvle4 $9)
-  % 10:12
-  $12 = extensionApp((ptr_to_bits_32 $11))
+  $9 = extensionApp((bits_to_ptr_64 $8))
+  % 9:12
+  $10 = (ptr_add $0 $9)
+  % 10:16
+  $11 = (ptr_sub $10 $9)
+  % 11:16
+  $12 = (ptr_eq $11 $0)
   % internal
-  $13 = extensionApp((bits_to_ptr_64 $3))
-  % 11:5
-  $14 = (macawWriteMem bvle8 $9 $13)
-  % 12:13
-  $15 = emptyApp()
-  % 12:5
-  return $15
+  $13 = (macawReadMem bvle4 $11)
+  % 12:12
+  $14 = extensionApp((ptr_to_bits_32 $13))
+  % 13:5
+  $15 = (macawWriteMem bvle8 $11 $4)
+  % 14:13
+  $16 = emptyApp()
+  % 14:5
+  return $16
   % no postdom
diff --git a/symbolic-syntax/test-data/ops.out.good b/symbolic-syntax/test-data/ops.out.good
@@ -1,6 +1,8 @@
 (defun @ops ((p Pointer) (q Pointer)) Unit
    (start start:
       (let b (bv-typed-literal SizeT 42))
+      (let bp (bits-to-pointer b))
+      (let pb (pointer-to-bits bp))
       (let n (pointer-make-null))
       (let d (pointer-diff p q))
       (let r (pointer-add p d))
@@ -16,30 +18,32 @@ ops
   $2 = intLit(42)
   % 4:12
   $3 = integerToBV(64, $2)
-  % 5:12
-  $4 = extensionApp(null_ptr)
-  % internal
-  $5 = (ptr_sub $0 $1)
-  % 6:12
-  $6 = extensionApp((ptr_to_bits_64 $5))
-  % internal
-  $7 = extensionApp((bits_to_ptr_64 $6))
+  % 5:13
+  $4 = extensionApp((bits_to_ptr_64 $3))
+  % 6:13
+  $5 = extensionApp((ptr_to_bits_64 $4))
   % 7:12
-  $8 = (ptr_add $0 $7)
-  % 8:16
-  $9 = (ptr_sub $8 $7)
-  % 9:16
-  $10 = (ptr_eq $9 $0)
+  $6 = extensionApp(null_ptr)
+  % internal
+  $7 = (ptr_sub $0 $1)
+  % 8:12
+  $8 = extensionApp((ptr_to_bits_64 $7))
   % internal
-  $11 = (macawReadMem bvle4 $9)
-  % 10:12
-  $12 = extensionApp((ptr_to_bits_32 $11))
+  $9 = extensionApp((bits_to_ptr_64 $8))
+  % 9:12
+  $10 = (ptr_add $0 $9)
+  % 10:16
+  $11 = (ptr_sub $10 $9)
+  % 11:16
+  $12 = (ptr_eq $11 $0)
   % internal
-  $13 = extensionApp((bits_to_ptr_64 $3))
-  % 11:5
-  $14 = (macawWriteMem bvle8 $9 $13)
-  % 12:13
-  $15 = emptyApp()
-  % 12:5
-  return $15
+  $13 = (macawReadMem bvle4 $11)
+  % 12:12
+  $14 = extensionApp((ptr_to_bits_32 $13))
+  % 13:5
+  $15 = (macawWriteMem bvle8 $11 $4)
+  % 14:13
+  $16 = emptyApp()
+  % 14:5
+  return $16
   % no postdom