From 2791b1050f348922a27192d8a73ee538fed57629 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Thu, 9 Jun 2022 10:57:52 -0400
Subject: [PATCH] Adapt to GaloisInc/crucible#998

This bumps the `crucible` submodule to bring in the changes from
GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to
a handful of additional functions. This requires adding constraints to
some functions in `macaw-symbolic` to accommodate, as well as bumping the
`semmc` submodule to bring in analogous changes from GaloisInc/semmc#76.
---
 deps/crucible                              | 2 +-
 deps/semmc                                 | 2 +-
 symbolic/ChangeLog.md                      | 4 +++-
 symbolic/src/Data/Macaw/Symbolic/MemOps.hs | 4 ++--
 4 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index 1d2d95d2..994b4f94 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 1d2d95d232eb2aae076d68021e1d75d322968595
+Subproject commit 994b4f944630c561b9390f2a5f8d53d40f7318e5
diff --git a/deps/semmc b/deps/semmc
index a3b8b89b..fd356864 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit a3b8b89b9e88c94aab2ec6e06f993edcc9126cea
+Subproject commit fd3568642e1ffc0c31dab172f4f430c3c009286c
diff --git a/symbolic/ChangeLog.md b/symbolic/ChangeLog.md
index ecde0643..6c87f215 100644
--- a/symbolic/ChangeLog.md
+++ b/symbolic/ChangeLog.md
@@ -34,4 +34,6 @@
    - `addExtraBlock`
    - `freshValueIndex`
 
-- `Data.Macaw.Symbolic.Memory.newGlobalMemory` now has a `?memOpts :: MemOptions` constraint.
+- The following functions now have a `?memOpts :: MemOptions` constraint:
+  - `Data.Macaw.Symbolic.Memory.newGlobalMemory`
+  - `Data.Macaw.Symbolic.MemOps.{doWriteMem,doCondWriteMem}`
diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
index fba78e7d..4aa6c392 100644
--- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
@@ -1073,7 +1073,7 @@ doCondReadMem bak mem ptrWidth memRep cond ptr def = hasPtrClass ptrWidth $
 --     arg5 : Address to write to
 --     arg6 : Value to write
 doWriteMem ::
-  (IsSymBackend sym bak, Mem.HasLLVMAnn sym) =>
+  (IsSymBackend sym bak, Mem.HasLLVMAnn sym, ?memOpts :: Mem.MemOptions) =>
   bak ->
   MemImpl sym ->
   M.AddrWidthRepr ptrW ->
@@ -1104,7 +1104,7 @@ doWriteMem bak mem ptrWidth memRep ptr val = hasPtrClass ptrWidth $
 --     arg6 : Address to write to
 --     arg7 : Value to write
 doCondWriteMem ::
-  (IsSymBackend sym bak, Mem.HasLLVMAnn sym) =>
+  (IsSymBackend sym bak, Mem.HasLLVMAnn sym, ?memOpts :: Mem.MemOptions) =>
   bak ->
   MemImpl sym ->
   M.AddrWidthRepr ptrW ->