Merge branch 'master' of github.com:GaloisInc/macaw

x86/src/Data/Macaw/X86/ArchTypes.hs

@@ -73,7 +73,7 @@ instance HasRepr SIMDWidth NatRepr where
 ------------------------------------------------------------------------
 -- RepValSize
 
--- | Rep value
+-- | A value for distinguishing between 1,2,4 and 8 byte values.
 data RepValSize w
    = (w ~  8) => ByteRepVal
    | (w ~ 16) => WordRepVal
@@ -807,40 +807,40 @@ x86PrimFnHasSideEffects f =
 -- X86Stmt
 
 -- | An X86 specific statement.
-data X86Stmt (v :: Type -> *)
-   = forall tp .
-     WriteLoc !(X86PrimLoc tp) !(v tp)
-   | StoreX87Control !(v (BVType 64))
-     -- ^ Store the X87 control register in the given location.
-   | MemCopy !Integer
-             !(v (BVType 64))
-             !(v (BVType 64))
-             !(v (BVType 64))
-             !(v BoolType)
-     -- ^ Copy a region of memory from a source buffer to a destination buffer.
-     --
-     -- In an expression @MemCopy bc v src dest dir@
-     -- * @bc@ is the number of bytes to copy at a time (1,2,4,8)
-     -- * @v@ is the number of values to move.
-     -- * @src@ is the start of source buffer.
-     -- * @dest@ is the start of destination buffer.
-     -- * @dir@ is a flag that indicates whether direction of move:
-     --   * 'True' means we should decrement buffer pointers after each copy.
-     --   * 'False' means we should increment the buffer pointers after each copy.
-   | forall n .
-     MemSet !(v (BVType 64))
-            -- /\ Number of values to assign
-            !(v (BVType n))
-            -- /\ Value to assign
-            !(v (BVType 64))
-            -- /\ Address to start assigning from.
-            !(v BoolType)
-            -- /\ Direction flag
+data X86Stmt (v :: Type -> *) where
+  WriteLoc :: !(X86PrimLoc tp) -> !(v tp) -> X86Stmt v
+  StoreX87Control :: !(v (BVType 64)) -> X86Stmt v
+  -- ^ Store the X87 control register in the given address.
 
-    | EMMS
-      -- ^ Empty MMX technology State. Sets the x87 FPU tag word to empty.
-      -- Probably OK to use this for both EMMS FEMMS, the second being a
-      -- a faster version from AMD 3D now.
+  RepMovs :: !(RepValSize w)
+          -> !(v (BVType 64))
+          -> !(v (BVType 64))
+          -> !(v (BVType 64))
+          -> !(v BoolType)
+          -> X86Stmt v
+  -- ^ Copy a region of memory from a source buffer to a destination buffer.
+  --
+  -- In an expression @RepMovs bc cnt src dest dir@
+  -- * @bc@ denotes the bytes to copy at a time.
+  -- * @cnt@ is the number of values to move.
+  -- * @src@ is the start of source buffer.
+  -- * @dest@ is the start of destination buffer.
+  -- * @dir@ is a flag that indicates whether direction of move:
+  --   * 'True' means we should decrement buffer pointers after each copy.
+  --   * 'False' means we should increment the buffer pointers after each copy.
+  MemSet :: !(v (BVType 64))
+             -- /\ Number of values to assign
+          -> !(v (BVType n))
+             -- /\ Value to assign
+          -> !(v (BVType 64))
+             -- /\ Address to start assigning from.
+          -> !(v BoolType)
+            -- /\ Direction flag
+          -> X86Stmt v
+  EMMS :: X86Stmt v
+  -- ^ Empty MMX technology State. Sets the x87 FPU tag word to empty.
+  -- Probably OK to use this for both EMMS FEMMS, the second being a a
+  -- faster version from AMD 3D now.
 
 instance FunctorF X86Stmt where
   fmapF = fmapFDefault
@@ -853,7 +853,7 @@ instance TraversableF X86Stmt where
     case stmt of
       WriteLoc loc v    -> WriteLoc loc <$> go v
       StoreX87Control v -> StoreX87Control <$> go v
-      MemCopy bc v src dest dir -> MemCopy bc <$> go v <*> go src <*> go dest <*> go dir
+      RepMovs bc v src dest dir -> RepMovs bc <$> go v <*> go src <*> go dest <*> go dir
       MemSet  v src dest dir    -> MemSet <$> go v <*> go src <*> go dest <*> go dir
       EMMS -> pure EMMS
 
@@ -862,9 +862,9 @@ instance IsArchStmt X86Stmt where
     case stmt of
       WriteLoc loc rhs -> pretty loc <+> text ":=" <+> pp rhs
       StoreX87Control addr -> pp addr <+> text ":= x87_control"
-      MemCopy sz cnt src dest rev ->
-          text "memcopy" <+> parens (hcat $ punctuate comma args)
-        where args = [pretty sz, pp cnt, pp src, pp dest, pp rev]
+      RepMovs sz cnt src dest rev ->
+          text "repMovs" <+> parens (hcat $ punctuate comma args)
+        where args = [pretty (repValSizeByteCount sz), pp cnt, pp src, pp dest, pp rev]
       MemSet cnt val dest d ->
           text "memset" <+> parens (hcat $ punctuate comma args)
         where args = [pp cnt, pp val, pp dest, pp d]

x86/src/Data/Macaw/X86/Monad.hs

@@ -154,7 +154,6 @@ module Data.Macaw.X86.Monad
   , Data.Macaw.X86.Generator.eval
   , Data.Macaw.X86.Generator.evalArchFn
   , Data.Macaw.X86.Generator.addArchTermStmt
-  , memcopy
   , memset
   , even_parity
   , fnstcw
@@ -1606,67 +1605,6 @@ modify r f = do
   x <- get r
   r .= f x
 
--- | Move n bits at a time, with count moves
---
--- Semantic sketch. The effect on memory should be like @memcopy@
--- below, not like @memcopy2@. These sketches ignore the issue of
--- copying in chunks of size `bytes`, which should only be an
--- efficiency concern.
---
--- @
--- void memcopy(int bytes, int copies, char *src, char *dst, int reversed) {
---   int maybeFlip = reversed ? -1 : 1;
---   for (int c = 0; c < copies; ++c) {
---     for (int b = 0; b < bytes; ++b) {
---       int offset = maybeFlip * (b + c * bytes);
---       *(dst + offset) = *(src + offset);
---     }
---   }
--- }
--- @
---
--- Compare with:
---
--- @
--- void memcopy2(int bytes, int copies, char *src, char *dst, int reversed) {
---   int maybeFlip = reversed ? -1 : 1;
---   /* The only difference from `memcopy` above: here the same memory is
---      copied whether `reversed` is true or false -- only the order of
---      copies changes -- whereas above different memory is copied for
---      each direction. */
---   if (reversed) {
---     /* Start at the end and work backwards. */
---     src += copies * bytes - 1;
---     dst += copies * bytes - 1;
---   }
---   for (int c = 0; c < copies; ++c) {
---     for (int b = 0; b < bytes; ++b) {
---       int offset = maybeFlip * (b + c * bytes);
---       *(dst + offset) = *(src + offset);
---     }
---   }
--- }
--- @
-memcopy :: Integer
-           -- ^ Number of bytes to copy at a time (1,2,4,8)
-        -> BVExpr ids 64
-           -- ^ Number of values to move.
-        -> Addr ids
-           -- ^ Start of source buffer
-        -> Addr ids
-           -- ^ Start of destination buffer.
-        -> Expr ids BoolType
-           -- ^ Flag indicates direction of move:
-           -- True means we should decrement buffer pointers after each copy.
-           -- False means we should increment the buffer pointers after each copy.
-        -> X86Generator st ids ()
-memcopy val_sz count src dest is_reverse = do
-  count_v <- eval count
-  src_v   <- eval src
-  dest_v  <- eval dest
-  is_reverse_v <- eval is_reverse
-  addArchStmt $ MemCopy val_sz count_v src_v dest_v is_reverse_v
-
 -- | Set memory to the given value, for the number of words (nbytes
 -- = count * typeWidth v)
 memset :: (1 <= n)

x86/src/Data/Macaw/X86/Semantics.hs

@@ -18,6 +18,7 @@ module Data.Macaw.X86.Semantics
   ( execInstruction
   ) where
 
+import           Control.Lens ((^.))
 import           Control.Monad (when)
 import qualified Data.Bits as Bits
 import           Data.Foldable
@@ -27,6 +28,7 @@ import           Data.Parameterized.Classes
 import qualified Data.Parameterized.List as P
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Some
+import           Data.Parameterized.TraversableF
 import           Data.Proxy
 import           Data.Word
 import qualified Flexdis86 as F
@@ -1159,54 +1161,51 @@ def_ret = defVariadic "ret"    $ \_ vs ->
 
 -- FIXME: probably doesn't work for 32 bit address sizes
 -- arguments are only for the size, they are fixed at rsi/rdi
-exec_movs :: 1 <= w
-          => Bool -- Flag indicating if RepPrefix appeared before instruction
-          -> NatRepr w -- Number of bytes to move at a time.
-          -> X86Generator st ids ()
-exec_movs False w = do
-  let bytesPerOp = bvLit n64 (natValue w)
-  let repr = BVMemRepr w LittleEndian
-  -- The direction flag indicates post decrement or post increment.
-  df <- get df_loc
-  src  <- get rsi
-  dest <- get rdi
-  v' <- get $ MemoryAddr src repr
-  MemoryAddr dest repr .= v'
-
-  rsi .= mux df (src  .- bytesPerOp) (src  .+ bytesPerOp)
-  rdi .= mux df (dest .- bytesPerOp) (dest .+ bytesPerOp)
-exec_movs True w = do
-    -- FIXME: aso modifies this
-  let count_reg = rcx
-      bytesPerOp = natValue w
-      bytesPerOpv = bvLit n64 bytesPerOp
-  -- The direction flag indicates post decrement or post increment.
-  df <- get df_loc
-  src   <- get rsi
-  dest  <- get rdi
-  count <- get count_reg
-  let total_bytes = count .* bytesPerOpv
-  -- FIXME: we might need direction for overlapping regions
-  count_reg .= bvLit n64 (0::Integer)
-  memcopy bytesPerOp count src dest df
-  rsi .= mux df (src   .- total_bytes) (src   .+ total_bytes)
-  rdi .= mux df (dest  .- total_bytes) (dest  .+ total_bytes)
 
 def_movs :: InstructionDef
 def_movs = defBinary "movs" $ \ii loc _ -> do
-  case loc of
-    F.Mem8 F.Addr_64{} ->
-      exec_movs (F.iiLockPrefix ii == F.RepPrefix) (knownNat :: NatRepr 1)
-    F.Mem16 F.Addr_64{} ->
-      exec_movs (F.iiLockPrefix ii == F.RepPrefix) (knownNat :: NatRepr 2)
-    F.Mem32 F.Addr_64{} ->
-      exec_movs (F.iiLockPrefix ii == F.RepPrefix) (knownNat :: NatRepr 4)
-    F.Mem64 F.Addr_64{} ->
-      exec_movs (F.iiLockPrefix ii == F.RepPrefix) (knownNat :: NatRepr 8)
-    _ -> fail "Bad argument to movs"
+  let pfx = F.iiPrefixes ii
+  Some w <-
+        case loc of
+          F.Mem8{}  -> pure (Some ByteRepVal)
+          F.Mem16{} -> pure (Some WordRepVal)
+          F.Mem32{} -> pure (Some DWordRepVal)
+          F.Mem64{} -> pure (Some QWordRepVal)
+          _ -> error "Bad argument to movs"
+  let bytesPerOp = bvLit n64 (repValSizeByteCount w)
+  df   <- get df_loc
+  src  <- get rsi
+  dest <- get rdi
+  case pfx^.F.prLockPrefix of
+    F.RepPrefix -> do
+      when (pfx^.F.prASO) $ do
+        fail "Rep prefix semantics not defined when address size override is true."
+      -- The direction flag indicates post decrement or post increment.
+      count <- get rcx
+      addArchStmt =<< traverseF eval (RepMovs w count src dest df)
+
+      -- We adjust rsi and rdi by a negative value if df is true.
+      -- The formula is organized so that the bytesPerOp literal is
+      -- passed to the multiply and we can avoid non-linear arithmetic.
+      let adj = bytesPerOp .* mux df (bvNeg count) count
+      rcx .= bvLit n64 (0::Integer)
+      rsi .= src  .+ adj
+      rdi .= dest .+ adj
+    F.NoLockPrefix -> do
+      let repr = repValSizeMemRepr w
+      -- The direction flag indicates post decrement or post increment.
+      v' <- get $ MemoryAddr src repr
+      MemoryAddr dest repr .= v'
+      -- We adjust rsi and rdi by a negative value if df is true.
+      -- The formula is organized so that the bytesPerOp literal is
+      -- passed to the multiply and we can avoid non-linear arithmetic.
+      let adj = mux df (bvNeg bytesPerOp) bytesPerOp
+      rsi .= src  .+ adj
+      rdi .= dest .+ adj
+    _ -> do
+      fail "movs given unsupported lock prefix"
+
 
--- FIXME: can also take rep prefix
--- FIXME: we ignore the aso here.
 -- | CMPS/CMPSB Compare string/Compare byte string
 -- CMPS/CMPSW Compare string/Compare word string
 -- CMPS/CMPSD Compare string/Compare doubleword string