Merge remote-tracking branch 'public/stable' into jhx-x86-improvements

deps/crucible

@@ -1 +1 @@
-Subproject commit 536faad39d9dce9476e69dd6ccfecd1ff4948817
+Subproject commit 60a10a7933bcfab2c444dd436aee82eed449cec9

symbolic/src/Data/Macaw/Symbolic.hs

@@ -59,14 +59,14 @@ import           What4.Symbol (userSymbol)
 import qualified Lang.Crucible.Analysis.Postdom as C
 import           Lang.Crucible.Backend
 import qualified Lang.Crucible.CFG.Core as C
+import qualified Lang.Crucible.CFG.Extension as C
 import qualified Lang.Crucible.CFG.Reg as CR
 import qualified Lang.Crucible.CFG.SSAConversion as C
 import qualified Lang.Crucible.FunctionHandle as C
+
+import qualified Lang.Crucible.Simulator as C
 import qualified Lang.Crucible.Simulator.ExecutionTree as C
-import qualified Lang.Crucible.Simulator.Intrinsics as C
 import qualified Lang.Crucible.Simulator.GlobalState as C
-import qualified Lang.Crucible.Simulator.OverrideSim as C
-import qualified Lang.Crucible.Simulator.RegMap as C
 
 import           System.IO (stdout)
 
@@ -421,7 +421,7 @@ execMacawStmtExtension archStmtFn mvar globs lookupH s0 st =
                M.BoolTypeRepr -> freshConstant sym nm C.BaseBoolRepr
                _ -> error ("MacawFreshSymbolic: XXX type " ++ show t)
          return (v,st)
-      where sym = C.stateSymInterface st
+      where sym = st^.C.stateSymInterface
 
     MacawLookupFunctionHandle _ args -> do
       hv <- C.HandleFnVal <$> doLookupFunctionHandle lookupH st mvar (C.regValue args)
@@ -506,7 +506,7 @@ type GlobalMap sym arch = Map M.RegionIndex
 
 -- | Run the simulator over a contiguous set of code.
 runCodeBlock :: forall sym arch blocks
-           .  IsSymInterface sym
+           .  (C.IsSyntaxExtension (MacawExt arch), IsSymInterface sym)
            => sym
            -> MacawSymbolicArchFunctions arch
               -- ^ Translation functions
@@ -542,8 +542,8 @@ runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH g regStruct = d
                          }
   -- Create the symbolic simulator state
   let initGlobals = C.insertGlobal mvar initMem C.emptyGlobals
-  let s = C.initSimState ctx initGlobals C.defaultErrorHandler
-  a <- C.runOverrideSim s macawStructRepr $ do
+  let s = C.initSimState ctx initGlobals C.defaultAbortHandler
+  a <- C.executeCrucible s $ C.runOverrideSim macawStructRepr $ do
     let args :: C.RegMap sym (MacawFunctionArgs arch)
         args = C.RegMap (Ctx.singleton (C.RegEntry macawStructRepr regStruct))
     crucGenArchConstraints archFns $

symbolic/src/Data/Macaw/Symbolic/MemOps.hs

@@ -126,7 +126,7 @@ doGetGlobal st mvar globs addr =
                         ]
     Just region ->
       do mem <- getMem st mvar
-         let sym = stateSymInterface st
+         let sym = st^.stateSymInterface
          let w = M.addrWidthRepr addr
          LeqProof <- pure $ addrWidthAtLeast16 w
          let ?ptrWidth = M.addrWidthNatRepr w
@@ -328,7 +328,7 @@ doReadMem st mvar globs w (BVMemRepr bytes endian) ptr0 =
   do mem <- getMem st mvar
      checkEndian mem endian
 
-     let sym   = stateSymInterface st
+     let sym   = st^.stateSymInterface
          ty    = bitvectorType (toBytes (widthVal bytes))
          bitw  = natMultiply (knownNat @8) bytes
 
@@ -370,7 +370,7 @@ doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
          def  = regValue def0
      mem <- getMem st mvar
      checkEndian mem endian
-     let sym   = stateSymInterface st
+     let sym   = st^.stateSymInterface
          ty    = bitvectorType (toBytes (widthVal bytes))
          bitw  = natMultiply (knownNat @8) bytes
 
@@ -419,7 +419,7 @@ doWriteMem st mvar globs w (BVMemRepr bytes endian) ptr0 val =
   do mem <- getMem st mvar
      checkEndian mem endian
 
-     let sym   = stateSymInterface st
+     let sym   = st^.stateSymInterface
          ty    = bitvectorType (toBytes (widthVal bytes))
 
      LeqProof <- pure $ addrWidthIsPos w
@@ -477,7 +477,7 @@ ptrOp ::
 ptrOp k st mvar w x0 y0 =
   do mem <- getMem st mvar
      LeqProof <- return (addrWidthIsPos w)
-     let sym = stateSymInterface st
+     let sym = st^.stateSymInterface
          x   = regValue x0
          y   = regValue y0
 

x86_symbolic/src/Data/Macaw/X86/Crucible.hs

@@ -31,12 +31,11 @@ module Data.Macaw.X86.Crucible
 
   ) where
 
-import           Data.Parameterized.NatRepr
+import           Control.Lens ((^.))
+import           Data.Bits hiding (xor)
 import           Data.Parameterized.Context.Unsafe (empty,extend)
-
-import           Data.Bits (shiftR, (.&.))
+import           Data.Parameterized.NatRepr
 import           Data.Word (Word8)
-import           Data.Bits (shiftL,testBit)
 import           GHC.TypeLits (KnownNat)
 
 import           What4.Interface hiding (IsExpr)
@@ -72,8 +71,8 @@ funcSemantics ::
   SymFuns sym ->
   M.X86PrimFn (AtomWrapper (RegEntry sym)) mt ->
   S sym rtp bs r ctx -> IO (RegValue sym t, S sym rtp bs r ctx)
-funcSemantics fs x s = do let sym = Sym { symIface = stateSymInterface s
-                                        , symTys   = stateIntrinsicTypes s
+funcSemantics fs x s = do let sym = Sym { symIface = s^.stateSymInterface
+                                        , symTys   = s^.stateIntrinsicTypes
                                         , symFuns  = fs
                                         }
                           v <- pureSem sym x

x86_symbolic/tests/Main.hs

@@ -131,7 +131,7 @@ main = do
      MS.runCodeBlock sym x86ArchFns (MX.x86_64MacawEvalFn symFuns)
         halloc (initMem, globalMap) lookupFn g regs
   case execResult of
-    (_,C.FinishedExecution _ (C.TotalRes _pair))-> do
+    (_,C.FinishedResult _ (C.TotalRes _pair))-> do
       putStrLn "Done"
     _ -> do
       fail "Partial execution returned."