From d19dd0760cdb96f3de8768e735b12ddcf1a71db6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Tue, 31 Oct 2023 15:29:16 -0400 Subject: [PATCH] crucible-llvm-syntax: Syntax for all LLVM expressions --- crucible-llvm-syntax/README.md | 5 ++- .../crucible-llvm-syntax.cabal | 1 - .../src/Lang/Crucible/LLVM/Syntax.hs | 45 +++++++++++++++---- crucible-llvm-syntax/test-data/ptr.cbl | 10 ++++- crucible-llvm-syntax/test-data/ptr.out.good | 22 +++++---- 5 files changed, 59 insertions(+), 24 deletions(-) diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md index 49f3c95ee..7e1799193 100644 --- a/crucible-llvm-syntax/README.md +++ b/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 diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal index ae426d449..b40ca3804 100644 --- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal +++ b/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, diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs index 817968cf4..dcfb09a8b 100644 --- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs +++ b/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 diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl index cd41be60d..0c5c55c74 100644 --- a/crucible-llvm-syntax/test-data/ptr.cbl +++ b/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))) diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good index 55df6b539..0fb593a25 100644 --- a/crucible-llvm-syntax/test-data/ptr.out.good +++ b/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