Fix macaw-x86-symbolic and update crucible.

deps/crucible

@@ -1 +1 @@
-Subproject commit da77394455d06241c4c01807745922ebb97fe40c
+Subproject commit d0c8f1e1a712e779f9995363689b352ce10b17dd

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

@@ -30,6 +30,9 @@ module Data.Macaw.Symbolic.Backend (
   , MO.doGetGlobal
   , MO.doLookupFunctionHandle
   , MO.doPtrToBits
+  , MO.getMem
+  , MO.setMem
+  , MO.tryGlobPtr
     -- ** Register Mapping
   , PS.RegIndexMap
   , PS.mkRegIndexMap

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

@@ -595,7 +595,7 @@ memReprToStorageType reqEnd memRep =
   case memRep of
     M.BVMemRepr bytes endian -> do
       checkEndian reqEnd endian
-      pure $ Mem.bitvectorType (Bytes (natValue bytes))
+      pure $ Mem.bitvectorType (Bytes (intValue bytes))
     M.FloatMemRepr floatRep endian -> do
       checkEndian reqEnd endian
       case floatRep of
@@ -605,7 +605,7 @@ memReprToStorageType reqEnd memRep =
         _ -> Left $ "Do not support memory accesses to " ++ show floatRep ++ " values."
     M.PackedVecMemRepr n eltType -> do
       eltStorageType <- memReprToStorageType reqEnd eltType
-      pure $ Mem.arrayType (Bytes (natValue n)) eltStorageType
+      pure $ Mem.arrayType (Bytes (intValue n)) eltStorageType
 
 -- | Convert a Crucible register value to a LLVM memory mode lvalue
 resolveMemVal :: MemRepr ty -> -- ^ What/how we are writing
@@ -623,7 +623,7 @@ resolveMemVal (M.FloatMemRepr floatRep _endian) _ val =
     _ -> error $ "Do not support memory accesses to " ++ show floatRep ++ " values."
 resolveMemVal (M.PackedVecMemRepr n eltType) stp val =
   case Mem.storageTypeF stp of
-    Mem.Array cnt eltStp | cnt == fromIntegral (natValue n), fromIntegral (V.length val) == natValue n ->
+    Mem.Array cnt eltStp | cnt == Bytes (intValue n), fromIntegral (V.length val) == natValue n ->
       Mem.LLVMValArray eltStp (resolveMemVal eltType eltStp <$> val)
     _ -> error $ "Unexpected storage type for packed vec."
 

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

@@ -70,13 +70,13 @@ import           Lang.Crucible.LLVM.MemModel
                    )
 
 import qualified Data.Macaw.CFG.Core as M
+import qualified Data.Macaw.CFG.Core as MC
 import qualified Data.Macaw.Memory as M
-import qualified Data.Macaw.Types as M
 import           Data.Macaw.Symbolic
 import           Data.Macaw.Symbolic.Backend
+import qualified Data.Macaw.Types as M
 import qualified Data.Macaw.X86 as M
 import qualified Data.Macaw.X86.ArchTypes as M
-import qualified Data.Macaw.CFG.Core as MC
 
 import           Prelude
 
@@ -134,35 +134,29 @@ stmtSemantics _sym_funs global_var_mem globals stmt state = do
         let mem_repr = M.repValSizeMemRepr val_size
         curr_dest_ptr <- ptrAdd sym knownNat (regValue dest) offset
         curr_src_ptr <- ptrAdd sym knownNat (regValue src) offset
-        (val, after_read_state) <- doReadMem
-          acc_state
-          global_var_mem
-          globals
-          M.Addr64
-          mem_repr
-          (RegEntry knownRepr curr_src_ptr)
-        (_, after_write_state) <- doWriteMem
-          after_read_state
-          global_var_mem
-          globals
-          M.Addr64
-          mem_repr
-          (RegEntry knownRepr curr_dest_ptr)
-          (RegEntry (typeToCrucible $ M.typeRepr mem_repr) val)
-        return after_write_state
+        -- Get simulator and memory
+        mem <- getMem acc_state global_var_mem
+        -- Resolve source pointer
+        resolvedSrcPtr <- tryGlobPtr sym mem globals curr_src_ptr
+        -- Read resolvePtr
+        val <- doReadMem sym mem M.Addr64 mem_repr resolvedSrcPtr
+        -- Resolve destination pointer
+        resolvedDestPtr <- tryGlobPtr sym mem globals curr_dest_ptr
+        afterWriteMem <- doWriteMem sym mem M.Addr64 mem_repr resolvedDestPtr val
+        -- Update the final state
+        pure $! setMem acc_state global_var_mem afterWriteMem
     M.RepStos val_size (AtomWrapper dest) (AtomWrapper val) count dir ->
       withConcreteCountAndDir state val_size count dir $ \acc_state offset -> do
-          let mem_repr = M.repValSizeMemRepr val_size
-          curr_dest_ptr <- ptrAdd sym knownNat (regValue dest) offset
-          (_, after_write_state) <- doWriteMem
-            acc_state
-            global_var_mem
-            globals
-            M.Addr64
-            mem_repr
-            (RegEntry knownRepr curr_dest_ptr)
-            val
-          return after_write_state
+        let mem_repr = M.repValSizeMemRepr val_size
+        -- Get simulator and memory
+        mem <- getMem acc_state global_var_mem
+        -- Resolve address to write to.
+        curr_dest_ptr <- ptrAdd sym knownNat (regValue dest) offset
+        resolvedDestPtr <- tryGlobPtr sym mem globals curr_dest_ptr
+        -- Perform write
+        afterWriteMem <- doWriteMem sym mem M.Addr64 mem_repr resolvedDestPtr (regValue val)
+        -- Update the final state
+        pure $! setMem acc_state global_var_mem afterWriteMem
     _ -> error $
       "Symbolic execution semantics for x86 statement are not implemented yet: "
       <> (show $ MC.ppArchStmt (liftAtomIn (pretty . regType)) stmt)

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

@@ -216,6 +216,7 @@ freshValue sym str w ty =
          WI.freshConstant sym nm C.BaseBoolRepr
 
     M.TupleTypeRepr {} -> crash [ "Unexpected symbolic tuple:", show str ]
+    M.VecTypeRepr {} -> crash [ "Unexpected symbolic vector:", show str ]
 
   where
   symName x =