From dcf553643c9c795ebe7f48c051a2d33d119acb87 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Nov 2021 16:37:14 -0500 Subject: [PATCH 1/2] Update llvm-pretty-bc-parser submodule This updates the `llvm-pretty-bc-parser` to include these PRs: * GaloisInc/llvm-pretty-bc-parser#159 (`Support parsing fneg instructions`) * GaloisInc/llvm-pretty-bc-parser#166 (`Support parsing freeze instructions`) * GaloisInc/llvm-pretty-bc-parser#164 (`Parse DebugInfoEnumerator properly on LLVM 12+`) * GaloisInc/llvm-pretty-bc-parser#162 (`Support parsing dict{Associated,Allocated,Rank} fields introduced in LLVM 12`) The `llvm-pretty` submodule had corresponding changes as well. These were included as part of a previous commit to update the `llvm-pretty` submodule (952fe5578d0409c14fb8b6552534965dbd818f75), but the `llvm-pretty-bc-parser` submodule was not updated at the same time. This commit brings the two back into harmony. --- deps/llvm-pretty-bc-parser | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser index bea158b7..24dc69a4 160000 --- a/deps/llvm-pretty-bc-parser +++ b/deps/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit bea158b759d7315cdb4f4c4a364c9fd2c2f9b5a4 +Subproject commit 24dc69a4e718193d65874d84466a7daecf8d8356 From b1b5a72fd358e7d71ded7247806c21ef510f9c7f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 22 Nov 2021 16:41:28 -0500 Subject: [PATCH 2/2] 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