macaw-aarch32-syntax: Syntactic sugar for for AArch32 CFGs

2024-11-22 05:45:51 +03:00 · 2024-11-19 13:11:04 -05:00 · 2024-11-19 13:11:04 -05:00 · 54e587a2a3
commit 54e587a2a3
parent d7470c1d6c
11 changed files with 679 additions and 0 deletions
--- a/cabal.project.dist
+++ b/cabal.project.dist
@ -1,6 +1,7 @@
 packages: base/
          macaw-aarch32/
          macaw-aarch32-symbolic/
+          macaw-aarch32-syntax/
          macaw-dump/
          macaw-semmc/
          macaw-ppc/
--- a/macaw-aarch32-syntax/LICENSE
+++ b/macaw-aarch32-syntax/LICENSE
@ -0,0 +1,30 @@
+Copyright (c) 2024 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * Neither the name of Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
--- a/macaw-aarch32-syntax/README.md
+++ b/macaw-aarch32-syntax/README.md
@ -0,0 +1,70 @@
+# macaw-aarch32-syntax
+
+This package provides concrete syntax for macaw-aarch32-symbolic types and
+operations.
+
+Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn].
+This `ParserHooks` supports the following types and operations:
+
+**Types**:
+
+- `AArch32Regs`: the struct of all AArch32 registers
+
+**Operations**:
+
+- `get-reg :: AArch32Reg -> AArch32Regs -> t`: extract an x86 register
+- `set-reg :: AArch32Reg -> t -> AArch32Regs -> AArch32Regs`: set an x86 register
+- Registers:
+  - `r0 :: AArch32Reg`
+  - `r1 :: AArch32Reg`
+  - `r2 :: AArch32Reg`
+  - `r3 :: AArch32Reg`
+  - `r4 :: AArch32Reg`
+  - `r5 :: AArch32Reg`
+  - `r6 :: AArch32Reg`
+  - `r7 :: AArch32Reg`
+  - `r8 :: AArch32Reg`
+  - `r9 :: AArch32Reg`
+  - `r10 :: AArch32Reg`
+  - `r11 :: AArch32Reg`, AKA `fp`
+  - `fp :: AArch32Reg`, AKA `r11`
+  - `r12 :: AArch32Reg`, AKA `ip`
+  - `ip :: AArch32Reg`, AKA `r12`
+  - `r13 :: AArch32Reg`, AKA `sp`
+  - `sp :: AArch32Reg`, AKA `r13`
+  - `r14 :: AArch32Reg`, AKA `lr`
+  - `lr :: AArch32Reg`, AKA `r14`
+  - `v0 :: AArch32Reg`
+  - `v1 :: AArch32Reg`
+  - `v2 :: AArch32Reg`
+  - `v3 :: AArch32Reg`
+  - `v4 :: AArch32Reg`
+  - `v5 :: AArch32Reg`
+  - `v6 :: AArch32Reg`
+  - `v7 :: AArch32Reg`
+  - `v8 :: AArch32Reg`
+  - `v9 :: AArch32Reg`
+  - `v10 :: AArch32Reg`
+  - `v11 :: AArch32Reg`
+  - `v12 :: AArch32Reg`
+  - `v13 :: AArch32Reg`
+  - `v14 :: AArch32Reg`
+  - `v15 :: AArch32Reg`
+  - `v16 :: AArch32Reg`
+  - `v17 :: AArch32Reg`
+  - `v18 :: AArch32Reg`
+  - `v19 :: AArch32Reg`
+  - `v20 :: AArch32Reg`
+  - `v21 :: AArch32Reg`
+  - `v22 :: AArch32Reg`
+  - `v23 :: AArch32Reg`
+  - `v24 :: AArch32Reg`
+  - `v25 :: AArch32Reg`
+  - `v26 :: AArch32Reg`
+  - `v27 :: AArch32Reg`
+  - `v28 :: AArch32Reg`
+  - `v29 :: AArch32Reg`
+  - `v30 :: AArch32Reg`
+  - `v31 :: AArch32Reg`
+
+[syn]: https://github.com/GaloisInc/crucible/tree/master/crucible-syntax
--- a/macaw-aarch32-syntax/macaw-aarch32-syntax.cabal
+++ b/macaw-aarch32-syntax/macaw-aarch32-syntax.cabal
@ -0,0 +1,127 @@
+Cabal-version: 2.2
+Name:          macaw-aarch32-syntax
+Version:       0.1
+Author:        Galois Inc.
+Maintainer:    langston@galois.com
+Build-type:    Simple
+License:       BSD-3-Clause
+License-file:  LICENSE
+Category:      Language
+Synopsis:      A syntax for macaw-aarch32-symbolic control-flow graphs
+-- Description:
+
+extra-doc-files: README.md
+extra-source-files:
+  test-data/*.cbl
+  test-data/*.out.good
+
+common shared
+  -- Specifying -Wall and -Werror can cause the project to fail to build on
+  -- newer versions of GHC simply due to new warnings being added to -Wall. To
+  -- prevent this from happening we manually list which warnings should be
+  -- considered errors. We also list some warnings that are not in -Wall, though
+  -- try to avoid "opinionated" warnings (though this judgement is clearly
+  -- subjective).
+  --
+  -- Warnings are grouped by the GHC version that introduced them, and then
+  -- alphabetically.
+  --
+  -- A list of warnings and the GHC version in which they were introduced is
+  -- available here:
+  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html
+
+  -- Since GHC 9.4 or earlier:
+  ghc-options:
+    -Wall
+    -Werror=ambiguous-fields
+    -Werror=compat-unqualified-imports
+    -Werror=deferred-type-errors
+    -Werror=deprecated-flags
+    -Werror=deprecations
+    -Werror=deriving-defaults
+    -Werror=dodgy-foreign-imports
+    -Werror=duplicate-exports
+    -Werror=empty-enumerations
+    -Werror=forall-identifier
+    -Werror=identities
+    -Werror=inaccessible-code
+    -Werror=incomplete-patterns
+    -Werror=incomplete-record-updates
+    -Werror=incomplete-uni-patterns
+    -Werror=inline-rule-shadowing
+    -Werror=misplaced-pragmas
+    -Werror=missed-extra-shared-lib
+    -Werror=missing-exported-signatures
+    -Werror=missing-fields
+    -Werror=missing-home-modules
+    -Werror=missing-methods
+    -Werror=operator-whitespace
+    -Werror=operator-whitespace-ext-conflict
+    -Werror=overflowed-literals
+    -Werror=overlapping-patterns
+    -Werror=partial-fields
+    -Werror=partial-type-signatures
+    -Werror=redundant-bang-patterns
+    -Werror=redundant-strictness-flags
+    -Werror=simplifiable-class-constraints
+    -Werror=star-binder
+    -Werror=star-is-type
+    -Werror=tabs
+    -Werror=typed-holes
+    -Werror=type-equality-out-of-scope
+    -Werror=type-equality-requires-operators
+    -Werror=unrecognised-pragmas
+    -Werror=unrecognised-warning-flags
+    -Werror=unsupported-calling-conventions
+    -Werror=unsupported-llvm-version
+    -Werror=unticked-promoted-constructors
+    -Werror=unused-imports
+    -Werror=warnings-deprecations
+    -Werror=wrong-do-bind
+
+  ghc-prof-options: -O2 -fprof-auto-top
+  default-language: Haskell2010
+
+library
+  import: shared
+
+  build-depends:
+    base >= 4.13,
+    containers,
+    crucible,
+    crucible-syntax,
+    macaw-aarch32,
+    macaw-aarch32-symbolic,
+    macaw-base,
+    macaw-symbolic,
+    mtl,
+    parameterized-utils,
+    text,
+    what4,
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Data.Macaw.AArch32.Symbolic.Syntax
+
+test-suite macaw-aarch32-syntax-tests
+  import: shared
+  type: exitcode-stdio-1.0
+  main-is: Test.hs
+  hs-source-dirs: test
+  build-depends:
+    base,
+    containers,
+    crucible >= 0.1,
+    crucible-syntax,
+    crucible-llvm-syntax,
+    filepath,
+    macaw-aarch32,
+    macaw-aarch32-symbolic,
+    macaw-aarch32-syntax,
+    macaw-symbolic,
+    macaw-symbolic-syntax,
+    parameterized-utils >= 0.1.7,
+    tasty,
+    tasty-golden,
+    text,
--- a/macaw-aarch32-syntax/src/Data/Macaw/AArch32/Symbolic/Syntax.hs
+++ b/macaw-aarch32-syntax/src/Data/Macaw/AArch32/Symbolic/Syntax.hs
@ -0,0 +1,175 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+-- | 'LCSC.ParserHooks' for parsing macaw-aarch32-symbolic CFGs.
+module Data.Macaw.AArch32.Symbolic.Syntax
+  ( aarch32ParserHooks
+    -- * Types
+  , aarch32TypeParser
+    -- * Operations
+  , parseRegs
+  , parseReg
+  , aarch32AtomParser
+  ) where
+
+import Control.Applicative ( empty )
+import Control.Monad qualified as Monad
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.State.Strict (MonadState)
+import Control.Monad.Writer.Strict (MonadWriter)
+import Data.Text qualified as Text
+
+import Data.Macaw.Symbolic qualified as DMS
+import Data.Macaw.ARM qualified as ARM
+import Data.Macaw.AArch32.Symbolic qualified as AArch32
+import Data.Macaw.AArch32.Symbolic.Regs qualified as AArch32R
+import Data.Parameterized.Context qualified as Ctx
+import Data.Parameterized.Some (Some(..))
+import Lang.Crucible.CFG.Expr as Expr
+import Lang.Crucible.CFG.Reg (Atom, Stmt)
+import Lang.Crucible.CFG.Reg qualified as Reg
+import Lang.Crucible.Syntax.Atoms qualified as LCSA
+import Lang.Crucible.Syntax.Concrete qualified as LCSC
+import Lang.Crucible.Syntax.Monad qualified as LCSM
+import Lang.Crucible.Types qualified as LCT
+import What4.ProgramLoc (Posd(..))
+
+-- | Parser hooks for macaw-aarch32-symbolic CFGs
+aarch32ParserHooks :: LCSC.ParserHooks ext
+aarch32ParserHooks =
+  LCSC.ParserHooks
+  { LCSC.extensionTypeParser = aarch32TypeParser
+  , LCSC.extensionParser = aarch32AtomParser
+  }
+
+---------------------------------------------------------------------
+-- Types
+
+-- Helper, not exported
+namedAtom :: LCSM.MonadSyntax LCSA.Atomic m => Text.Text -> m ()
+namedAtom expectName = do
+  name <- LCSC.atomName
+  Monad.unless (name == LCSA.AtomName expectName) LCSM.cut
+
+-- Helper, not exported
+aarch32RegTypes :: Ctx.Assignment LCT.TypeRepr (DMS.MacawCrucibleRegTypes ARM.ARM)
+aarch32RegTypes = DMS.crucArchRegTypes AArch32.aarch32MacawSymbolicFns
+
+-- Helper, not exported
+aarch32RegStructType :: LCT.TypeRepr (DMS.ArchRegStruct ARM.ARM)
+aarch32RegStructType = LCT.StructRepr aarch32RegTypes
+
+-- | Parser for type extensions to Crucible syntax
+aarch32TypeParser ::
+  LCSM.MonadSyntax LCSA.Atomic m =>
+  m (Some LCT.TypeRepr)
+aarch32TypeParser = do
+  namedAtom "AArch32Regs"
+  pure (Some aarch32RegStructType)
+
+---------------------------------------------------------------------
+-- Operations
+
+parseRegs ::
+  ( LCSM.MonadSyntax LCSA.Atomic m
+  , MonadIO m
+  , MonadState (LCSC.SyntaxState s) m
+  , MonadWriter [Posd (Stmt ext s)] m
+  , IsSyntaxExtension ext
+  , ?parserHooks :: LCSC.ParserHooks ext
+  ) =>
+  m (Atom s (DMS.ArchRegStruct ARM.ARM))
+parseRegs =
+  LCSM.describe "a struct of AArch32 register values" $ do
+    assign <- LCSC.operands (Ctx.Empty Ctx.:> aarch32RegStructType)
+    pure (assign Ctx.! Ctx.baseIndex)
+
+parseReg :: LCSM.MonadSyntax LCSA.Atomic m => m (Some (Ctx.Index (DMS.MacawCrucibleRegTypes ARM.ARM)))
+parseReg =
+  LCSM.describe "an AArch32 register" $ do
+    name <- LCSC.atomName
+    case name of
+      LCSA.AtomName "r0" -> pure (Some AArch32R.r0)
+      LCSA.AtomName "r1" -> pure (Some AArch32R.r1)
+      LCSA.AtomName "r2" -> pure (Some AArch32R.r2)
+      LCSA.AtomName "r3" -> pure (Some AArch32R.r3)
+      LCSA.AtomName "r4" -> pure (Some AArch32R.r4)
+      LCSA.AtomName "r5" -> pure (Some AArch32R.r5)
+      LCSA.AtomName "r6" -> pure (Some AArch32R.r6)
+      LCSA.AtomName "r7" -> pure (Some AArch32R.r7)
+      LCSA.AtomName "r8" -> pure (Some AArch32R.r8)
+      LCSA.AtomName "r9" -> pure (Some AArch32R.r9)
+      LCSA.AtomName "r10" -> pure (Some AArch32R.r10)
+      LCSA.AtomName "r11" -> pure (Some AArch32R.r11)
+      LCSA.AtomName "fp" -> pure (Some AArch32R.fp)
+      LCSA.AtomName "r12" -> pure (Some AArch32R.r12)
+      LCSA.AtomName "ip" -> pure (Some AArch32R.ip)
+      LCSA.AtomName "r13" -> pure (Some AArch32R.r13)
+      LCSA.AtomName "sp" -> pure (Some AArch32R.sp)
+      LCSA.AtomName "r14" -> pure (Some AArch32R.r14)
+      LCSA.AtomName "lr" -> pure (Some AArch32R.lr)
+      LCSA.AtomName "v0" -> pure (Some AArch32R.v0)
+      LCSA.AtomName "v1" -> pure (Some AArch32R.v1)
+      LCSA.AtomName "v2" -> pure (Some AArch32R.v2)
+      LCSA.AtomName "v3" -> pure (Some AArch32R.v3)
+      LCSA.AtomName "v4" -> pure (Some AArch32R.v4)
+      LCSA.AtomName "v5" -> pure (Some AArch32R.v5)
+      LCSA.AtomName "v6" -> pure (Some AArch32R.v6)
+      LCSA.AtomName "v7" -> pure (Some AArch32R.v7)
+      LCSA.AtomName "v8" -> pure (Some AArch32R.v8)
+      LCSA.AtomName "v9" -> pure (Some AArch32R.v9)
+      LCSA.AtomName "v10" -> pure (Some AArch32R.v10)
+      LCSA.AtomName "v11" -> pure (Some AArch32R.v11)
+      LCSA.AtomName "v12" -> pure (Some AArch32R.v12)
+      LCSA.AtomName "v13" -> pure (Some AArch32R.v13)
+      LCSA.AtomName "v14" -> pure (Some AArch32R.v14)
+      LCSA.AtomName "v15" -> pure (Some AArch32R.v15)
+      LCSA.AtomName "v16" -> pure (Some AArch32R.v16)
+      LCSA.AtomName "v17" -> pure (Some AArch32R.v17)
+      LCSA.AtomName "v18" -> pure (Some AArch32R.v18)
+      LCSA.AtomName "v19" -> pure (Some AArch32R.v19)
+      LCSA.AtomName "v20" -> pure (Some AArch32R.v20)
+      LCSA.AtomName "v21" -> pure (Some AArch32R.v21)
+      LCSA.AtomName "v22" -> pure (Some AArch32R.v22)
+      LCSA.AtomName "v23" -> pure (Some AArch32R.v23)
+      LCSA.AtomName "v24" -> pure (Some AArch32R.v24)
+      LCSA.AtomName "v25" -> pure (Some AArch32R.v25)
+      LCSA.AtomName "v26" -> pure (Some AArch32R.v26)
+      LCSA.AtomName "v27" -> pure (Some AArch32R.v27)
+      LCSA.AtomName "v28" -> pure (Some AArch32R.v28)
+      LCSA.AtomName "v29" -> pure (Some AArch32R.v29)
+      LCSA.AtomName "v30" -> pure (Some AArch32R.v30)
+      LCSA.AtomName "v31" -> pure (Some AArch32R.v31)
+      LCSA.AtomName _ -> empty
+
+aarch32AtomParser ::
+  ( LCSM.MonadSyntax LCSA.Atomic m
+  , MonadIO m
+  , MonadState (LCSC.SyntaxState s) m
+  , MonadWriter [Posd (Stmt ext s)] m
+  , IsSyntaxExtension ext
+  , ?parserHooks :: LCSC.ParserHooks ext
+  ) =>
+  m (Some (Atom s))
+aarch32AtomParser =
+  LCSM.depCons LCSC.atomName $
+    \case
+      LCSA.AtomName "get-reg" -> do
+        loc <- LCSM.position
+        (Some reg, regs) <- LCSM.cons parseReg parseRegs
+        let regTy = aarch32RegTypes Ctx.! reg
+        Some <$> LCSC.freshAtom loc (Reg.EvalApp (Expr.GetStruct regs reg regTy))
+      LCSA.AtomName "set-reg" -> do
+        loc <- LCSM.position
+        LCSM.depCons parseReg $ \(Some reg) -> do
+          let regTy = aarch32RegTypes Ctx.! reg
+          assign <- LCSC.operands (Ctx.Empty Ctx.:> regTy Ctx.:> aarch32RegStructType)
+          let (rest, regs) = Ctx.decompose assign
+          let (Ctx.Empty, val) = Ctx.decompose rest
+          Some <$> LCSC.freshAtom loc (Reg.EvalApp (Expr.SetStruct aarch32RegTypes regs reg val))
+      LCSA.AtomName _ -> empty
--- a/macaw-aarch32-syntax/test-data/.gitignore
+++ b/macaw-aarch32-syntax/test-data/.gitignore
@ -0,0 +1 @@
+*.out
--- a/macaw-aarch32-syntax/test-data/get-regs.cbl
+++ b/macaw-aarch32-syntax/test-data/get-regs.cbl
@ -0,0 +1,54 @@
+(defun @id ((regs AArch32Regs)) AArch32Regs
+  (start start:
+    (let r0 (get-reg r0 regs))
+    (let r1 (get-reg r1 regs))
+    (let r2 (get-reg r2 regs))
+    (let r3 (get-reg r3 regs))
+    (let r4 (get-reg r4 regs))
+    (let r5 (get-reg r5 regs))
+    (let r6 (get-reg r6 regs))
+    (let r7 (get-reg r7 regs))
+    (let r8 (get-reg r8 regs))
+    (let r9 (get-reg r9 regs))
+    (let r10 (get-reg r10 regs))
+    (let r11 (get-reg r11 regs))
+    (let fp (get-reg fp regs))
+    (let r12 (get-reg r12 regs))
+    (let ip (get-reg ip regs))
+    (let r13 (get-reg r13 regs))
+    (let sp (get-reg sp regs))
+    (let r14 (get-reg r14 regs))
+    (let lr (get-reg lr regs))
+    (let v0 (get-reg v0 regs))
+    (let v1 (get-reg v1 regs))
+    (let v2 (get-reg v2 regs))
+    (let v3 (get-reg v3 regs))
+    (let v4 (get-reg v4 regs))
+    (let v5 (get-reg v5 regs))
+    (let v6 (get-reg v6 regs))
+    (let v7 (get-reg v7 regs))
+    (let v8 (get-reg v8 regs))
+    (let v9 (get-reg v9 regs))
+    (let v10 (get-reg v10 regs))
+    (let v11 (get-reg v11 regs))
+    (let v12 (get-reg v12 regs))
+    (let v13 (get-reg v13 regs))
+    (let v14 (get-reg v14 regs))
+    (let v15 (get-reg v15 regs))
+    (let v16 (get-reg v16 regs))
+    (let v17 (get-reg v17 regs))
+    (let v18 (get-reg v18 regs))
+    (let v19 (get-reg v19 regs))
+    (let v20 (get-reg v20 regs))
+    (let v21 (get-reg v21 regs))
+    (let v22 (get-reg v22 regs))
+    (let v23 (get-reg v23 regs))
+    (let v24 (get-reg v24 regs))
+    (let v25 (get-reg v25 regs))
+    (let v26 (get-reg v26 regs))
+    (let v27 (get-reg v27 regs))
+    (let v28 (get-reg v28 regs))
+    (let v29 (get-reg v29 regs))
+    (let v30 (get-reg v30 regs))
+    (let v31 (get-reg v31 regs))
+    (return regs)))
--- a/macaw-aarch32-syntax/test-data/get-regs.out.good
+++ b/macaw-aarch32-syntax/test-data/get-regs.out.good
@ -0,0 +1,154 @@
+(defun @id ((regs AArch32Regs)) AArch32Regs
+   (start start:
+      (let r0 (get-reg r0 regs))
+      (let r1 (get-reg r1 regs))
+      (let r2 (get-reg r2 regs))
+      (let r3 (get-reg r3 regs))
+      (let r4 (get-reg r4 regs))
+      (let r5 (get-reg r5 regs))
+      (let r6 (get-reg r6 regs))
+      (let r7 (get-reg r7 regs))
+      (let r8 (get-reg r8 regs))
+      (let r9 (get-reg r9 regs))
+      (let r10 (get-reg r10 regs))
+      (let r11 (get-reg r11 regs))
+      (let fp (get-reg fp regs))
+      (let r12 (get-reg r12 regs))
+      (let ip (get-reg ip regs))
+      (let r13 (get-reg r13 regs))
+      (let sp (get-reg sp regs))
+      (let r14 (get-reg r14 regs))
+      (let lr (get-reg lr regs))
+      (let v0 (get-reg v0 regs))
+      (let v1 (get-reg v1 regs))
+      (let v2 (get-reg v2 regs))
+      (let v3 (get-reg v3 regs))
+      (let v4 (get-reg v4 regs))
+      (let v5 (get-reg v5 regs))
+      (let v6 (get-reg v6 regs))
+      (let v7 (get-reg v7 regs))
+      (let v8 (get-reg v8 regs))
+      (let v9 (get-reg v9 regs))
+      (let v10 (get-reg v10 regs))
+      (let v11 (get-reg v11 regs))
+      (let v12 (get-reg v12 regs))
+      (let v13 (get-reg v13 regs))
+      (let v14 (get-reg v14 regs))
+      (let v15 (get-reg v15 regs))
+      (let v16 (get-reg v16 regs))
+      (let v17 (get-reg v17 regs))
+      (let v18 (get-reg v18 regs))
+      (let v19 (get-reg v19 regs))
+      (let v20 (get-reg v20 regs))
+      (let v21 (get-reg v21 regs))
+      (let v22 (get-reg v22 regs))
+      (let v23 (get-reg v23 regs))
+      (let v24 (get-reg v24 regs))
+      (let v25 (get-reg v25 regs))
+      (let v26 (get-reg v26 regs))
+      (let v27 (get-reg v27 regs))
+      (let v28 (get-reg v28 regs))
+      (let v29 (get-reg v29 regs))
+      (let v30 (get-reg v30 regs))
+      (let v31 (get-reg v31 regs))
+      (return regs)))
+
+id
+%0
+  % 3:13
+  $1 = getStruct($0, 36, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 4:13
+  $2 = getStruct($0, 37, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 5:13
+  $3 = getStruct($0, 38, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 6:13
+  $4 = getStruct($0, 39, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 7:13
+  $5 = getStruct($0, 40, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 8:13
+  $6 = getStruct($0, 41, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 9:13
+  $7 = getStruct($0, 42, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 10:13
+  $8 = getStruct($0, 43, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 11:13
+  $9 = getStruct($0, 44, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 12:13
+  $10 = getStruct($0, 45, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 13:14
+  $11 = getStruct($0, 46, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 14:14
+  $12 = getStruct($0, 47, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 16:14
+  $13 = getStruct($0, 48, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 18:14
+  $14 = getStruct($0, 49, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 20:14
+  $15 = getStruct($0, 50, IntrinsicRepr LLVM_pointer [BVRepr 32])
+  % 22:13
+  $16 = getStruct($0, 51, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 23:13
+  $17 = getStruct($0, 52, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 24:13
+  $18 = getStruct($0, 53, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 25:13
+  $19 = getStruct($0, 54, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 26:13
+  $20 = getStruct($0, 55, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 27:13
+  $21 = getStruct($0, 56, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 28:13
+  $22 = getStruct($0, 57, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 29:13
+  $23 = getStruct($0, 58, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 30:13
+  $24 = getStruct($0, 59, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 31:13
+  $25 = getStruct($0, 60, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 32:14
+  $26 = getStruct($0, 61, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 33:14
+  $27 = getStruct($0, 62, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 34:14
+  $28 = getStruct($0, 63, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 35:14
+  $29 = getStruct($0, 64, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 36:14
+  $30 = getStruct($0, 65, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 37:14
+  $31 = getStruct($0, 66, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 38:14
+  $32 = getStruct($0, 67, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 39:14
+  $33 = getStruct($0, 68, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 40:14
+  $34 = getStruct($0, 69, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 41:14
+  $35 = getStruct($0, 70, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 42:14
+  $36 = getStruct($0, 71, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 43:14
+  $37 = getStruct($0, 72, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 44:14
+  $38 = getStruct($0, 73, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 45:14
+  $39 = getStruct($0, 74, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 46:14
+  $40 = getStruct($0, 75, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 47:14
+  $41 = getStruct($0, 76, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 48:14
+  $42 = getStruct($0, 77, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 49:14
+  $43 = getStruct($0, 78, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 50:14
+  $44 = getStruct($0, 79, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 51:14
+  $45 = getStruct($0, 80, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 52:14
+  $46 = getStruct($0, 81, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 53:14
+  $47 = getStruct($0, 82, IntrinsicRepr LLVM_pointer [BVRepr 128])
+  % 54:5
+  return $0
+  % no postdom
--- a/macaw-aarch32-syntax/test-data/regs.cbl
+++ b/macaw-aarch32-syntax/test-data/regs.cbl
@ -0,0 +1,3 @@
+(defun @id ((regs AArch32Regs)) AArch32Regs
+  (start start:
+    (return regs)))
--- a/macaw-aarch32-syntax/test-data/regs.out.good
+++ b/macaw-aarch32-syntax/test-data/regs.out.good
@ -0,0 +1,8 @@
+(defun @id ((regs AArch32Regs)) AArch32Regs
+   (start start: (return regs)))
+
+id
+%0
+  % 3:5
+  return $0
+  % no postdom
--- a/macaw-aarch32-syntax/test/Test.hs
+++ b/macaw-aarch32-syntax/test/Test.hs
@ -0,0 +1,56 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Data.List (sort)
+import Data.Proxy (Proxy(Proxy))
+import Data.Text.IO qualified as T
+import System.FilePath
+import System.IO
+
+import Test.Tasty (defaultMain, TestTree, testGroup)
+import Test.Tasty.Golden
+
+import Lang.Crucible.Syntax.Prog (doParseCheck)
+
+import Data.Macaw.Symbolic.Syntax (machineCodeParserHooks)
+
+import Data.Macaw.ARM (ARM)
+import Data.Macaw.AArch32.Symbolic ()  -- TraversableFC instance for (MacawExt ARM) statements and expressions
+import Data.Macaw.AArch32.Symbolic.Syntax (aarch32ParserHooks)
+
+main :: IO ()
+main = do
+  parseTests <- findTests "Parse tests" "test-data" testParser
+  defaultMain $ testGroup "Tests" [parseTests]
+
+findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree
+findTests groupName testDir testAction =
+  do inputs <- findByExtension [".cbl"] testDir
+     return $ testGroup groupName
+       [ goldenFileTestCase input testAction
+       | input <- sort inputs
+       ]
+
+goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree
+goldenFileTestCase input testAction =
+  goldenVsFileDiff
+   (takeBaseName input) -- test name
+   (\x y -> ["diff", "-u", x, y])
+   goodFile -- golden file path
+   outFile
+   (testAction input outFile) -- action whose result is tested
+  where
+    outFile = replaceExtension input ".out"
+    goodFile = replaceExtension input ".out.good"
+
+testParser :: FilePath -> FilePath -> IO ()
+testParser inFile outFile =
+  do contents <- T.readFile inFile
+     let ?parserHooks = machineCodeParserHooks (Proxy @ARM) aarch32ParserHooks
+     withFile outFile WriteMode $ doParseCheck inFile contents True
+