From d3a53a676920ab56c8252a8d171098f2ad884ea8 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 22 Nov 2021 16:41:28 -0500
Subject: [PATCH] Update crucible, semmc submodules; adapt to
 GaloisInc/crucible#906

This updates the `crucible` submodule to include GaloisInc/crucible#906
(`Control granularity of reading uninitialized memory`), as well as the
`semmc` submodule to bring in corresponding changes on its side
(GaloisInc/semmc#69). Some additional `?memOpts :: MemOptions` constraints
needed to be added to some functions in `macaw-symbolic` and
`macaw-refinement` as a result.
---
 deps/crucible                                             | 2 +-
 deps/semmc                                                | 2 +-
 refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs | 1 +
 symbolic/ChangeLog.md                                     | 2 ++
 symbolic/src/Data/Macaw/Symbolic/Memory.hs                | 1 +
 5 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index f7fa4d20..f7a994dd 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit f7fa4d20ce1248861a41b4e758b49ea9cbc99fdc
+Subproject commit f7a994dd0cddfdf4bdbe5590a8e345e8e69926d6
diff --git a/deps/semmc b/deps/semmc
index 87782b4d..5acea2bd 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit 87782b4d9f21ec24b576170bd0892cdee11a89bc
+Subproject commit 5acea2bdc757d2aabf3b167abb78a701a2427360
diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
index 412692cf..4b129a5d 100644
--- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+++ b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
@@ -508,6 +508,7 @@ initializeMemory :: forall arch sym m proxy
                     , CB.IsSymInterface sym
                     , LLVM.HasLLVMAnn sym
                     , MonadIO m
+                    , ?memOpts :: LLVM.MemOptions
                     )
                  => proxy arch
                  -> sym
diff --git a/symbolic/ChangeLog.md b/symbolic/ChangeLog.md
index b189998a..07efa9f3 100644
--- a/symbolic/ChangeLog.md
+++ b/symbolic/ChangeLog.md
@@ -19,3 +19,5 @@
    - `setMachineRegs`
    - `addExtraBlock`
    - `freshValueIndex`
+
+- `Data.Macaw.Symbolic.Memory.newGlobalMemory` now has a `?memOpts :: MemOptions` constraint.
diff --git a/symbolic/src/Data/Macaw/Symbolic/Memory.hs b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
index a7f79ad9..f7b69847 100644
--- a/symbolic/src/Data/Macaw/Symbolic/Memory.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/Memory.hs
@@ -197,6 +197,7 @@ newGlobalMemory :: ( 16 <= MC.ArchAddrWidth arch
                    , CB.IsSymInterface sym
                    , CL.HasLLVMAnn sym
                    , MonadIO m
+                   , ?memOpts :: CL.MemOptions
                    )
                 => proxy arch
                 -- ^ A proxy to fix the architecture