From 5aeddebba8dc4f8d927ab74a6c880657470b652a Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 11:04:49 -0400
Subject: [PATCH 01/25] crucible-syntax: Export parsing helpers for positive
 nats

Will be helpful for crucible-llvm-syntax.
---
 crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index d21626813..eb322bbe9 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -43,6 +43,9 @@ module Lang.Crucible.Syntax.Concrete
   , string
   , isType
   , operands
+  , BoundedNat(..)
+  , PosNat
+  , posNat
   -- * Rules for pretty-printing language syntax
   , printExpr
   )

From 4aa29f4319f226e0a291384ebe35f42b7b94346d Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 11:07:33 -0400
Subject: [PATCH 02/25] crucible-syntax: Allow passing parser hooks to
 `doParseCheck`

---
 crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs | 5 +++--
 crucible-syntax/test/Tests.hs                    | 1 +
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
index da40054bc..58eb82960 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
@@ -30,6 +30,7 @@ import qualified Data.Parameterized.Context as Ctx
 import Data.Parameterized.Some (Some(Some))
 
 import qualified Lang.Crucible.CFG.Core as C
+import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import Lang.Crucible.CFG.Reg
 import Lang.Crucible.CFG.SSAConversion
 
@@ -56,7 +57,8 @@ import What4.Solver (defaultLogData, runZ3InOverride)
 
 -- | The main loop body, useful for both the program and for testing.
 doParseCheck
-   :: FilePath -- ^ The name of the input (appears in source locations)
+   :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)
+   => FilePath -- ^ The name of the input (appears in source locations)
    -> Text     -- ^ The contents of the input
    -> Bool     -- ^ Whether to pretty-print the input data as well
    -> Handle   -- ^ A handle that will receive the output
@@ -72,7 +74,6 @@ doParseCheck fn theInput pprint outh =
          do when pprint $
               forM_ v $
                 \e -> T.hPutStrLn outh (printExpr e) >> hPutStrLn outh ""
-            let ?parserHooks = defaultParserHooks
             cs <- top ng ha [] $ prog v
             case cs of
               Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
diff --git a/crucible-syntax/test/Tests.hs b/crucible-syntax/test/Tests.hs
index a5cff8ab3..f12896ca7 100644
--- a/crucible-syntax/test/Tests.hs
+++ b/crucible-syntax/test/Tests.hs
@@ -95,6 +95,7 @@ goldenFileTestCase input test_action =
 testParser :: FilePath -> FilePath -> IO ()
 testParser inFile outFile =
   do contents <- T.readFile inFile
+     let ?parserHooks = defaultParserHooks
      withFile outFile WriteMode $ doParseCheck inFile contents True
 
 testOptions :: [ConfigDesc]

From 8a351b4cb994c2c99f65f25056d27d7b09aa7b08 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 10:46:22 -0400
Subject: [PATCH 03/25] crucible-llvm-syntax: Concrete syntax for Crucible-LLVM

This commit introduces an instance of crucible-syntax's `ParserHooks` for the
LLVM language extension. It's far from optimal or complete, but later commits
can build on this foundation.
---
 .github/workflows/crux-llvm-build.yml         |  19 ++-
 .github/workflows/uc-crux-llvm-lint.yaml      |   9 +-
 cabal.project                                 |   1 +
 crucible-llvm-syntax/.hlint.yaml              |   8 ++
 crucible-llvm-syntax/LICENSE                  |  30 +++++
 .../crucible-llvm-syntax.cabal                | 124 ++++++++++++++++++
 .../src/Lang/Crucible/LLVM/Syntax.hs          |  70 ++++++++++
 crucible-llvm-syntax/test-data/.gitignore     |   1 +
 crucible-llvm-syntax/test-data/ptr.cbl        |   3 +
 crucible-llvm-syntax/test-data/ptr.out.good   |   9 ++
 crucible-llvm-syntax/test/Test.hs             |  85 ++++++++++++
 11 files changed, 351 insertions(+), 8 deletions(-)
 create mode 100644 crucible-llvm-syntax/.hlint.yaml
 create mode 100644 crucible-llvm-syntax/LICENSE
 create mode 100644 crucible-llvm-syntax/crucible-llvm-syntax.cabal
 create mode 100644 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
 create mode 100644 crucible-llvm-syntax/test-data/.gitignore
 create mode 100644 crucible-llvm-syntax/test-data/ptr.cbl
 create mode 100644 crucible-llvm-syntax/test-data/ptr.out.good
 create mode 100644 crucible-llvm-syntax/test/Test.hs

diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml
index 3a22fd5cd..c51a1f7a8 100644
--- a/.github/workflows/crux-llvm-build.yml
+++ b/.github/workflows/crux-llvm-build.yml
@@ -150,11 +150,12 @@ jobs:
           setup_src() { if [ ! -f Setup.hs ] ; then defsetup > DefSetup.hs; fi; ls *Setup.hs; }
           setup_bin() { echo setup.${{ matrix.ghc }}; }
           with_ghc()  { $NS -c ${@}; }
-          (cd crucible;      with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
-          (cd crucible-llvm; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
-          (cd crux;          with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
-          (cd crux-llvm;     with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
-          (cd uc-crux-llvm;  with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
+          (cd crucible;             with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
+          (cd crucible-llvm;        with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
+          (cd crucible-llvm-syntax; with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
+          (cd crux;                 with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
+          (cd crux-llvm;            with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
+          (cd uc-crux-llvm;         with_ghc ghc -o $(setup_bin) $(setup_src) && ./$(setup_bin) clean)
 
 
       - shell: bash
@@ -162,6 +163,7 @@ jobs:
 
       - shell: bash
         run: |
+          .github/ci.sh build lib:crucible-llvm-syntax
           .github/ci.sh build exe:crux-llvm
           .github/ci.sh build exe:crux-llvm-for-ide
           .github/ci.sh build exe:crux-llvm-svcomp
@@ -169,7 +171,7 @@ jobs:
 
       - shell: bash
         name: Haddock
-        run: cabal v2-haddock crucible-symio crucible-llvm crux-llvm uc-crux-llvm
+        run: cabal v2-haddock crucible-symio crucible-llvm{,-syntax} crux-llvm uc-crux-llvm
 
       - shell: bash
         name: Test crucible
@@ -189,6 +191,11 @@ jobs:
           LLVM_AS: "llvm-as-12"
           CLANG: "clang-12"
 
+      - shell: bash
+        name: Test crucible-llvm-syntax (Linux)
+        run: .github/ci.sh test crucible-llvm-syntax
+        if: runner.os == 'Linux'
+
       - shell: bash
         name: Test crux-llvm (Linux)
         run: .github/ci.sh test crux-llvm
diff --git a/.github/workflows/uc-crux-llvm-lint.yaml b/.github/workflows/uc-crux-llvm-lint.yaml
index 6ef5f116e..07f11280f 100644
--- a/.github/workflows/uc-crux-llvm-lint.yaml
+++ b/.github/workflows/uc-crux-llvm-lint.yaml
@@ -16,11 +16,16 @@ jobs:
 
       - shell: bash
         run: |
-          cd uc-crux-llvm/
           curl --location -o hlint.tar.gz \
             https://github.com/ndmitchell/hlint/releases/download/v3.3/hlint-3.3-x86_64-linux.tar.gz
           tar xvf hlint.tar.gz
-          ./hlint-3.3/hlint exe src test
+
+          pushd crucible-llvm-syntax/
+          ../hlint-3.3/hlint src test
+          popd
+
+          cd uc-crux-llvm/
+          ../hlint-3.3/hlint exe src test
 
       - uses: mrkkrp/ormolu-action@v2
         # This is currently disabled, since it complains about
diff --git a/cabal.project b/cabal.project
index 6be2d3c9e..4fe55bd54 100644
--- a/cabal.project
+++ b/cabal.project
@@ -9,6 +9,7 @@ packages:
   crucible-go/
   crucible-jvm/
   crucible-llvm/
+  crucible-llvm-syntax/
   crucible-mir/
   crucible-wasm/
   crucible-syntax/
diff --git a/crucible-llvm-syntax/.hlint.yaml b/crucible-llvm-syntax/.hlint.yaml
new file mode 100644
index 000000000..73c1c051f
--- /dev/null
+++ b/crucible-llvm-syntax/.hlint.yaml
@@ -0,0 +1,8 @@
+# HLint's default suggestions are opinionated, so we disable all of them by
+# default and enable just a small subset we can agree on.
+
+- ignore: {}  # ignore all
+- error: { name: "Redundant do" }
+- error: { name: "Use unless" }
+- error: { name: "Use when" }
+
diff --git a/crucible-llvm-syntax/LICENSE b/crucible-llvm-syntax/LICENSE
new file mode 100644
index 000000000..f01e82c96
--- /dev/null
+++ b/crucible-llvm-syntax/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2023 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.
diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
new file mode 100644
index 000000000..fdaee68b4
--- /dev/null
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -0,0 +1,124 @@
+Cabal-version: 2.2
+Name:          crucible-llvm-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 reading and writing Crucible-LLVM control-flow graphs
+-- Description:
+
+extra-doc-files: README.md
+extra-source-files:
+
+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 8.10 or earlier:
+  ghc-options:
+    -Wall
+    -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=identities
+    -Werror=inaccessible-code
+    -Werror=incomplete-patterns
+    -Werror=incomplete-record-updates
+    -Werror=incomplete-uni-patterns
+    -Werror=inline-rule-shadowing
+    -Werror=missed-extra-shared-lib
+    -Werror=missing-exported-signatures
+    -Werror=missing-fields
+    -Werror=missing-home-modules
+    -Werror=missing-methods
+    -Werror=overflowed-literals
+    -Werror=overlapping-patterns
+    -Werror=partial-fields
+    -Werror=partial-type-signatures
+    -Werror=simplifiable-class-constraints
+    -Werror=star-binder
+    -Werror=star-is-type
+    -Werror=tabs
+    -Werror=typed-holes
+    -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
+
+  if impl(ghc >= 9.2)
+    ghc-options:
+      -Werror=ambiguous-fields
+      -Werror=operator-whitespace
+      -Werror=operator-whitespace-ext-conflict
+      -Werror=redundant-bang-patterns
+
+  if impl(ghc >= 9.4)
+    ghc-options:
+      -Werror=forall-identifier
+      -Werror=misplaced-pragmas
+      -Werror=redundant-strictness-flags
+      -Werror=type-equality-out-of-scope
+      -Werror=type-equality-requires-operators
+  ghc-prof-options: -O2 -fprof-auto-top
+  default-language: Haskell2010
+
+library
+  import: shared
+
+  build-depends:
+    base >= 4.16,
+    crucible >= 0.1,
+    crucible-llvm,
+    crucible-syntax,
+    mtl,
+    parameterized-utils >= 0.1.7,
+    text,
+    what4,
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Lang.Crucible.LLVM.Syntax
+
+test-suite crucible-llvm-syntax-tests
+  type: exitcode-stdio-1.0
+  main-is: Test.hs
+  hs-source-dirs: test
+  build-depends:
+    base,
+    containers,
+    crucible >= 0.1,
+    crucible-llvm,
+    crucible-llvm-syntax,
+    crucible-syntax,
+    directory,
+    filepath,
+    parameterized-utils >= 0.1.7,
+    tasty,
+    tasty-golden,
+    tasty-hunit,
+    text,
+    what4,
diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
new file mode 100644
index 000000000..339cd9fdb
--- /dev/null
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Lang.Crucible.LLVM.Syntax where
+
+import Control.Monad (unless)
+import Control.Monad.IO.Class (MonadIO(..))
+import Control.Monad.State.Strict (MonadState(..))
+import Control.Monad.Writer.Strict (MonadWriter(..))
+import Data.Functor ((<&>))
+
+import Data.Parameterized.NatRepr (knownNat)
+import Data.Parameterized.Some (Some(..))
+
+import What4.ProgramLoc (Posd(..))
+
+import Lang.Crucible.CFG.Reg (Atom(..), Stmt(..))
+import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
+import Lang.Crucible.Types (TypeRepr(..))
+
+import Lang.Crucible.LLVM.Extension (LLVM)
+import Lang.Crucible.LLVM.MemModel (pattern LLVMPointerRepr)
+
+import Lang.Crucible.Syntax.Atoms (Atomic)
+import Lang.Crucible.Syntax.Concrete (ParserHooks(..), SyntaxState)
+import Lang.Crucible.Syntax.ExprParse (MonadSyntax)
+import qualified Lang.Crucible.Syntax.Concrete as Parse
+import qualified Lang.Crucible.Syntax.ExprParse as Parse
+
+unary :: MonadSyntax Atomic m => m b -> m a -> m a
+unary p0 p = Parse.followedBy p0 (Parse.commit *> Parse.cons p Parse.emptyList) <&> fst
+
+llvmParserHooks :: ParserHooks LLVM
+llvmParserHooks =
+  ParserHooks
+  { extensionTypeParser = llvmTypeParser
+  , extensionParser = llvmAtomParser
+  }
+
+llvmTypeParser :: MonadSyntax Atomic m => m (Some TypeRepr)
+llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType
+  where
+    ptrType :: MonadSyntax Atomic m => m (Some TypeRepr)
+    ptrType = do
+      let ptrName = do
+            atom <- Parse.string
+            unless (atom == "Ptr") Parse.cut
+
+      let ptrWidth = do
+            atom <- Parse.string
+            if atom == "64"
+            then pure (Some (LLVMPointerRepr (knownNat @64)))
+            else Parse.cut
+
+      unary ptrName ptrWidth
+
+llvmAtomParser ::
+  ( MonadSyntax Atomic m
+  , MonadWriter [Posd (Stmt ext s)] m
+  , MonadState (SyntaxState s) m
+  , MonadIO m
+  , IsSyntaxExtension ext
+  , ?parserHooks :: ParserHooks ext
+  ) =>
+  m (Some (Atom s))
+llvmAtomParser = Parse.cut
diff --git a/crucible-llvm-syntax/test-data/.gitignore b/crucible-llvm-syntax/test-data/.gitignore
new file mode 100644
index 000000000..f47cb2045
--- /dev/null
+++ b/crucible-llvm-syntax/test-data/.gitignore
@@ -0,0 +1 @@
+*.out
diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
new file mode 100644
index 000000000..e59a03c65
--- /dev/null
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -0,0 +1,3 @@
+(defun @test-ptr ((_ ("Ptr" "64"))) Bool
+  (start start:
+    (return #t)))
diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good
new file mode 100644
index 000000000..84cb62466
--- /dev/null
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -0,0 +1,9 @@
+(defun @test-ptr ((_ "Ptr64")) Bool (start start: (return #t)))
+
+test-ptr
+%0
+  % 3:13
+  $1 = boolLit(True)
+  % 3:5
+  return $1
+  % no postdom
diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs
new file mode 100644
index 000000000..37f05733d
--- /dev/null
+++ b/crucible-llvm-syntax/test/Test.hs
@@ -0,0 +1,85 @@
+{-# LANGUAGE ImplicitParams #-}
+
+module Main where
+
+import Control.Applicative
+import Control.Monad.IO.Class (MonadIO(..))
+import Control.Monad.ST
+
+import Data.List
+import qualified Data.Map as Map
+import Data.Map (Map)
+import Data.Monoid
+import qualified Data.Parameterized.Context as Ctx
+import Data.Parameterized.Some (Some(..))
+import Data.Text (Text)
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+
+import System.IO
+
+import Lang.Crucible.Syntax.Concrete hiding (SyntaxError)
+
+import Lang.Crucible.Backend (IsSymInterface)
+import Lang.Crucible.FunctionHandle
+import Lang.Crucible.Simulator.ExecutionTree
+import Lang.Crucible.Simulator.GlobalState (SymGlobalState, insertGlobal)
+import Lang.Crucible.Simulator.OverrideSim
+import Lang.Crucible.Syntax.Atoms (GlobalName(..))
+import Lang.Crucible.Syntax.Prog
+import Lang.Crucible.Syntax.SExpr
+import Lang.Crucible.Syntax.ExprParse
+import Lang.Crucible.Syntax.Overrides as SyntaxOvrs
+import Lang.Crucible.Types
+import Lang.Crucible.CFG.Common (GlobalVar(..))
+import Lang.Crucible.CFG.SSAConversion
+
+import Test.Tasty (defaultMain, TestTree, testGroup)
+import Test.Tasty.Golden
+import Test.Tasty.HUnit
+import System.FilePath
+import System.Directory
+
+import What4.Config
+import What4.FunctionName
+import What4.Interface (intLit)
+import What4.ProgramLoc
+import What4.Solver.Z3 (z3Options)
+
+import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
+
+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 = llvmParserHooks
+     withFile outFile WriteMode $ doParseCheck inFile contents True
+
+testOptions :: [ConfigDesc]
+testOptions = z3Options
+

From 24d5da14203507b36dd408f3ae53f800d1d4b888 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 10:54:14 -0400
Subject: [PATCH 04/25] crucible-llvm-syntax: Allow arbitrary widths in pointer
 types

---
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 11 ++++-------
 crucible-llvm-syntax/test-data/ptr.cbl                |  2 +-
 crucible-llvm-syntax/test-data/ptr.out.good           |  3 ++-
 crucible-llvm-syntax/test/Test.hs                     |  2 +-
 4 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 339cd9fdb..1ed6bae6e 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -13,7 +13,6 @@ import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
 
-import Data.Parameterized.NatRepr (knownNat)
 import Data.Parameterized.Some (Some(..))
 
 import What4.ProgramLoc (Posd(..))
@@ -47,14 +46,12 @@ llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType
     ptrType :: MonadSyntax Atomic m => m (Some TypeRepr)
     ptrType = do
       let ptrName = do
-            atom <- Parse.string
-            unless (atom == "Ptr") Parse.cut
+            s <- Parse.string
+            unless (s == "Ptr") Parse.cut
 
       let ptrWidth = do
-            atom <- Parse.string
-            if atom == "64"
-            then pure (Some (LLVMPointerRepr (knownNat @64)))
-            else Parse.cut
+            Parse.BoundedNat n <- Parse.posNat
+            pure (Some (LLVMPointerRepr n))
 
       unary ptrName ptrWidth
 
diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
index e59a03c65..9aad950fd 100644
--- a/crucible-llvm-syntax/test-data/ptr.cbl
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -1,3 +1,3 @@
-(defun @test-ptr ((_ ("Ptr" "64"))) Bool
+(defun @test-ptr ((_ ("Ptr" 64))) Bool
   (start start:
     (return #t)))
diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good
index 84cb62466..7021b002e 100644
--- a/crucible-llvm-syntax/test-data/ptr.out.good
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -1,4 +1,5 @@
-(defun @test-ptr ((_ "Ptr64")) Bool (start start: (return #t)))
+(defun @test-ptr ((_ ("Ptr" 64))) Bool
+   (start start: (return #t)))
 
 test-ptr
 %0
diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs
index 37f05733d..35c993cc4 100644
--- a/crucible-llvm-syntax/test/Test.hs
+++ b/crucible-llvm-syntax/test/Test.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE ImplicitParams #-}
 
-module Main where
+module Main (main) where
 
 import Control.Applicative
 import Control.Monad.IO.Class (MonadIO(..))

From 3367f5ba2d034d4501d7f1226f252858c02913a3 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 11:09:30 -0400
Subject: [PATCH 05/25] crucible-llvm-syntax: Remove dead code

---
 crucible-llvm-syntax/test/Test.hs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs
index 35c993cc4..451b13c43 100644
--- a/crucible-llvm-syntax/test/Test.hs
+++ b/crucible-llvm-syntax/test/Test.hs
@@ -80,6 +80,3 @@ testParser inFile outFile =
      let ?parserHooks = llvmParserHooks
      withFile outFile WriteMode $ doParseCheck inFile contents True
 
-testOptions :: [ConfigDesc]
-testOptions = z3Options
-

From 63caae5ac4ee0d6883eb435ee226796cd291da02 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 11:12:14 -0400
Subject: [PATCH 06/25] crucible-llvm-syntax: Fix warnings in test suite

---
 .../crucible-llvm-syntax.cabal                |  4 +-
 crucible-llvm-syntax/test/Test.hs             | 41 ++-----------------
 2 files changed, 4 insertions(+), 41 deletions(-)

diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
index fdaee68b4..fd564f6b9 100644
--- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -104,6 +104,7 @@ library
     Lang.Crucible.LLVM.Syntax
 
 test-suite crucible-llvm-syntax-tests
+  import: shared
   type: exitcode-stdio-1.0
   main-is: Test.hs
   hs-source-dirs: test
@@ -114,11 +115,8 @@ test-suite crucible-llvm-syntax-tests
     crucible-llvm,
     crucible-llvm-syntax,
     crucible-syntax,
-    directory,
     filepath,
     parameterized-utils >= 0.1.7,
     tasty,
     tasty-golden,
-    tasty-hunit,
     text,
-    what4,
diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs
index 451b13c43..56a7ccd26 100644
--- a/crucible-llvm-syntax/test/Test.hs
+++ b/crucible-llvm-syntax/test/Test.hs
@@ -2,50 +2,15 @@
 
 module Main (main) where
 
-import Control.Applicative
-import Control.Monad.IO.Class (MonadIO(..))
-import Control.Monad.ST
-
-import Data.List
-import qualified Data.Map as Map
-import Data.Map (Map)
-import Data.Monoid
-import qualified Data.Parameterized.Context as Ctx
-import Data.Parameterized.Some (Some(..))
-import Data.Text (Text)
-import Data.Type.Equality (TestEquality(..), (:~:)(..))
-import qualified Data.Text as T
+import Data.List (sort)
 import qualified Data.Text.IO as T
-
+import System.FilePath
 import System.IO
 
-import Lang.Crucible.Syntax.Concrete hiding (SyntaxError)
-
-import Lang.Crucible.Backend (IsSymInterface)
-import Lang.Crucible.FunctionHandle
-import Lang.Crucible.Simulator.ExecutionTree
-import Lang.Crucible.Simulator.GlobalState (SymGlobalState, insertGlobal)
-import Lang.Crucible.Simulator.OverrideSim
-import Lang.Crucible.Syntax.Atoms (GlobalName(..))
-import Lang.Crucible.Syntax.Prog
-import Lang.Crucible.Syntax.SExpr
-import Lang.Crucible.Syntax.ExprParse
-import Lang.Crucible.Syntax.Overrides as SyntaxOvrs
-import Lang.Crucible.Types
-import Lang.Crucible.CFG.Common (GlobalVar(..))
-import Lang.Crucible.CFG.SSAConversion
-
 import Test.Tasty (defaultMain, TestTree, testGroup)
 import Test.Tasty.Golden
-import Test.Tasty.HUnit
-import System.FilePath
-import System.Directory
 
-import What4.Config
-import What4.FunctionName
-import What4.Interface (intLit)
-import What4.ProgramLoc
-import What4.Solver.Z3 (z3Options)
+import Lang.Crucible.Syntax.Prog (doParseCheck)
 
 import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
 

From 1b2122a5eca8fd32e336f840c21075d7bcedfd85 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 11:19:29 -0400
Subject: [PATCH 07/25] crucible-llvm-syntax: Parse pointer type as an atom
 name, not a string

Also, use `ImportQualifiedPost` everywhere
---
 crucible-llvm-syntax/crucible-llvm-syntax.cabal       |  1 +
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 10 ++++++----
 crucible-llvm-syntax/test-data/ptr.cbl                |  2 +-
 crucible-llvm-syntax/test-data/ptr.out.good           |  3 +--
 crucible-llvm-syntax/test/Test.hs                     |  3 ++-
 5 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
index fd564f6b9..22bffe82b 100644
--- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -82,6 +82,7 @@ common shared
       -Werror=redundant-strictness-flags
       -Werror=type-equality-out-of-scope
       -Werror=type-equality-requires-operators
+
   ghc-prof-options: -O2 -fprof-auto-top
   default-language: Haskell2010
 
diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 1ed6bae6e..b8c7b783e 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeApplications #-}
@@ -25,10 +26,11 @@ import Lang.Crucible.LLVM.Extension (LLVM)
 import Lang.Crucible.LLVM.MemModel (pattern LLVMPointerRepr)
 
 import Lang.Crucible.Syntax.Atoms (Atomic)
+import Lang.Crucible.Syntax.Atoms qualified as Atom
 import Lang.Crucible.Syntax.Concrete (ParserHooks(..), SyntaxState)
+import Lang.Crucible.Syntax.Concrete qualified as Parse
 import Lang.Crucible.Syntax.ExprParse (MonadSyntax)
-import qualified Lang.Crucible.Syntax.Concrete as Parse
-import qualified Lang.Crucible.Syntax.ExprParse as Parse
+import Lang.Crucible.Syntax.ExprParse qualified as Parse
 
 unary :: MonadSyntax Atomic m => m b -> m a -> m a
 unary p0 p = Parse.followedBy p0 (Parse.commit *> Parse.cons p Parse.emptyList) <&> fst
@@ -46,8 +48,8 @@ llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType
     ptrType :: MonadSyntax Atomic m => m (Some TypeRepr)
     ptrType = do
       let ptrName = do
-            s <- Parse.string
-            unless (s == "Ptr") Parse.cut
+            s <- Parse.atomName
+            unless (s == Atom.AtomName "Ptr") Parse.cut
 
       let ptrWidth = do
             Parse.BoundedNat n <- Parse.posNat
diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
index 9aad950fd..88a812d28 100644
--- a/crucible-llvm-syntax/test-data/ptr.cbl
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -1,3 +1,3 @@
-(defun @test-ptr ((_ ("Ptr" 64))) Bool
+(defun @test-ptr ((_ (Ptr 64))) Bool
   (start start:
     (return #t)))
diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good
index 7021b002e..a446dba04 100644
--- a/crucible-llvm-syntax/test-data/ptr.out.good
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -1,5 +1,4 @@
-(defun @test-ptr ((_ ("Ptr" 64))) Bool
-   (start start: (return #t)))
+(defun @test-ptr ((_ (Ptr 64))) Bool (start start: (return #t)))
 
 test-ptr
 %0
diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs
index 56a7ccd26..cbfb6dda5 100644
--- a/crucible-llvm-syntax/test/Test.hs
+++ b/crucible-llvm-syntax/test/Test.hs
@@ -1,9 +1,10 @@
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImportQualifiedPost #-}
 
 module Main (main) where
 
 import Data.List (sort)
-import qualified Data.Text.IO as T
+import Data.Text.IO qualified as T
 import System.FilePath
 import System.IO
 

From 826112a2d5157f76ada3ee04167f4300ef9da17a Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 12:26:23 -0400
Subject: [PATCH 08/25] crucible-llvm-syntax: Add null pointer statement

Also, take an LLVM memory global variable as an argument. Not yet necessary,
but would be if we were to ever support operations like loading and storing.
---
 crucible-llvm-syntax/.hlint.yaml              |  2 +-
 .../crucible-llvm-syntax.cabal                |  3 +-
 .../src/Lang/Crucible/LLVM/Syntax.hs          | 65 +++++++++++++++----
 crucible-llvm-syntax/test-data/ptr.cbl        |  5 +-
 crucible-llvm-syntax/test-data/ptr.out.good   | 15 +++--
 crucible-llvm-syntax/test/Test.hs             | 21 +++++-
 6 files changed, 88 insertions(+), 23 deletions(-)

diff --git a/crucible-llvm-syntax/.hlint.yaml b/crucible-llvm-syntax/.hlint.yaml
index 73c1c051f..33e11424c 100644
--- a/crucible-llvm-syntax/.hlint.yaml
+++ b/crucible-llvm-syntax/.hlint.yaml
@@ -3,6 +3,6 @@
 
 - ignore: {}  # ignore all
 - error: { name: "Redundant do" }
+- error: { name: "Unused LANGUAGE pragma" }
 - error: { name: "Use unless" }
 - error: { name: "Use when" }
-
diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
index 22bffe82b..ae426d449 100644
--- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -90,7 +90,8 @@ library
   import: shared
 
   build-depends:
-    base >= 4.16,
+    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 b8c7b783e..10c4e49a2 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -1,29 +1,42 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Lang.Crucible.LLVM.Syntax where
 
+import Control.Applicative (empty)
 import Control.Monad (unless)
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
+import GHC.TypeLits (type (<=))
 
+import Data.BitVector.Sized qualified as BV
+
+import Data.Parameterized.NatRepr (NatRepr)
+import Data.Parameterized.NatRepr qualified as Nat
 import Data.Parameterized.Some (Some(..))
 
 import What4.ProgramLoc (Posd(..))
 
-import Lang.Crucible.CFG.Reg (Atom(..), Stmt(..))
+import Lang.Crucible.CFG.Expr qualified as Expr
+import Lang.Crucible.CFG.Reg (Atom, GlobalVar, Stmt)
+import Lang.Crucible.CFG.Reg qualified as Reg
 import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import Lang.Crucible.Types (TypeRepr(..))
 
 import Lang.Crucible.LLVM.Extension (LLVM)
-import Lang.Crucible.LLVM.MemModel (pattern LLVMPointerRepr)
+import Lang.Crucible.LLVM.Extension qualified as Ext
+import Lang.Crucible.LLVM.MemModel (Mem, pattern LLVMPointerRepr)
+import Lang.Crucible.LLVM.MemModel qualified as Mem
 
 import Lang.Crucible.Syntax.Atoms (Atomic)
 import Lang.Crucible.Syntax.Atoms qualified as Atom
@@ -35,11 +48,14 @@ import Lang.Crucible.Syntax.ExprParse qualified as Parse
 unary :: MonadSyntax Atomic m => m b -> m a -> m a
 unary p0 p = Parse.followedBy p0 (Parse.commit *> Parse.cons p Parse.emptyList) <&> fst
 
-llvmParserHooks :: ParserHooks LLVM
-llvmParserHooks =
+llvmParserHooks :: 
+  Mem.HasPtrWidth w =>
+  GlobalVar Mem ->
+  ParserHooks LLVM
+llvmParserHooks mvar =
   ParserHooks
   { extensionTypeParser = llvmTypeParser
-  , extensionParser = llvmAtomParser
+  , extensionParser = llvmAtomParser mvar
   }
 
 llvmTypeParser :: MonadSyntax Atomic m => m (Some TypeRepr)
@@ -50,20 +66,43 @@ llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType
       let ptrName = do
             s <- Parse.atomName
             unless (s == Atom.AtomName "Ptr") Parse.cut
+      unary ptrName $ do
+        PtrWidth w <- ptrWidth
+        return (Some (LLVMPointerRepr w))
 
-      let ptrWidth = do
-            Parse.BoundedNat n <- Parse.posNat
-            pure (Some (LLVMPointerRepr n))
+data PtrWidth =
+  forall w. (1 <= w, 16 <= w) => PtrWidth (NatRepr w)
 
-      unary ptrName ptrWidth
+ptrWidth :: MonadSyntax Atomic m => m PtrWidth
+ptrWidth =
+   do i <- Parse.sideCondition "nat literal >= 16" checkPosNat Parse.nat
+      maybe empty return $ do 
+        Some x <- return $ Nat.mkNatRepr i
+        let minPtrWidth = Nat.knownNat @16
+        Nat.LeqProof <- Nat.testLeq (Nat.knownNat @1) x
+        Nat.LeqProof <- Nat.testLeq minPtrWidth x
+        return (PtrWidth x)
+  where checkPosNat i | i > 16 = Just i
+        checkPosNat _ = Nothing
 
 llvmAtomParser ::
   ( MonadSyntax Atomic m
-  , MonadWriter [Posd (Stmt ext s)] m
+  , MonadWriter [Posd (Stmt LLVM s)] m
   , MonadState (SyntaxState s) m
   , MonadIO m
-  , IsSyntaxExtension ext
-  , ?parserHooks :: ParserHooks ext
+  , IsSyntaxExtension LLVM
+  , ?parserHooks :: ParserHooks LLVM
+  , Mem.HasPtrWidth w
   ) =>
+  GlobalVar Mem -> 
   m (Some (Atom s))
-llvmAtomParser = Parse.cut
+llvmAtomParser _mvar =
+  Parse.depCons Parse.atomName $
+    \case
+      Atom.AtomName "null" -> 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)
+      _ -> empty
diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
index 88a812d28..cd41be60d 100644
--- a/crucible-llvm-syntax/test-data/ptr.cbl
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -1,3 +1,4 @@
-(defun @test-ptr ((_ (Ptr 64))) Bool
+(defun @test-ptr () (Ptr 64)
   (start start:
-    (return #t)))
+    (let n (null))
+    (return n)))
diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good
index a446dba04..55df6b539 100644
--- a/crucible-llvm-syntax/test-data/ptr.out.good
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -1,9 +1,14 @@
-(defun @test-ptr ((_ (Ptr 64))) Bool (start start: (return #t)))
+(defun @test-ptr () (Ptr 64)
+   (start start: (let n (null)) (return n)))
 
 test-ptr
 %0
-  % 3:13
-  $1 = boolLit(True)
-  % 3:5
-  return $1
+  % 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
diff --git a/crucible-llvm-syntax/test/Test.hs b/crucible-llvm-syntax/test/Test.hs
index cbfb6dda5..507e1c6e0 100644
--- a/crucible-llvm-syntax/test/Test.hs
+++ b/crucible-llvm-syntax/test/Test.hs
@@ -1,5 +1,8 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE ImportQualifiedPost #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
 
 module Main (main) where
 
@@ -11,6 +14,14 @@ import System.IO
 import Test.Tasty (defaultMain, TestTree, testGroup)
 import Test.Tasty.Golden
 
+import Data.Parameterized.NatRepr (knownNat)
+
+import Lang.Crucible.FunctionHandle (newHandleAllocator)
+
+import Lang.Crucible.LLVM.Extension (LLVM)
+import Lang.Crucible.LLVM.MemModel (mkMemVar)
+
+import Lang.Crucible.Syntax.Concrete (ParserHooks)
 import Lang.Crucible.Syntax.Prog (doParseCheck)
 
 import Lang.Crucible.LLVM.Syntax (llvmParserHooks)
@@ -40,9 +51,17 @@ goldenFileTestCase input testAction =
     outFile = replaceExtension input ".out"
     goodFile = replaceExtension input ".out.good"
 
+parserHooks :: IO (ParserHooks LLVM)
+parserHooks = do
+  halloc <- newHandleAllocator
+  memVar <- mkMemVar "crucible-llvm-syntax-test-memory" halloc
+  let ?ptrWidth = knownNat @64
+  return (llvmParserHooks memVar)
+
 testParser :: FilePath -> FilePath -> IO ()
 testParser inFile outFile =
   do contents <- T.readFile inFile
-     let ?parserHooks = llvmParserHooks
+     hooks <- parserHooks
+     let ?parserHooks = hooks
      withFile outFile WriteMode $ doParseCheck inFile contents True
 

From 4229b6f30e11603dba91cee8a7dbb190d1f48e54 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 12:28:45 -0400
Subject: [PATCH 09/25] crucible-llvm-syntax: Simplify parsing of pointer types

---
 .../src/Lang/Crucible/LLVM/Syntax.hs          | 25 +++----------------
 1 file changed, 4 insertions(+), 21 deletions(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 10c4e49a2..a78f1d06d 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -17,12 +17,9 @@ import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
-import GHC.TypeLits (type (<=))
 
 import Data.BitVector.Sized qualified as BV
 
-import Data.Parameterized.NatRepr (NatRepr)
-import Data.Parameterized.NatRepr qualified as Nat
 import Data.Parameterized.Some (Some(..))
 
 import What4.ProgramLoc (Posd(..))
@@ -66,24 +63,10 @@ llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType
       let ptrName = do
             s <- Parse.atomName
             unless (s == Atom.AtomName "Ptr") Parse.cut
-      unary ptrName $ do
-        PtrWidth w <- ptrWidth
-        return (Some (LLVMPointerRepr w))
-
-data PtrWidth =
-  forall w. (1 <= w, 16 <= w) => PtrWidth (NatRepr w)
-
-ptrWidth :: MonadSyntax Atomic m => m PtrWidth
-ptrWidth =
-   do i <- Parse.sideCondition "nat literal >= 16" checkPosNat Parse.nat
-      maybe empty return $ do 
-        Some x <- return $ Nat.mkNatRepr i
-        let minPtrWidth = Nat.knownNat @16
-        Nat.LeqProof <- Nat.testLeq (Nat.knownNat @1) x
-        Nat.LeqProof <- Nat.testLeq minPtrWidth x
-        return (PtrWidth x)
-  where checkPosNat i | i > 16 = Just i
-        checkPosNat _ = Nothing
+      let ptrWidth = do
+            Parse.BoundedNat n <- Parse.posNat
+            pure (Some (LLVMPointerRepr n))
+      unary ptrName ptrWidth
 
 llvmAtomParser ::
   ( MonadSyntax Atomic m

From 3d7ced7f969c1bdc57ee3105184ff7cc3eb57fe6 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 12:36:12 -0400
Subject: [PATCH 10/25] crucible-llvm-syntax: README

---
 crucible-llvm-syntax/README.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 crucible-llvm-syntax/README.md

diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md
new file mode 100644
index 000000000..49f3c95ee
--- /dev/null
+++ b/crucible-llvm-syntax/README.md
@@ -0,0 +1,16 @@
+# crucible-llvm-syntax
+
+This package provides concrete syntax for Crucible-LLVM types and operations.
+
+Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn].
+This `ParserHooks` supports the following types and statements:
+
+**Types**:
+
+- `(Ptr n)` for a positive numeral `n` represents the type of LLVM pointers that are `n` bits wide. For example `(Ptr 8)` is the type of bytes.
+
+**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`
+
+[syn]: ../crucible-syntax

From 2c6c89cda8162eebe2222f213322df83847c404c Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 12:50:19 -0400
Subject: [PATCH 11/25] crucible-llvm-syntax: Fix hlint warnings

---
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 2 --
 1 file changed, 2 deletions(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index a78f1d06d..817968cf4 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -6,8 +6,6 @@
 {-# LANGUAGE ImportQualifiedPost #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeOperators #-}
 
 module Lang.Crucible.LLVM.Syntax where
 

From 7b4c01ec94a0bebc3e54a67494b722d4cb86b8bb Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 15:29:16 -0400
Subject: [PATCH 12/25] 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        | 11 ++++-
 crucible-llvm-syntax/test-data/ptr.out.good   | 41 ++++++++++++++---
 5 files changed, 85 insertions(+), 18 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..342919ded 100644
--- a/crucible-llvm-syntax/test-data/ptr.cbl
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -1,4 +1,11 @@
 (defun @test-ptr () (Ptr 64)
   (start start:
-    (let n (null))
-    (return n)))
+    (let blk0 (the Nat 0))
+    (let off0 (bv 64 0))
+    (let p0 (ptr 64 blk0 off0))
+    (let p (ptr-ite 64 #t p0 p0))
+    (let blk (ptr-block 64 p))
+    (let off (ptr-offset 64 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..9524529bd 100644
--- a/crucible-llvm-syntax/test-data/ptr.out.good
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -1,14 +1,43 @@
 (defun @test-ptr () (Ptr 64)
-   (start start: (let n (null)) (return n)))
+   (start start:
+      (let blk0 (the Nat 0))
+      (let off0 (bv 64 0))
+      (let p0 (ptr 64 blk0 off0))
+      (let p (ptr-ite 64 #t p0 p0))
+      (let blk (ptr-block 64 p))
+      (let off (ptr-offset 64 p))
+      (assert! (equal? blk0 blk) "block numbers equal")
+      (assert! (equal? off0 off) "offsets equal")
+      (return p)))
 
 test-ptr
 %0
-  % 3:12
+  % 3:15
   $0 = natLit(0)
-  % 3:12
+  % 4:15
   $1 = bVLit(64, BV 0)
-  % 3:12
+  % 5:13
   $2 = extensionApp(pointerExpr $0 $1)
-  % 4:5
-  return $2
+  % 6:12
+  $3 = boolLit(True)
+  % 6:12
+  $4 = extensionApp(pointerIte $3 $2 $2)
+  % 7:14
+  $5 = extensionApp(pointerBlock $4)
+  % 8:14
+  $6 = extensionApp(pointerOffset $4)
+  % 9:14
+  $7 = natEq($0, $5)
+  % 9:32
+  $8 = stringLit("block numbers equal")
+  % 9:5
+  assert($7, $8)
+  % 10:14
+  $9 = baseIsEq(BaseBVRepr 64, $1, $6)
+  % 10:32
+  $10 = stringLit("offsets equal")
+  % 10:5
+  assert($9, $10)
+  % 11:5
+  return $4
   % no postdom

From cae623221de6a9ff6f378c2ecd89d5bb618c31ef Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 16:54:52 -0400
Subject: [PATCH 13/25] crucible-llvm-syntax: Syntax for LLVM alloca statement

---
 .../crucible-llvm-syntax.cabal                |  1 +
 .../src/Lang/Crucible/LLVM/Syntax.hs          | 22 ++++++++++++++++++-
 crucible-llvm-syntax/test-data/ptr.cbl        |  4 ++++
 crucible-llvm-syntax/test-data/ptr.out.good   |  8 ++++++-
 4 files changed, 33 insertions(+), 2 deletions(-)

diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
index b40ca3804..e0271cb30 100644
--- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -96,6 +96,7 @@ library
     crucible-syntax,
     mtl,
     parameterized-utils >= 0.1.7,
+    prettyprinter,
     text,
     what4,
 
diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index dcfb09a8b..cb609da7c 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -16,6 +16,8 @@ import Control.Monad.State.Strict (MonadState(..))
 import Control.Monad.Writer.Strict (MonadWriter(..))
 import Data.Functor ((<&>))
 
+import Prettyprinter (pretty)
+
 import Data.Parameterized.Context qualified as Ctx
 import Data.Parameterized.Some (Some(..))
 
@@ -27,6 +29,8 @@ import Lang.Crucible.CFG.Reg qualified as Reg
 import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
 import Lang.Crucible.Types (TypeRepr(..))
 
+import Lang.Crucible.LLVM.DataLayout (Alignment)
+import Lang.Crucible.LLVM.DataLayout qualified as DataLayout
 import Lang.Crucible.LLVM.Extension (LLVM)
 import Lang.Crucible.LLVM.Extension qualified as Ext
 import Lang.Crucible.LLVM.MemModel (Mem, pattern LLVMPointerRepr)
@@ -76,7 +80,7 @@ llvmAtomParser ::
   ) =>
   GlobalVar Mem -> 
   m (Some (Atom s))
-llvmAtomParser _mvar =
+llvmAtomParser mvar =
   Parse.depCons Parse.atomName $
     \case
       Atom.AtomName "ptr" -> do
@@ -115,4 +119,20 @@ llvmAtomParser _mvar =
           let expr = Ext.LLVM_PointerIte w b p1 p2
           Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
 
+      Atom.AtomName "alloca" -> do
+        loc <- Parse.position
+        (align, assign) <- 
+          Parse.cons
+            parseAlign
+            (Parse.operands (Ctx.Empty Ctx.:> BVRepr ?ptrWidth))
+        let (Ctx.Empty, sz) = Ctx.decompose assign
+        let stmt = Ext.LLVM_Alloca ?ptrWidth mvar sz align (show (pretty loc))
+        Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       _ -> empty
+  where
+    parseAlign :: MonadSyntax Atomic m => m Alignment
+    parseAlign = do
+      s <- Parse.atomName
+      unless (s == Atom.AtomName "none") Parse.cut
+      pure DataLayout.noAlignment
diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
index 342919ded..3fffecdb7 100644
--- a/crucible-llvm-syntax/test-data/ptr.cbl
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -8,4 +8,8 @@
     (let off (ptr-offset 64 p))
     (assert! (equal? blk0 blk) "block numbers equal")
     (assert! (equal? off0 off) "offsets equal")
+
+    (let sz (bv 64 1))
+    (let a (alloca none sz))
+
     (return p)))
diff --git a/crucible-llvm-syntax/test-data/ptr.out.good b/crucible-llvm-syntax/test-data/ptr.out.good
index 9524529bd..7f16190b3 100644
--- a/crucible-llvm-syntax/test-data/ptr.out.good
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -8,6 +8,8 @@
       (let off (ptr-offset 64 p))
       (assert! (equal? blk0 blk) "block numbers equal")
       (assert! (equal? off0 off) "offsets equal")
+      (let sz (bv 64 1))
+      (let a (alloca none sz))
       (return p)))
 
 test-ptr
@@ -38,6 +40,10 @@ test-ptr
   $10 = stringLit("offsets equal")
   % 10:5
   assert($9, $10)
-  % 11:5
+  % 12:13
+  $11 = bVLit(64, BV 1)
+  % 13:12
+  $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12
+  % 15:5
   return $4
   % no postdom

From 42e85c344dede69c609aea2a355145b0130108ce Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 31 Oct 2023 17:45:06 -0400
Subject: [PATCH 14/25] crucible-llvm-syntax: Syntax for LLVM load, store
 statements

---
 .../src/Lang/Crucible/LLVM/Syntax.hs          | 46 ++++++++++++++++++-
 crucible-llvm-syntax/test-data/ptr.cbl        |  9 ++++
 crucible-llvm-syntax/test-data/ptr.out.good   | 35 +++++++++++++-
 3 files changed, 88 insertions(+), 2 deletions(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index cb609da7c..9ff279969 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -35,6 +35,9 @@ import Lang.Crucible.LLVM.Extension (LLVM)
 import Lang.Crucible.LLVM.Extension qualified as Ext
 import Lang.Crucible.LLVM.MemModel (Mem, pattern LLVMPointerRepr)
 import Lang.Crucible.LLVM.MemModel qualified as Mem
+import Lang.Crucible.LLVM.MemType (MemType)
+import Lang.Crucible.LLVM.MemType qualified as MemType
+import Lang.Crucible.LLVM.Translation (llvmTypeAsRepr)
 
 import Lang.Crucible.Syntax.Atoms (Atomic)
 import Lang.Crucible.Syntax.Atoms qualified as Atom
@@ -129,10 +132,51 @@ llvmAtomParser mvar =
         let stmt = Ext.LLVM_Alloca ?ptrWidth mvar sz align (show (pretty loc))
         Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
 
+      Atom.AtomName "load" -> Parse.describe "LLVM load arguments" $ do
+        loc <- Parse.position
+        (align, (memTy, assign)) <- 
+          Parse.cons
+            parseAlign
+            (Parse.cons
+              parseMemType
+              (Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth)))
+        llvmTypeAsRepr memTy $ \tyRep -> do
+          case Mem.toStorableType memTy of
+            Nothing -> empty
+            Just storTy -> do
+              let (Ctx.Empty, ptr) = Ctx.decompose assign
+              let stmt = Ext.LLVM_Load mvar ptr tyRep storTy align
+              Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
+      Atom.AtomName "store" -> Parse.describe "LLVM store arguments" $ do
+        loc <- Parse.position
+        Parse.depCons parseAlign $ \align ->
+          Parse.depCons parseMemType $ \memTy -> do
+            llvmTypeAsRepr memTy $ \tyRep -> do
+              assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth Ctx.:> tyRep)
+              case Mem.toStorableType memTy of
+                Nothing -> empty
+                Just storTy -> do
+                  let (rest, val) = Ctx.decompose assign
+                  let (Ctx.Empty, ptr) = Ctx.decompose rest
+                  let stmt = Ext.LLVM_Store mvar ptr tyRep storTy align val
+                  Some <$> Parse.freshAtom loc (Reg.EvalExt stmt)
+
       _ -> empty
   where
     parseAlign :: MonadSyntax Atomic m => m Alignment
-    parseAlign = do
+    parseAlign = Parse.describe "alignment" $ do
       s <- Parse.atomName
       unless (s == Atom.AtomName "none") Parse.cut
       pure DataLayout.noAlignment
+
+    parseMemType :: MonadSyntax Atomic m => m MemType
+    parseMemType = Parse.describe "LLVM type" $ do
+      nm <- Parse.atomName
+      case nm of
+        Atom.AtomName "i8" -> pure (MemType.IntType 8)
+        Atom.AtomName "i16" -> pure (MemType.IntType 16)
+        Atom.AtomName "i32" -> pure (MemType.IntType 32)
+        Atom.AtomName "i64" -> pure (MemType.IntType 64)
+        Atom.AtomName "ptr" -> pure MemType.PtrOpaqueType
+        _ -> empty
diff --git a/crucible-llvm-syntax/test-data/ptr.cbl b/crucible-llvm-syntax/test-data/ptr.cbl
index 3fffecdb7..4faec82c8 100644
--- a/crucible-llvm-syntax/test-data/ptr.cbl
+++ b/crucible-llvm-syntax/test-data/ptr.cbl
@@ -11,5 +11,14 @@
 
     (let sz (bv 64 1))
     (let a (alloca none sz))
+    (let vblk0 (the Nat 0))
+    (let voff0 (bv 8 255))
+    (let v0 (ptr 8 vblk0 voff0))
+    (store none i8 a v0)
+    (let v (load none i8 a))
+    (let vblk (ptr-block 8 v))
+    (let voff (ptr-offset 8 v))
+    (assert! (equal? vblk0 vblk) "stored block numbers equal")
+    (assert! (equal? voff0 voff) "stored 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 7f16190b3..691192e90 100644
--- a/crucible-llvm-syntax/test-data/ptr.out.good
+++ b/crucible-llvm-syntax/test-data/ptr.out.good
@@ -10,6 +10,15 @@
       (assert! (equal? off0 off) "offsets equal")
       (let sz (bv 64 1))
       (let a (alloca none sz))
+      (let vblk0 (the Nat 0))
+      (let voff0 (bv 8 255))
+      (let v0 (ptr 8 vblk0 voff0))
+      (store none i8 a v0)
+      (let v (load none i8 a))
+      (let vblk (ptr-block 8 v))
+      (let voff (ptr-offset 8 v))
+      (assert! (equal? vblk0 vblk) "stored block numbers equal")
+      (assert! (equal? voff0 voff) "stored offsets equal")
       (return p)))
 
 test-ptr
@@ -44,6 +53,30 @@ test-ptr
   $11 = bVLit(64, BV 1)
   % 13:12
   $12 = alloca crucible-llvm-syntax-test-memory $11 Alignment 0 test-data/ptr.cbl:13:12
-  % 15:5
+  % 15:16
+  $13 = bVLit(8, BV 255)
+  % 16:13
+  $14 = extensionApp(pointerExpr $0 $13)
+  % 17:5
+  $15 = store crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0 $14
+  % 18:12
+  $16 = load crucible-llvm-syntax-test-memory $12 bitvectorType 1 Alignment 0
+  % 19:15
+  $17 = extensionApp(pointerBlock $16)
+  % 20:15
+  $18 = extensionApp(pointerOffset $16)
+  % 21:14
+  $19 = natEq($0, $17)
+  % 21:34
+  $20 = stringLit("stored block numbers equal")
+  % 21:5
+  assert($19, $20)
+  % 22:14
+  $21 = baseIsEq(BaseBVRepr 8, $13, $18)
+  % 22:34
+  $22 = stringLit("stored offsets equal")
+  % 22:5
+  assert($21, $22)
+  % 24:5
   return $4
   % no postdom

From 7022ffaa0fc56483ddd321c38678c2cbd8073bec Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:38:21 -0400
Subject: [PATCH 15/25] crucible-llvm-syntax: Additional documentation

---
 crucible-llvm-syntax/README.md | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md
index 7e1799193..d3b852c9a 100644
--- a/crucible-llvm-syntax/README.md
+++ b/crucible-llvm-syntax/README.md
@@ -3,17 +3,32 @@
 This package provides concrete syntax for Crucible-LLVM types and operations.
 
 Concretely, it implements a `ParserHooks` for use with [`crucible-syntax`][syn].
-This `ParserHooks` supports the following types and statements:
+This `ParserHooks` supports the following types, primitive atoms, and
+statements:
 
 **Types**:
 
 - `(Ptr n)` for a positive numeral `n` represents the type of LLVM pointers that are `n` bits wide. For example `(Ptr 8)` is the type of bytes.
 
+**Primitive atoms**:
+
+- `none : Alignment`: no alignment
+- `i8 : LLVMType`
+- `i16 : LLVMType`
+- `i32 : LLVMType`
+- `i64 : LLVMType`
+- `ptr : LLVMType`
+
 **Statements**:
 
+If the numeral representing `w` the pointer width and `n` is an arbitrary numeral,
+
 - `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
+- `ptr-block : Ptr n -> Nat`: get the block number of a pointer
+- `ptr-offset : Ptr n -> Bitvector n`: get the offset of a pointer
+- `ptr-ite : Bool -> Ptr n -> Ptr n -> Ptr n`: if-then-else for pointers
+- `alloca : Alignment -> BV w -> Ptr w`: allocate space on the stack
+- `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`
 
 [syn]: ../crucible-syntax

From 00bf64e9cd80fa624c6eccb98ea820dc7389489d Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:43:44 -0400
Subject: [PATCH 16/25] crucible-llvm-syntax: Remove redundant `do`

---
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 9ff279969..d1086667e 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -151,7 +151,7 @@ llvmAtomParser mvar =
       Atom.AtomName "store" -> Parse.describe "LLVM store arguments" $ do
         loc <- Parse.position
         Parse.depCons parseAlign $ \align ->
-          Parse.depCons parseMemType $ \memTy -> do
+          Parse.depCons parseMemType $ \memTy ->
             llvmTypeAsRepr memTy $ \tyRep -> do
               assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr ?ptrWidth Ctx.:> tyRep)
               case Mem.toStorableType memTy of

From dd5af778af29c5589a26dbf294b927e31c47f386 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:49:18 -0400
Subject: [PATCH 17/25] crucible-llvm-syntax: Add haddock

---
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index d1086667e..5c5c20c20 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -46,6 +46,8 @@ import Lang.Crucible.Syntax.Concrete qualified as Parse
 import Lang.Crucible.Syntax.ExprParse (MonadSyntax)
 import Lang.Crucible.Syntax.ExprParse qualified as Parse
 
+-- | Like 'Lang.Crucible.Syntax.Concrete.Unary', but takes an arbitrary parser
+-- for its first argument.
 unary :: MonadSyntax Atomic m => m b -> m a -> m a
 unary p0 p = Parse.followedBy p0 (Parse.commit *> Parse.cons p Parse.emptyList) <&> fst
 

From 30fbe476f45c03e3798613bca3b892cb8cf072bd Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:53:58 -0400
Subject: [PATCH 18/25] crucible-llvm-syntax: README tweaks

---
 crucible-llvm-syntax/README.md | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md
index d3b852c9a..82053ad60 100644
--- a/crucible-llvm-syntax/README.md
+++ b/crucible-llvm-syntax/README.md
@@ -8,22 +8,25 @@ statements:
 
 **Types**:
 
-- `(Ptr n)` for a positive numeral `n` represents the type of LLVM pointers that are `n` bits wide. For example `(Ptr 8)` is the type of bytes.
+- `(Ptr n)` for a positive numeral `n` represents the type of LLVM pointers that are `n` bits wide; for example `(Ptr 8)` is the type of bytes
 
 **Primitive atoms**:
 
 - `none : Alignment`: no alignment
-- `i8 : LLVMType`
-- `i16 : LLVMType`
-- `i32 : LLVMType`
-- `i64 : LLVMType`
-- `ptr : LLVMType`
+- `i8 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 8 :: MemType`
+- `i16 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 16 :: MemType`
+- `i32 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 32 :: MemType`
+- `i64 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 64 :: MemType`
+- `ptr : LLVMType`: [LLVM docs][ptr-type], corresponds to Crucible-LLVM's `IntType 64 :: PtrOpaqueType`
+
+[int-type]: https://llvm.org/docs/LangRef.html#integer-type
+[ptr-type]: https://llvm.org/docs/LangRef.html#pointer-type
 
 **Statements**:
 
 If the numeral representing `w` the pointer width and `n` is an arbitrary numeral,
 
-- `ptr : Nat -> Bitvector w -> Ptr w`: construct a pointer from a block and offset
+- `ptr : Nat -> Bitvector n -> Ptr n`: construct a pointer from a block and offset
 - `ptr-block : Ptr n -> Nat`: get the block number of a pointer
 - `ptr-offset : Ptr n -> Bitvector n`: get the offset of a pointer
 - `ptr-ite : Bool -> Ptr n -> Ptr n -> Ptr n`: if-then-else for pointers

From a7a96a53e06a6a5d97f673625f6545883737d5b3 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:54:56 -0400
Subject: [PATCH 19/25] crucible-llvm-syntax: README typo

---
 crucible-llvm-syntax/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md
index 82053ad60..1c4a1cdc6 100644
--- a/crucible-llvm-syntax/README.md
+++ b/crucible-llvm-syntax/README.md
@@ -24,7 +24,7 @@ statements:
 
 **Statements**:
 
-If the numeral representing `w` the pointer width and `n` is an arbitrary numeral,
+If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral,
 
 - `ptr : Nat -> Bitvector n -> Ptr n`: construct a pointer from a block and offset
 - `ptr-block : Ptr n -> Nat`: get the block number of a pointer

From c9674d04de543b215ed978558e4d3a255e5f30ab Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:55:33 -0400
Subject: [PATCH 20/25] crucible-llvm-syntax: `BV` -> `Bitvector`

---
 crucible-llvm-syntax/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md
index 1c4a1cdc6..d08eea4fc 100644
--- a/crucible-llvm-syntax/README.md
+++ b/crucible-llvm-syntax/README.md
@@ -30,7 +30,7 @@ If the numeral `w` is the width of a pointer and `n` is an arbitrary numeral,
 - `ptr-block : Ptr n -> Nat`: get the block number of a pointer
 - `ptr-offset : Ptr n -> Bitvector n`: get the offset of a pointer
 - `ptr-ite : Bool -> Ptr n -> Ptr n -> Ptr n`: if-then-else for pointers
-- `alloca : Alignment -> BV w -> Ptr w`: allocate space on the stack
+- `alloca : Alignment -> Bitvector w -> Ptr w`: allocate space on the stack
 - `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`
 

From 5c340c88474b807d5de3df5c95b3e2e472302945 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 11:58:29 -0400
Subject: [PATCH 21/25] crucible-llvm-syntax: Improve error messages with
 `describe`

---
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 5c5c20c20..1d9d7fc47 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -88,7 +88,7 @@ llvmAtomParser ::
 llvmAtomParser mvar =
   Parse.depCons Parse.atomName $
     \case
-      Atom.AtomName "ptr" -> do
+      Atom.AtomName "ptr" -> Parse.describe "LLVM ptr arguments" $ do
         loc <- Parse.position
         Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
           assign <- Parse.operands (Ctx.Empty Ctx.:> NatRepr Ctx.:> BVRepr w)
@@ -98,7 +98,7 @@ llvmAtomParser mvar =
           ptrAtom <- Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
           return (Some ptrAtom)
 
-      Atom.AtomName "ptr-block" -> do
+      Atom.AtomName "ptr-block" -> Parse.describe "LLVM ptr-block arguments" $ do
         loc <- Parse.position
         Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
           assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr w)
@@ -106,7 +106,7 @@ llvmAtomParser mvar =
           let expr = Ext.LLVM_PointerBlock w ptr
           Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
 
-      Atom.AtomName "ptr-offset" -> do
+      Atom.AtomName "ptr-offset" -> Parse.describe "LLVM ptr-offset arguments" $ do
         loc <- Parse.position
         Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
           assign <- Parse.operands (Ctx.Empty Ctx.:> LLVMPointerRepr w)
@@ -114,7 +114,7 @@ llvmAtomParser mvar =
           let expr = Ext.LLVM_PointerOffset w ptr
           Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
 
-      Atom.AtomName "ptr-ite" -> do
+      Atom.AtomName "ptr-ite" -> Parse.describe "LLVM ptr-ite arguments" $ do
         loc <- Parse.position
         Parse.depCons Parse.posNat $ \(Parse.BoundedNat w) -> do
           assign <- Parse.operands (Ctx.Empty Ctx.:> BoolRepr Ctx.:> LLVMPointerRepr w Ctx.:> LLVMPointerRepr w)
@@ -124,7 +124,7 @@ llvmAtomParser mvar =
           let expr = Ext.LLVM_PointerIte w b p1 p2
           Some <$> Parse.freshAtom loc (Reg.EvalApp (Expr.ExtensionApp expr))
 
-      Atom.AtomName "alloca" -> do
+      Atom.AtomName "alloca" -> Parse.describe "LLVM alloca arguments" $ do
         loc <- Parse.position
         (align, assign) <- 
           Parse.cons

From f4b2c4f615d902b52d26200118fe55cb76ea9c51 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 12:47:33 -0400
Subject: [PATCH 22/25] crucible-llvm-syntax: Add golden test files to
 extra-source-files

---
 crucible-llvm-syntax/crucible-llvm-syntax.cabal | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crucible-llvm-syntax/crucible-llvm-syntax.cabal b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
index e0271cb30..aca0ae3a1 100644
--- a/crucible-llvm-syntax/crucible-llvm-syntax.cabal
+++ b/crucible-llvm-syntax/crucible-llvm-syntax.cabal
@@ -12,6 +12,8 @@ Synopsis:      A syntax for reading and writing Crucible-LLVM control-flow graph
 
 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

From abac7c929819a28ceba21fbe11b40329ae2cd242 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 12:48:18 -0400
Subject: [PATCH 23/25] ci: Tweak syntax of hlint command

---
 .github/workflows/uc-crux-llvm-lint.yaml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/workflows/uc-crux-llvm-lint.yaml b/.github/workflows/uc-crux-llvm-lint.yaml
index 07f11280f..437fb3951 100644
--- a/.github/workflows/uc-crux-llvm-lint.yaml
+++ b/.github/workflows/uc-crux-llvm-lint.yaml
@@ -20,9 +20,7 @@ jobs:
             https://github.com/ndmitchell/hlint/releases/download/v3.3/hlint-3.3-x86_64-linux.tar.gz
           tar xvf hlint.tar.gz
 
-          pushd crucible-llvm-syntax/
-          ../hlint-3.3/hlint src test
-          popd
+          (cd crucible-llvm-syntax/; ../hlint-3.3/hlint src test)
 
           cd uc-crux-llvm/
           ../hlint-3.3/hlint exe src test

From bb3501b6dba3002661b7e0d2cdeb51d3bab6407d Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 13:27:52 -0400
Subject: [PATCH 24/25] crucible-llvm-syntax: Add type signature for GHC 8.10
 compatibility

---
 crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 1d9d7fc47..71bce2c27 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -69,7 +69,9 @@ llvmTypeParser = Parse.describe "LLVM type" $ Parse.call ptrType
       let ptrName = do
             s <- Parse.atomName
             unless (s == Atom.AtomName "Ptr") Parse.cut
-      let ptrWidth = do
+      let -- This type signature is needed for GHC 8.10
+          ptrWidth :: MonadSyntax Atomic m => m (Some TypeRepr)
+          ptrWidth = do
             Parse.BoundedNat n <- Parse.posNat
             pure (Some (LLVMPointerRepr n))
       unary ptrName ptrWidth

From 18e4db9a8219cbf3f36b38a4b9d1d739c9ae2b13 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 1 Nov 2023 15:45:28 -0400
Subject: [PATCH 25/25] crucible-llvm-syntax: Fix README typo

Co-authored-by: Ryan Scott <ryan.gl.scott@gmail.com>
---
 crucible-llvm-syntax/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-llvm-syntax/README.md b/crucible-llvm-syntax/README.md
index d08eea4fc..7bccded00 100644
--- a/crucible-llvm-syntax/README.md
+++ b/crucible-llvm-syntax/README.md
@@ -17,7 +17,7 @@ statements:
 - `i16 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 16 :: MemType`
 - `i32 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 32 :: MemType`
 - `i64 : LLVMType`: [LLVM docs][int-type], corresponds to Crucible-LLVM's `IntType 64 :: MemType`
-- `ptr : LLVMType`: [LLVM docs][ptr-type], corresponds to Crucible-LLVM's `IntType 64 :: PtrOpaqueType`
+- `ptr : LLVMType`: [LLVM docs][ptr-type], corresponds to Crucible-LLVM's `PtrOpaqueType :: MemType`
 
 [int-type]: https://llvm.org/docs/LangRef.html#integer-type
 [ptr-type]: https://llvm.org/docs/LangRef.html#pointer-type