Merge pull request #1592 from GaloisInc/macaw-264

Bump `macaw` submodule, adapt to GaloisInc/macaw#264
GaloisInc · Feb 22, 2022 · 70f5197 · 70f5197
2 parents 2c726dd + 2847921
commit 70f5197
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 4 deletions.
diff --git a/deps/macaw b/deps/macaw
diff --git 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
@@ -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.
+1 −1		macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
+7 −7		macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/Functions.hs
+1 −1		macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
+15 −15		macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Functions.hs
+9 −0		symbolic/ChangeLog.md
+16 −16		symbolic/src/Data/Macaw/Symbolic.hs
+2 −2		symbolic/src/Data/Macaw/Symbolic/Backend.hs
+11 −2		symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+7 −7		symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+2 −2		symbolic/src/Data/Macaw/Symbolic/Testing.hs
+11 −11		x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+1 −1		x86_symbolic/src/Data/Macaw/X86/Symbolic.hs