diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,66 @@
+# 0.9 -- 2026-01-29
+
+* The `LLVM_Debug` data constructor for `LLVMStmt`, as well as the related
+  `LLVM_Dbg` data type, have been removed.
+* Remove `aggInfo` in favor of `aggregateAlignment`, a lens that retrieves an
+  `Alignment` instead of a full `AlignInfo`. In practice, `aggInfo` would only
+  ever contain a single size (`0`) in its `AlignInfo`, and the concept of
+  "size" doesn't really apply to aggregate alignments in data layout strings,
+  so this was simplified to just be an `Alignment` instead.
+* Support simulating bitcode that uses features from LLVM 19, including
+  [debug records](https://llvm.org/docs/RemoveDIsDebugInfo.html) and
+  [`getelementptr`
+  attributes](https://releases.llvm.org/19.1.0/docs/LangRef.html#id237).
+* Support the `nneg` flag in `zext` and `uitofp` instructions. If `nneg` is
+  set, then converting a negative argument will yield a poisoned result.
+* Support the `nuw` and `nsw` flags in `trunc` instructions. If `nuw` or `nsw`
+  is set, then performing a truncation that would result in unsigned or signed
+  integer overflow, respectively, will yield a poisoned result.
+* Support the `samesign` flag in `icmp` instructions. If `samesign` is set, then
+  comparing two integers of different signs will yield a poisoned result.
+* Support the `llvm.tan`, `llvm.a{sin,cos,tan}`, `llvm.{sin,cos,tan}h`, and
+  `llvm.atan2` floating-point intrinsics.
+* Add extremely limited support for representing `poison` constants. For more
+  details on the extent to which `crucible-llvm` can reason about `poison`, see
+  `doc/limitations.md`.
+
+  As part of these changes:
+
+  * `LLVMVal` now features an additional `LLVMValPoison` data constructor.
+  * `LLVMExpr` now features an additional `PoisonExpr` data constructor.
+  * `LLVMConst` now features an addition `PoisonConst` data constructor.
+  * `LLVMExtensionExpr` now features `LLVM_Poison{BV,Float}` data constructors,
+    which represent primitive `poison` values.
+* Remove the `Eq LLVMConst` instance. This instance was inherently unreliable
+  because it cannot easily compute a simple `True`-or-`False` answer in the
+  presence of `undef` or `poison` values.
+* Replace `Data.Dynamic.Dynamic` with `SomeFnHandle` in
+  `MemModel.{doInstallHandle,doLookupHandle}`.
+* Add pretty-printing functions for use with `Lang.Crucible.Types.ppTypeRepr`
+  * `Lang.Crucible.LLVM.MemModel.ppLLVMIntrinsicTypes`
+  * `Lang.Crucible.LLVM.MemModel.ppLLVMMemIntrinsicType`
+  * `Lang.Crucible.LLVM.MemModel.Pointer.ppLLVMPointerIntrinsicType`
+* Overrides for `strnlen`, `strcpy`, `strdup`, and `strndup` supported by new
+  APIs in `Lang.Crucible.LLVM.MemModel.Strings`.
+
+# 0.8.0 -- 2025-11-09
+
+* `Lang.Crucible.LLVM.MemModel.{loadString,loadMaybeString,strLen}`
+  should now be imported from `Lang.Crucible.LLVM.MemModel.Strings`.
+* Two new functions for loading C-style null-terminated strings from
+  LLVM memory were added to `Lang.Crucible.LLVM.MemModel.Strings`:
+  `loadConcretelyNullTerminatedString` and `loadProvablyNullTerminatedString`.
+* Add a new "low-level" API for loading strings to
+  `Lang.Crucible.LLVM.MemModel.Strings`: `ByteLoader`, `ByteChecker`, and
+  `loadBytes`.
+* Support simulating LLVM bitcode files whose data layout strings specify
+  function pointer alignment.
+* Fix a bug that would cause the simuator to compute incorrect results for the
+  `llvm.is.fpclass` intrinsic. (Among other things, this is used to power the
+  `isnan` function in Clang 17 or later.)
+* Support vectorized versions of the `llvm.u{min,max}` and `llvm.s{min,max}`
+  intrinsics.
+
 # 0.7.1 -- 2025-03-21
 
 * Fix a bug in which the memory model would panic when attempting to unpack
@@ -52,7 +115,7 @@
   * `Lang.Crucible.LLVM.Globals`: `populateGlobal`
   * `Lang.Crucible.LLVM.MemModel.Generic`: `writeMem` and `writeConstMem`
 * `Lang.Crucible.LLVM`: `registerModuleFn` has changed type to
-  accomodate lazy loading of Crucible IR.
+  accommodate lazy loading of Crucible IR.
 * `Lang.Crucible.LLVM.Translation` : The `ModuleTranslation` record is
   now opaque, the `cfgMap` is no longer exported and `globalInitMap`
   and `modTransNonce` have become lens-style getters instead of record
diff --git a/crucible-llvm.cabal b/crucible-llvm.cabal
--- a/crucible-llvm.cabal
+++ b/crucible-llvm.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible-llvm
-Version:       0.7.1
+Version:       0.9
 Author:        Galois Inc.
 Copyright:     (c) Galois, Inc 2014-2022
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
@@ -29,22 +29,112 @@
   ghc-prof-options: -O2 -fprof-auto-exported
   default-language: Haskell2010
 
+common warns
+  -- 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.6 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=deriving-typeable
+    -Werror=dodgy-foreign-imports
+    -Werror=duplicate-exports
+    -Werror=empty-enumerations
+    -Werror=gadt-mono-local-binds
+    -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=missing-pattern-synonym-signatures
+    -Werror=missing-signatures
+    -Werror=name-shadowing
+    -Werror=noncanonical-monad-instances
+    -Werror=noncanonical-monoid-instances
+    -Werror=operator-whitespace
+    -Werror=operator-whitespace-ext-conflict
+    -Werror=orphans
+    -Werror=overflowed-literals
+    -Werror=overlapping-patterns
+    -Werror=partial-fields
+    -Werror=partial-type-signatures
+    -Werror=redundant-bang-patterns
+    -Werror=redundant-record-wildcards
+    -Werror=redundant-strictness-flags
+    -Werror=simplifiable-class-constraints
+    -Werror=star-binder
+    -Werror=star-is-type
+    -Werror=tabs
+    -Werror=type-defaults
+    -Werror=typed-holes
+    -Werror=type-equality-out-of-scope
+    -Werror=type-equality-requires-operators
+    -Werror=unicode-bidirectional-format-characters
+    -Werror=unrecognised-pragmas
+    -Werror=unrecognised-warning-flags
+    -Werror=unsupported-calling-conventions
+    -Werror=unsupported-llvm-version
+    -Werror=unused-do-bind
+    -Werror=unused-imports
+    -Werror=unused-record-wildcards
+    -Werror=warnings-deprecations
+    -Werror=wrong-do-bind
+
+  if impl(ghc < 9.8)
+    ghc-options:
+      -Werror=forall-identifier
+
+  if impl(ghc >= 9.8)
+    ghc-options:
+      -Werror=incomplete-export-warnings
+      -Werror=inconsistent-flags
+
+  if impl(ghc >= 9.10)
+    ghc-options:
+      -Werror=badly-staged-types
+      -Werror=data-kinds-tc
+      -Werror=deprecated-type-abstractions
+      -Werror=incomplete-record-selectors
+
 library
   import: bldflags
   build-depends:
-    base >= 4.13 && < 4.20,
+    base >= 4.13 && < 4.21,
     attoparsec,
     bv-sized >= 1.0.0,
     bytestring,
     containers >= 0.5.8.0,
     crucible >= 0.5,
     crucible-symio,
-    what4 >= 0.4.1,
+    what4 >= 0.5,
     extra,
     lens,
     itanium-abi >= 0.1.1.1 && < 0.2,
-    llvm-pretty >= 0.12.1 && < 0.14,
+    llvm-pretty >= 0.12.1 && < 0.15,
     mtl,
     parameterized-utils >= 2.1.5 && < 2.2,
     pretty,
@@ -73,6 +163,7 @@
     Lang.Crucible.LLVM.Extension
     Lang.Crucible.LLVM.Functions
     Lang.Crucible.LLVM.Globals
+    Lang.Crucible.LLVM.Internal
     Lang.Crucible.LLVM.Intrinsics
     Lang.Crucible.LLVM.Intrinsics.Cast
     Lang.Crucible.LLVM.Intrinsics.Libc
@@ -85,6 +176,7 @@
     Lang.Crucible.LLVM.MemModel.MemLog
     Lang.Crucible.LLVM.MemModel.Partial
     Lang.Crucible.LLVM.MemModel.Pointer
+    Lang.Crucible.LLVM.MemModel.Strings
     Lang.Crucible.LLVM.MemType
     Lang.Crucible.LLVM.PrettyPrint
     Lang.Crucible.LLVM.Printf
@@ -124,6 +216,7 @@
 
 test-suite crucible-llvm-tests
   import: bldflags
+  import: warns
   type: exitcode-stdio-1.0
   main-is: Tests.hs
   hs-source-dirs: test
diff --git a/src/Lang/Crucible/LLVM/DataLayout.hs b/src/Lang/Crucible/LLVM/DataLayout.hs
--- a/src/Lang/Crucible/LLVM/DataLayout.hs
+++ b/src/Lang/Crucible/LLVM/DataLayout.hs
@@ -42,7 +42,6 @@
 import Control.Monad.State.Strict
 import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Maybe (fromMaybe)
 import Data.Word (Word32)
 import qualified Text.LLVM as L
 import Numeric.Natural
@@ -131,11 +130,6 @@
 floatAlignment dl w = Map.lookup w t
   where AT t = dl^.floatInfo
 
--- | Get the basic alignment for aggregate types.
-aggregateAlignment :: DataLayout -> Alignment
-aggregateAlignment dl =
-  fromMaybe noAlignment (findExact 0 (dl^.aggInfo))
-
 -- | Return maximum alignment constraint stored in tree.
 maxAlignmentInTree :: AlignInfo -> Alignment
 maxAlignmentInTree (AT t) = foldrOf folded max noAlignment t
@@ -164,12 +158,13 @@
 data DataLayout
    = DL { _intLayout :: EndianForm
         , _stackAlignment :: !Alignment
+        , _functionPtrAlignment :: !Alignment
+        , _aggregateAlignment :: !Alignment
         , _ptrSize     :: !Bytes
         , _ptrAlign    :: !Alignment
         , _integerInfo :: !AlignInfo
         , _vectorInfo  :: !AlignInfo
         , _floatInfo   :: !AlignInfo
-        , _aggInfo     :: !AlignInfo
         , _stackInfo   :: !AlignInfo
         , _layoutWarnings :: [L.LayoutSpec]
         }
@@ -184,6 +179,14 @@
 stackAlignment :: Lens' DataLayout Alignment
 stackAlignment = lens _stackAlignment (\s v -> s { _stackAlignment = v})
 
+functionPtrAlignment :: Lens' DataLayout Alignment
+functionPtrAlignment =
+  lens _functionPtrAlignment (\s v -> s { _functionPtrAlignment = v})
+
+aggregateAlignment :: Lens' DataLayout Alignment
+aggregateAlignment =
+  lens _aggregateAlignment (\s v -> s { _aggregateAlignment = v})
+
 -- | Size of pointers in bytes.
 ptrSize :: Lens' DataLayout Bytes
 ptrSize = lens _ptrSize (\s v -> s { _ptrSize = v})
@@ -201,10 +204,6 @@
 floatInfo :: Lens' DataLayout AlignInfo
 floatInfo = lens _floatInfo (\s v -> s { _floatInfo = v})
 
--- | Information about aggregate size.
-aggInfo :: Lens' DataLayout AlignInfo
-aggInfo = lens _aggInfo (\s v -> s { _aggInfo = v})
-
 -- | Layout constraints on a stack object with the given size.
 stackInfo :: Lens' DataLayout AlignInfo
 stackInfo = lens _stackInfo (\s v -> s { _stackInfo = v})
@@ -238,12 +237,13 @@
 defaultDataLayout = execState defaults dl
   where dl = DL { _intLayout = BigEndian
                 , _stackAlignment = noAlignment
+                , _functionPtrAlignment = noAlignment
                 , _ptrSize  = 8 -- 64 bit pointers = 8 bytes
                 , _ptrAlign = Alignment 3 -- 64 bit alignment: 2^3=8 byte boundaries
+                , _aggregateAlignment = noAlignment -- Aggregates are 1-byte aligned.
                 , _integerInfo = emptyAlignInfo
                 , _floatInfo   = emptyAlignInfo
                 , _vectorInfo  = emptyAlignInfo
-                , _aggInfo     = emptyAlignInfo
                 , _stackInfo   = emptyAlignInfo
                 , _layoutWarnings = []
                 }
@@ -262,18 +262,17 @@
           -- Default vector alignments.
           setAt vectorInfo  64 (Alignment 3) -- 64-bit vector is 8 byte aligned.
           setAt vectorInfo 128 (Alignment 4) -- 128-bit vector is 16 byte aligned.
-          -- Default aggregate alignments.
-          setAt aggInfo  0 noAlignment  -- Aggregates are 1-byte aligned.
 
 -- | Maximum alignment for any type (used by malloc).
 maxAlignment :: DataLayout -> Alignment
 maxAlignment dl =
   maximum [ dl^.stackAlignment
+          , dl^.functionPtrAlignment
           , dl^.ptrAlign
+          , dl^.aggregateAlignment
           , maxAlignmentInTree (dl^.integerInfo)
           , maxAlignmentInTree (dl^.vectorInfo)
           , maxAlignmentInTree (dl^.floatInfo)
-          , maxAlignmentInTree (dl^.aggInfo)
           , maxAlignmentInTree (dl^.stackInfo)
           ]
 
@@ -282,14 +281,14 @@
            | otherwise = fromIntegral i
 
 -- | Insert alignment into spec.
-setAtBits :: Lens' DataLayout AlignInfo -> L.LayoutSpec -> Int -> Int -> State DataLayout ()
-setAtBits f spec sz a =
-  case fromBits a of
+setAtBits :: Lens' DataLayout AlignInfo -> L.LayoutSpec -> L.Storage -> State DataLayout ()
+setAtBits f spec st =
+  case fromBits (L.alignABI (L.storageAlignment st)) of
     Left{} -> layoutWarnings %= (spec:)
-    Right w -> f . at (fromSize sz) .= Just w
+    Right w -> f . at (fromSize (L.storageSize st)) .= Just w
 
 -- | Insert alignment into spec.
-setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> Int -> State DataLayout ()
+setBits :: Lens' DataLayout Alignment -> L.LayoutSpec -> L.NumBits -> State DataLayout ()
 setBits f spec a =
   case fromBits a of
     Left{} -> layoutWarnings %= (spec:)
@@ -302,27 +301,46 @@
     case ls of
       L.BigEndian    -> intLayout .= BigEndian
       L.LittleEndian -> intLayout .= LittleEndian
-      L.PointerSize n sz a _
+      L.PointerSize ps
            -- Currently, we assume that only default address space (0) is used.
            -- We use that address space as the sole arbiter of what pointer
            -- size to use, and we ignore all other PointerSize layout specs.
            -- See doc/limitations.md for more discussion.
-        |  n == 0
-        -> case fromBits a of
+        |  L.ptrAddrSpace ps == 0
+        -> case fromBits (L.alignABI (L.storageAlignment st)) of
              Right a' | r == 0 -> do ptrSize .= fromIntegral w
                                      ptrAlign .= a'
              _ -> layoutWarnings %= (ls:)
         |  otherwise
         -> return ()
-       where (w,r) = sz `divMod` 8
-      L.IntegerSize    sz a _ -> setAtBits integerInfo ls sz a
-      L.VectorSize     sz a _ -> setAtBits vectorInfo  ls sz a
-      L.FloatSize      sz a _ -> setAtBits floatInfo   ls sz a
-      L.AggregateSize  sz a _ -> setAtBits aggInfo     ls sz a
-      L.StackObjSize   sz a _ -> setAtBits stackInfo   ls sz a
+       where st = L.ptrStorage ps
+             (w,r) = L.storageSize st `divMod` 8
+      L.IntegerSize st -> setStorageAlignInfo integerInfo st
+      L.VectorSize st -> setStorageAlignInfo vectorInfo st
+      L.FloatSize st -> setStorageAlignInfo floatInfo st
+      L.StackObjSize st -> setStorageAlignInfo stackInfo st
+      L.AggregateSize _ a -> setBits aggregateAlignment ls (L.alignABI a)
       L.NativeIntSize _ -> return ()
       L.StackAlign a    -> setBits stackAlignment ls a
+      -- TODO: For now, we ignore the FunctionPointerAlignType field. This tells
+      -- us whether the function pointer alignment is related to the alignment
+      -- of functions, but llvm-pretty currently does not track the alignment of
+      -- individual functions, so we have no use for this info just yet. When
+      -- https://github.com/GaloisInc/llvm-pretty/issues/164 is implemented, we
+      -- should revisit this.
+      L.FunctionPointerAlign _ a -> setBits functionPtrAlignment ls a
       L.Mangling _      -> return ()
+      -- Currently, we assume that only the default address space (0) is used,
+      -- and we ignore all other address space-related layout specs.
+      -- See doc/limitations.md for more discussion.
+      L.ProgramAddrSpace {} -> return ()
+      L.GlobalAddrSpace {} -> return ()
+      L.AllocaAddrSpace {} -> return ()
+      L.NonIntegralPointerSpaces {} -> return ()
+  where
+    setStorageAlignInfo ::
+      Lens' DataLayout AlignInfo -> L.Storage -> State DataLayout ()
+    setStorageAlignInfo info st = setAtBits info ls st
 
 -- | Create parsed data layout from layout spec AST.
 parseDataLayout :: L.DataLayout -> DataLayout
diff --git a/src/Lang/Crucible/LLVM/Errors/MemoryError.hs b/src/Lang/Crucible/LLVM/Errors/MemoryError.hs
--- a/src/Lang/Crucible/LLVM/Errors/MemoryError.hs
+++ b/src/Lang/Crucible/LLVM/Errors/MemoryError.hs
@@ -6,6 +6,7 @@
 -- Maintainer       : Langston Barrett <lbarrett@galois.com>
 -- Stability        : provisional
 --
+-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these.
 --------------------------------------------------------------------------
 
 {-# LANGUAGE DataKinds #-}
@@ -37,7 +38,6 @@
 
 import           Data.Text (Text)
 import qualified Text.LLVM.AST as L
-import           Type.Reflection (SomeTypeRep(SomeTypeRep))
 import           Prettyprinter
 
 import           What4.Interface
@@ -99,7 +99,6 @@
   = SymbolicPointer
   | RawBitvector
   | NoOverride
-  | Uncallable SomeTypeRep
   deriving (Eq, Ord)
 
 ppFuncLookupError :: FuncLookupError -> Doc ann
@@ -108,10 +107,6 @@
     SymbolicPointer -> "Cannot resolve a symbolic pointer to a function handle"
     RawBitvector -> "Cannot treat raw bitvector as function pointer"
     NoOverride -> "No implementation or override found for pointer"
-    Uncallable (SomeTypeRep typeRep) ->
-      vsep [ "Data associated with the pointer found, but was not a callable function:"
-           , hang 2 (viaShow typeRep)
-           ]
 
 type MemErrContext sym w = MemoryOp sym w
 
diff --git a/src/Lang/Crucible/LLVM/Errors/Poison.hs b/src/Lang/Crucible/LLVM/Errors/Poison.hs
--- a/src/Lang/Crucible/LLVM/Errors/Poison.hs
+++ b/src/Lang/Crucible/LLVM/Errors/Poison.hs
@@ -130,6 +130,22 @@
   GEPOutOfBounds      :: (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr)
                       -> e (BVType w)
                       -> Poison e
+  ZExtNonNegative     :: (1 <= w)
+                      => e (BVType w)
+                      -> Poison e
+  UiToFpNonNegative   :: (1 <= w)
+                      => e (BVType w)
+                      -> Poison e
+  TruncNoUnsignedWrap :: (1 <= w)
+                      => e (BVType w)
+                      -> Poison e
+  TruncNoSignedWrap   :: (1 <= w)
+                      => e (BVType w)
+                      -> Poison e
+  ICmpSameSign        :: (1 <= w)
+                      => e (BVType w)
+                      -> e (BVType w)
+                      -> Poison e
   deriving (Typeable)
 
 standard :: Poison e -> Standard
@@ -154,6 +170,11 @@
     InsertElementIndex _    -> LLVMRef LLVM8
     LLVMAbsIntMin _         -> LLVMRef LLVM12
     GEPOutOfBounds _ _      -> LLVMRef LLVM8
+    ZExtNonNegative _       -> LLVMRef LLVM18
+    UiToFpNonNegative _     -> LLVMRef LLVM19
+    TruncNoUnsignedWrap _   -> LLVMRef LLVM20
+    TruncNoSignedWrap _     -> LLVMRef LLVM20
+    ICmpSameSign _ _        -> LLVMRef LLVM20
 
 -- | Which section(s) of the document state that this is poison?
 cite :: Poison e -> Doc ann
@@ -178,6 +199,11 @@
     InsertElementIndex _    -> "‘insertelement’ Instruction (Semantics)"
     LLVMAbsIntMin _         -> "‘llvm.abs.*’ Intrinsic (Semantics)"
     GEPOutOfBounds _ _      -> "‘getelementptr’ Instruction (Semantics)"
+    ZExtNonNegative _       -> "‘zext’ Instruction (Semantics)"
+    UiToFpNonNegative _     -> "‘uitofp’ Instruction (Semantics)"
+    TruncNoUnsignedWrap _   -> "‘trunc’ Instruction (Semantics)"
+    TruncNoSignedWrap _     -> "‘trunc’ Instruction (Semantics)"
+    ICmpSameSign _ _        -> "‘icmp’ Instruction (Semantics)"
 
 explain :: Poison e -> Doc ann
 explain =
@@ -226,13 +252,24 @@
       ]
 
     -- The following explanation is a bit unsatisfactory, because it is specific
-    -- to how we treat this instruction in Crucible.
+    -- to how we treat this instruction in Crucible. (See also #1605.)
     GEPOutOfBounds _ _ -> cat $
       [ "Calling `getelementptr` resulted in an index that was out of bounds for the"
       , "given allocation (likely due to arithmetic overflow), but Crucible currently"
-      , "treats all GEP instructions as if they had the `inbounds` flag set."
+      , "treats all GEP instructions as if they had the `inbounds` attribute set."
       ]
 
+    ZExtNonNegative _ ->
+      "A negative integer was zero-extended even though the `nneg` flag was set"
+    UiToFpNonNegative _ ->
+      "A negative integer was converted to a floating-point value even though the `nneg` flag was set"
+    TruncNoUnsignedWrap _ ->
+      "Unsigned truncation caused wrapping even though the `nuw` flag was set"
+    TruncNoSignedWrap _ ->
+      "Signed truncation caused wrapping even though the `nsw` flag was set"
+    ICmpSameSign _ _ ->
+      "Two integers with different signs were compared even though the `samesign` flag was set"
+
 details :: forall sym ann.
   W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> [Doc ann]
 details =
@@ -259,6 +296,11 @@
       [ "Pointer:" <+> ppPtr ptr
       , "Bitvector:" <+> W4I.printSymExpr bv
       ]
+    ZExtNonNegative v -> args [v]
+    UiToFpNonNegative v -> args [v]
+    TruncNoUnsignedWrap v -> args [v]
+    TruncNoSignedWrap v -> args [v]
+    ICmpSameSign v1 v2 -> args [v1, v2]
 
  where
  args :: forall w. [RegValue' sym (BVType w)] -> [Doc ann]
@@ -334,6 +376,16 @@
       GEPOutOfBounds <$> concPtr' sym conc p <*> bv v
     LLVMAbsIntMin v ->
       LLVMAbsIntMin <$> bv v
+    ZExtNonNegative v ->
+      ZExtNonNegative <$> bv v
+    UiToFpNonNegative v ->
+      UiToFpNonNegative <$> bv v
+    TruncNoUnsignedWrap v ->
+      TruncNoUnsignedWrap <$> bv v
+    TruncNoSignedWrap v ->
+      TruncNoSignedWrap <$> bv v
+    ICmpSameSign v1 v2 ->
+      ICmpSameSign <$> bv v1 <*> bv v2
 
 
 -- -----------------------------------------------------------------------
diff --git a/src/Lang/Crucible/LLVM/Errors/Standards.hs b/src/Lang/Crucible/LLVM/Errors/Standards.hs
--- a/src/Lang/Crucible/LLVM/Errors/Standards.hs
+++ b/src/Lang/Crucible/LLVM/Errors/Standards.hs
@@ -69,6 +69,9 @@
   | LLVM7
   | LLVM8
   | LLVM12
+  | LLVM18
+  | LLVM19
+  | LLVM20
   deriving (Data, Eq, Enum, Generic, Ord, Read, Show, Typeable)
 
 ppLLVMRefVer :: LLVMRefVer -> Text
@@ -79,6 +82,9 @@
 ppLLVMRefVer LLVM7  = "7"
 ppLLVMRefVer LLVM8  = "8"
 ppLLVMRefVer LLVM12 = "12"
+ppLLVMRefVer LLVM18 = "18"
+ppLLVMRefVer LLVM19 = "19"
+ppLLVMRefVer LLVM20 = "20"
 
 stdURL :: Standard -> Maybe Text
 stdURL (CStd   C11)     = Just "http://www.iso-9899.info/n1570.html"
@@ -90,6 +96,9 @@
 stdURL (LLVMRef LLVM7)  = Just "https://releases.llvm.org/7.0.0/docs/LangRef.html"
 stdURL (LLVMRef LLVM8)  = Just "https://releases.llvm.org/8.0.0/docs/LangRef.html"
 stdURL (LLVMRef LLVM12) = Just "https://releases.llvm.org/12.0.0/docs/LangRef.html"
+stdURL (LLVMRef LLVM18) = Just "https://releases.llvm.org/18.1.0/docs/LangRef.html"
+stdURL (LLVMRef LLVM19) = Just "https://releases.llvm.org/19.1.0/docs/LangRef.html"
+stdURL (LLVMRef LLVM20) = Just "https://releases.llvm.org/20.1.0/docs/LangRef.html"
 stdURL _                = Nothing
 
 ppStd :: Standard -> Text
diff --git a/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs b/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs
--- a/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs
+++ b/src/Lang/Crucible/LLVM/Errors/UndefinedBehavior.hs
@@ -20,6 +20,8 @@
 -- code essentially have an additional hypothesis: that the LLVM
 -- compiler/hardware platform behave identically to Crucible's simulator when
 -- encountering such behavior.
+--
+-- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these.
 --------------------------------------------------------------------------
 
 {-# LANGUAGE DataKinds #-}
diff --git a/src/Lang/Crucible/LLVM/Eval.hs b/src/Lang/Crucible/LLVM/Eval.hs
--- a/src/Lang/Crucible/LLVM/Eval.hs
+++ b/src/Lang/Crucible/LLVM/Eval.hs
@@ -23,6 +23,7 @@
 import           Lang.Crucible.Simulator.Evaluation
 import           Lang.Crucible.Simulator.RegValue
 import           Lang.Crucible.Simulator.SimError
+import           Lang.Crucible.Types (TypeRepr(..))
 import           Lang.Crucible.Panic (panic)
 
 import qualified Lang.Crucible.LLVM.Arch.X86 as X86
@@ -99,3 +100,14 @@
          blk <- natIte sym cond xblk yblk
          off <- bvIte sym cond xoff yoff
          return (LLVMPointer blk off)
+
+    -- These are not necessarily considered correct, see crucible#366
+    LLVM_PoisonBV w -> poisonPanic (BVRepr w)
+    LLVM_PoisonFloat fi -> poisonPanic (FloatRepr fi)
+  where
+    poisonPanic tpr =
+      panic
+        "llvmExtensionEval"
+        [ "Attempting to evaluate poison value"
+        , "Type: " ++ show tpr
+        ]
diff --git a/src/Lang/Crucible/LLVM/Extension/Syntax.hs b/src/Lang/Crucible/LLVM/Extension/Syntax.hs
--- a/src/Lang/Crucible/LLVM/Extension/Syntax.hs
+++ b/src/Lang/Crucible/LLVM/Extension/Syntax.hs
@@ -98,7 +98,18 @@
     !(f BoolType) -> !(f (LLVMPointerType w)) -> !(f (LLVMPointerType w)) ->
     LLVMExtensionExpr f (LLVMPointerType w)
 
+  -- | A @poison@ bitvector value. The semantics of this construct are still
+  -- under discussion, see crucible#366.
+  LLVM_PoisonBV ::
+    (1 <= w) => !(NatRepr w) ->
+    LLVMExtensionExpr f (BVType w)
 
+  -- | A @poison@ float value. The semantics of this construct are still under
+  -- discussion, see crucible#366.
+  LLVM_PoisonFloat ::
+    !(FloatInfoRepr fi) ->
+    LLVMExtensionExpr f (FloatType fi)
+
 -- | Extension statements for LLVM.  These statements represent the operations
 --   necessary to interact with the LLVM memory model.
 data LLVMStmt (f :: CrucibleType -> Type) :: CrucibleType -> Type where
@@ -230,43 +241,6 @@
      !(f (LLVMPointerType wptr)) {- Second pointer -} ->
      LLVMStmt f (BVType wptr)
 
-  -- | Debug information
-  LLVM_Debug ::
-    !(LLVM_Dbg f c)              {- Debug variant -} ->
-    LLVMStmt f UnitType
-
--- | Debug statement variants - these have no semantic meaning
-data LLVM_Dbg f c where
-  -- | Annotates a value pointed to by a pointer with local-variable debug information
-  --
-  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-addr>
-  LLVM_Dbg_Addr ::
-    HasPtrWidth wptr =>
-    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->
-    L.DILocalVariable            {- Local variable information -} ->
-    L.DIExpression               {- Complex expression -} ->
-    LLVM_Dbg f (LLVMPointerType wptr)
-
-  -- | Annotates a value pointed to by a pointer with local-variable debug information
-  --
-  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-declare>
-  LLVM_Dbg_Declare ::
-    HasPtrWidth wptr =>
-    !(f (LLVMPointerType wptr))  {- Pointer to local variable -} ->
-    L.DILocalVariable            {- Local variable information -} ->
-    L.DIExpression               {- Complex expression -} ->
-    LLVM_Dbg f (LLVMPointerType wptr)
-
-  -- | Annotates a value with local-variable debug information
-  --
-  -- <https://llvm.org/docs/SourceLevelDebugging.html#llvm-dbg-value>
-  LLVM_Dbg_Value ::
-    !(TypeRepr c)                {- Type of local variable -} ->
-    !(f c)                       {- Value of local variable -} ->
-    L.DILocalVariable            {- Local variable information -} ->
-    L.DIExpression               {- Complex expression -} ->
-    LLVM_Dbg f c
-
 $(return [])
 
 instance TypeApp LLVMExtensionExpr where
@@ -278,6 +252,8 @@
       LLVM_PointerBlock _ _  -> NatRepr
       LLVM_PointerOffset w _ -> BVRepr w
       LLVM_PointerIte w _ _ _ -> LLVMPointerRepr w
+      LLVM_PoisonBV w -> BVRepr w
+      LLVM_PoisonFloat fi -> FloatRepr fi
 
 instance PrettyApp LLVMExtensionExpr where
   ppApp pp e =
@@ -293,11 +269,16 @@
         pretty "pointerOffset" <+> pp ptr
       LLVM_PointerIte _ cond x y ->
         pretty "pointerIte" <+> pp cond <+> pp x <+> pp y
+      LLVM_PoisonBV _ ->
+        pretty "poisonBV"
+      LLVM_PoisonFloat _ ->
+        pretty "poisonFloat"
 
 instance TestEqualityFC LLVMExtensionExpr where
   testEqualityFC testSubterm =
     $(U.structuralTypeEquality [t|LLVMExtensionExpr|]
        [ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
+       , (U.ConType [t|FloatInfoRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        , (U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])
@@ -311,6 +292,7 @@
   compareFC testSubterm =
     $(U.structuralTypeOrd [t|LLVMExtensionExpr|]
        [ (U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
+       , (U.ConType [t|FloatInfoRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        , (U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        , (U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])
@@ -357,7 +339,6 @@
     LLVM_PtrLe{} -> knownRepr
     LLVM_PtrAddOffset w _ _ _ -> LLVMPointerRepr w
     LLVM_PtrSubtract w _ _ _ -> BVRepr w
-    LLVM_Debug{} -> knownRepr
 
 instance PrettyApp LLVMStmt where
   ppApp pp = \case
@@ -385,14 +366,7 @@
        pretty "ptrAddOffset" <+> ppGlobalVar mvar <+> pp x <+> pp y
     LLVM_PtrSubtract _ mvar x y ->
        pretty "ptrSubtract" <+> ppGlobalVar mvar <+> pp x <+> pp y
-    LLVM_Debug dbg -> ppApp pp dbg
 
-instance PrettyApp LLVM_Dbg where
-  ppApp pp = \case
-    LLVM_Dbg_Addr    x _ _ -> pretty "dbg.addr"    <+> pp x
-    LLVM_Dbg_Declare x _ _ -> pretty "dbg.declare" <+> pp x
-    LLVM_Dbg_Value _ x _ _ -> pretty "dbg.value"   <+> pp x
-
 -- TODO: move to a Pretty instance
 ppGlobalVar :: GlobalVar Mem -> Doc ann
 ppGlobalVar = viaShow
@@ -401,26 +375,6 @@
 ppAlignment :: Alignment -> Doc ann
 ppAlignment = viaShow
 
-instance TestEqualityFC LLVM_Dbg where
-  testEqualityFC testSubterm = $(U.structuralTypeEquality [t|LLVM_Dbg|]
-    [(U.DataArg 0 `U.TypeApp` U.AnyType, [|testSubterm|])
-    ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
-    ])
-
-instance OrdFC LLVM_Dbg where
-  compareFC compareSubterm = $(U.structuralTypeOrd [t|LLVM_Dbg|]
-    [(U.DataArg 0 `U.TypeApp` U.AnyType, [|compareSubterm|])
-    ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
-    ])
-
-instance FoldableFC LLVM_Dbg where
-  foldMapFC = foldMapFCDefault
-instance FunctorFC LLVM_Dbg where
-  fmapFC = fmapFCDefault
-
-instance TraversableFC LLVM_Dbg where
-  traverseFC = $(U.structuralTraversal [t|LLVM_Dbg|] [])
-
 instance TestEqualityFC LLVMStmt where
   testEqualityFC testSubterm =
     $(U.structuralTypeEquality [t|LLVMStmt|]
@@ -429,7 +383,6 @@
        ,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|testEquality|])
        ,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
        ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
-       ,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|testEqualityFC testSubterm|])
        ])
 
 instance OrdFC LLVMStmt where
@@ -440,7 +393,6 @@
        ,(U.ConType [t|GlobalVar|] `U.TypeApp` U.AnyType, [|compareF|])
        ,(U.ConType [t|CtxRepr|] `U.TypeApp` U.AnyType, [|compareF|])
        ,(U.ConType [t|TypeRepr|] `U.TypeApp` U.AnyType, [|compareF|])
-       ,(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|compareFC compareSubterm|])
        ])
 
 instance FunctorFC LLVMStmt where
@@ -451,6 +403,4 @@
 
 instance TraversableFC LLVMStmt where
   traverseFC =
-    $(U.structuralTraversal [t|LLVMStmt|]
-      [(U.ConType [t|LLVM_Dbg|] `U.TypeApp` U.DataArg 0 `U.TypeApp` U.AnyType, [|traverseFC|])
-      ])
+    $(U.structuralTraversal [t|LLVMStmt|] [])
diff --git a/src/Lang/Crucible/LLVM/Globals.hs b/src/Lang/Crucible/LLVM/Globals.hs
--- a/src/Lang/Crucible/LLVM/Globals.hs
+++ b/src/Lang/Crucible/LLVM/Globals.hs
@@ -46,7 +46,8 @@
 import           Control.Monad.IO.Class (MonadIO(..))
 import           Control.Monad.Except (MonadError(..))
 import           Control.Lens hiding (op, (:>) )
-import           Data.List (foldl', genericLength, isPrefixOf)
+import qualified Data.Foldable as Foldable
+import           Data.List (genericLength, isPrefixOf)
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
@@ -107,7 +108,7 @@
               => LLVMContext arch
               -> L.Module
               -> GlobalInitializerMap
-makeGlobalMap ctx m = foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))
+makeGlobalMap ctx m = Foldable.foldl' addAliases globalMap1 (Map.toList (llvmGlobalAliases ctx))
 
   where
    addAliases mp (glob, aliases) =
@@ -433,8 +434,8 @@
     basicBlockConstInits bb = foldMap stmtConstInits (L.bbStmts bb)
 
     stmtConstInits :: L.Stmt -> LoadRelConstInitMap
-    stmtConstInits (L.Result _ instr _) = instrConstInits instr
-    stmtConstInits (L.Effect instr _)   = instrConstInits instr
+    stmtConstInits (L.Result _ instr _ _) = instrConstInits instr
+    stmtConstInits (L.Effect instr _ _)   = instrConstInits instr
 
     instrConstInits :: L.Instr -> LoadRelConstInitMap
     instrConstInits (L.Call _ _ (L.ValSymbol fun) [ptr, _offset])
@@ -482,7 +483,8 @@
     foldLoadRelConstInitElem :: L.Global -> L.Value -> Maybe L.Value
     foldLoadRelConstInitElem global constInitElem
       | L.ValConstExpr
-          (L.ConstConv L.Trunc
+          (L.ConstConv
+            (L.Trunc False False)
             (L.Typed { L.typedValue =
               L.ValConstExpr
                 (L.ConstArith
diff --git a/src/Lang/Crucible/LLVM/Internal.hs b/src/Lang/Crucible/LLVM/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/LLVM/Internal.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeApplications #-}
+
+-- | Items in this module should /not/ be considered part of Crucible-LLVM's
+-- API, they are exported only for the sake of the test suite.
+module Lang.Crucible.LLVM.Internal
+  ( assertionsEnabled
+  ) where
+
+import qualified Control.Exception as X
+import           Data.Functor ((<&>))
+
+-- | Check if assertions are enabled.
+--
+-- Note [Asserts]: When optimizations are enabled, GHC compiles 'X.assert' to
+-- a no-op. However, Cabal enables @-O1@ by default. Therefore, if we want our
+-- assertions to be checked by our test suite, we must carefully ensure that we
+-- pass the correct flags to GHC for the @lib:crucible-llvm@ target. We verify
+-- that we have done so by asserting as much in the test suite.
+assertionsEnabled :: IO Bool
+assertionsEnabled = do
+  X.try @X.AssertionFailed (X.assert False (pure ())) <&>
+    \case
+      Left _ -> True
+      Right () -> False
diff --git a/src/Lang/Crucible/LLVM/Intrinsics.hs b/src/Lang/Crucible/LLVM/Intrinsics.hs
--- a/src/Lang/Crucible/LLVM/Intrinsics.hs
+++ b/src/Lang/Crucible/LLVM/Intrinsics.hs
@@ -26,6 +26,7 @@
 , register_llvm_overrides
 , register_llvm_overrides_
 , llvmDeclToFunHandleRepr
+, declare_overrides
 
 , module Lang.Crucible.LLVM.Intrinsics.Common
 , module Lang.Crucible.LLVM.Intrinsics.Options
diff --git a/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs b/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
--- a/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
+++ b/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs
@@ -134,7 +134,9 @@
   , SomeLLVMOverride llvmPrefetchOverride_preLLVM10
 
   , SomeLLVMOverride llvmStacksave
+  , SomeLLVMOverride llvmStacksave_preLLVM18
   , SomeLLVMOverride llvmStackrestore
+  , SomeLLVMOverride llvmStackrestore_preLLVM18
 
   , SomeLLVMOverride (llvmBSwapOverride (knownNat @2))  -- 16 = 2 * 8
   , SomeLLVMOverride (llvmBSwapOverride (knownNat @4))  -- 32 = 4 * 8
@@ -160,6 +162,22 @@
   , SomeLLVMOverride llvmSinOverride_F64
   , SomeLLVMOverride llvmCosOverride_F32
   , SomeLLVMOverride llvmCosOverride_F64
+  , SomeLLVMOverride llvmTanOverride_F32
+  , SomeLLVMOverride llvmTanOverride_F64
+  , SomeLLVMOverride llvmAsinOverride_F32
+  , SomeLLVMOverride llvmAsinOverride_F64
+  , SomeLLVMOverride llvmAcosOverride_F32
+  , SomeLLVMOverride llvmAcosOverride_F64
+  , SomeLLVMOverride llvmAtanOverride_F32
+  , SomeLLVMOverride llvmAtanOverride_F64
+  , SomeLLVMOverride llvmAtan2Override_F32
+  , SomeLLVMOverride llvmAtan2Override_F64
+  , SomeLLVMOverride llvmSinhOverride_F32
+  , SomeLLVMOverride llvmSinhOverride_F64
+  , SomeLLVMOverride llvmCoshOverride_F32
+  , SomeLLVMOverride llvmCoshOverride_F64
+  , SomeLLVMOverride llvmTanhOverride_F32
+  , SomeLLVMOverride llvmTanhOverride_F64
   , SomeLLVMOverride llvmPowOverride_F32
   , SomeLLVMOverride llvmPowOverride_F64
   , SomeLLVMOverride llvmExpOverride_F32
@@ -307,6 +325,23 @@
     , Poly1VecLLVMOverride $ \vecSz intSz ->
         SomeLLVMOverride (llvmVectorReduceUmin vecSz intSz)
     )
+
+  , ("llvm.smax"
+    , Poly1VecLLVMOverride $ \vecSz intSz ->
+        SomeLLVMOverride (llvmSmaxVector vecSz intSz)
+    )
+  , ("llvm.smin"
+    , Poly1VecLLVMOverride $ \vecSz intSz ->
+        SomeLLVMOverride (llvmSminVector vecSz intSz)
+    )
+  , ("llvm.umax"
+    , Poly1VecLLVMOverride $ \vecSz intSz ->
+        SomeLLVMOverride (llvmUmaxVector vecSz intSz)
+    )
+  , ("llvm.umin"
+    , Poly1VecLLVMOverride $ \vecSz intSz ->
+        SomeLLVMOverride (llvmUminVector vecSz intSz)
+    )
   ]
 
 ------------------------------------------------------------------------
@@ -467,17 +502,47 @@
     ovrWithBackend $ \bak ->
       liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.ubsantrap() called" "")
 
+-- | TODO(#130): This override ought to impose proof obligations related to
+-- proper block scoping.
 llvmStacksave
   :: (IsSymInterface sym, HasPtrWidth wptr)
   => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr)
 llvmStacksave =
+  [llvmOvr| i8* @llvm.stacksave.p0() |]
+  (\_memOps _args -> mkNull)
+
+-- | TODO(#130): This override ought to impose proof obligations related to
+-- proper block scoping.
+--
+-- See also 'llvmStacksave'. This version exists for compatibility with
+-- pre-18 versions of LLVM, where @llvm.stacksave@ always assumed that the
+-- returned pointer value resides in address space 0.
+llvmStacksave_preLLVM18
+  :: (IsSymInterface sym, HasPtrWidth wptr)
+  => LLVMOverride p sym ext EmptyCtx (LLVMPointerType wptr)
+llvmStacksave_preLLVM18 =
   [llvmOvr| i8* @llvm.stacksave() |]
   (\_memOps _args -> mkNull)
 
+-- | TODO(#130): This override ought to impose proof obligations related to
+-- proper block scoping.
 llvmStackrestore
   :: (IsSymInterface sym, HasPtrWidth wptr)
   => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType
 llvmStackrestore =
+  [llvmOvr| void @llvm.stackrestore.p0( i8* ) |]
+  (\_memOps _args -> return ())
+
+-- | TODO(#130): This override ought to impose proof obligations related to
+-- proper block scoping.
+--
+-- See also 'llvmStackrestore'. This version exists for compatibility with
+-- pre-18 versions of LLVM, where @llvm.stackrestore@ always assumed that the
+-- pointer argument resides in address space 0.
+llvmStackrestore_preLLVM18
+  :: (IsSymInterface sym, HasPtrWidth wptr)
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) UnitType
+llvmStackrestore_preLLVM18 =
   [llvmOvr| void @llvm.stackrestore( i8* ) |]
   (\_memOps _args -> return ())
 
@@ -1159,6 +1224,150 @@
   [llvmOvr| double @llvm.cos.f64( double ) |]
   (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cos) args)
 
+llvmTanOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmTanOverride_F32 =
+  [llvmOvr| float @llvm.tan.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tan) args)
+
+llvmTanOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmTanOverride_F64 =
+  [llvmOvr| double @llvm.tan.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tan) args)
+
+llvmAsinOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmAsinOverride_F32 =
+  [llvmOvr| float @llvm.asin.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arcsin) args)
+
+llvmAsinOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmAsinOverride_F64 =
+  [llvmOvr| double @llvm.asin.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arcsin) args)
+
+llvmAcosOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmAcosOverride_F32 =
+  [llvmOvr| float @llvm.acos.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arccos) args)
+
+llvmAcosOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmAcosOverride_F64 =
+  [llvmOvr| double @llvm.acos.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arccos) args)
+
+llvmAtanOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmAtanOverride_F32 =
+  [llvmOvr| float @llvm.atan.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arctan) args)
+
+llvmAtanOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmAtanOverride_F64 =
+  [llvmOvr| double @llvm.atan.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Arctan) args)
+
+llvmSinhOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmSinhOverride_F32 =
+  [llvmOvr| float @llvm.sinh.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sinh) args)
+
+llvmSinhOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmSinhOverride_F64 =
+  [llvmOvr| double @llvm.sinh.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Sinh) args)
+
+llvmCoshOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmCoshOverride_F32 =
+  [llvmOvr| float @llvm.cosh.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cosh) args)
+
+llvmCoshOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmCoshOverride_F64 =
+  [llvmOvr| double @llvm.cosh.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Cosh) args)
+
+llvmTanhOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmTanhOverride_F32 =
+  [llvmOvr| float @llvm.tanh.f32( float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tanh) args)
+
+llvmTanhOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmTanhOverride_F64 =
+  [llvmOvr| double @llvm.tanh.f64( double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 W4.Tanh) args)
+
+llvmAtan2Override_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
+     (FloatType SingleFloat)
+llvmAtan2Override_F32 =
+  [llvmOvr| float @llvm.atan2.f32( float, float ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Arctan2) args)
+
+llvmAtan2Override_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym ext
+     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
+     (FloatType DoubleFloat)
+llvmAtan2Override_F64 =
+  [llvmOvr| double @llvm.atan2.f64( double, double ) |]
+  (\_memOps args -> Ctx.uncurryAssignment (Libc.callSpecialFunction2 W4.Arctan2) args)
+
 llvmPowOverride_F32 ::
   IsSymInterface sym =>
   LLVMOverride p sym ext
@@ -1469,6 +1678,67 @@
         (BVType intSz)
 llvmVectorReduceUmin = llvmVectorReduce "umin" callVectorReduceUmin
 
+-- | Build an 'LLVMOverride' for a vector map intrinsic.
+llvmVectorMap ::
+  (1 <= intSz) =>
+  -- | The name of the operation to map (@umin@, @smin@, etc.).
+  String ->
+  -- | The semantics of the override.
+  (forall r args ret.
+    IsSymInterface sym =>
+    RegEntry sym (VectorType (BVType intSz)) ->
+    RegEntry sym (VectorType (BVType intSz)) ->
+    OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))) ->
+  -- | The size of the vector type.
+  NatRepr vecSz ->
+  -- | The size of the integer type.
+  NatRepr intSz ->
+  LLVMOverride p sym ext
+    (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))
+    (VectorType (BVType intSz))
+llvmVectorMap opName callMap vecSz intSz =
+  let nm = L.Symbol ("llvm." ++ opName ++
+                     ".v" ++ show (natValue vecSz) ++
+                     "i" ++ show (natValue intSz)) in
+    [llvmOvr| <#vecSz x #intSz> $nm( <#vecSz x #intSz>, <#vecSz x #intSz> ) |]
+    (\_memOps args -> Ctx.uncurryAssignment callMap args)
+
+llvmSmaxVector ::
+  (1 <= intSz) =>
+  NatRepr vecSz ->
+  NatRepr intSz ->
+  LLVMOverride p sym ext
+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))
+     (VectorType (BVType intSz))
+llvmSmaxVector = llvmVectorMap "smax" callVectorMapSmax
+
+llvmSminVector ::
+  (1 <= intSz) =>
+  NatRepr vecSz ->
+  NatRepr intSz ->
+  LLVMOverride p sym ext
+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))
+     (VectorType (BVType intSz))
+llvmSminVector = llvmVectorMap "smin" callVectorMapSmin
+
+llvmUmaxVector ::
+  (1 <= intSz) =>
+  NatRepr vecSz ->
+  NatRepr intSz ->
+  LLVMOverride p sym ext
+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))
+     (VectorType (BVType intSz))
+llvmUmaxVector = llvmVectorMap "umax" callVectorMapUmax
+
+llvmUminVector ::
+  (1 <= intSz) =>
+  NatRepr vecSz ->
+  NatRepr intSz ->
+  LLVMOverride p sym ext
+     (EmptyCtx ::> VectorType (BVType intSz) ::> VectorType (BVType intSz))
+     (VectorType (BVType intSz))
+llvmUminVector = llvmVectorMap "umin" callVectorMapUmin
+
 ------------------------------------------------------------------------
 -- ** Implementations
 
@@ -1933,8 +2203,8 @@
 callIsFpclass regOp@(regValue -> op) (regValue -> test) = do
   sym <- getSymInterface
   let w1 = knownNat @1
-  bv1 <- liftIO $ bvZero sym w1
-  bv0 <- liftIO $ bvOne sym w1
+  bv1 <- liftIO $ bvOne sym w1
+  bv0 <- liftIO $ bvZero sym w1
 
   let negative bit = liftIO $ do
         isNeg <- iFloatIsNeg @_ @fi sym op
@@ -2140,3 +2410,52 @@
   sym <- getSymInterface
   umax <- liftIO $ maxUnsignedBV sym intSz
   callVectorReduce (bvUmin sym) umax vec
+
+-- | The semantics of an LLVM vector map intrinsic.
+callVectorMap ::
+  -- | The operation to apply when mapping (e.g., @umin@, @smin@, etc.)
+  (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp)) ->
+  -- | The first vector to map over.
+  RegEntry sym (VectorType tp) ->
+  -- | The second vector to map over.
+  RegEntry sym (VectorType tp) ->
+  -- | The result of mapping over the vectors.
+  OverrideSim p sym ext r args ret (V.Vector (RegValue sym tp))
+callVectorMap mapOp (regValue -> vec1) (regValue -> vec2) =
+  liftIO $ V.zipWithM mapOp vec1 vec2
+
+callVectorMapSmax ::
+  (IsSymInterface sym, 1 <= intSz) =>
+  RegEntry sym (VectorType (BVType intSz)) ->
+  RegEntry sym (VectorType (BVType intSz)) ->
+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+callVectorMapSmax vec1 vec2 = do
+  sym <- getSymInterface
+  callVectorMap (bvSmax sym) vec1 vec2
+
+callVectorMapSmin ::
+  (IsSymInterface sym, 1 <= intSz) =>
+  RegEntry sym (VectorType (BVType intSz)) ->
+  RegEntry sym (VectorType (BVType intSz)) ->
+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+callVectorMapSmin vec1 vec2 = do
+  sym <- getSymInterface
+  callVectorMap (bvSmin sym) vec1 vec2
+
+callVectorMapUmax ::
+  (IsSymInterface sym, 1 <= intSz) =>
+  RegEntry sym (VectorType (BVType intSz)) ->
+  RegEntry sym (VectorType (BVType intSz)) ->
+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+callVectorMapUmax vec1 vec2 = do
+  sym <- getSymInterface
+  callVectorMap (bvUmax sym) vec1 vec2
+
+callVectorMapUmin ::
+  (IsSymInterface sym, 1 <= intSz) =>
+  RegEntry sym (VectorType (BVType intSz)) ->
+  RegEntry sym (VectorType (BVType intSz)) ->
+  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+callVectorMapUmin vec1 vec2 = do
+  sym <- getSymInterface
+  callVectorMap (bvUmin sym) vec1 vec2
diff --git a/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs b/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
--- a/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
+++ b/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs
@@ -65,6 +65,7 @@
 import qualified Lang.Crucible.LLVM.MemModel.Generic as G
 import           Lang.Crucible.LLVM.MemModel.Partial
 import qualified Lang.Crucible.LLVM.MemModel.Pointer as Ptr
+import           Lang.Crucible.LLVM.MemModel.Strings as CStr
 import           Lang.Crucible.LLVM.Printf
 import           Lang.Crucible.LLVM.QQ( llvmOvr )
 import           Lang.Crucible.LLVM.TypeContext
@@ -94,6 +95,10 @@
   , SomeLLVMOverride llvmFreeOverride
   , SomeLLVMOverride llvmReallocOverride
   , SomeLLVMOverride llvmStrlenOverride
+  , SomeLLVMOverride llvmStrnlenOverride
+  , SomeLLVMOverride llvmStrcpyOverride
+  , SomeLLVMOverride llvmStrdupOverride
+  , SomeLLVMOverride llvmStrndupOverride
   , SomeLLVMOverride llvmPrintfOverride
   , SomeLLVMOverride llvmPrintfChkOverride
   , SomeLLVMOverride llvmPutsOverride
@@ -391,6 +396,38 @@
   [llvmOvr| size_t @strlen( i8* ) |]
   (\memOps args -> Ctx.uncurryAssignment (callStrlen memOps) args)
 
+llvmStrnlenOverride
+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
+     , ?memOpts :: MemOptions )
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (BVType wptr)
+llvmStrnlenOverride =
+  [llvmOvr| size_t @strnlen( i8*, size_t ) |]
+  (\memOps args -> Ctx.uncurryAssignment (callStrnlen memOps) args)
+
+llvmStrcpyOverride
+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
+     , ?memOpts :: MemOptions )
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> LLVMPointerType wptr) (LLVMPointerType wptr)
+llvmStrcpyOverride =
+  [llvmOvr| i8* @strcpy( i8*, i8* ) |]
+  (\memOps args -> Ctx.uncurryAssignment (callStrcpy memOps) args)
+
+llvmStrdupOverride
+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
+     , ?memOpts :: MemOptions )
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr) (LLVMPointerType wptr)
+llvmStrdupOverride =
+  [llvmOvr| i8* @strdup( i8* ) |]
+  (\memOps args -> Ctx.uncurryAssignment (callStrdup memOps) args)
+
+llvmStrndupOverride
+  :: ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr
+     , ?memOpts :: MemOptions )
+  => LLVMOverride p sym ext (EmptyCtx ::> LLVMPointerType wptr ::> BVType wptr) (LLVMPointerType wptr)
+llvmStrndupOverride =
+  [llvmOvr| i8* @strndup( i8*, size_t ) |]
+  (\memOps args -> Ctx.uncurryAssignment (callStrndup memOps) args)
+
 ------------------------------------------------------------------------
 -- ** Implementations
 
@@ -596,7 +633,7 @@
   (regValue -> strPtr) =
     ovrWithBackend $ \bak -> do
       mem <- readGlobal mvar
-      str <- liftIO $ loadString bak mem strPtr Nothing
+      str <- liftIO $ CStr.loadString bak mem strPtr Nothing
       h <- printHandle <$> getContext
       liftIO $ hPutStrLn h (UTF8.toString str)
       -- return non-negative value on success
@@ -613,6 +650,66 @@
     mem <- readGlobal mvar
     liftIO $ strLen bak mem strPtr
 
+callStrnlen
+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
+     , ?memOpts :: MemOptions )
+  => GlobalVar Mem
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> RegEntry sym (BVType wptr)
+  -> OverrideSim p sym ext r args ret (RegValue sym (BVType wptr))
+callStrnlen mvar (regValue -> strPtr) (regValue -> bound) =
+  ovrWithBackend $ \bak -> do
+    mem <- readGlobal mvar
+    liftIO $ CStr.strnlen bak mem strPtr bound
+
+callStrcpy
+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
+     , ?memOpts :: MemOptions )
+  => GlobalVar Mem
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
+callStrcpy mvar (regValue -> dst) (regValue -> src) =
+  ovrWithBackend $ \bak ->
+    modifyGlobal mvar $ \mem -> do
+      mem' <- liftIO $ CStr.copyConcretelyNullTerminatedString bak mem dst src Nothing
+      pure (dst, mem')
+
+callStrdup
+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
+     , ?memOpts :: MemOptions )
+  => GlobalVar Mem
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
+callStrdup mvar (regValue -> src) =
+  ovrWithBackend $ \bak ->
+    modifyGlobal mvar $ \mem -> liftIO $ do
+      let sym = backendGetSym bak
+      loc <- plSourceLoc <$> getCurrentProgramLoc sym
+      let loc' = "<strdup> " ++ show loc
+      CStr.dupConcretelyNullTerminatedString bak mem src Nothing loc' noAlignment
+
+callStrndup
+  :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
+     , ?memOpts :: MemOptions )
+  => GlobalVar Mem
+  -> RegEntry sym (LLVMPointerType wptr)
+  -> RegEntry sym (BVType wptr)
+  -> OverrideSim p sym ext r args ret (RegValue sym (LLVMPointerType wptr))
+callStrndup mvar (regValue -> src) (regValue -> bound) =
+  ovrWithBackend $ \bak ->
+    modifyGlobal mvar $ \mem -> liftIO $ do
+      let sym = backendGetSym bak
+      loc <- plSourceLoc <$> getCurrentProgramLoc sym
+      let loc' = "<strndup> " ++ show loc
+      case BV.asUnsigned <$> asBV bound of
+        Nothing -> do
+          let err = AssertFailureSimError "`strndup` called with symbolic max length" ""
+          addFailedAssertion bak err
+        Just b ->
+          let bound' = Just (fromIntegral b) in
+          CStr.dupConcretelyNullTerminatedString bak mem src bound' loc' noAlignment
+
 callAssert
   :: ( IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym
      , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions )
@@ -629,7 +726,7 @@
     let sym = backendGetSym bak
     when failUponExit $
       do mem <- readGlobal mvar
-         txt <- liftIO $ loadString bak mem (regValue ptxt) Nothing
+         txt <- liftIO $ CStr.loadString bak mem (regValue ptxt) Nothing
          let err = AssertFailureSimError "Call to assert()" (UTF8.toString txt)
          liftIO $ addFailedAssertion bak err
     liftIO $
@@ -667,7 +764,7 @@
   (regValue -> valist) =
     ovrWithBackend $ \bak -> do
       mem <- readGlobal mvar
-      formatStr <- liftIO $ loadString bak mem strPtr Nothing
+      formatStr <- liftIO $ CStr.loadString bak mem strPtr Nothing
       case parseDirectives formatStr of
         Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err
         Right ds -> do
@@ -731,7 +828,7 @@
      case valist V.!? (i-1) of
        Just (AnyValue PtrRepr ptr) ->
            do mem <- get
-              liftIO $ loadString bak mem ptr numchars
+              liftIO $ CStr.loadString bak mem ptr numchars
        Just (AnyValue tpr _) ->
          lift $ addFailedAssertion bak
               $ AssertFailureSimError
diff --git a/src/Lang/Crucible/LLVM/MemModel.hs b/src/Lang/Crucible/LLVM/MemModel.hs
--- a/src/Lang/Crucible/LLVM/MemModel.hs
+++ b/src/Lang/Crucible/LLVM/MemModel.hs
@@ -46,6 +46,8 @@
   , IndeterminateLoadBehavior(..)
   , defaultMemOptions
   , laxPointerMemOptions
+  , ppLLVMMemIntrinsicType
+  , ppLLVMIntrinsicTypes
 
   -- * Pointers
   , LLVMPointerType
@@ -83,9 +85,15 @@
   , doArrayStoreUnbounded
   , doArrayConstStore
   , doArrayConstStoreUnbounded
-  , loadString
-  , loadMaybeString
-  , strLen
+  -- TODO(#1308): When GHC 9.6 support is dropped, deprecate these imports
+  -- TOOD(#1406): After they have been deprecated for a while, move the
+  -- implementations to `Strings` and remove these exports.
+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}
+    loadString
+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}
+    loadMaybeString
+  , -- {-# DEPRECATED "Exported from Crucible.LLVM.MemModel.Strings instead" #-}
+    strLen
   , uncheckedMemcpy
 
     -- * \"Raw\" operations with LLVMVal
@@ -194,7 +202,6 @@
 import           Control.Monad.IO.Class
 import           Control.Monad.Trans (lift)
 import           Control.Monad.Trans.State
-import           Data.Dynamic
 import           Data.IORef
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -203,6 +210,7 @@
 import           Data.Word
 import qualified GHC.Stack as GHC
 import           Numeric.Natural (Natural)
+import qualified Prettyprinter as PP
 import           System.IO (Handle, hPutStrLn)
 
 import qualified Data.BitVector.Sized as BV
@@ -270,7 +278,7 @@
   { memImplBlockSource :: BlockSource
   , memImplGlobalMap   :: GlobalMap sym
   , memImplSymbolMap   :: Map Natural L.Symbol -- inverse mapping to 'memImplGlobalMap'
-  , memImplHandleMap   :: Map Natural Dynamic
+  , memImplHandleMap   :: Map Natural SomeFnHandle
   , memImplHeap        :: G.Mem sym
   }
 
@@ -353,6 +361,34 @@
         --putStrLn "MEM ABORT BRANCH"
         return $ MemImpl nxt gMap sMap hMap $ G.branchAbortMem m
 
+-- | An intrinsic-printing function for 'MemImpl' for use with
+-- 'Lang.Crucible.Types.ppTypeRepr'.
+ppLLVMMemIntrinsicType ::
+  Applicative f =>
+  -- | Fallback for other instrinsics, can be
+  -- 'Lang.Crucible.Types.ppIntrinsicDefault'.
+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) ->
+  SymbolRepr symb ->
+  CtxRepr ctx ->
+  f (PP.Doc ann)
+ppLLVMMemIntrinsicType fallback symbRepr tyCtx =
+  case testEquality symbRepr (knownSymbol @"LLVM_memory") of
+    Nothing -> fallback symbRepr tyCtx
+    Just Refl -> pure "LLVMMemory"
+
+-- | An intrinsic-printing function for the LLVM intrinsic types for use with
+-- 'Lang.Crucible.Types.ppTypeRepr'.
+ppLLVMIntrinsicTypes ::
+  Applicative f =>
+  -- | Fallback for other instrinsics, can be
+  -- 'Lang.Crucible.Types.ppIntrinsicDefault'.
+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) ->
+  SymbolRepr symb ->
+  CtxRepr ctx ->
+  f (PP.Doc ann)
+ppLLVMIntrinsicTypes fallback =
+  ppLLVMMemIntrinsicType (ppLLVMPointerIntrinsicType fallback)
+
 -- | Top-level evaluation function for LLVM extension statements.
 --   LLVM extension statements are used to implement the memory model operations.
 llvmStatementExec ::
@@ -527,9 +563,7 @@
     do mem <- getMem mvar
        liftIO $ doPtrSubtract bak mem x y
 
-  eval LLVM_Debug{} = pure ()
 
-
 mkMemVar :: Text
          -> HandleAllocator
          -> IO (GlobalVar Mem)
@@ -713,16 +747,16 @@
 --
 -- See also "Lang.Crucible.LLVM.Functions".
 doInstallHandle
-  :: (Typeable a, IsSymBackend sym bak)
+  :: IsSymBackend sym bak
   => bak
   -> LLVMPtr sym wptr
-  -> a {- ^ handle -}
+  -> SomeFnHandle
   -> MemImpl sym
   -> IO (MemImpl sym)
-doInstallHandle _bak ptr x mem =
+doInstallHandle _bak ptr hdl mem =
   case asNat (llvmPointerBlock ptr) of
     Just blkNum ->
-      do let hMap' = Map.insert blkNum (toDyn x) (memImplHandleMap mem)
+      do let hMap' = Map.insert blkNum hdl (memImplHandleMap mem)
          return mem{ memImplHandleMap = hMap' }
     Nothing ->
       panic "MemModel.doInstallHandle"
@@ -732,11 +766,11 @@
 
 -- | Look up the handle associated with the given pointer, if any.
 doLookupHandle
-  :: (Typeable a, IsSymInterface sym)
+  :: IsSymInterface sym
   => sym
   -> MemImpl sym
   -> LLVMPtr sym wptr
-  -> IO (Either ME.FuncLookupError a)
+  -> IO (Either ME.FuncLookupError SomeFnHandle)
 doLookupHandle _sym mem ptr = do
   let LLVMPointer blk _ = ptr
   case asNat blk of
@@ -746,10 +780,7 @@
       | otherwise ->
           case Map.lookup i (memImplHandleMap mem) of
             Nothing -> return (Left ME.NoOverride)
-            Just x ->
-              case fromDynamic x of
-                Nothing -> return (Left (ME.Uncallable (dynTypeRep x)))
-                Just a  -> return (Right a)
+            Just hdl -> return (Right hdl)
 
 -- | Free the memory region pointed to by the given pointer.
 --
@@ -1558,6 +1589,13 @@
     , "*** Undef value: " ++ show v
     ]
 
+unpackMemValue _ tpr v@(LLVMValPoison _) =
+  panic "MemModel.unpackMemValue"
+    [ "Cannot unpack a `poison` value"
+    , "*** Crucible type: " ++ show tpr
+    , "*** Poison value: " ++ show v
+    ]
+
 unpackMemValue _ tpr v =
   panic "MemModel.unpackMemValue"
     [ "Crucible type mismatch when unpacking LLVM value"
@@ -1770,6 +1808,8 @@
   LLVMValZero <$> toStorableType memty
 constToLLVMValP _sym _look (UndefConst memty) = liftIO $
   LLVMValUndef <$> toStorableType memty
+constToLLVMValP _sym _look (PoisonConst memty) = liftIO $
+  LLVMValPoison <$> toStorableType memty
 
 
 -- | Translate a constant into an LLVM runtime value. Assumes all necessary
diff --git a/src/Lang/Crucible/LLVM/MemModel/Common.hs b/src/Lang/Crucible/LLVM/MemModel/Common.hs
--- a/src/Lang/Crucible/LLVM/MemModel/Common.hs
+++ b/src/Lang/Crucible/LLVM/MemModel/Common.hs
@@ -467,8 +467,10 @@
         let d = lo - so
         -- Store is before load.
         valueLoad lo ltp lo (SelectSuffixBV d (sw - d) v)
-      | otherwise -> assert (lo == so && lw < sw) $
+      | otherwise ->
+        -- TODO(#1560): This assertion can fail.
         -- Load ends before store ends.
+        -- assert (lo == so && lw < sw) $
         valueLoad lo ltp so (SelectPrefixBV lw (sw - lw) v)
     Float -> valueLoad lo ltp so (FloatToBV v)
     Double -> valueLoad lo ltp so (DoubleToBV v)
@@ -511,8 +513,10 @@
   ValueView {- ^ view of stored value -} ->
   ValueCtor (ValueLoad Addr)
 valueLoad lo ltp so v
-  | le <= so = ValueCtorVar (OldMemory lo ltp) -- Load ends before store
-  | se <= lo = ValueCtorVar (OldMemory lo ltp) -- Store ends before load
+  -- The non-zero test ensures that 0-byte loads are always overlapping
+  -- with the most recent store so that they're not spuriously rejected.
+  | le <= so && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Load ends before store
+  | se <= lo && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Store ends before load
     -- Load is before store.
   | lo < so  = splitTypeValue ltp (so - lo) (\o tp -> valueLoad (lo+o) tp so v)
     -- Load ends after store ends.
@@ -534,6 +538,7 @@
  where stp = fromMaybe (error ("Coerce value given bad view " ++ show v)) (viewType v)
        le = typeEnd lo ltp
        se = so + storageTypeSize stp
+       nonZeroLoad = le - lo > 0
 
 -- | @LinearLoadStoreOffsetDiff stride delta@ represents the fact that
 --   the difference between the load offset and the store offset is
diff --git a/src/Lang/Crucible/LLVM/MemModel/Generic.hs b/src/Lang/Crucible/LLVM/MemModel/Generic.hs
--- a/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+++ b/src/Lang/Crucible/LLVM/MemModel/Generic.hs
@@ -76,6 +76,7 @@
 
 import           Prelude hiding (pred)
 
+import qualified Control.Exception as X
 import           Control.Lens
 import           Control.Monad
 import           Control.Monad.State.Strict
@@ -91,6 +92,7 @@
 import           Numeric.Natural
 import           Prettyprinter
 import           Lang.Crucible.Panic (panic)
+import qualified Data.Vector as V
 
 import           Data.BitVector.Sized (BV)
 import qualified Data.BitVector.Sized as BV
@@ -695,6 +697,21 @@
       | otherwise
       = liftIO (Partial.partErr sym mop $ Invalidated msg)
 
+-- | Construct a value of a type that has no in-memory representation at all
+buildEmptyVal :: StorageType -> Maybe (LLVMVal sym)
+buildEmptyVal t =
+  case storageTypeF t of
+    Struct fields   -> LLVMValStruct <$> traverse emptyStorageField fields
+    Array n eltTy
+      | n == 0      -> Just (LLVMValArray eltTy V.empty)
+      | otherwise   -> LLVMValArray eltTy . V.replicate (fromIntegral n) <$> buildEmptyVal eltTy
+    X86_FP80        -> Nothing
+    Float           -> Nothing
+    Double          -> Nothing
+    Bitvector {}    -> Nothing -- Bitvectors can't be empty; they have a non-zero size invariant
+  where
+    emptyStorageField field = (,) field <$> buildEmptyVal (field ^. fieldVal)
+
 -- | Read a value from memory.
 readMem :: forall sym w.
   ( 1 <= w, IsSymInterface sym, HasLLVMAnn sym
@@ -707,6 +724,12 @@
   Alignment ->
   Mem sym ->
   IO (PartLLVMVal sym)
+readMem sym _ _ _ tp _ _
+  -- no actual memory read happens when reading a value with
+  -- no memory representation. This check comes up in
+  -- particular when evaluating llvm_points_to statements
+  -- in SAW script.
+  | Just v <- buildEmptyVal tp = pure (Partial.totalLLVMVal sym v)
 readMem sym w gsym l tp alignment m = do
   sz         <- bvLit sym w (bytesToBV w (typeEnd 0 tp))
   p1         <- isAllocated sym w alignment l (Just sz) m
@@ -1584,21 +1607,43 @@
     isHeapMutable (AllocInfo HeapAlloc _ Mutable _ _) = pure (truePred sym)
     isHeapMutable _ = pure (falsePred sym)
 
+-- | Prepare memory so that it can later be merged via 'mergeMem'.
+--
+-- This is primarily intended for use in the implementation of
+-- 'Lang.Crucible.Simulator.Intrinsics.pushBranchIntrinsic' for LLVM memory.
+-- It would be nice to remove this someday, see #890.
+--
+-- For more information about branching and merging, see the comment on 'Mem'.
 branchMem :: Mem sym -> Mem sym
 branchMem = memState %~ \s ->
   BranchFrame (memStateAllocCount s) (memStateWriteCount s) emptyChanges s
 
+-- | Remove the top 'BranchFrame', adding changes to the underlying memory.
+--
+-- This is primarily intended for use in the implementation of
+-- 'Lang.Crucible.Simulator.Intrinsics.abortBranchIntrinsic' for LLVM memory.
 branchAbortMem :: Mem sym -> Mem sym
 branchAbortMem = memState %~ popf
   where popf (BranchFrame _ _ c s) = s & memStateAddChanges c
         popf _ = error "branchAbortMem given unexpected memory"
 
+-- | Merge memory that was previously prepared via 'branchMem'.
+--
+-- This is primarily intended for use in the implementation of
+-- 'Lang.Crucible.Simulator.Intrinsics.muxIntrinsic' for LLVM memory.
+--
+-- For more information about branching and merging, see the comment on 'Mem'.
 mergeMem :: IsExpr (SymExpr sym) => Pred sym -> Mem sym -> Mem sym -> Mem sym
 mergeMem c x y =
   case (x^.memState, y^.memState) of
-    (BranchFrame _ _ a s, BranchFrame _ _ b _) ->
-      let s' = s & memStateAddChanges (muxChanges c a b)
-      in x & memState .~ s'
+    (BranchFrame _ _ a s, BranchFrame _ _ b s') ->
+      -- The memories to be merged must have originated from the same memory,
+      -- and in particular, should have matching alloc/write counts.
+      let allocsEq = memStateAllocCount s == memStateAllocCount s' in
+      let writesEq = memStateWriteCount s == memStateWriteCount s' in
+      X.assert (allocsEq && writesEq) $
+        let s' = s & memStateAddChanges (muxChanges c a b)
+        in x & memState .~ s'
     _ -> error "mergeMem given unexpected memories"
 
 --------------------------------------------------------------------------------
diff --git a/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
--- a/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
+++ b/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
@@ -344,8 +344,12 @@
     -- of the list.
   | StackFrame !Int !Int Text (MemChanges sym) (MemState sym)
     -- | Represents a push of a branch frame, and changes since that branch.
+    --
     -- Changes are stored in order, with more recent changes closer to the head
     -- of the list.
+    --
+    -- For more information about branching and merging, see the comment on
+    -- 'Mem'.
   | BranchFrame !Int !Int (MemChanges sym) (MemState sym)
 
 type MemChanges sym = (MemAllocs sym, MemWrites sym)
@@ -672,7 +676,9 @@
 concLLVMVal _ _ v@LLVMValString{} = pure v
 concLLVMVal _ _ v@LLVMValZero{} = pure v
 concLLVMVal _ _ (LLVMValUndef st) =
-  pure (LLVMValZero st) -- ??? does it make sense to turn Undef into Zero?
+  pure (LLVMValUndef st)
+concLLVMVal _ _ (LLVMValPoison st) =
+  pure (LLVMValPoison st)
 
 
 concWriteSource ::
diff --git a/src/Lang/Crucible/LLVM/MemModel/Partial.hs b/src/Lang/Crucible/LLVM/MemModel/Partial.hs
--- a/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+++ b/src/Lang/Crucible/LLVM/MemModel/Partial.hs
@@ -381,6 +381,9 @@
 floatToBV _ _ (NoErr p (LLVMValUndef (StorageType Float _))) =
   return (NoErr p (LLVMValUndef (Type.bitvectorType 4)))
 
+floatToBV _ _ (NoErr p (LLVMValPoison (StorageType Float _))) =
+  return (NoErr p (LLVMValPoison (Type.bitvectorType 4)))
+
 floatToBV sym _ (NoErr p (LLVMValZero (StorageType Float _))) =
   do nz <- W4I.natLit sym 0
      iz <- W4I.bvZero sym (knownNat @32)
@@ -407,6 +410,9 @@
 doubleToBV _ _ (NoErr p (LLVMValUndef (StorageType Double _))) =
   return (NoErr p (LLVMValUndef (Type.bitvectorType 8)))
 
+doubleToBV _ _ (NoErr p (LLVMValPoison (StorageType Double _))) =
+  return (NoErr p (LLVMValPoison (Type.bitvectorType 8)))
+
 doubleToBV sym _ (NoErr p (LLVMValZero (StorageType Double _))) =
   do nz <- W4I.natLit sym 0
      iz <- W4I.bvZero sym (knownNat @64)
@@ -433,6 +439,9 @@
 fp80ToBV _ _ (NoErr p (LLVMValUndef (StorageType X86_FP80 _))) =
   return (NoErr p (LLVMValUndef (Type.bitvectorType 10)))
 
+fp80ToBV _ _ (NoErr p (LLVMValPoison (StorageType X86_FP80 _))) =
+  return (NoErr p (LLVMValPoison (Type.bitvectorType 10)))
+
 fp80ToBV sym _ (NoErr p (LLVMValZero (StorageType X86_FP80 _))) =
   do nz <- W4I.natLit sym 0
      iz <- W4I.bvLit sym (knownNat @80) (BV.zero knownNat)
@@ -937,6 +946,12 @@
                                           , "Undef type: " ++ show tpu
                                           ]
 
+      LLVMValPoison tpp ->
+        -- TODO: Is this the right behavior?
+        panic "Cannot mux zero and poison" [ "Zero type: " ++ show tpz
+                                           , "Poison type: " ++ show tpp
+                                           ]
+
       LLVMValString bs -> muxzero cond tpz =<< Value.explodeStringValue sym bs
 
       LLVMValInt base off ->
@@ -1007,6 +1022,9 @@
           LLVMValArray tp1 <$> V.zipWithM (muxval cond) v1 v2
 
     muxval _ v1@(LLVMValUndef tp1) (LLVMValUndef tp2)
+      | tp1 == tp2 = pure v1
+
+    muxval _ v1@(LLVMValPoison tp1) (LLVMValPoison tp2)
       | tp1 == tp2 = pure v1
 
     muxval _ v1 v2 =
diff --git a/src/Lang/Crucible/LLVM/MemModel/Pointer.hs b/src/Lang/Crucible/LLVM/MemModel/Pointer.hs
--- a/src/Lang/Crucible/LLVM/MemModel/Pointer.hs
+++ b/src/Lang/Crucible/LLVM/MemModel/Pointer.hs
@@ -78,6 +78,7 @@
 
     -- * Pretty printing
   , ppPtr
+  , ppLLVMPointerIntrinsicType
 
     -- * Annotation
   , annotatePointerBlock
@@ -89,6 +90,7 @@
 import qualified Data.Map as Map (lookup)
 import           Numeric.Natural
 import           Prettyprinter
+import qualified Prettyprinter as PP
 
 import           GHC.TypeLits (TypeError, ErrorMessage(..))
 import           GHC.TypeNats
@@ -250,10 +252,14 @@
        panic "LLVM.MemModel.Pointer.concPtrFn"
          [ "Impossible: LLVMPointerType ill-formed context" ]
 
+-- | Helper, not exported
+ptrSymb :: SymbolRepr "LLVM_pointer"
+ptrSymb = knownSymbol
+
 -- | A singleton map suitable for use in a 'Conc.ConcCtx' if LLVM pointers are
 -- the only intrinsic type in use
 concPtrFnMap :: MapF.MapF SymbolRepr (Conc.IntrinsicConcFn t)
-concPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concPtrFn
+concPtrFnMap = MapF.singleton ptrSymb concPtrFn
 
 -- | A 'Conc.IntrinsicConcToSymFn' for LLVM pointers
 concToSymPtrFn :: Conc.IntrinsicConcToSymFn "LLVM_pointer"
@@ -272,7 +278,7 @@
 -- | A singleton map suitable for use in 'Crucible.Concretize.concToSym' if LLVM
 -- pointers are the only intrinsic type in use
 concToSymPtrFnMap :: MapF.MapF SymbolRepr Conc.IntrinsicConcToSymFn
-concToSymPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concToSymPtrFn
+concToSymPtrFnMap = MapF.singleton ptrSymb concToSymPtrFn
 
 -- | Mux function specialized to LLVM pointer values.
 muxLLVMPtr ::
@@ -424,6 +430,33 @@
      let blk_doc = printSymNat blk
          off_doc = printSymExpr bv
       in pretty "(" <> blk_doc <> pretty "," <+> off_doc <> pretty ")"
+
+-- | An intrinsic-printing function for use with
+-- 'Lang.Crucible.Types.ppTypeRepr'.
+ppLLVMPointerIntrinsicType ::
+  Applicative f =>
+  -- | Fallback for other instrinsics, can be
+  -- 'Lang.Crucible.Types.ppIntrinsicDefault'.
+  (forall s ctx'. SymbolRepr s -> CtxRepr ctx' -> f (PP.Doc ann)) ->
+  SymbolRepr symb ->
+  CtxRepr ctx ->
+  f (PP.Doc ann)
+ppLLVMPointerIntrinsicType fallback symbRepr tyCtx =
+  case testEquality symbRepr ptrSymb of
+    Nothing -> fallback symbRepr tyCtx
+    Just Refl ->
+      case Ctx.viewAssign tyCtx of
+        Ctx.AssignExtend (Ctx.viewAssign -> Ctx.AssignEmpty) (BVRepr w) ->
+          pure (PP.pretty "(Ptr" PP.<+> PP.viaShow w <> PP.pretty ")")
+        -- These are impossible by the definition of LLVMPointerImpl
+        Ctx.AssignEmpty ->
+          panic
+          "ppLLVMPointerIntrinsicType"
+          ["Impossible: LLVMPointerType empty context"]
+        Ctx.AssignExtend _ _ ->
+          panic
+          "ppLLVMPointerIntrinsicType"
+          ["Impossible: LLVMPointerType ill-formed context"]
 
 -- | Look up a pointer in the 'memImplGlobalMap' to see if it's a global.
 --
diff --git a/src/Lang/Crucible/LLVM/MemModel/Strings.hs b/src/Lang/Crucible/LLVM/MemModel/Strings.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/LLVM/MemModel/Strings.hs
@@ -0,0 +1,866 @@
+-- TODO(#1406): Move the definitions of the deprecated imports into this module,
+-- and remove the exports from MemModel.
+{-# OPTIONS_GHC -Wno-warnings-deprecations #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Manipulating C-style null-terminated strings
+module Lang.Crucible.LLVM.MemModel.Strings
+  ( storeString
+  -- * Loading strings
+  , Mem.loadString
+  , Mem.loadMaybeString
+  , loadConcretelyNullTerminatedString
+  , loadProvablyNullTerminatedString
+  -- * String length
+  , Mem.strLen
+  , strnlen
+  , strlenConcreteString
+  , strlenConcretelyNullTerminatedString
+  , strlenProvablyNullTerminatedString
+  -- * String copying
+  , copyConcreteString
+  , copyConcretelyNullTerminatedString
+  , copyProvablyNullTerminatedString
+  -- * String duplication
+  , dupConcreteString
+  , dupConcretelyNullTerminatedString
+  , dupProvablyNullTerminatedString
+  -- * Low-level string loading primitives
+  -- ** 'ByteChecker'
+  , ControlFlow(..)
+  , ByteChecker(..)
+  , withMaxChars
+  -- *** For loading strings
+  , fullyConcreteNullTerminatedString
+  , concretelyNullTerminatedString
+  , provablyNullTerminatedString
+  -- *** For string length
+  , fullyConcreteNullTerminatedStringLength
+  , concretelyNullTerminatedStringLength
+  , provablyNullTerminatedStringLength
+  -- ** 'ByteLoader'
+  , ByteLoader(..)
+  , llvmByteLoader
+  -- ** 'loadBytes'
+  , loadBytes
+  ) where
+
+import           Control.Lens ((^.), to)
+import           Data.Bifunctor (Bifunctor(bimap))
+import           Control.Monad.IO.Class (MonadIO, liftIO)
+import qualified Control.Monad.State.Strict as State
+import qualified Data.BitVector.Sized as BV
+import           Data.Functor ((<&>))
+import qualified Data.Parameterized.NatRepr as DPN
+import           Data.Word (Word8)
+import qualified Data.Vector as Vec
+import qualified GHC.Stack as GHC
+import qualified Lang.Crucible.Backend as LCB
+import qualified Lang.Crucible.Backend.Online as LCBO
+import qualified Lang.Crucible.Simulator as LCS
+import qualified Lang.Crucible.LLVM.DataLayout as CLD
+import qualified Lang.Crucible.LLVM.Errors.MemoryError as MemErr
+import qualified Lang.Crucible.LLVM.MemModel as LCLM
+import qualified Lang.Crucible.LLVM.MemModel as Mem
+import qualified Lang.Crucible.LLVM.MemModel.Generic as Mem.G
+import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial
+import qualified What4.Expr.Builder as WEB
+import qualified What4.Interface as WI
+import qualified What4.Protocol.Online as WPO
+import qualified What4.SatResult as WS
+
+-- | Store a null-terminated string to memory.
+storeNullTerminatedString ::
+  forall sym bak w.
+  ( LCB.IsSymBackend sym bak
+  , WI.IsExpr (WI.SymExpr sym)
+  , LCLM.HasPtrWidth w
+  , LCLM.HasLLVMAnn sym
+  , ?memOpts :: LCLM.MemOptions
+  ) =>
+  bak ->
+  LCLM.MemImpl sym ->
+  -- | Pointer to write string to
+  LCLM.LLVMPtr sym w ->
+  -- | The bytes of the string to write (null terminator included)
+  Vec.Vector (WI.SymBV sym 8) ->
+  IO (LCLM.MemImpl sym)
+storeNullTerminatedString bak mem ptr bytesBvs = do
+  let sym = LCB.backendGetSym bak
+  zeroNat <- WI.natLit sym 0
+  let bytes = Vec.map (Mem.LLVMValInt zeroNat) bytesBvs
+  let val = Mem.LLVMValArray (Mem.bitvectorType 1) bytes
+  let storTy = Mem.llvmValStorableType @sym val
+  Mem.storeRaw bak mem ptr storTy CLD.noAlignment val
+
+-- | Store a string to memory, adding a null terminator at the end.
+storeString ::
+  forall sym bak w.
+  ( LCB.IsSymBackend sym bak
+  , WI.IsExpr (WI.SymExpr sym)
+  , LCLM.HasPtrWidth w
+  , LCLM.HasLLVMAnn sym
+  , ?memOpts :: LCLM.MemOptions
+  ) =>
+  bak ->
+  LCLM.MemImpl sym ->
+  -- | Pointer to write string to
+  LCLM.LLVMPtr sym w ->
+  -- | The bytes of the string to write (null terminator not included)
+  Vec.Vector (WI.SymBV sym 8) ->
+  IO (LCLM.MemImpl sym)
+storeString bak mem ptr bytesBvs = do
+  let sym = LCB.backendGetSym bak
+  zeroByte <- WI.bvZero sym (DPN.knownNat @8)
+  let nullTerminatedBytes = Vec.snoc bytesBvs zeroByte
+  storeNullTerminatedString bak mem ptr nullTerminatedBytes
+
+---------------------------------------------------------------------
+-- * Loading strings
+
+-- | Load a null-terminated string (with a concrete null terminator) from memory.
+--
+-- The string must contain a concrete null terminator. If a maximum number of
+-- characters is provided, no more than that number of characters will be read.
+-- In either case, 'loadConcretelyNullTerminatedString' will stop reading if it
+-- encounters a (concretely) null terminator.
+--
+-- Note that the loaded string may actually be smaller than the returned list if
+-- any of the symbolic bytes are equal to 0.
+loadConcretelyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO [WI.SymBV sym 8]
+loadConcretelyNullTerminatedString bak mem ptr limit =
+  let loader = llvmByteLoader mem in
+  case limit of
+    Nothing -> loadBytes bak mem id ptr loader concretelyNullTerminatedString
+    Just l ->
+      let byteChecker = withMaxChars l (\f -> pure (f [])) concretelyNullTerminatedString in
+      loadBytes bak mem (id, 0) ptr loader byteChecker
+
+-- | Load a null-terminated string from memory.
+--
+-- Consults an SMT solver to check if any of the loaded bytes are known
+-- to be null (0). If a maximum number of characters is provided, no
+-- more than that number of charcters will be read. In either case,
+-- 'loadProvablyNullTerminatedString' will stop reading if it encounters a null
+-- terminator.
+--
+-- Note that the loaded string may actually be smaller than the returned list if
+-- any of the symbolic bytes are equal to 0.
+loadProvablyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , sym ~ WEB.ExprBuilder scope st fs
+  , bak ~ LCBO.OnlineBackend solver scope st fs
+  , WPO.OnlineSolver solver
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO [WI.SymBV sym 8]
+loadProvablyNullTerminatedString bak mem ptr limit =
+  let loader = llvmByteLoader mem in
+  case limit of
+    Nothing -> loadBytes bak mem id ptr loader provablyNullTerminatedString
+    Just l ->
+      let byteChecker = withMaxChars l (\f -> pure (f [])) provablyNullTerminatedString in
+      loadBytes bak mem (id, 0) ptr loader byteChecker
+
+---------------------------------------------------------------------
+-- * String length
+
+-- | Implementation of libc @strnlen@.
+strnlen ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Pointer to null-terminated string
+  Mem.LLVMPtr sym wptr ->
+  -- | Size
+  --
+  -- If this is not concrete, this will generate an assertion failure.
+  WI.SymBV sym wptr ->
+  IO (WI.SymBV sym wptr)
+strnlen bak mem ptr bound = do
+  case BV.asUnsigned <$> WI.asBV bound of
+    Nothing ->
+      let err = LCS.AssertFailureSimError "`strnlen` called with symbolic max length" "" in
+      LCB.addFailedAssertion bak err
+    Just b ->
+      let bound' = Just (fromIntegral b) in
+      strlenConcretelyNullTerminatedString bak mem ptr bound'
+ 
+-- | @strlen@ of a concrete string.
+--
+-- If any symbolic bytes are encountered, an assertion failure will be
+-- generated. If a maximum number of characters is provided, no more than that
+-- number of characters will be read. In either case, 'strlenConcreteString'
+-- will stop reading if it encounters a null terminator.
+strlenConcreteString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO Int
+strlenConcreteString bak mem ptr limit = do
+  let loader = llvmByteLoader mem
+  case limit of
+    Nothing -> loadBytes bak mem 0 ptr loader fullyConcreteNullTerminatedStringLength
+    Just 0 -> pure 0
+    Just l -> do
+      let byteChecker = withMaxChars l pure fullyConcreteNullTerminatedStringLength
+      loadBytes bak mem (0, 0) ptr loader byteChecker
+ 
+-- | @strlen@ of a null-terminated string (with a concrete null terminator).
+--
+-- The string must contain a concrete null terminator. If a maximum number of
+-- characters is provided, no more than that number of characters will be read.
+-- In either case, 'strlenConcretelyNullTerminatedString' will stop reading if
+-- it encounters a (concretely) null terminator.
+--
+-- This has the same behavior as 'Lang.Crucible.LLVM.MemModel.strLen', except
+-- that it supports a maximum length.
+strlenConcretelyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO (WI.SymBV sym wptr)
+strlenConcretelyNullTerminatedString bak mem ptr limit = do
+  let loader = llvmByteLoader mem
+  let sym = LCB.backendGetSym bak
+  z <- WI.bvZero sym ?ptrWidth
+  flip State.evalStateT (WI.truePred sym) $
+    case limit of
+      Nothing -> loadBytes bak mem z ptr loader concretelyNullTerminatedStringLength
+      Just 0 -> liftIO (WI.bvZero (LCB.backendGetSym bak) ?ptrWidth)
+      Just l -> do
+        let byteChecker = withMaxChars l pure concretelyNullTerminatedStringLength
+        loadBytes bak mem (z, 0) ptr loader byteChecker
+
+-- | @strlen@ of a provably null-terminated string.
+--
+-- Consults an SMT solver to check if any of the loaded bytes are known
+-- to be null (0). If a maximum number of characters is provided, no
+-- more than that number of charcters will be read. In either case,
+-- 'strlenProvablyNullTerminatedString' will stop reading if it encounters a
+-- (provably) null terminator.
+strlenProvablyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  , sym ~ WEB.ExprBuilder scope st fs
+  , bak ~ LCBO.OnlineBackend solver scope st fs
+  , WPO.OnlineSolver solver
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO (WI.SymBV sym wptr)
+strlenProvablyNullTerminatedString bak mem ptr limit = do
+  let loader = llvmByteLoader mem
+  let sym = LCB.backendGetSym bak
+  z <- WI.bvZero sym ?ptrWidth
+  flip State.evalStateT (WI.truePred sym) $
+    case limit of
+      Nothing -> loadBytes bak mem z ptr loader provablyNullTerminatedStringLength
+      Just 0 -> liftIO (WI.bvZero (LCB.backendGetSym bak) ?ptrWidth)
+      Just l -> do
+        let byteChecker = withMaxChars l pure provablyNullTerminatedStringLength
+        loadBytes bak mem (z, 0) ptr loader byteChecker
+
+---------------------------------------------------------------------
+-- * String copying
+
+-- | Helper, not exported
+strcpyAssertDisjoint ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Loaded bytes
+  Vec.Vector (WI.SymBV sym 8) ->
+  -- | Destination pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  IO ()
+strcpyAssertDisjoint bak mem bytes dst src = do
+  let sym = LCB.backendGetSym bak
+  let len = fromIntegral (Vec.length bytes)
+  sz <- WI.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth len)
+  let heap = mem ^. to Mem.memImplHeap
+  let memOp =
+        MemErr.MemCopyOp (Just "strcpy dst", dst) (Just "strcpy src", src) sz heap
+  Mem.assertDisjointRegions bak memOp ?ptrWidth dst sz src sz
+
+-- | @strcpy@ of a concrete string.
+--
+-- Uses 'Mem.loadString' to load the string, see that function for details.
+--
+-- Asserts that the regions are disjoint.
+copyConcreteString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Destination pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  IO (Mem.MemImpl sym)
+copyConcreteString bak mem dst src = do
+  bytes <- Mem.loadString bak mem src Nothing
+  let sym = LCB.backendGetSym bak
+  symBytes <- mapM (WI.bvLit sym WI.knownRepr . BV.word8) bytes
+  let bytesVec = Vec.fromList symBytes
+  strcpyAssertDisjoint bak mem bytesVec dst src
+  storeString bak mem dst (Vec.fromList symBytes)
+
+-- | @strcpy@ of a concretely null-terminated string.
+--
+-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that
+-- function for details.
+--
+-- Asserts that the regions are disjoint.
+copyConcretelyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Destination pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO (Mem.MemImpl sym)
+copyConcretelyNullTerminatedString bak mem dst src bounds = do
+  bytes <- loadConcretelyNullTerminatedString bak mem src bounds
+  let bytesVec = Vec.fromList bytes
+  strcpyAssertDisjoint bak mem bytesVec dst src
+  storeString bak mem dst bytesVec
+
+-- | @strcpy@ of a concrete string.
+--
+-- Uses 'loadProvablyNullTerminatedString' to load the string, see that
+-- function for details.
+--
+-- Asserts that the regions are disjoint.
+copyProvablyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , sym ~ WEB.ExprBuilder scope st fs
+  , bak ~ LCBO.OnlineBackend solver scope st fs
+  , WPO.OnlineSolver solver
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Destination pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  IO (Mem.MemImpl sym)
+copyProvablyNullTerminatedString bak mem dst src bounds = do
+  bytes <- loadProvablyNullTerminatedString bak mem src bounds
+  let bytesVec = Vec.fromList bytes
+  strcpyAssertDisjoint bak mem bytesVec dst src
+  storeString bak mem dst bytesVec
+
+---------------------------------------------------------------------
+-- * String duplication
+
+-- | Helper function: allocate memory and store bytes for string duplication.
+--
+-- Takes a vector of bytes (NOT including null terminator) and:
+-- 1. Allocates memory of the appropriate size (length + 1 for null terminator)
+-- 2. Stores the bytes with null terminator to the allocated memory
+-- 3. Returns the new pointer and updated memory
+dupFromLoadedBytes ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  Vec.Vector (WI.SymBV sym 8) ->
+  String ->
+  CLD.Alignment ->
+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
+dupFromLoadedBytes bak mem bytesVec displayString alignment = do
+  let len = fromIntegral (Vec.length bytesVec) + 1  -- +1 for null terminator
+  let sym = LCB.backendGetSym bak
+  sz <- WI.bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth len)
+  (dst, mem') <- Mem.doMalloc bak Mem.G.HeapAlloc Mem.G.Mutable displayString mem sz alignment
+  mem'' <- storeString bak mem' dst bytesVec
+  pure (dst, mem'')
+
+-- | @strdup@ of a concrete string.
+--
+-- Uses 'Mem.loadString' to load the string, see that function for details.
+--
+-- Allocates memory and copies the string to it, returning the new pointer.
+dupConcreteString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Display string for allocation
+  String ->
+  -- | Alignment
+  CLD.Alignment ->
+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
+dupConcreteString bak mem src displayString alignment = do
+  bytes <- Mem.loadString bak mem src Nothing
+  let sym = LCB.backendGetSym bak
+  symBytes <- mapM (WI.bvLit sym WI.knownRepr . BV.word8) bytes
+  dupFromLoadedBytes bak mem (Vec.fromList symBytes) displayString alignment
+
+-- | @strdup@ of a concretely null-terminated string.
+--
+-- Uses 'loadConcretelyNullTerminatedString' to load the string, see that
+-- function for details.
+--
+-- Allocates memory and copies the string to it, returning the new pointer.
+dupConcretelyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  -- | Display string for allocation
+  String ->
+  CLD.Alignment ->
+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
+dupConcretelyNullTerminatedString bak mem src bounds displayString alignment = do
+  bytes <- loadConcretelyNullTerminatedString bak mem src bounds
+  dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment
+
+-- | @strdup@ of a provably null-terminated string.
+--
+-- Uses 'loadProvablyNullTerminatedString' to load the string, see that
+-- function for details.
+--
+-- Allocates memory and copies the string to it, returning the new pointer.
+dupProvablyNullTerminatedString ::
+  ( LCB.IsSymBackend sym bak
+  , sym ~ WEB.ExprBuilder scope st fs
+  , bak ~ LCBO.OnlineBackend solver scope st fs
+  , WPO.OnlineSolver solver
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Source pointer
+  Mem.LLVMPtr sym wptr ->
+  -- | Maximum number of characters to read
+  Maybe Int ->
+  -- | Display string for allocation
+  String ->
+  CLD.Alignment ->
+  IO (Mem.LLVMPtr sym wptr, Mem.MemImpl sym)
+dupProvablyNullTerminatedString bak mem src bounds displayString alignment = do
+  bytes <- loadProvablyNullTerminatedString bak mem src bounds
+  dupFromLoadedBytes bak mem (Vec.fromList bytes) displayString alignment
+
+---------------------------------------------------------------------
+-- * Low-level string loading primitives
+
+---------------------------------------------------------------------
+-- ** 'ByteChecker'
+
+-- | Whether to stop or keep going
+--
+-- Like Rust's @std::ops::ControlFlow@.
+data ControlFlow a b
+  = Continue a
+  | Break b
+  deriving Functor
+
+-- NB: 'first' is used in this module
+instance Bifunctor ControlFlow where
+  bimap l r =
+    \case
+      Continue x -> Continue (l x)
+      Break x -> Break (r x)
+
+-- | Compute a result from a symbolic byte, and check if the load should
+-- continue to the next byte.
+--
+-- Used to:
+--
+-- * Check if the byte is concrete ('fullyConcreteNullTerminatedString')
+-- * Check if the byte is concretely a null terminator
+--   ('concretelyNullTerminatedString')
+-- * Check if a byte is known by a solver to be a null terminator ('nullTerminatedString')
+-- * Check if we have surpassed a length limit ('withMaxChars')
+--
+-- Note that it is relatively common for @a@ to be a function @[b] -> [b]@. This
+-- is used to build up a snoc-list.
+newtype ByteChecker m sym bak a b
+  = ByteChecker { runByteChecker :: bak -> a -> Mem.LLVMPtr sym 8 -> m (ControlFlow a b) }
+
+-- Helper, not exported
+ptrToBv8 ::
+  LCB.IsSymBackend sym bak =>
+  bak ->
+  Mem.LLVMPtr sym 8 ->
+  IO (WI.SymBV sym 8)
+ptrToBv8 bak bytePtr = do
+  let err = LCS.AssertFailureSimError "Found pointer instead of byte when loading string" ""
+  Partial.ptrToBv bak err bytePtr
+
+-- | 'ByteChecker' for adding a maximum character length.
+withMaxChars ::
+  MonadIO m =>
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  Functor m =>
+  -- | Maximum number of bytes to load
+  Int ->
+  -- | What to do when the maximum is reached
+  (a -> m b) ->
+  ByteChecker m sym bak a b ->
+  ByteChecker m sym bak (a, Int) b
+withMaxChars limit done checker =
+  ByteChecker $ \bak (acc, i) bytePtr ->
+    runByteChecker checker bak acc bytePtr >>=
+      \case
+        Break r -> pure (Break r)
+        Continue r ->
+          if i + 1 >= limit
+          then Break <$> done r
+          else pure (Continue (r, i + 1))
+
+---------------------------------------------------------------------
+-- *** For loading strings
+
+-- | 'ByteChecker' for loading concrete strings.
+--
+-- Currently unused internally, but analogous with
+-- 'Lang.Crucible.LLVM.MemModel.loadString'. In fact, it would be good to define
+-- that function in terms of this one. However, this is blocked on TODO(#1406).
+fullyConcreteNullTerminatedString ::
+  MonadIO m =>
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  ByteChecker m sym bak ([Word8] -> [Word8]) [Word8]
+fullyConcreteNullTerminatedString =
+  ByteChecker $ \bak acc bytePtr -> do
+    byte <- liftIO (ptrToBv8 bak bytePtr)
+    case BV.asUnsigned <$> WI.asBV byte of
+      Just 0 -> pure (Break (acc []))
+      Just c -> do
+        let c' = toEnum @Word8 (fromInteger c)
+        pure (Continue (\l -> acc (c' : l)))
+      Nothing -> do
+        let msg = "Symbolic value encountered when loading a string"
+        liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg))
+
+-- | 'ByteChecker' for loading symbolic strings with a concrete null terminator.
+--
+-- Used in 'loadConcretelyNullTerminatedString'.
+concretelyNullTerminatedString ::
+  MonadIO m =>
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]
+concretelyNullTerminatedString =
+  ByteChecker $ \bak acc bytePtr -> do
+    byte <- liftIO (ptrToBv8 bak bytePtr)
+    if isConcreteNullTerminator byte
+    then pure (Break (acc []))
+    else  pure (Continue (\l -> acc (byte : l)))
+  where
+    isConcreteNullTerminator symByte =
+      case BV.asUnsigned <$> WI.asBV symByte of
+        Just 0 -> True
+        _ -> False
+
+-- | 'ByteChecker' for loading symbolic strings with a provably-null terminator.
+--
+-- Used in 'loadSymbolicString'.
+provablyNullTerminatedString ::
+  MonadIO m =>
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  sym ~ WEB.ExprBuilder scope st fs =>
+  bak ~ LCBO.OnlineBackend solver scope st fs =>
+  WPO.OnlineSolver solver =>
+  ByteChecker m sym bak ([WI.SymBV sym 8] -> [WI.SymBV sym 8]) [WI.SymBV sym 8]
+provablyNullTerminatedString =
+  ByteChecker $ \bak acc bytePtr -> liftIO $ do
+    byte <- ptrToBv8 bak bytePtr
+    let sym = LCB.backendGetSym bak
+    isNullTerm <- isProvablyNullTerminator bak sym byte
+    if isNullTerm
+    then pure (Break (acc []))
+    else  pure (Continue (\l -> acc (byte : l)))
+
+-- Helper, not exported
+isProvablyNullTerminator ::
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  sym ~ WEB.ExprBuilder scope st fs =>
+  bak ~ LCBO.OnlineBackend solver scope st fs =>
+  WPO.OnlineSolver solver =>
+  bak ->
+  sym ->
+  WI.SymBV sym 8 ->
+  IO Bool
+isProvablyNullTerminator bak sym symByte =
+  case BV.asUnsigned <$> WI.asBV symByte of
+    Just 0 -> pure True
+    Just _ -> pure False
+    _ ->
+      LCBO.withSolverProcess bak (pure False) $ \proc -> do
+        z <- WI.bvZero sym (WI.knownNat @8)
+        p <- WI.notPred sym =<< WI.bvEq sym z symByte
+        WPO.checkSatisfiable proc "isProvablyNullTerminator" p <&>
+          \case
+            WS.Unsat () -> True
+            WS.Sat () -> False
+            WS.Unknown -> False
+
+---------------------------------------------------------------------
+-- *** For string length
+
+-- | 'ByteChecker' for @strlen@ of concrete strings.
+fullyConcreteNullTerminatedStringLength ::
+  MonadIO m =>
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  ByteChecker m sym bak Int Int
+fullyConcreteNullTerminatedStringLength =
+  ByteChecker $ \bak acc bytePtr -> do
+    byte <- liftIO (ptrToBv8 bak bytePtr)
+    case BV.asUnsigned <$> WI.asBV byte of
+      Just 0 -> pure (Break acc)
+      Just _ -> pure (Continue $! acc + 1)
+      Nothing -> do
+        let msg = "Symbolic value encountered when loading a string"
+        liftIO (LCB.addFailedAssertion bak (LCS.Unsupported GHC.callStack msg))
+
+-- Helper, not exported
+symStringLength ::
+  MonadIO m =>
+  State.MonadState (WI.Pred sym) m =>
+  GHC.HasCallStack =>
+  Mem.HasPtrWidth wptr =>
+  LCB.IsSymBackend sym bak =>
+  -- | How to check if a predicate is false
+  (bak -> WI.Pred sym -> m Bool) ->
+  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)
+symStringLength predIsFalse =
+  ByteChecker $ \bak len bytePtr -> do
+    byte <- liftIO (ptrToBv8 bak bytePtr)
+    keepGoing <- State.get
+    let sym = LCB.backendGetSym bak
+    byteWasNonNull <- liftIO (WI.bvIsNonzero sym byte)
+    keepGoing' <- liftIO (WI.andPred sym keepGoing byteWasNonNull)
+    stopHere <- predIsFalse bak keepGoing'
+    if stopHere
+    then pure (Break len)
+    else do
+      State.put keepGoing'
+      lenPlusOne <- liftIO (WI.bvAdd sym len =<< WI.bvOne sym ?ptrWidth)
+      Continue <$> liftIO (WI.bvIte sym keepGoing' lenPlusOne len)
+
+-- | 'ByteChecker' for @strlen@ of strings with a concrete null terminator.
+concretelyNullTerminatedStringLength ::
+  MonadIO m =>
+  State.MonadState (WI.Pred sym) m =>
+  GHC.HasCallStack =>
+  Mem.HasPtrWidth wptr =>
+  LCB.IsSymBackend sym bak =>
+  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)
+concretelyNullTerminatedStringLength =
+  symStringLength (\_bak p -> pure (WI.asConstantPred p == Just False))
+
+-- | 'ByteChecker' for @strlen@ for strings with a provably-null terminator.
+provablyNullTerminatedStringLength ::
+  MonadIO m =>
+  State.MonadState (WI.Pred sym) m =>
+  GHC.HasCallStack =>
+  LCB.IsSymBackend sym bak =>
+  Mem.HasPtrWidth wptr =>
+  sym ~ WEB.ExprBuilder scope st fs =>
+  bak ~ LCBO.OnlineBackend solver scope st fs =>
+  WPO.OnlineSolver solver =>
+  ByteChecker m sym bak (WI.SymBV sym wptr) (WI.SymBV sym wptr)
+provablyNullTerminatedStringLength =
+  symStringLength $ \bak p ->
+    case WI.asConstantPred p of
+      Just b -> pure b
+      _ ->
+        liftIO $ LCBO.withSolverProcess bak (pure False) $ \proc -> do
+          WPO.checkSatisfiable proc "provablyNullTerminatedStringLength" p <&>
+            \case
+              WS.Unsat () -> True
+              WS.Sat () -> False
+              WS.Unknown -> False
+
+---------------------------------------------------------------------
+-- ** 'ByteLoader'
+
+-- | Load a byte from memory.
+--
+-- The only 'ByteLoader' defined here is 'llvmByteLoader', but Macaw users will
+-- most often want one based on @doReadMemModel@.
+newtype ByteLoader m sym bak wptr
+  = ByteLoader { runByteLoader :: bak -> Mem.LLVMPtr sym wptr -> m (Mem.LLVMPtr sym 8) }
+
+-- | A 'ByteLoader' for LLVM memory based on 'Mem.doLoad'.
+llvmByteLoader ::
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  , MonadIO m
+  ) =>
+  Mem.MemImpl sym ->
+  ByteLoader m sym bak wptr
+llvmByteLoader mem =
+  ByteLoader $ \bak ptr -> do
+    let i1 = Mem.bitvectorType 1
+    let p8 = Mem.LLVMPointerRepr (DPN.knownNat @8)
+    liftIO (Mem.doLoad bak mem ptr i1 p8 CLD.noAlignment)
+
+---------------------------------------------------------------------
+-- * 'loadBytes'
+
+-- | Load a sequence of bytes, one at a time.
+--
+-- Used to implement 'loadConcretelyNullTerminatedString' and
+-- 'loadSymbolicString'. Highly customizable via 'ByteLoader' and 'ByteChecker'.
+loadBytes ::
+  forall m a b sym bak wptr.
+  ( LCB.IsSymBackend sym bak
+  , Mem.HasPtrWidth wptr
+  , Mem.HasLLVMAnn sym
+  , ?memOpts :: Mem.MemOptions
+  , GHC.HasCallStack
+  , MonadIO m
+  ) =>
+  bak ->
+  Mem.MemImpl sym ->
+  -- | Initial accumulator
+  a ->
+  -- | Pointer to load from
+  Mem.LLVMPtr sym wptr ->
+  -- | How to load a byte from memory
+  ByteLoader m sym bak wptr ->
+  -- | How to check if we should continue loading the next byte
+  ByteChecker m sym bak a b ->
+  m b
+loadBytes bak mem = go
+ where
+  sym = LCB.backendGetSym bak
+  go ::
+    a ->
+    Mem.LLVMPtr sym wptr ->
+    ByteLoader m sym bak wptr ->
+    ByteChecker m sym bak a b ->
+    m b
+  go acc ptr loader checker = do
+    byte <- runByteLoader loader bak ptr
+    runByteChecker checker bak acc byte >>=
+      \case
+        Break result -> pure result
+        Continue acc' -> do
+          -- It is important that safety assertions for later loads can use
+          -- the assumption that earlier bytes were nonzero, see #1463 or
+          -- `crucible-llvm-cli/test-data/T1463-read-bytes.cbl` for details.
+          prevByteWasNonNull <-
+            liftIO (WI.notPred sym =<< Mem.ptrIsNull sym (WI.knownNat @8) byte)
+          loc <- liftIO (WI.getCurrentProgramLoc sym)
+          let assump = LCB.BranchCondition loc Nothing prevByteWasNonNull
+          liftIO (LCB.addAssumption bak assump)
+
+          ptr' <- liftIO (Mem.doPtrAddOffset bak mem ptr =<< WI.bvOne sym Mem.PtrWidth)
+          go acc' ptr' loader checker 
diff --git a/src/Lang/Crucible/LLVM/MemModel/Value.hs b/src/Lang/Crucible/LLVM/MemModel/Value.hs
--- a/src/Lang/Crucible/LLVM/MemModel/Value.hs
+++ b/src/Lang/Crucible/LLVM/MemModel/Value.hs
@@ -107,8 +107,11 @@
   -- | The @undef@ value exists at all storage types.
   LLVMValUndef :: StorageType -> LLVMVal sym
 
+  -- | The @poison@ value exists at all storage types.
+  LLVMValPoison :: StorageType -> LLVMVal sym
 
-llvmValStorableType :: IsExprBuilder sym => LLVMVal sym -> StorageType
+
+llvmValStorableType :: IsExpr (SymExpr sym) => LLVMVal sym -> StorageType
 llvmValStorableType v =
   case v of
     LLVMValInt _ bv -> bitvectorType (bitsToBytes (natValue (bvWidth bv)))
@@ -120,6 +123,7 @@
     LLVMValString bs -> arrayType (fromIntegral (BS.length bs)) (bitvectorType (Bytes 1))
     LLVMValZero tp -> tp
     LLVMValUndef tp -> tp
+    LLVMValPoison tp -> tp
 
 -- | Create a fresh 'LLVMVal' of the given type.
 freshLLVMVal :: IsSymInterface sym =>
@@ -145,6 +149,7 @@
   case t of
     LLVMValZero _tp -> pretty "0"
     LLVMValUndef tp -> pretty "<undef : " <> viaShow tp <> pretty ">"
+    LLVMValPoison tp -> pretty "<poison : " <> viaShow tp <> pretty ">"
     LLVMValString bs -> viaShow bs
     LLVMValInt base off -> ppPtr @sym (LLVMPointer base off)
     LLVMValFloat _ v -> printSymExpr v
@@ -191,6 +196,7 @@
     \case
       (LLVMValZero tp) -> pure $ angles (typed "zero" tp)
       (LLVMValUndef tp) -> pure $ angles (typed "undef" tp)
+      (LLVMValPoison tp) -> pure $ angles (typed "poison" tp)
       (LLVMValString bs) -> pure $ viaShow bs
       (LLVMValInt blk w) -> fromMaybe otherDoc <$> ppInt blk w
         where
@@ -257,6 +263,7 @@
 instance IsExpr (SymExpr sym) => Show (LLVMVal sym) where
   show (LLVMValZero _tp) = "0"
   show (LLVMValUndef tp) = "<undef : " ++ show tp ++ ">"
+  show (LLVMValPoison tp) = "<poison : " ++ show tp ++ ">"
   show (LLVMValString  _) = "<string>"
   show (LLVMValInt blk w)
     | Just 0 <- asNat blk = "<int" ++ show (bvWidth w) ++ ">"
@@ -333,9 +340,9 @@
 --
 -- Should be faster than using 'testEqual' with 'zeroExpandLLVMVal' for compound
 -- values, because we 'traverse' subcomponents of vectors and structs, quitting
--- early on a constantly false answer or 'LLVMValUndef'.
+-- early on a constantly false answer or 'LLVMValUndef' or 'LLVMValPoison'.
 --
--- Returns 'Nothing' for 'LLVMValUndef'.
+-- Returns 'Nothing' for 'LLVMValUndef' or 'LLVMValPoison'.
 isZero :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)
        => sym -> LLVMVal sym -> IO (Maybe (Pred sym))
 isZero sym v =
@@ -345,9 +352,9 @@
     LLVMValString bs  -> pure $ Just $ backendPred sym $ not $ isJust $ BS.find (/= 0) bs
     LLVMValZero _     -> pure (Just $ truePred sym)
     LLVMValUndef _    -> pure Nothing
-    _                 ->
-      -- For atomic types, we simply expand and compare.
-      testEqual sym v =<< zeroExpandLLVMVal sym (llvmValStorableType v)
+    LLVMValPoison _   -> pure Nothing
+    LLVMValInt {}     -> compareToZeroExpansion
+    LLVMValFloat {}   -> compareToZeroExpansion
   where
     areZero :: Traversable t => t (LLVMVal sym) -> IO (Maybe (t (Pred sym)))
     areZero = fmap sequence . traverse (isZero sym)
@@ -356,9 +363,15 @@
       -- This could probably be simplified with a well-placed =<<...
       join $ fmap commuteMaybe $ fmap (fmap (allOf sym . toList)) $ areZero vs
 
+    -- Check if a value is equal to itself after zero-expansion. This is
+    -- suitable for checking atomic types (e.g., integers and floats).
+    compareToZeroExpansion =
+      testEqual sym v =<< zeroExpandLLVMVal sym (llvmValStorableType v)
+
 -- | A predicate denoting the equality of two LLVMVals.
 --
--- Returns 'Nothing' in the event that one of the values contains 'LLVMValUndef'.
+-- Returns 'Nothing' in the event that one of the values contains 'LLVMValUndef'
+-- or 'LLVMValPoison'.
 testEqual :: forall sym. (IsExprBuilder sym, IsInterpretedFloatExprBuilder sym)
           => sym -> LLVMVal sym -> LLVMVal sym -> IO (Maybe (Pred sym))
 testEqual sym v1 v2 =
@@ -394,6 +407,8 @@
     (other, LLVMValZero tp) -> compareZero tp other
     (LLVMValUndef _, _) -> pure Nothing
     (_, LLVMValUndef _) -> pure Nothing
+    (LLVMValPoison _, _) -> pure Nothing
+    (_, LLVMValPoison _) -> pure Nothing
     (_, _) -> false -- type mismatch
 
   where true = pure (Just $ truePred sym)
diff --git a/src/Lang/Crucible/LLVM/MemType.hs b/src/Lang/Crucible/LLVM/MemType.hs
--- a/src/Lang/Crucible/LLVM/MemType.hs
+++ b/src/Lang/Crucible/LLVM/MemType.hs
@@ -313,7 +313,7 @@
              -> StructInfo
 mkStructInfo dl packed tps0 = go [] 0 a0 tps0
   where a0 | packed    = noAlignment
-           | otherwise = nextAlign noAlignment tps0 `max` aggregateAlignment dl
+           | otherwise = nextAlign noAlignment tps0 `max` (dl ^. aggregateAlignment)
         -- Padding after each field depends on the alignment of the
         -- type of the next field, if there is one. Padding after the
         -- last field depends on the alignment of the whole struct
diff --git a/src/Lang/Crucible/LLVM/SymIO.hs b/src/Lang/Crucible/LLVM/SymIO.hs
--- a/src/Lang/Crucible/LLVM/SymIO.hs
+++ b/src/Lang/Crucible/LLVM/SymIO.hs
@@ -102,6 +102,7 @@
 
 import           Lang.Crucible.LLVM.Bytes (toBytes)
 import           Lang.Crucible.LLVM.MemModel
+import qualified Lang.Crucible.LLVM.MemModel.Strings as CStr
 import           Lang.Crucible.LLVM.Extension ( ArchWidth )
 import           Lang.Crucible.LLVM.DataLayout ( noAlignment )
 import           Lang.Crucible.LLVM.Intrinsics
@@ -380,7 +381,7 @@
 loadFileIdent memOps filename_ptr =
   ovrWithBackend $ \bak ->
    do mem <- readGlobal memOps
-      filename_bytes <- liftIO $ loadString bak mem filename_ptr Nothing
+      filename_bytes <- liftIO $ CStr.loadString bak mem filename_ptr Nothing
       liftIO $ W4.stringLit (backendGetSym bak) (W4.Char8Literal (BS.pack filename_bytes))
 
 returnIOError32
diff --git a/src/Lang/Crucible/LLVM/Translation.hs b/src/Lang/Crucible/LLVM/Translation.hs
--- a/src/Lang/Crucible/LLVM/Translation.hs
+++ b/src/Lang/Crucible/LLVM/Translation.hs
@@ -97,7 +97,6 @@
 import           Data.IORef (IORef, newIORef, readIORef, modifyIORef)
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Maybe
 import           Data.String
@@ -206,8 +205,8 @@
           , fromString msg
           ]
 
-    stmt m (L.Effect _ _) = return m
-    stmt m (L.Result ident instr _) = do
+    stmt m (L.Effect _ _ _) = return m
+    stmt m (L.Result ident instr _ _) = do
          ty <- either (err instr) return $ instrResultType instr
          ex <- typeToRegExpr ty
          case Map.lookup ident m of
@@ -223,26 +222,25 @@
 generateStmts :: (?transOpts :: TranslationOptions)
         => TypeRepr ret
         -> L.BlockLabel
-        -> Set L.Ident {- ^ Set of usable identifiers -}
         -> [L.Stmt]
         -> LLVMGenerator s arch ret a
-generateStmts retType lab defSet0 stmts = go defSet0 (processDbgDeclare stmts)
- where go _ [] = fail "LLVM basic block ended without a terminating instruction"
-       go defSet (x:xs) =
+generateStmts retType lab stmts = go (processDbgDeclare stmts)
+ where go [] = fail "LLVM basic block ended without a terminating instruction"
+       go (x:xs) =
          case x of
            -- a result statement assigns the result of the instruction into a register
-           L.Result ident instr md ->
-              do setLocation md
-                 generateInstr retType lab defSet instr
+           L.Result ident instr dr md ->
+              do setLocation md dr
+                 generateInstr retType lab instr
                    (assignLLVMReg ident)
-                   (go (Set.insert ident defSet) xs)
+                   (go xs)
 
            -- an effect statement simply executes the instruction for its effects and discards the result
-           L.Effect instr md ->
-              do setLocation md
-                 generateInstr retType lab defSet instr
+           L.Effect instr dr md ->
+              do setLocation md dr
+                 generateInstr retType lab instr
                    (\_ -> return ())
-                   (go defSet xs)
+                   (go xs)
 
 -- | Search for calls to intrinsic 'llvm.dbg.declare' and copy the
 -- metadata onto the corresponding 'alloca' statement.  Also copy
@@ -255,18 +253,18 @@
     go (stmt : stmts) =
       let (m, stmts') = go stmts in
       case stmt of
-        L.Result x instr@L.Alloca{} md ->
+        L.Result x instr@L.Alloca{} dr md ->
           case Map.lookup x m of
-            Just md' -> (m, L.Result x instr (md' ++ md) : stmts')
+            Just md' -> (m, L.Result x instr dr (md' ++ md) : stmts')
             Nothing -> (m, stmt : stmts')
               --error $ "Identifier not found: " ++ show x ++ "\nPossible identifiers: " ++ show (Map.keys m)
 
-        L.Result x (L.Conv L.BitCast (L.Typed _ (L.ValIdent y)) _) md ->
+        L.Result x (L.Conv L.BitCast (L.Typed _ (L.ValIdent y)) _) _dr md ->
           let md' = md ++ fromMaybe [] (Map.lookup x m)
               m'  = Map.alter (Just . maybe md' (md'++)) y m
            in (m', stmt:stmts)
 
-        L.Effect (L.Call _ _ (L.ValSymbol "llvm.dbg.declare") (L.Typed _ (L.ValMd (L.ValMdValue (L.Typed _ (L.ValIdent x)))) : _)) md ->
+        L.Effect (L.Call _ _ (L.ValSymbol "llvm.dbg.declare") (L.Typed _ (L.ValMd (L.ValMdValue (L.Typed _ (L.ValIdent x)))) : _)) _dr md ->
           (Map.insert x md m, stmt : stmts')
 
         -- This is needlessly fragile. Let's just ignore debug declarations we don't understand.
@@ -275,25 +273,67 @@
 
         _ -> (m, stmt : stmts')
 
-setLocation
-  :: [(String,L.ValMd)]
-  -> LLVMGenerator s arch ret ()
-setLocation [] = return ()
-setLocation (x:xs) =
-  case x of
-    ("dbg",L.ValMdLoc dl) ->
-      let ln   = fromIntegral $ L.dlLine dl
-          col  = fromIntegral $ L.dlCol dl
-          file = getFile $ L.dlScope dl
-       in setPosition (SourcePos file ln col)
-    ("dbg",L.ValMdDebugInfo (L.DebugInfoSubprogram subp))
-      | Just file' <- L.dispFile subp
-      -> let ln = fromIntegral $ L.dispLine subp
-             file = getFile file'
-          in setPosition (SourcePos file ln 0)
-    _ -> setLocation xs
-
+-- | Search for an instruction's nearest debug location that was attached as a
+-- metadata attribute using the @!dbg@ identifier, and then set the
+-- `LLVMGenerator`'s position using the location. If such a metadata attribute
+-- cannot be found, look at the debug records as a fallback. (In practice, LLVM
+-- will usually attach debug locations as metadata attributes, so it makes more
+-- sense to look through the metadata attributes first.)
+setLocation ::
+  forall s arch ret.
+  -- | The metadata attributes.
+  [(String,L.ValMd)] ->
+  -- | The debug records.
+  [L.DebugRecord] ->
+  LLVMGenerator s arch ret ()
+setLocation mds drs = setMetadataLocation mds
  where
+ setMetadataLocation :: [(String,L.ValMd)] -> LLVMGenerator s arch ret ()
+ setMetadataLocation [] =
+   -- If we can't find a @!dbg@ metadata location, fall back to searching the
+   -- debug records.
+   setDebugRecordLocation drs
+ setMetadataLocation (x:xs) =
+   case x of
+     ("dbg",md)
+       | Just posn <- valMdPosition md ->
+         setPosition posn
+     _ -> setMetadataLocation xs
+
+ setDebugRecordLocation :: [L.DebugRecord] -> LLVMGenerator s arch ret ()
+ setDebugRecordLocation [] = return ()
+ setDebugRecordLocation (x:xs) =
+   case x of
+     L.DebugRecordValue drv
+       | Just posn <- valMdPosition (L.drvLocation drv) ->
+         setPosition posn
+     L.DebugRecordValueSimple drvs
+       | Just posn <- valMdPosition (L.drvsLocation drvs) ->
+         setPosition posn
+     L.DebugRecordDeclare drd
+       | Just posn <- valMdPosition (L.drdLocation drd) ->
+         setPosition posn
+     L.DebugRecordAssign dra
+       | Just posn <- valMdPosition (L.draLocation dra) ->
+         setPosition posn
+     L.DebugRecordLabel drl
+       | Just posn <- valMdPosition (L.drlLocation drl) ->
+         setPosition posn
+     _ -> setDebugRecordLocation xs
+
+ valMdPosition :: L.ValMd -> Maybe Position
+ valMdPosition (L.ValMdLoc dl) =
+   let ln   = fromIntegral $ L.dlLine dl
+       col  = fromIntegral $ L.dlCol dl
+       file = getFile $ L.dlScope dl
+    in Just (SourcePos file ln col)
+ valMdPosition (L.ValMdDebugInfo (L.DebugInfoSubprogram subp))
+   | Just file' <- L.dispFile subp =
+     let ln = fromIntegral $ L.dispLine subp
+         file = getFile file'
+     in Just (SourcePos file ln 0)
+ valMdPosition _ = Nothing
+
  getFile = Text.pack . maybe "" filenm . findFile
 
  -- The typical values available here will be something like:
@@ -353,7 +393,7 @@
         -> LLVMGenerator s arch ret ()
 defineLLVMBlock retType lm L.BasicBlock{ L.bbLabel = Just lab, L.bbStmts = stmts } = do
   case Map.lookup lab lm of
-    Just bi -> defineBlock (block_label bi) (generateStmts retType lab (block_use_set bi) stmts)
+    Just bi -> defineBlock (block_label bi) (generateStmts retType lab stmts)
     Nothing -> fail $ unwords ["LLVM basic block not found in block info map", show lab]
 
 defineLLVMBlock _ _ _ = fail "LLVM basic block has no label!"
@@ -375,7 +415,7 @@
     ( L.BasicBlock{ L.bbLabel = Just entry_lab } : _ ) -> do
       let (L.Symbol nm) = L.defName defn
       callPushFrame $ Text.pack nm
-      setLocation $ Map.toList (L.defMetadata defn)
+      setLocation (Map.toList (L.defMetadata defn)) []
 
       bim <- buildBlockInfoMap defn
       blockInfoMap .= bim
diff --git a/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs b/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs
--- a/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs
+++ b/src/Lang/Crucible/LLVM/Translation/BlockInfo.hs
@@ -25,7 +25,7 @@
   ) where
 
 import Data.Foldable (toList)
-import Data.List (foldl')
+import qualified Data.Foldable as Foldable
 import Data.Maybe
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
@@ -131,7 +131,7 @@
 
 -- | Compute predecessor sets from the successor sets already computed in @buildBlockInfo@
 updatePredSets :: LLVMBlockInfoMap s -> LLVMBlockInfoMap s
-updatePredSets bim0 = foldl' upd bim0 predEdges
+updatePredSets bim0 = Foldable.foldl' upd bim0 predEdges
   where
    upd bim (to,from) = Map.adjust (\bi -> bi{ block_pred_set = Set.insert from (block_pred_set bi) }) to bim
 
@@ -190,7 +190,7 @@
   -- to registers: the return values can only be used in the "normal" successor
   -- block.
 
-  loop (L.Result nm i _md:ss) =
+  loop (L.Result nm i _dr _md:ss) =
     case i of
       L.Invoke _tp f args l_normal l_unwind ->
             -- the use sets from the function value, arguments, and unwind label
@@ -214,7 +214,7 @@
       -- defined here
       _ -> Set.union (instrUse lab i bim) (Set.delete nm (loop ss))
 
-  loop (L.Effect i _md:ss) = Set.union (instrUse lab i bim) (loop ss)
+  loop (L.Effect i _dr _md:ss) = Set.union (instrUse lab i bim) (loop ss)
 
 instrUse :: L.BlockLabel -> L.Instr -> Map L.BlockLabel (LLVMBlockInfo s) -> Set L.Ident
 instrUse from i bim = Set.unions $ case i of
@@ -237,7 +237,7 @@
   L.Fence{} -> []
   L.CmpXchg _weak _vol p v1 v2 _s _o1 _o2 -> map useTypedVal [p,v1,v2]
   L.AtomicRW _vol _op p v _s _o -> [useTypedVal p, useTypedVal v]
-  L.ICmp _op x y -> [useTypedVal x, useVal y]
+  L.ICmp _samesign _op x y -> [useTypedVal x, useVal y]
   L.FCmp _op x y -> [useTypedVal x, useVal y]
   L.GEP _ib _tp base args -> useTypedVal base : map useTypedVal args
   L.Select c x y -> [ useTypedVal c, useTypedVal x, useVal y ]
@@ -312,7 +312,7 @@
 -- compute the list of assignments that must be made for each predecessor block.
 buildPhiMap :: [L.Stmt] -> Map L.BlockLabel (Seq (L.Ident, L.Type, L.Value))
 buildPhiMap ss = go ss Map.empty
- where go (L.Result ident (L.Phi tp xs) _ : stmts) m = go stmts (go' ident tp xs m)
+ where go (L.Result ident (L.Phi tp xs) _ _ : stmts) m = go stmts (go' ident tp xs m)
        go _ m = m
 
        f x mseq = Just (fromMaybe Seq.empty mseq Seq.|> x)
diff --git a/src/Lang/Crucible/LLVM/Translation/Constant.hs b/src/Lang/Crucible/LLVM/Translation/Constant.hs
--- a/src/Lang/Crucible/LLVM/Translation/Constant.hs
+++ b/src/Lang/Crucible/LLVM/Translation/Constant.hs
@@ -52,6 +52,7 @@
   , testBreakpointFunction
   ) where
 
+import qualified Control.Exception as X
 import           Control.Lens( to, (^.) )
 import           Control.Monad
 import           Control.Monad.Except
@@ -73,7 +74,6 @@
 import qualified Data.BitVector.Sized.Overflow as BV
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Some
-import           Data.Parameterized.DecidableEq (decEq)
 
 import           Lang.Crucible.LLVM.Bytes
 import           Lang.Crucible.LLVM.DataLayout( intLayout, EndianForm(..) )
@@ -152,8 +152,7 @@
 -- types, computing vectorization lanes, etc.
 --
 -- As a concrete example, consider a call to
--- @'translateGEP' inbounds baseTy basePtr elts@ with the following
--- instruction:
+-- @'translateGEP' attrs baseTy basePtr elts@ with the following instruction:
 --
 -- @
 -- getelementptr [12 x i8], ptr %aptr, i64 0, i32 1
@@ -161,8 +160,10 @@
 --
 -- Here:
 --
--- * @inbounds@ is 'False', as the keyword of the same name is missing from
---   the instruction. (Currently, @crucible-llvm@ ignores this information.)
+-- * @attrs@ is @[]@, as there are no @inbounds@, @nusw@, @nuw@, or @inrange@
+--   attributes used in the instruction. (Currently, @crucible-llvm@ ignores
+--   attribute information. See
+--   <https://github.com/GaloisInc/crucible/issues/1605>.)
 --
 -- * @baseTy@ is @[12 x i8]@. This is the type used as the basis for
 --   subsequent calculations.
@@ -175,7 +176,7 @@
 --   which of the elements of the aggregate object are indexed.
 translateGEP :: forall wptr m.
   (?lc :: TypeContext, MonadError String m, HasPtrWidth wptr) =>
-  Bool              {- ^ inbounds flag -} ->
+  [L.GEPAttr]       {- ^ attributes -} ->
   L.Type            {- ^ base type for calculations -} ->
   L.Typed L.Value   {- ^ base pointer expression -} ->
   [L.Typed L.Value] {- ^ index arguments -} ->
@@ -184,7 +185,7 @@
 translateGEP _ _ _ [] =
   throwError "getelementpointer must have at least one index"
 
-translateGEP inbounds baseTy basePtr elts =
+translateGEP attrs baseTy basePtr elts =
   do baseMemType <- liftMemType baseTy
      mt <- liftMemType (L.typedType basePtr)
      -- Input value to a GEP must have a pointer type (or be a vector of pointer
@@ -209,7 +210,7 @@
          -> badGEP
  where
  badGEP :: m a
- badGEP = throwError $ unlines [ "Invalid GEP", showInstr (L.GEP inbounds baseTy basePtr elts) ]
+ badGEP = throwError $ unlines [ "Invalid GEP", showInstr (L.GEP attrs baseTy basePtr elts) ]
 
  -- This auxilary function builds up the intermediate GEP mini-instructions that compute
  -- the overall GEP, as well as the resulting memory type of the final pointers and the
@@ -337,6 +338,9 @@
   -- | The @undef@ value is quite strange. See: The LLVM Language Reference,
   -- § Undefined Values.
   UndefConst    :: !MemType -> LLVMConst
+  -- | The @poison@ value is quite strange. See: The LLVM Language Reference,
+  -- § Poison Values.
+  PoisonConst   :: !MemType -> LLVMConst
 
 
 -- | This also can't be derived, but is completely uninteresting.
@@ -353,29 +357,9 @@
       (StructConst si a)  -> ["StructConst", show si, show a]
       (SymbolConst s x)   -> ["SymbolConst", show s, show x]
       (UndefConst mem)    -> ["UndefConst", show mem]
+      (PoisonConst mem)   -> ["PoisonConst", show mem]
       (StringConst bs)    -> ["StringConst", show bs]
 
--- | The interesting cases here are:
---  * @IntConst@: GHC can't derive this because @IntConst@ existentially
---    quantifies the integer's width. We say that two integers are equal when
---    they have the same width *and* the same value.
---  * @UndefConst@: Two @undef@ values aren't necessarily the same...
-instance Eq LLVMConst where
-  (ZeroConst mem1)      == (ZeroConst mem2)      = mem1 == mem2
-  (IntConst w1 x1)      == (IntConst w2 x2)      =
-    case decEq w1 w2 of
-      Left Refl -> x1 == x2
-      Right _   -> False
-  (FloatConst f1)       == (FloatConst f2)       = f1 == f2
-  (DoubleConst d1)      == (DoubleConst d2)      = d1 == d2
-  (LongDoubleConst ld1) == (LongDoubleConst ld2) = ld1 == ld2
-  (ArrayConst mem1 a1)  == (ArrayConst mem2 a2)  = mem1 == mem2 && a1 == a2
-  (VectorConst mem1 v1) == (VectorConst mem2 v2) = mem1 == mem2 && v1 == v2
-  (StructConst si1 a1)  == (StructConst si2 a2)  = si1 == si2   && a1 == a2
-  (SymbolConst s1 x1)   == (SymbolConst s2 x2)   = s1 == s2     && x1 == x2
-  (UndefConst  _)       == (UndefConst _)        = False
-  _                     == _                     = False
-
 -- | Create an LLVM constant value from a boolean.
 boolConst :: Bool -> LLVMConst
 boolConst False = IntConst (knownNat @1) (BV.zero knownNat)
@@ -423,6 +407,8 @@
   m LLVMConst
 transConstant' tp (L.ValUndef) =
   return (UndefConst tp)
+transConstant' tp (L.ValPoison) =
+  return (PoisonConst tp)
 transConstant' (IntType n) (L.ValInteger x) =
   intConst n x
 transConstant' (IntType 1) (L.ValBool b) =
@@ -805,14 +791,19 @@
       , DoubleConst d <- x
       -> return $ IntConst w (BV.mkBV w (truncate d))
 
-    L.UiToFp
+    L.UiToFp nneg
       | FloatType <- mt
       , IntConst _w i <- x
-      -> return $ FloatConst (fromInteger (BV.asUnsigned i) :: Float)
+      -> -- LLVM does not currently enable the `nneg` flag in constant
+         -- expressions, only in instructions. As such, we don't use the flag
+         -- below except to assert that it's disabled.
+         X.assert (not nneg) $
+         return $ FloatConst (fromInteger (BV.asUnsigned i) :: Float)
 
       | DoubleType <- mt
       , IntConst _w i <- x
-      -> return $ DoubleConst (fromInteger (BV.asUnsigned i) :: Double)
+      -> X.assert (not nneg) $
+         return $ DoubleConst (fromInteger (BV.asUnsigned i) :: Double)
 
     L.SiToFp
       | FloatType <- mt
@@ -823,23 +814,32 @@
       , IntConst w i <- x
       -> return $ DoubleConst (fromInteger (BV.asSigned w i) :: Double)
 
-    L.Trunc
+    L.Trunc nuw nsw
       | IntType n <- mt
       , IntConst w i <- x
       , Just (Some w') <- someNat n
       , Just LeqProof <- isPosNat w'
-      -> case testNatCases w' w of
+      -> -- LLVM does not currently enable the `nuw` or `nsw` flags in constant
+         -- expressions, only in instructions. As such, we don't use the flags
+         -- below except to assert that they're disabled.
+         X.assert (not nuw) $
+         X.assert (not nsw) $
+         case testNatCases w' w of
           NatCaseLT LeqProof -> return $ IntConst w' (BV.trunc w' i)
           NatCaseEQ -> return x
           NatCaseGT LeqProof ->
             throwError $ "Attempted to truncate " <> show w <> " bits to " <> show w'
 
-    L.ZExt
+    L.ZExt nneg
       | IntType n <- mt
       , IntConst w i <- x
       , Just (Some w') <- someNat n
       , Just LeqProof <- isPosNat w'
-      -> case testNatCases w w' of
+      -> -- LLVM does not currently enable the `nneg` flag in constant
+         -- expressions, only in instructions. As such, we don't use the flag
+         -- below except to assert that it's disabled.
+         X.assert (not nneg) $
+         case testNatCases w w' of
           NatCaseLT LeqProof -> return $ IntConst w' (BV.zext w' i)
           NatCaseEQ -> return x
           NatCaseGT LeqProof ->
@@ -1085,8 +1085,8 @@
   L.ConstExpr ->
   m LLVMConst
 transConstantExpr expr = case expr of
-  L.ConstGEP inbounds _inrange baseTy base exps -> -- TODO? pay attention to the inrange flag
-    do gep <- translateGEP inbounds baseTy base exps
+  L.ConstGEP attrs _inrange baseTy base exps -> -- TODO(#1605)? pay attention to the inrange flag
+    do gep <- translateGEP attrs baseTy base exps
        gep' <- traverse transConstant gep
        snd <$> evalConstGEP gep'
 
diff --git a/src/Lang/Crucible/LLVM/Translation/Expr.hs b/src/Lang/Crucible/LLVM/Translation/Expr.hs
--- a/src/Lang/Crucible/LLVM/Translation/Expr.hs
+++ b/src/Lang/Crucible/LLVM/Translation/Expr.hs
@@ -35,12 +35,15 @@
   , pattern PointerExpr
   , pattern BitvectorAsPointerExpr
   , pointerAsBitvectorExpr
+  , poisonBvExpr
+  , poisonFloatExpr
 
   , unpackOne
   , unpackVec
   , unpackArgs
   , zeroExpand
   , undefExpand
+  , poisonExpand
   , explodeVector
 
   , constToLLVMVal
@@ -121,6 +124,7 @@
    BaseExpr   :: TypeRepr tp -> Expr LLVM s tp -> LLVMExpr s arch
    ZeroExpr   :: MemType -> LLVMExpr s arch
    UndefExpr  :: MemType -> LLVMExpr s arch
+   PoisonExpr :: MemType -> LLVMExpr s arch
    VecExpr    :: MemType -> Seq (LLVMExpr s arch) -> LLVMExpr s arch
    StructExpr :: Seq (MemType, LLVMExpr s arch) -> LLVMExpr s arch
 
@@ -128,6 +132,7 @@
   show (BaseExpr ty x)  = C.showF x ++ " : " ++ show ty
   show (ZeroExpr mt)    = "<zero :" ++ show mt ++ ">"
   show (UndefExpr mt)   = "<undef :" ++ show mt ++ ">"
+  show (PoisonExpr mt)  = "<poison :" ++ show mt ++ ">"
   show (VecExpr _mt xs) = "[" ++ List.intercalate ", " (map show (toList xs)) ++ "]"
   show (StructExpr xs)  = "{" ++ List.intercalate ", " (map f (toList xs)) ++ "}"
     where f (_mt,x) = show x
@@ -150,6 +155,9 @@
 asScalar (UndefExpr llvmtp)
   = let ?err = error
      in undefExpand proxy# llvmtp $ \archProxy tpr ex -> Scalar archProxy tpr ex
+asScalar (PoisonExpr llvmtp)
+  = let ?err = error
+     in poisonExpand proxy# llvmtp $ \archProxy tpr ex -> Scalar archProxy tpr ex
 asScalar _ = NotScalar
 
 -- | Turn the expression into an explicit vector.
@@ -158,6 +166,7 @@
   case v of
     ZeroExpr (VecType n t)  -> Just (t, Seq.replicate (fromIntegral n) (ZeroExpr t))
     UndefExpr (VecType n t) -> Just (t, Seq.replicate (fromIntegral n) (UndefExpr t))
+    PoisonExpr (VecType n t) -> Just (t, Seq.replicate (fromIntegral n) (PoisonExpr t))
     VecExpr t s             -> Just (t, s)
     _                       -> Nothing
 
@@ -198,8 +207,18 @@
                 (litExpr "Expected bitvector, but found pointer")
      return off
 
+poisonBvExpr ::
+  (1 <= w) =>
+  NatRepr w ->
+  Expr LLVM s (BVType w)
+poisonBvExpr w = App (ExtensionApp (LLVM_PoisonBV w))
 
+poisonFloatExpr ::
+  FloatInfoRepr fi ->
+  Expr LLVM s (FloatType fi)
+poisonFloatExpr fi = App (ExtensionApp (LLVM_PoisonFloat fi))
 
+
 -- | Given a list of LLVMExpressions, "unpack" them into an assignment
 --   of crucible expressions.
 unpackArgs :: forall s a arch
@@ -225,6 +244,7 @@
    -> a
 unpackOne (BaseExpr tyr ex) k = k proxy# tyr ex
 unpackOne (UndefExpr tp) k = undefExpand proxy# tp k
+unpackOne (PoisonExpr tp) k = poisonExpand proxy# tp k
 unpackOne (ZeroExpr tp) k = zeroExpand proxy# tp k
 unpackOne (StructExpr vs) k =
   unpackArgs (map snd $ toList vs) $ \archProxy struct_ctx struct_asgn ->
@@ -284,36 +304,103 @@
             -> MemType
             -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
             -> a
-undefExpand _archProxy (IntType w) k =
-  case mkNatRepr w of
-    Some w' | Just LeqProof <- isPosNat w' ->
-      k proxy# (LLVMPointerRepr w') $
-         BitvectorAsPointerExpr w' $
-         App $ BVUndef w'
+undefExpand archProxy t k =
+  case t of
+    IntType w ->
+      case mkNatRepr w of
+        Some w' | Just LeqProof <- isPosNat w' ->
+          k proxy# (LLVMPointerRepr w') $
+             BitvectorAsPointerExpr w' $
+             App $ BVUndef w'
 
-    _ -> ?err $ unwords ["illegal integer size", show w]
-undefExpand _archProxy (PtrType _tp) k =
-   k proxy# PtrRepr $ BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth
-undefExpand _archProxy PtrOpaqueType k =
-   k proxy# PtrRepr $ BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth
-undefExpand _archProxy (StructType si) k =
-   unpackArgs (map UndefExpr tps) $ \archProxy ctx asgn -> k archProxy (StructRepr ctx) (mkStruct ctx asgn)
- where tps = map fiType $ toList $ siFields si
-undefExpand archProxy (ArrayType n tp) k =
-  llvmTypeAsRepr tp $ \tpr -> unpackVec archProxy tpr (replicate (fromIntegral n) (UndefExpr tp)) $ k proxy# (VectorRepr tpr)
-undefExpand archProxy (VecType n tp) k =
-  llvmTypeAsRepr tp $ \tpr -> unpackVec archProxy tpr (replicate (fromIntegral n) (UndefExpr tp)) $ k proxy# (VectorRepr tpr)
-undefExpand _archProxy FloatType k =
-  k proxy# (FloatRepr SingleFloatRepr) (App (FloatUndef SingleFloatRepr))
-undefExpand _archProxy DoubleType k =
-  k proxy# (FloatRepr DoubleFloatRepr) (App (FloatUndef DoubleFloatRepr))
-undefExpand _archProxy X86_FP80Type k =
-  k proxy# (FloatRepr X86_80FloatRepr) (App (FloatUndef X86_80FloatRepr))
-undefExpand _archPrxy tp _ = ?err $ unwords ["cannot undef expand type:", show tp]
+        _ -> ?err $ unwords ["illegal integer size", show w]
+    PtrType _tp ->
+      k proxy# PtrRepr $
+        BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth
+    PtrOpaqueType ->
+      k proxy# PtrRepr $
+        BitvectorAsPointerExpr PtrWidth $ App $ BVUndef PtrWidth
+    StructType si ->
+      unpackArgs (map UndefExpr tps) $ \structArchProxy ctx asgn ->
+        k structArchProxy (StructRepr ctx) (mkStruct ctx asgn)
+      where tps = map fiType $ toList $ siFields si
+    ArrayType n tp ->
+      llvmTypeAsRepr tp $ \tpr ->
+        unpackVec
+          archProxy
+          tpr
+          (replicate (fromIntegral n) (UndefExpr tp))
+          (k proxy# (VectorRepr tpr))
+    VecType n tp ->
+      llvmTypeAsRepr tp $ \tpr ->
+        unpackVec
+          archProxy
+          tpr
+          (replicate (fromIntegral n) (UndefExpr tp))
+          (k proxy# (VectorRepr tpr))
+    FloatType ->
+      k proxy# (FloatRepr SingleFloatRepr) (App (FloatUndef SingleFloatRepr))
+    DoubleType ->
+      k proxy# (FloatRepr DoubleFloatRepr) (App (FloatUndef DoubleFloatRepr))
+    X86_FP80Type ->
+      k proxy# (FloatRepr X86_80FloatRepr) (App (FloatUndef X86_80FloatRepr))
+    MetadataType ->
+      ?err $ unwords ["cannot undef expand metadata type"]
 
+poisonExpand :: ( ?err :: String -> a
+                , HasPtrWidth (ArchWidth arch)
+                )
+             => Proxy# arch
+             -> MemType
+             -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
+             -> a
+poisonExpand archProxy t k =
+  case t of
+    IntType w ->
+      case mkNatRepr w of
+        Some w' | Just LeqProof <- isPosNat w' ->
+          k proxy# (LLVMPointerRepr w') $
+             BitvectorAsPointerExpr w' $
+             poisonBvExpr w'
 
+        _ -> ?err $ unwords ["illegal integer size", show w]
+    PtrType _tp ->
+      k proxy# PtrRepr $
+        BitvectorAsPointerExpr PtrWidth $ poisonBvExpr PtrWidth
+    PtrOpaqueType ->
+      k proxy# PtrRepr $
+        BitvectorAsPointerExpr PtrWidth $ poisonBvExpr PtrWidth
+    StructType si ->
+      unpackArgs (map PoisonExpr tps) $ \structArchProxy ctx asgn ->
+        k structArchProxy (StructRepr ctx) (mkStruct ctx asgn)
+      where tps = map fiType $ toList $ siFields si
+    ArrayType n tp ->
+      llvmTypeAsRepr tp $ \tpr ->
+        unpackVec
+          archProxy
+          tpr
+          (replicate (fromIntegral n) (PoisonExpr tp))
+          (k proxy# (VectorRepr tpr))
+    VecType n tp ->
+      llvmTypeAsRepr tp $ \tpr ->
+        unpackVec
+          archProxy
+          tpr
+          (replicate (fromIntegral n) (PoisonExpr tp))
+          (k proxy# (VectorRepr tpr))
+    FloatType ->
+      k proxy# (FloatRepr SingleFloatRepr) (poisonFloatExpr SingleFloatRepr)
+    DoubleType ->
+      k proxy# (FloatRepr DoubleFloatRepr) (poisonFloatExpr DoubleFloatRepr)
+    X86_FP80Type ->
+      k proxy# (FloatRepr X86_80FloatRepr) (poisonFloatExpr X86_80FloatRepr)
+    MetadataType ->
+      ?err $ unwords ["cannot poison expand metadata type"]
+
+
 explodeVector :: Natural -> LLVMExpr s arch -> Maybe (Seq (LLVMExpr s arch))
 explodeVector n (UndefExpr (VecType n' tp)) | n == n' = return (Seq.replicate (fromIntegral n) (UndefExpr tp))
+explodeVector n (PoisonExpr (VecType n' tp)) | n == n' = return (Seq.replicate (fromIntegral n) (PoisonExpr tp))
 explodeVector n (ZeroExpr (VecType n' tp)) | n == n' = return (Seq.replicate (fromIntegral n) (ZeroExpr tp))
 explodeVector n (VecExpr _tp xs)
   | n == fromIntegral (length xs) = return xs
@@ -335,6 +422,8 @@
     return $ ZeroExpr mt
   UndefConst mt ->
     return $ UndefExpr mt
+  PoisonConst mt ->
+    return $ PoisonExpr mt
   IntConst w i ->
     return $ BaseExpr (LLVMPointerRepr w) (BitvectorAsPointerExpr w (App (BVLit w i)))
   FloatConst f ->
@@ -395,6 +484,9 @@
 
 transValue ty L.ValUndef =
   return $ UndefExpr ty
+
+transValue ty L.ValPoison =
+  return $ PoisonExpr ty
 
 transValue ty L.ValZeroInit =
   return $ ZeroExpr ty
diff --git a/src/Lang/Crucible/LLVM/Translation/Instruction.hs b/src/Lang/Crucible/LLVM/Translation/Instruction.hs
--- a/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+++ b/src/Lang/Crucible/LLVM/Translation/Instruction.hs
@@ -51,8 +51,6 @@
 import           Data.List.NonEmpty (NonEmpty((:|)))
 import qualified Data.Map.Strict as Map
 import           Data.Maybe
-import           Data.Set (Set)
-import qualified Data.Set as Set
 import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import           Data.String
@@ -81,7 +79,6 @@
 import           Lang.Crucible.LLVM.Extension
 import           Lang.Crucible.LLVM.MemModel
 import           Lang.Crucible.LLVM.MemType
-import qualified Lang.Crucible.LLVM.PrettyPrint as LPP
 import           Lang.Crucible.LLVM.Translation.Constant
 import           Lang.Crucible.LLVM.Translation.Expr
 import           Lang.Crucible.LLVM.Translation.Monad
@@ -159,7 +156,7 @@
     L.CallBr ty _ _ _ _ -> throwError $ unwords ["unexpected non-function type in callbr:", show ty]
     L.Alloca ty _ _ -> liftMemType (L.PtrTo ty)
     L.Load tp _ _ _ -> liftMemType tp
-    L.ICmp _op tv _ -> do
+    L.ICmp _samesign _op tv _ -> do
       inpType <- liftMemType (L.typedType tv)
       case inpType of
         VecType len _ -> return (VecType len (IntType 1))
@@ -171,8 +168,8 @@
         _ -> return (IntType 1)
     L.Phi tp _   -> liftMemType tp
 
-    L.GEP inbounds baseTy basePtr elts ->
-       do gepRes <- runExceptT (translateGEP inbounds baseTy basePtr elts)
+    L.GEP attrs baseTy basePtr elts ->
+       do gepRes <- runExceptT (translateGEP attrs baseTy basePtr elts)
           case gepRes of
             Left err -> throwError err
             Right (GEPResult lanes tp _gep) ->
@@ -237,10 +234,14 @@
     -> LLVMGenerator s arch ret (LLVMExpr s arch)
 extractElt _instr ty _n (UndefExpr _) _i =
    return $ UndefExpr ty
+extractElt _instr ty _n (PoisonExpr _) _i =
+   return $ PoisonExpr ty
 extractElt _instr ty _n (ZeroExpr _) _i =
    return $ ZeroExpr ty
 extractElt _ ty _ _ (UndefExpr _) =
    return $ UndefExpr ty
+extractElt _ ty _ _ (PoisonExpr _) =
+   return $ PoisonExpr ty
 extractElt instr ty n v (ZeroExpr zty) =
    let ?err = fail in
    zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> extractElt instr ty n v (BaseExpr tyr ex)
@@ -293,12 +294,16 @@
     -> LLVMGenerator s arch ret (LLVMExpr s arch)
 insertElt _ ty _ _ _ (UndefExpr _) = do
    return $ UndefExpr ty
+insertElt _ ty _ _ _ (PoisonExpr _) = do
+   return $ PoisonExpr ty
 insertElt instr ty n v a (ZeroExpr zty) = do
    let ?err = fail
    zeroExpand (proxy# :: Proxy# arch) zty $ \_archProxy tyr ex -> insertElt instr ty n v a (BaseExpr tyr ex)
 
 insertElt instr ty n (UndefExpr _) a i  = do
   insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (UndefExpr ty))) a i
+insertElt instr ty n (PoisonExpr _) a i  = do
+  insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (PoisonExpr ty))) a i
 insertElt instr ty n (ZeroExpr _) a i   = do
   insertElt instr ty n (VecExpr ty (Seq.replicate (fromInteger n) (ZeroExpr ty))) a i
 
@@ -357,6 +362,11 @@
  where tps = map fiType $ toList $ siFields si
 extractValue (UndefExpr (ArrayType n tp)) is =
    extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) is
+extractValue (PoisonExpr (StructType si)) is =
+   extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, PoisonExpr tp)) tps) is
+ where tps = map fiType $ toList $ siFields si
+extractValue (PoisonExpr (ArrayType n tp)) is =
+   extractValue (VecExpr tp $ Seq.replicate (fromIntegral n) (PoisonExpr tp)) is
 extractValue (ZeroExpr (StructType si)) is =
    extractValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) is
  where tps = map fiType $ toList $ siFields si
@@ -390,6 +400,11 @@
  where tps = map fiType $ toList $ siFields si
 insertValue (UndefExpr (ArrayType n tp)) v is =
    insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (UndefExpr tp)) v is
+insertValue (PoisonExpr (StructType si)) v is =
+   insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, PoisonExpr tp)) tps) v is
+ where tps = map fiType $ toList $ siFields si
+insertValue (PoisonExpr (ArrayType n tp)) v is =
+   insertValue (VecExpr tp $ Seq.replicate (fromIntegral n) (PoisonExpr tp)) v is
 insertValue (ZeroExpr (StructType si)) v is =
    insertValue (StructExpr $ Seq.fromList $ map (\tp -> (tp, ZeroExpr tp)) tps) v is
  where tps = map fiType $ toList $ siFields si
@@ -533,8 +548,8 @@
              in
                -- Multiplication overflow will result in a pointer which is not "in
                -- bounds" for the given allocation. We translate all GEP
-               -- instructions as if they had the `inbounds` flag set, so the
-               -- result would be a poison value.
+               -- instructions as if they had the `inbounds` attribute set, so
+               -- the result would be a poison value.
                poisonSideCondition mvar (BVRepr PtrWidth) poison off0 cond
 
      -- Perform the pointer offset arithmetic
@@ -575,8 +590,10 @@
   | n == m = VecExpr outty <$> traverse (\x -> translateConversion instr op inty x outty) xs
 
 -- Otherwise, assume scalar values and do the basic conversions
-translateConversion instr op _inty x outty =
- let showI = showInstr instr in
+translateConversion instr op _inty x outty = do
+ mvar <- getMemVar
+ let showI = showInstr instr
+ let noLaxArith = not (laxArith ?transOpts)
  case op of
     L.IntToPtr -> do
        llvmTypeAsRepr outty $ \outty' ->
@@ -599,26 +616,46 @@
               , Just Refl <- testEquality w' PtrWidth -> return x
            _ -> fail (unlines ["pointer-to-integer conversion failed", showI])
 
-    L.Trunc -> do
+    L.Trunc nuw nsw -> do
        llvmTypeAsRepr outty $ \outty' ->
          case (asScalar x, outty') of
            (Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
              | Just LeqProof <- isPosNat w'
              , Just LeqProof <- testLeq (incNat w') w ->
                  do x_bv <- pointerAsBitvectorExpr w x'
-                    let bv' = App (BVTrunc w' w x_bv)
-                    return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
+                    bv' <- AtomExpr <$> mkAtom (App (BVTrunc w' w x_bv))
+                    result <- sideConditionsA mvar (BVRepr w') bv'
+                      [ ( nuw && noLaxArith
+                        , fmap (App . BVEq w x_bv . AtomExpr)
+                               (mkAtom (App (BVZext w w' bv')))
+                        , UB.PoisonValueCreated $ Poison.TruncNoUnsignedWrap x_bv
+                        )
+                      , ( nsw && noLaxArith
+                        , fmap (App . BVEq w x_bv . AtomExpr)
+                               (mkAtom (App (BVSext w w' bv')))
+                        , UB.PoisonValueCreated $ Poison.TruncNoSignedWrap x_bv
+                        )
+                      ]
+                    return (BaseExpr outty' (BitvectorAsPointerExpr w' result))
            _ -> fail (unlines [unwords ["invalid truncation:", show x, show outty], showI])
 
-    L.ZExt -> do
+    L.ZExt nneg -> do
        llvmTypeAsRepr outty $ \outty' ->
          case (asScalar x, outty') of
            (Scalar _archProxy (LLVMPointerRepr w) x', (LLVMPointerRepr w'))
              | Just LeqProof <- isPosNat w
              , Just LeqProof <- testLeq (incNat w) w' ->
                  do x_bv <- pointerAsBitvectorExpr w x'
-                    let bv' = App (BVZext w' w x_bv)
-                    return (BaseExpr outty' (BitvectorAsPointerExpr w' bv'))
+                    bv' <- AtomExpr <$> mkAtom (App (BVZext w' w x_bv))
+                    let z = App $ BVLit w $ BV.zero w
+                    result <-
+                      sideConditionsA mvar (BVRepr w') bv'
+                        [ ( nneg
+                          , pure $ App $ BVSle w z x_bv
+                          , UB.PoisonValueCreated $ Poison.ZExtNonNegative x_bv
+                          )
+                        ]
+                    return (BaseExpr outty' (BitvectorAsPointerExpr w' result))
            _ -> fail (unlines [unwords ["invalid zero extension:", show x, show outty], showI])
 
     L.SExt -> do
@@ -638,12 +675,21 @@
     L.BitCast -> bitCast _inty x outty
 #endif
 
-    L.UiToFp -> do
+    L.UiToFp nneg -> do
        llvmTypeAsRepr outty $ \outty' ->
          case (asScalar x, outty') of
            (Scalar _archProxy (LLVMPointerRepr w) x', FloatRepr fi) -> do
              bv <- pointerAsBitvectorExpr w x'
-             return $ BaseExpr (FloatRepr fi) $ App $ FloatFromBV fi RNE bv
+             bvFp <- AtomExpr <$> mkAtom (App (FloatFromBV fi RNE bv))
+             let z = App $ BVLit w $ BV.zero w
+             result <-
+               sideConditionsA mvar outty' bvFp
+                 [ ( nneg
+                   , pure $ App $ BVSle w z bv
+                   , UB.PoisonValueCreated $ Poison.UiToFpNonNegative bv
+                   )
+                 ]
+             return $ BaseExpr (FloatRepr fi) result
            _ -> fail (unlines [unwords ["Invalid uitofp:", show op, show x, show outty], showI])
 
     L.SiToFp -> do
@@ -699,6 +745,8 @@
 
 bitCast _ (UndefExpr _) tgtT = return (UndefExpr tgtT)
 
+bitCast _ (PoisonExpr _) tgtT = return (PoisonExpr tgtT)
+
 -- pointer casts always succeed
 bitCast (PtrType _) expr (PtrType _) = return expr
 bitCast (PtrType _) expr PtrOpaqueType = return expr
@@ -1269,25 +1317,30 @@
 
 
 integerCompare ::
+  -- ^ If 'True', require that the arguments have the same sign.
+  Bool ->
   L.ICmpOp ->
   MemType ->
   LLVMExpr s arch ->
   LLVMExpr s arch ->
   LLVMGenerator s arch ret (LLVMExpr s arch)
-integerCompare op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
-  VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare op tp x y) xs ys)
+integerCompare samesign op (VecType n tp) (explodeVector n -> Just xs) (explodeVector n -> Just ys) =
+  VecExpr (IntType 1) <$> sequence (Seq.zipWith (\x y -> integerCompare samesign op tp x y) xs ys)
 
-integerCompare op _ x y = do
-  b <- scalarIntegerCompare op x y
+integerCompare samesign op _ x y = do
+  b <- scalarIntegerCompare samesign op x y
   return (BaseExpr (LLVMPointerRepr (knownNat :: NatRepr 1))
                    (BitvectorAsPointerExpr knownNat (App (BoolToBV knownNat b))))
 
 scalarIntegerCompare ::
+  -- ^ If 'True', require that the arguments have the same sign.
+  Bool ->
   L.ICmpOp ->
   LLVMExpr s arch ->
   LLVMExpr s arch ->
   LLVMGenerator s arch ret (Expr LLVM s BoolType)
-scalarIntegerCompare op x y =
+scalarIntegerCompare samesign op x y = do
+  mvar <- getMemVar
   case (asScalar x, asScalar y) of
     (Scalar _archProxy (LLVMPointerRepr w) x'', Scalar _archProxy' (LLVMPointerRepr w') y'')
        | Just Refl <- testEquality w w'
@@ -1296,7 +1349,14 @@
        | Just Refl <- testEquality w w'
        -> do xbv <- pointerAsBitvectorExpr w x''
              ybv <- pointerAsBitvectorExpr w y''
-             return (intcmp w op xbv ybv)
+             result <- AtomExpr <$> mkAtom (intcmp w op xbv ybv)
+             let z = App $ BVLit w $ BV.zero w
+             sideConditionsA mvar BoolRepr result
+               [ ( samesign
+                 , pure $ App $ BoolEq (App (BVSlt w xbv z)) (App (BVSlt w ybv z))
+                 , UB.PoisonValueCreated $ Poison.ICmpSameSign xbv ybv
+                 )
+               ]
     _ -> fail $ unlines [ "arithmetic comparison on incompatible values"
                         , "Comparison: " ++ show op
                         , "Value 1: " ++ show x
@@ -1512,7 +1572,6 @@
    (?transOpts :: TranslationOptions) =>
    TypeRepr ret   {- ^ Type of the function return value -} ->
    L.BlockLabel   {- ^ The label of the current LLVM basic block -} ->
-   Set L.Ident {- ^ Set of usable identifiers -} ->
    L.Instr        {- ^ The instruction to translate -} ->
    (LLVMExpr s arch -> LLVMGenerator s arch ret ())
      {- ^ A continuation to assign the produced value of this instruction to a register -} ->
@@ -1521,7 +1580,7 @@
           Straightline instructions should enter this continuation,
           but block-terminating instructions should not. -} ->
    LLVMGenerator s arch ret a
-generateInstr retType lab defSet instr assign_f k =
+generateInstr retType lab instr assign_f k =
   case instr of
     -- skip phi instructions, they are handled in definePhiBlock
     L.Phi _ _ -> k
@@ -1589,6 +1648,7 @@
                  do let getV x =
                           case x of
                             UndefExpr _ -> return $ UndefExpr elTy
+                            PoisonExpr _ -> return $ PoisonExpr elTy
                             ZeroExpr _  -> return $ Seq.index v1 0
                             BaseExpr (LLVMPointerRepr _) (BitvectorAsPointerExpr _ (App (BVLit _ i)))
                               | BV.asUnsigned i < inL -> return $ Seq.index v1 (fromIntegral (BV.asUnsigned i))
@@ -1669,11 +1729,14 @@
       callStore vTp ptr' v' align'
       k
 
-    -- NB We treat every GEP as though it has the "inbounds" flag set;
+    -- NB We treat every GEP as though it has the "inbounds" attribute set;
     --    thus, the calculation of out-of-bounds pointers results in
     --    a runtime error.
-    L.GEP inbounds baseTy basePtr elts -> do
-      runExceptT (translateGEP inbounds baseTy basePtr elts) >>= \case
+    --
+    --    TODO(#1605): Don't error immediately if the "inbounds" attribute isn't
+    --    set.
+    L.GEP attrs baseTy basePtr elts -> do
+      runExceptT (translateGEP attrs baseTy basePtr elts) >>= \case
         Left err -> reportError $ fromString $ unlines ["Error translating GEP", err]
         Right gep ->
           do gep' <- traverse (\v -> transTypedValue v) gep
@@ -1690,14 +1753,14 @@
          k
 
     L.Call tailcall fnTy fn args ->
-      callFunction defSet instr tailcall fnTy fn args assign_f >> k
+      callFunction instr tailcall fnTy fn args assign_f >> k
 
     L.Invoke fnTy fn args normLabel _unwindLabel -> do
-      do callFunction defSet instr False fnTy fn args assign_f
+      do callFunction instr False fnTy fn args assign_f
          definePhiBlock lab normLabel
 
     L.CallBr fnTy fn args normLabel otherLabels -> do
-      do callFunction defSet instr False fnTy fn args assign_f
+      do callFunction instr False fnTy fn args assign_f
          for_ otherLabels $ \lab' -> void (definePhiBlock lab lab')
          definePhiBlock lab normLabel
 
@@ -1732,11 +1795,11 @@
            assign_f cmp
            k
 
-    L.ICmp op x y -> do
+    L.ICmp samesign op x y -> do
            tp <- liftMemType' (L.typedType x)
            x' <- transTypedValue x
            y' <- transTypedValue (L.Typed (L.typedType x) y)
-           cmp <- integerCompare op tp x' y'
+           cmp <- integerCompare samesign op tp x' y'
            assign_f cmp
            k
 
@@ -1801,7 +1864,7 @@
 
               let a0 = memTypeAlign (llvmDataLayout ?lc) resTy
               oldVal <- callLoad resTy expectTy ptr' a0
-              cmp <- scalarIntegerCompare L.Ieq oldVal cmpVal
+              cmp <- scalarIntegerCompare False L.Ieq oldVal cmpVal
               let flag = BaseExpr (LLVMPointerRepr (knownNat @1))
                                   (BitvectorAsPointerExpr knownNat
                                      (App (BoolToBV knownNat cmp)))
@@ -2004,7 +2067,6 @@
 -- for debugging intrinsics and breakpoint functions.
 callFunction :: forall s arch ret.
    (?transOpts :: TranslationOptions) =>
-   Set L.Ident {- ^ Set of usable identifiers -} ->
    L.Instr {- ^ Source instruction of the call -} ->
    Bool    {- ^ Is the function a tail call? -} ->
    L.Type  {- ^ type of the function to call -} ->
@@ -2012,42 +2074,8 @@
    [L.Typed L.Value] {- ^ argument list -} ->
    (LLVMExpr s arch -> LLVMGenerator s arch ret ()) {- ^ assignment continuation for return value -} ->
    LLVMGenerator s arch ret ()
-callFunction defSet instr tailCall_ fnTy fn args assign_f
-
-     -- Supports LLVM 4-12
-     | L.ValSymbol "llvm.dbg.declare" <- fn
-     , debugIntrinsics ?transOpts =
-       do mbArgs <- dbgArgs defSet args
-          case mbArgs of
-            Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->
-              do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Declare ptr lv di))
-                 return ()
-            Left msg -> addWarning (Text.pack msg)
-            _ -> addWarning "Unexpected argument in llvm.dbg.declare"
-
-     -- Supports LLVM 6-12
-     | L.ValSymbol "llvm.dbg.addr" <- fn
-     , debugIntrinsics ?transOpts =
-       do mbArgs <- dbgArgs defSet args
-          case mbArgs of
-            Right (asScalar -> Scalar _ PtrRepr ptr, lv, di) ->
-              do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Addr ptr lv di))
-                 return ()
-            Left msg -> addWarning (Text.pack msg)
-            _ -> addWarning "Unexpected argument in llvm.dbg.addr"
-
-     -- Supports LLVM 6-12 (earlier versions had an extra argument)
-     | L.ValSymbol "llvm.dbg.value" <- fn
-     , debugIntrinsics ?transOpts =
-       do mbArgs <- dbgArgs defSet args
-          case mbArgs of
-            Right (asScalar -> Scalar _ repr val, lv, di) ->
-              do _ <- extensionStmt (LLVM_Debug (LLVM_Dbg_Value repr val lv di))
-                 return ()
-            Left msg -> addWarning (Text.pack msg)
-            _ -> addWarning "Unexpected argument in llvm.dbg.value"
-
-     -- Skip calls to other debugging intrinsics.
+callFunction instr tailCall_ fnTy fn args assign_f
+     -- Skip calls to debugging intrinsics.
      | L.ValSymbol nm <- fn
      , nm `elem` [ "llvm.dbg.label"
                  , "llvm.dbg.declare"
@@ -2078,33 +2106,6 @@
 
      | otherwise = callOrdinaryFunction (Just instr) tailCall_ fnTy fn args assign_f
 
--- | Match the arguments used by @dbg.addr@, @dbg.declare@, and @dbg.value@.
-dbgArgs ::
-  Set L.Ident {- ^ Set of usable identifiers -} ->
-  [L.Typed L.Value] {- ^ debug call arguments -} ->
-  LLVMGenerator s arch ret (Either String (LLVMExpr s arch, L.DILocalVariable, L.DIExpression))
-dbgArgs defSet args =
-    case args of
-      [valArg, lvArg, diArg] ->
-        case valArg of
-          L.Typed _ (L.ValMd (L.ValMdValue val)) ->
-            case lvArg of
-              L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoLocalVariable lv))) ->
-                case diArg of
-                  L.Typed _ (L.ValMd (L.ValMdDebugInfo (L.DebugInfoExpression di))) ->
-                    let unusableIdents = Set.difference (useTypedVal val) defSet
-                    in if Set.null unusableIdents then
-                         do v <- transTypedValue val
-                            pure (Right (v, lv, di))
-                       else
-                         do let msg = unwords (["dbg intrinsic def/use violation for:"] ++
-                                       map (show . LPP.ppIdent) (Set.toList unusableIdents))
-                            pure (Left msg)
-                  _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg))
-              _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg))
-          _ -> pure (Left ("dbg: argument 1 expected value metadata, got: " ++ show valArg))
-      _ -> pure (Left ("dbg: expected 3 arguments, got: " ++ show (length args)))
-
 typedValueAsCrucibleValue ::
   L.Typed L.Value ->
   LLVMGenerator s arch ret (Some (Value s))
@@ -2213,6 +2214,12 @@
     case testEquality (typeOfReg r) tpr of
       Just Refl -> assignReg r ex
       Nothing -> reportError $ fromString $ "type mismatch when assigning undef value"
+doAssign (Some r) (PoisonExpr tp) = do
+  let ?err = fail
+  poisonExpand (proxy# :: Proxy# arch) tp $ \_archProxy (tpr :: TypeRepr t) (ex :: Expr LLVM s t) ->
+    case testEquality (typeOfReg r) tpr of
+      Just Refl -> assignReg r ex
+      Nothing -> reportError $ fromString $ "type mismatch when assigning poison value"
 doAssign (Some r) (VecExpr tp vs) = do
   let ?err = fail
   llvmTypeAsRepr tp $ \tpr ->
diff --git a/test/TestFunctions.hs b/test/TestFunctions.hs
--- a/test/TestFunctions.hs
+++ b/test/TestFunctions.hs
@@ -60,7 +60,8 @@
                           (L.PtrTo
                             (L.Alias (L.Ident "class.std::cls"))) Nothing (Just 8))
                         []
-                      , L.Effect L.RetVoid []
+                        []
+                      , L.Effect L.RetVoid [] []
                       ]
                   }
                 ]
diff --git a/test/TestMemory.hs b/test/TestMemory.hs
--- a/test/TestMemory.hs
+++ b/test/TestMemory.hs
@@ -592,8 +592,8 @@
                checkField bak' expectedBV actualPtrRV = do
                  actualSymBV <- projectLLVM_bv bak' $ CS.unRV actualPtrRV
                  Just expectedBV @=? What4.asBV actualSymBV
-           checkField bak struct_bv1 (struct_val'^._1)
-           checkField bak struct_bv2 (struct_val'^._2)
+           checkField bak struct_bv1 (struct_val' ^. _1)
+           checkField bak struct_bv2 (struct_val' ^. _2)
 
      testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = False })
      testWithOpts (?memOpts{ LLVMMem.laxLoadsAndStores = True
diff --git a/test/Tests.hs b/test/Tests.hs
--- a/test/Tests.hs
+++ b/test/Tests.hs
@@ -9,12 +9,13 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
-module Main where
+module Main (main) where
 
 -- Crucible
 import           Lang.Crucible.FunctionHandle ( newHandleAllocator )
 
 import qualified Data.BitVector.Sized as BV
+import           Data.Parameterized.DecidableEq ( decEq )
 import           Data.Parameterized.Some
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.SymbolRepr ( SomeSym(SomeSym) )
@@ -35,6 +36,8 @@
 import           Control.Lens (view)
 import           Control.Monad
 import           Data.Either ( fromRight )
+import           Data.Functor.Classes ( Eq1(liftEq) )
+import           Data.Functor.Identity ( Identity(..) )
 import           Data.Maybe ( catMaybes )
 import           GHC.TypeLits
 import qualified Data.Map.Strict as Map
@@ -46,7 +49,11 @@
 import qualified System.IO as IO
 import qualified System.Process as Proc
 
+
+import qualified What4.Internal as WInt
+
 -- Modules being tested
+import           Lang.Crucible.LLVM.Internal (assertionsEnabled)
 import           Lang.Crucible.LLVM.MemModel ( mkMemVar )
 import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.Translation
@@ -157,7 +164,15 @@
 
        defaultMainWithIngredients llvmTestIngredients $
          testGroup "Tests"
-         [ functionTests
+         [ -- See Note [Asserts] in crucible-llvm
+           testCase "assertions enabled" $ do
+             assertsEnabled <- assertionsEnabled
+             assertBool "assertions should be enabled" assertsEnabled
+         , -- See Note [Asserts] in what4
+           testCase "What4 assertions enabled" $ do
+             assertsEnabled <- WInt.assertionsEnabled
+             assertBool "What4 assertions should be enabled" assertsEnabled
+         , functionTests
          , globalTests
          , memoryTests
          , translationTests
@@ -252,31 +267,133 @@
   "extern_int" ->
     testCase "valid global extern variable reference" $ do
     Some t <- getTrans
-    Map.singleton (L.Symbol "extern_int") (Right (i32, Nothing)) @=?
-      Map.map snd (view globalInitMap t)
+    case snd <$> Map.lookup (L.Symbol "extern_int") (view globalInitMap t) of
+      Just (Right (actualTy, actualMbConst)) -> do
+        let expectedTy = i32
+        let expectedMbConst = Nothing
+        expectedTy @=? actualTy
+        assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst
+      _ -> assertFailure "Could not look up extern_int"
 
   "x=42" ->
     testCase "valid global integer symbol reference" $ do
     Some t <- getTrans
-    Map.singleton (L.Symbol "x") (Right $ (i32, Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42))) @=?
-      Map.map snd (view globalInitMap t)
+    case snd <$> Map.lookup (L.Symbol "x") (view globalInitMap t) of
+      Just (Right (actualTy, actualMbConst)) -> do
+        let expectedTy = i32
+        let expectedMbConst = Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42)
+        expectedTy @=? actualTy
+        assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst
+      _ -> assertFailure "Could not look up x"
 
   "z.xx=17" ->
     testCase "valid global struct field symbol reference" $ do
     Some t <- getTrans
-    IntConst (knownNat @32) (BV.mkBV knownNat 17) @=?
-      case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of
-        Just (Right (_, Just (StructConst _ (x : _)))) -> x
-        _ -> IntConst (knownNat @1) (BV.zero knownNat)
+    case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of
+      Just (Right (_, actualMbConst)) ->
+        case actualMbConst of
+          Just (StructConst _ (actualXField : _)) -> do
+            let expectedXField = IntConst (knownNat @32) (BV.mkBV knownNat 17)
+            assertLiftEq
+              llvmConstSyntacticEq
+              (Identity expectedXField)
+              (Identity actualXField)
+          _ -> assertFailure $
+            "Expected x to be a struct with at least one field, " ++
+            "but it was actually " ++ show actualMbConst
+      _ -> assertFailure "Could not look up z"
 
   "x uninitialized" ->
     testCase "valid global unitialized variable reference" $ do
     Some t <- getTrans
-    Map.singleton (L.Symbol "x") (Right $ (i32, Just $ ZeroConst i32)) @=?
-      Map.map snd (view globalInitMap t)
+    case snd <$> Map.lookup (L.Symbol "x") (view globalInitMap t) of
+      Just (Right (actualTy, actualMbConst)) -> do
+        let expectedTy = i32
+        let expectedMbConst = Just $ ZeroConst i32
+        expectedTy @=? actualTy
+        assertLiftEq llvmConstSyntacticEq expectedMbConst actualMbConst
+      _ -> assertFailure "Could not look up x"
 
   -- We're really just checking that the translation succeeds without
   -- exceptions.
   "" -> testCase "no additional checks" $ return ()
 
   other -> testCase other $ assertFailure $ "Unknown check: " <> other
+
+-- | Helper, not exported
+--
+-- Compare two 'LLVMConst's for syntactic equality. This should not be confused
+-- with the semantic notion of equality that LLVM typically uses. For instance,
+-- this function considers two 'UndefConst's values to be syntactically equal,
+-- but LLVM's semantic equality could deem two @undef@ values to be not equal.
+llvmConstSyntacticEq :: LLVMConst -> LLVMConst -> Bool
+llvmConstSyntacticEq (ZeroConst mem1) (ZeroConst mem2) =
+  mem1 == mem2
+llvmConstSyntacticEq (IntConst w1 x1) (IntConst w2 x2) =
+  case decEq w1 w2 of
+    Left Refl -> x1 == x2
+    Right _   -> False
+llvmConstSyntacticEq (FloatConst f1) (FloatConst f2) =
+  f1 == f2
+llvmConstSyntacticEq (DoubleConst d1) (DoubleConst d2) =
+  d1 == d2
+llvmConstSyntacticEq (LongDoubleConst ld1) (LongDoubleConst ld2) =
+  ld1 == ld2
+llvmConstSyntacticEq (StringConst s1) (StringConst s2) =
+  s1 == s2
+llvmConstSyntacticEq (ArrayConst mem1 a1) (ArrayConst mem2 a2) =
+  mem1 == mem2 && liftEq llvmConstSyntacticEq a1 a2
+llvmConstSyntacticEq (VectorConst mem1 v1) (VectorConst mem2 v2) =
+  mem1 == mem2 && liftEq llvmConstSyntacticEq v1 v2
+llvmConstSyntacticEq (StructConst si1 a1) (StructConst si2 a2) =
+  si1 == si2 && liftEq llvmConstSyntacticEq a1 a2
+llvmConstSyntacticEq (SymbolConst s1 x1) (SymbolConst s2 x2) =
+  s1 == s2 && x1 == x2
+llvmConstSyntacticEq (UndefConst tp1) (UndefConst tp2) =
+  tp1 == tp2
+llvmConstSyntacticEq (PoisonConst tp1) (PoisonConst tp2) =
+  tp1 == tp2
+
+llvmConstSyntacticEq (ZeroConst {}) _ =
+  False
+llvmConstSyntacticEq (IntConst {}) _ =
+  False
+llvmConstSyntacticEq (FloatConst {}) _ =
+  False
+llvmConstSyntacticEq (DoubleConst {}) _ =
+  False
+llvmConstSyntacticEq (LongDoubleConst {}) _ =
+  False
+llvmConstSyntacticEq (StringConst {}) _ =
+  False
+llvmConstSyntacticEq (ArrayConst {}) _ =
+  False
+llvmConstSyntacticEq (VectorConst {}) _ =
+  False
+llvmConstSyntacticEq (StructConst {}) _ =
+  False
+llvmConstSyntacticEq (SymbolConst {}) _ =
+  False
+llvmConstSyntacticEq (UndefConst {}) _ =
+  False
+llvmConstSyntacticEq (PoisonConst {}) _ =
+  False
+
+-- | Helper, not exported
+--
+-- Like 'assertEqual', but lifted to work over an 'Eq1' instance instead of an
+-- 'Eq' instance. In addition, this allows the user to customize how to check
+-- the underlying values (of type @expected@ and @actual@) for equality.
+assertLiftEq ::
+  (Eq1 f, Show (f expected), Show (f actual), HasCallStack) =>
+  -- | How to check the underlying values for equality
+  (expected -> actual -> Bool) ->
+  -- | The expected value
+  f expected ->
+  -- | The actual value
+  f actual ->
+  Assertion
+assertLiftEq eq expected actual =
+  unless (liftEq eq expected actual) (assertFailure msg)
+  where
+    msg = "expected: " ++ show expected ++ "\n but got: " ++ show actual