Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

crucible-llvm-syntax: Make the parser extensible, introduce type aliases (e.g., long) #1120

Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions crucible-llvm-syntax/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,4 +34,10 @@ If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral,
- `load : Alignment -> LLVMType -> Ptr w -> T`: load a value from memory, where the type `T` is determined by the `LLVMType`
- `store : Alignment -> LLVMType -> Ptr w -> T -> Unit`: store a value to memory, where the type `T` is determined by the `LLVMType`

## Further extensions

The parser hooks can be further customized by passing yet another `ParserHooks`
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
to them. The `TypeAlias` module implements one such example, for translating
types like `Long` into `(Ptr n)` or `(Bitvector n)` for appropriate `n`.
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

[syn]: ../crucible-syntax
2 changes: 2 additions & 0 deletions crucible-llvm-syntax/crucible-llvm-syntax.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,7 @@ library

build-depends:
base >= 4.13,
containers,
crucible >= 0.1,
crucible-llvm,
crucible-syntax,
Expand All @@ -106,6 +107,7 @@ library

exposed-modules:
Lang.Crucible.LLVM.Syntax
Lang.Crucible.LLVM.Syntax.TypeAlias

test-suite crucible-llvm-syntax-tests
import: shared
Expand Down
29 changes: 20 additions & 9 deletions crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,12 @@
{-# LANGUAGE PatternSynonyms #-}

module Lang.Crucible.LLVM.Syntax
( llvmParserHooks
( emptyParserHooks
, llvmParserHooks
, pointerTypeParser
) where

import Control.Applicative (empty)
import Control.Applicative ((<|>), empty)
import Control.Monad (unless)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.State.Strict (MonadState(..))
Expand Down Expand Up @@ -49,14 +50,24 @@ import Lang.Crucible.Syntax.Concrete qualified as Parse
import Lang.Crucible.Syntax.ExprParse (MonadSyntax)
import Lang.Crucible.Syntax.ExprParse qualified as Parse

llvmParserHooks ::
-- | A 'ParserHooks' instance that adds no further extensions to the language.
emptyParserHooks :: ParserHooks ext
emptyParserHooks = ParserHooks empty empty

llvmParserHooks ::
Mem.HasPtrWidth w =>
-- | Hooks with which to further extend this parser
ParserHooks LLVM ->
GlobalVar Mem ->
ParserHooks LLVM
llvmParserHooks mvar =
llvmParserHooks hooks mvar =
ParserHooks
{ extensionTypeParser = llvmTypeParser
, extensionParser = llvmAtomParser mvar
{ extensionTypeParser =
Parse.describe "LLVM type" $
Parse.call (llvmTypeParser <|> extensionTypeParser hooks)
, extensionParser =
Parse.describe "LLVM operation" $
Parse.call (llvmAtomParser mvar <|> extensionParser hooks)
}

---------------------------------------------------------------------
Expand Down Expand Up @@ -91,7 +102,7 @@ llvmAtomParser ::
, ?parserHooks :: ParserHooks LLVM
, Mem.HasPtrWidth w
) =>
GlobalVar Mem ->
GlobalVar Mem ->
m (Some (Atom s))
llvmAtomParser mvar =
Parse.depCons Parse.atomName $
Expand Down Expand Up @@ -134,7 +145,7 @@ llvmAtomParser mvar =

Atom.AtomName "alloca" -> Parse.describe "LLVM alloca arguments" $ do
loc <- Parse.position
(align, assign) <-
(align, assign) <-
Parse.cons
parseAlign
(Parse.operands (Ctx.Empty Ctx.:> BVRepr ?ptrWidth))
Expand All @@ -144,7 +155,7 @@ llvmAtomParser mvar =

Atom.AtomName "load" -> Parse.describe "LLVM load arguments" $ do
loc <- Parse.position
(align, (memTy, assign)) <-
(align, (memTy, assign)) <-
Parse.cons
parseAlign
(Parse.cons
Expand Down
96 changes: 96 additions & 0 deletions crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeApplications #-}

module Lang.Crucible.LLVM.Syntax.TypeAlias
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
( TypeAlias(..)
, TypeLookup(..)
, aarch32LinuxTypes
, x86_64LinuxTypes
, typeAliasParser
, typeAliasParserHooks
) where

import Control.Applicative ( Alternative(empty) )
import qualified Data.Map as Map
import qualified Data.Text as Text

import qualified Data.Parameterized.NatRepr as PN
import Data.Parameterized.Some ( Some(..) )

import qualified Lang.Crucible.LLVM.MemModel as LCLM
import qualified Lang.Crucible.Syntax.Atoms as LCSA
import qualified Lang.Crucible.Syntax.Concrete as LCSC
import qualified Lang.Crucible.Syntax.ExprParse as LCSE
import qualified Lang.Crucible.Types as LCT

-- | Additional types beyond those built into crucible-llvm-syntax.
data TypeAlias = Byte | Int | Long | PidT | Pointer | Short | SizeT | UidT
deriving (Bounded, Enum, Eq, Show)

-- | Lookup function from a 'TypeAlias' to the underlying crucible type it
-- represents.
newtype TypeLookup = TypeLookup (TypeAlias -> (Some LCT.TypeRepr))

-- | A lookup function from 'AFE.TypeAlias' to types with the appropriate width
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved
-- on Arm32 Linux.
aarch32LinuxTypes :: TypeLookup
aarch32LinuxTypes =
TypeLookup $
\case
Byte -> Some (LCT.BVRepr (PN.knownNat @8))
Int -> Some (LCT.BVRepr (PN.knownNat @32))
Long -> Some (LCT.BVRepr (PN.knownNat @32))
PidT -> Some (LCT.BVRepr (PN.knownNat @32))
Pointer -> Some (LCLM.LLVMPointerRepr (PN.knownNat @32))
Short -> Some (LCT.BVRepr (PN.knownNat @16))
SizeT -> Some (LCT.BVRepr (PN.knownNat @32))
UidT -> Some (LCT.BVRepr (PN.knownNat @32))

-- | A lookup function from 'TypeAlias' to types with the appropriate width on
-- X86_64 Linux.
x86_64LinuxTypes :: TypeLookup
x86_64LinuxTypes =
TypeLookup $
\case
Byte -> Some (LCT.BVRepr (PN.knownNat @8))
Int -> Some (LCT.BVRepr (PN.knownNat @32))
Long -> Some (LCT.BVRepr (PN.knownNat @64))
PidT -> Some (LCT.BVRepr (PN.knownNat @32))
Pointer -> Some (LCLM.LLVMPointerRepr (PN.knownNat @64))
Short -> Some (LCT.BVRepr (PN.knownNat @16))
SizeT -> Some (LCT.BVRepr (PN.knownNat @64))
UidT -> Some (LCT.BVRepr (PN.knownNat @32))

-- | Parser for type extensions to Crucible syntax
typeMapParser ::
LCSE.MonadSyntax LCSA.Atomic m =>
-- | A mapping from type names to the crucible types they represent
Map.Map LCSA.AtomName (Some LCT.TypeRepr) ->
m (Some LCT.TypeRepr)
typeMapParser types = do
name <- LCSC.atomName
case Map.lookup name types of
Just someTypeRepr -> return someTypeRepr
Nothing -> empty

-- | Parser for type aliases for the Crucible-LLVM syntax
typeAliasParser ::
LCSE.MonadSyntax LCSA.Atomic m =>
TypeLookup ->
m (Some LCT.TypeRepr)
typeAliasParser (TypeLookup lookupFn) =
typeMapParser $
Map.fromList
[ (LCSA.AtomName (Text.pack (show t)), lookupFn t)
| t <- [minBound..maxBound]
]

-- | Parser hooks with 'LCSC.extensionTypeParser' set to 'typeAliasParser'
typeAliasParserHooks :: TypeLookup -> LCSC.ParserHooks ext
typeAliasParserHooks lookupFn =
LCSC.ParserHooks
{ LCSC.extensionTypeParser = typeAliasParser lookupFn
, LCSC.extensionParser = empty
}
13 changes: 13 additions & 0 deletions crucible-llvm-syntax/test-data/type.cbl
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
(defun @test-type () Unit
(start start:
(let byte (the Byte (bv 8 0)))
(let int (the Int (bv 32 0)))
(let long (the Long (bv 64 0)))
(let pid (the PidT (bv 32 0)))
(let blk (the Nat 0))
(let off (bv 64 0))
(let p (ptr 64 blk off))
(let ptr (the Pointer p))
(let short (the Short (bv 16 0)))
(let size (the SizeT (bv 64 0)))
(return ())))
33 changes: 33 additions & 0 deletions crucible-llvm-syntax/test-data/type.out.good
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
(defun @test-type () Unit
(start start:
(let byte (the Byte (bv 8 0)))
(let int (the Int (bv 32 0)))
(let long (the Long (bv 64 0)))
(let pid (the PidT (bv 32 0)))
(let blk (the Nat 0))
(let off (bv 64 0))
(let p (ptr 64 blk off))
(let ptr (the Pointer p))
(let short (the Short (bv 16 0)))
(let size (the SizeT (bv 64 0)))
(return ())))

test-type
%0
% 3:15
$0 = bVLit(8, BV 0)
% 4:14
$1 = bVLit(32, BV 0)
% 5:15
$2 = bVLit(64, BV 0)
% 7:14
$3 = natLit(0)
% 9:16
$4 = extensionApp(pointerExpr $3 $2)
% 11:16
$5 = bVLit(16, BV 0)
% 13:13
$6 = emptyApp()
% 13:5
return $6
% no postdom
4 changes: 3 additions & 1 deletion crucible-llvm-syntax/test/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import Lang.Crucible.Syntax.Concrete (ParserHooks)
import Lang.Crucible.Syntax.Prog (doParseCheck)

import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
import Lang.Crucible.LLVM.Syntax.TypeAlias (typeAliasParserHooks, x86_64LinuxTypes)

main :: IO ()
main = do
Expand Down Expand Up @@ -56,7 +57,8 @@ parserHooks = do
halloc <- newHandleAllocator
memVar <- mkMemVar "crucible-llvm-syntax-test-memory" halloc
let ?ptrWidth = knownNat @64
return (llvmParserHooks memVar)
let hooks = typeAliasParserHooks x86_64LinuxTypes
return (llvmParserHooks hooks memVar)

testParser :: FilePath -> FilePath -> IO ()
testParser inFile outFile =
Expand Down
Loading