crucible-llvm-syntax: Syntax for all LLVM expressions

crucible-llvm-syntax/README.md

@@ -11,6 +11,9 @@ This `ParserHooks` supports the following types and statements:
 
 **Statements**:
 
-- `null : Ptr n` is the null pointer, i.e. the pointer with both block number and offset concretely set to zero. The width of the null pointer is determined by the `?ptrWidth` implicit parameter used when constructing the `ParserHooks`
+- `ptr : Nat -> Bitvector w -> Ptr w`: construct a pointer from a block and offset
+- `ptr-block : Ptr w -> Nat`: get the block number of a pointer
+- `ptr-offset : Ptr w -> Bitvector w`: get the offset of a pointer
+- `ptr-ite : Bool -> Ptr w -> Ptr w -> Ptr w`: if-then-else for pointers
 
 [syn]: ../crucible-syntax

crucible-llvm-syntax/crucible-llvm-syntax.cabal

@@ -91,7 +91,6 @@ library
 
   build-depends:
     base >= 4.13,
-    bv-sized,
     crucible >= 0.1,
     crucible-llvm,
     crucible-syntax,

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

@@ -7,7 +7,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 
-module Lang.Crucible.LLVM.Syntax where
+module Lang.Crucible.LLVM.Syntax (llvmParserHooks) where
 
 import Control.Applicative (empty)
 import Control.Monad (unless)
@@ -16,8 +16,7 @@ import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
 
-import Data.BitVector.Sized qualified as BV
-
+import Data.Parameterized.Context qualified as Ctx
 import Data.Parameterized.Some (Some(..))
 
 import What4.ProgramLoc (Posd(..))
@@ -80,10 +79,40 @@ llvmAtomParser ::
 llvmAtomParser _mvar =
   Parse.depCons Parse.atomName $
     \case
-      Atom.AtomName "null" -> do
+      Atom.AtomName "ptr" -> do
+        loc <- Parse.position
+        Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
+          assign <- Parse.operands (Ctx.Empty Ctx.:> NatRepr Ctx.:> BVRepr w)
+          let (rest, off) = Ctx.decompose assign
+          let (Ctx.Empty, blk) = Ctx.decompose rest
+          let expr = Ext.LLVM_PointerExpr w blk off
+          ptrAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
+          return (Some ptrAtom)
+
+      Atom.AtomName "ptr-block" -> do
+        loc <- Parse.position
+        Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
+          assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr w)
+          let (Ctx.Empty, ptr) = Ctx.decompose assign
+          let expr = Ext.LLVM_PointerBlock w ptr
+          Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
+
+      Atom.AtomName "ptr-offset" -> do
+        loc <- Parse.position
+        Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
+          assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr w)
+          let (Ctx.Empty, ptr) = Ctx.decompose assign
+          let expr = Ext.LLVM_PointerOffset w ptr
+          Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
+
+      Atom.AtomName "ptr-ite" -> do
         loc <- Parse.position
-        blkAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.NatLit 0))
-        offAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.BVLit ?ptrWidth (BV.zero ?ptrWidth)))
-        ptrAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp (Ext.LLVM_PointerExpr ?ptrWidth blkAtom offAtom)))
-        return (Some ptrAtom)
+        Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
+          assign <- Parse.operands (Ctx.Empty Ctx.:> BoolRepr Ctx.:> LLVMPointerRepr w Ctx.:> LLVMPointerRepr w)
+          let (rest, p2) = Ctx.decompose assign
+          let (rest', p1) = Ctx.decompose rest
+          let (Ctx.Empty, b) = Ctx.decompose rest'
+          let expr = Ext.LLVM_PointerIte w b p1 p2
+          Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
+
       _ -> empty

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

@@ -1,4 +1,10 @@
 (defun @test-ptr () (Ptr 64)
   (start start:
-    (let n (null))
-    (return n)))
+    (let blk0 (fresh Nat))
+    (let off0 (bv 64 0))
+    (let p (ptr blk0 off0))
+    (let blk (ptr-blk p))
+    (let off (ptr-off p))
+    (assert! (equal? blk0 blk) "block numbers equal")
+    (assert! (equal? off0 off) "offsets equal")
+    (return p)))

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

@@ -1,14 +1,12 @@
 (defun @test-ptr () (Ptr 64)
-   (start start: (let n (null)) (return n)))
+   (start start:
+      (let blk0 (fresh Nat))
+      (let off0 (bv 64 0))
+      (let p (ptr blk0 off0))
+      (let blk (ptr-blk p))
+      (let off (ptr-off p))
+      (assert! (equal? blk0 blk) "block numbers equal")
+      (assert! (equal? off0 off) "offsets equal")
+      (return p)))
 
-test-ptr
-%0
-  % 3:12
-  $0 = natLit(0)
-  % 3:12
-  $1 = bVLit(64, BV 0)
-  % 3:12
-  $2 = extensionApp(pointerExpr $0 $1)
-  % 4:5
-  return $2
-  % no postdom
+At test-data/ptr.cbl:5:17, expected natural literal but got blk0