Update and adapt to GaloisInc/macaw#230.

GaloisInc · Oct 27, 2021 · 6d31d53 · 6d31d53
1 parent 2bbe28d
commit 6d31d53
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 4 deletions.
diff --git a/deps/macaw b/deps/macaw
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -386,10 +386,12 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
                       [ "Unable to find CFG for function at address "
                       , show $ W4.ppExpr off
                       ]
+        archEvalFns = Macaw.x86_64MacawEvalFn sfs Macaw.defaultMacawArchStmtExtensionOverride
         lookupSyscall = Macaw.unsupportedSyscalls "saw-script"
         noExtraValidityPred _ _ _ _ = return Nothing
-        defaultMacawExtensions_x86_64 = Macaw.macawExtensions
-          (Macaw.x86_64MacawEvalFn sfs) mvar
+        defaultMacawExtensions_x86_64 =
+          Macaw.macawExtensions
+          archEvalFns mvar
           (mkGlobalMap . Map.singleton 0 $ preState ^. x86GlobalBase)
           funcLookup
           lookupSyscall

diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
@@ -105,6 +105,7 @@ import Data.Macaw.Symbolic( ArchRegStruct
                           , MacawSimulatorState(..)
                           , macawExtensions
                           , unsupportedSyscalls
+                          , defaultMacawArchStmtExtensionOverride
                           )
 import qualified Data.Macaw.Symbolic as Macaw ( LookupFunctionHandle(..) )
 import Data.Macaw.Symbolic( MacawExt
@@ -474,14 +475,15 @@ doSim opts elf sfs name (globs,overs) st checkPost =
        -- The memory setup for this verifier does not have that problem, and
        -- thus does not need any additional validity predicates.
        let noExtraValidityPred _ _ _ _ = return Nothing
+       let archEvalFns = x86_64MacawEvalFn sfs defaultMacawArchStmtExtensionOverride
        let lookupSyscall = unsupportedSyscalls "saw-script"
        let ctx :: SimContext (MacawSimulatorState Sym) Sym (MacawExt X86_64)
            ctx = SimContext { _ctxSymInterface = sym
                               , ctxSolverProof = \a -> a
                               , ctxIntrinsicTypes = llvmIntrinsicTypes
                               , simHandleAllocator = allocator opts
                               , printHandle = stdout
-                              , extensionImpl = macawExtensions (x86_64MacawEvalFn sfs) mvar globs (callHandler overs sym) lookupSyscall noExtraValidityPred
+                              , extensionImpl = macawExtensions archEvalFns mvar globs (callHandler overs sym) lookupSyscall noExtraValidityPred
                               , _functionBindings = FnBindings $
                                 insertHandleMap (cfgHandle cfg) (UseCFG cfg (postdomInfo cfg)) emptyHandleMap
                               , _cruciblePersonality = MacawSimulatorState
+16 −7		macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
+1 −1		macaw-aarch32-symbolic/tests/Main.hs
+21 −8		macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
+1 −1		macaw-ppc-symbolic/tests/Main.hs
+1 −1		refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+1 −1		refinement/tests/RefinementTests.hs
+1 −1		symbolic/examples/translation.hs
+32 −3		symbolic/src/Data/Macaw/Symbolic.hs
+17 −8		x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+1 −1		x86_symbolic/tests/Main.hs