diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md index 7bccded00..eecc9bf11 100644 --- a/crucible-llvm-syntax/README.md +++ b/crucible-llvm-syntax/README.md @@ -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` +to them. The `TypeAlias` module implements one such example, for translating +types like `Long` into `(Ptr n)` or `(Bitvector n)` for appropriate `n`. + [syn]: ../crucible-syntax diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal index aca0ae3a1..e5fa453b0 100644 --- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal +++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal @@ -93,6 +93,7 @@ library build-depends: base >= 4.13, + containers, crucible >= 0.1, crucible-llvm, crucible-syntax, @@ -106,6 +107,7 @@ library exposed-modules: Lang.Crucible.LLVM.Syntax + Lang.Crucible.LLVM.Syntax.TypeAlias test-suite crucible-llvm-syntax-tests import: shared diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs index b32e22236..6e818807c 100644 --- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs +++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs @@ -8,7 +8,8 @@ {-# LANGUAGE PatternSynonyms #-} module Lang.Crucible.LLVM.Syntax - ( llvmParserHooks + ( emptyParserHooks + , llvmParserHooks , pointerTypeParser ) where @@ -49,7 +50,11 @@ 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 -> @@ -57,10 +62,10 @@ llvmParserHooks :: ParserHooks LLVM llvmParserHooks hooks mvar = ParserHooks - { extensionTypeParser = + { extensionTypeParser = Parse.describe "LLVM type" $ Parse.call (llvmTypeParser <|> extensionTypeParser hooks) - , extensionParser = + , extensionParser = Parse.describe "LLVM operation" $ Parse.call (llvmAtomParser mvar <|> extensionParser hooks) } @@ -97,7 +102,7 @@ llvmAtomParser :: , ?parserHooks :: ParserHooks LLVM , Mem.HasPtrWidth w ) => - GlobalVar Mem -> + GlobalVar Mem -> m (Some (Atom s)) llvmAtomParser mvar = Parse.depCons Parse.atomName $ @@ -140,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)) @@ -150,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 diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs new file mode 100644 index 000000000..78f329b8b --- /dev/null +++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs @@ -0,0 +1,95 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeApplications #-} + +module Lang.Crucible.LLVM.Syntax.TypeAlias + ( 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 +-- 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 extensions to Crucible 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] + ] + +typeAliasParserHooks :: TypeLookup -> LCSC.ParserHooks ext +typeAliasParserHooks lookupFn = + LCSC.ParserHooks + { LCSC.extensionTypeParser = typeAliasParser lookupFn + , LCSC.extensionParser = empty + } diff --git a/crucible-llvm-syntax/test-data/type.cbl b/crucible-llvm-syntax/test-data/type.cbl new file mode 100644 index 000000000..85cc448e6 --- /dev/null +++ b/crucible-llvm-syntax/test-data/type.cbl @@ -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 ()))) diff --git a/crucible-llvm-syntax/test-data/type.out.good b/crucible-llvm-syntax/test-data/type.out.good new file mode 100644 index 000000000..d261613e3 --- /dev/null +++ b/crucible-llvm-syntax/test-data/type.out.good @@ -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 diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs index 507e1c6e0..8561eebb6 100644 --- a/crucible-llvm-syntax/test/Test.hs +++ b/crucible-llvm-syntax/test/Test.hs @@ -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 @@ -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 =