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 (the Nat 0))
+ (let off0 (bv 64 0))
+ (let p (ptr 64 blk0 off0))
+ (let blk (ptr-block 64 p))
+ (let off (ptr-offset 64 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,38 @@
 (defun @test-ptr () (Ptr 64)
- (start start: (let n (null)) (return n)))
+ (start start:
+ (let blk0 (the Nat 0))
+ (let off0 (bv 64 0))
+ (let p (ptr 64 blk0 off0))
+ (let blk (ptr-block 64 p))
+ (let off (ptr-offset 64 p))
+ (assert! (equal? blk0 blk) "block numbers equal")
+ (assert! (equal? off0 off) "offsets equal")
+ (return p)))
 
 test-ptr
 %0
- % 3:12
+ % 3:15
  $0 = natLit(0)
- % 3:12
+ % 4:15
  $1 = bVLit(64, BV 0)
- % 3:12
+ % 5:12
  $2 = extensionApp(pointerExpr $0 $1)
- % 4:5
+ % 6:14
+ $3 = extensionApp(pointerBlock $2)
+ % 7:14
+ $4 = extensionApp(pointerOffset $2)
+ % 8:14
+ $5 = natEq($0, $3)
+ % 8:32
+ $6 = stringLit("block numbers equal")
+ % 8:5
+ assert($5, $6)
+ % 9:14
+ $7 = baseIsEq(BaseBVRepr 64, $1, $4)
+ % 9:32
+ $8 = stringLit("offsets equal")
+ % 9:5
+ assert($7, $8)
+ % 10:5
  return $2
  % no postdom