From 2847921807daa3067622c220832fabb3bc11c3a9 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 21 Feb 2022 13:28:56 -0500 Subject: [PATCH] Bump macaw submodule, adapt to GaloisInc/macaw#264 This bumps the `macaw` submodule, which brings in changes from GaloisInc/macaw#264. This requires explicitly instantiating the new `personality` type variable of `LookupFunctionHandle` to accommodate. --- deps/macaw | 2 +- src/SAWScript/X86.hs | 2 +- src/SAWScript/X86Spec.hs | 7 +++++-- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/deps/macaw b/deps/macaw index ad51ae3c54..a43151963d 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit ad51ae3c54be97f4f7d15e8eaed9344341ce88e4 +Subproject commit a43151963da70e4d4c3d69f9605e82e44ff30731 diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 578d2cbf35..ce90faef4b 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -185,7 +185,7 @@ data Fun = Fun { funName :: ByteString, funSpec :: FunSpec } -------------------------------------------------------------------------------- -type CallHandler = Sym -> Macaw.LookupFunctionHandle Sym X86_64 +type CallHandler = Sym -> Macaw.LookupFunctionHandle (MacawSimulatorState Sym) Sym X86_64 -- | Run a top-level proof. -- Should be used when making a standalone proof script. diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index f160e6bc00..d11e3ef2ae 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -123,7 +123,10 @@ import Lang.Crucible.Types import Verifier.SAW.SharedTerm (Term,scApplyAll,scVector,scBitvector,scAt,scNat) import Data.Macaw.Memory(RegionIndex) -import Data.Macaw.Symbolic(GlobalMap(..), ToCrucibleType, LookupFunctionHandle(..), MacawCrucibleRegTypes) +import Data.Macaw.Symbolic + ( GlobalMap(..), ToCrucibleType, LookupFunctionHandle(..) + , MacawCrucibleRegTypes, MacawSimulatorState + ) import Data.Macaw.Symbolic.Backend ( crucArchRegTypes ) import Data.Macaw.X86.X86Reg import Data.Macaw.X86.Symbolic @@ -1203,7 +1206,7 @@ _debugDumpGoals opts = sh (ProofGoal _hyps g) = print (view labeledPredMsg g) -type Overrides = Map (Natural,Integer) (Sym -> LookupFunctionHandle Sym X86_64) +type Overrides = Map (Natural,Integer) (Sym -> LookupFunctionHandle (MacawSimulatorState Sym) Sym X86_64) -- | Use a specification to verify a function. -- Returns the initial state for the function, and a post-condition.