Merge pull request #1120 from langston-barrett/lb/crucible-llvm-synta…

…x-ext

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

crucible-llvm-syntax/README.md

@@ -34,4 +34,11 @@ 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 LLVM 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 `(Bitvector n)` and `Pointer` into `(Ptr n)` for
+appropriate `n`.
+
 [syn]: ../crucible-syntax

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

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

@@ -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(..))
@@ -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)
   }
 
 ---------------------------------------------------------------------
@@ -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 $
@@ -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))
@@ -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

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

@@ -0,0 +1,112 @@
+{-
+Module           : Lang.Crucible.LLVM.Syntax.TypeAlias
+Copyright        : (c) Galois, Inc 2023
+Maintainer       : Langston Barrett <[email protected]>
+License          : BSD3
+
+This module provides facilities for parsing C-like types and translating them
+to appropriate Crucible-LLVM types, given a target triple. For example, the
+syntax @Long@ is parsed as the Crucible-LLVM 64-bit bitvector type for the
+x86_64 Linux target ('x86_64LinuxTypes'), but the 32-bit bitvector type for 
+32-bit ARM Linux targets ('aarch32LinuxTypes'). This can be useful if you want
+to write Crucible CFGs that can be simulated in the context of LLVM modules
+for several different architectures, for example if you want to override system
+calls.
+-}
+
+{-# 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 '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 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
+  }

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 ())))

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

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 =