content: {-# Language GADTs #-}
  {-# Language DataKinds #-}
  {-# Language KindSignatures #-}
  {-# Language TypeOperators #-}
  {-# Language ExplicitNamespaces #-}
  {-# Language TemplateHaskell #-}
  {-# Language RankNTypes #-}
  {-# Language ScopedTypeVariables #-}
  {-# Language PatternGuards #-}
  {-# Language MultiWayIf #-}
  module Lang.Crucible.LLVM.Arch.X86 where
  
  import qualified Data.BitVector.Sized as BV
  import Data.Word(Word8)
  import Data.Bits
  import Data.Kind
  import GHC.TypeNats (type (<=))
  
  import Data.Parameterized.NatRepr(knownNat)
  import Data.Parameterized.Classes(testEquality,compareF)
  import Data.Parameterized.TraversableFC
  import Data.Parameterized.TH.GADT as U
  
  import           What4.Interface (SymBV)
  import qualified What4.Interface as I
  
  import Lang.Crucible.CFG.Extension
  import Lang.Crucible.Types(CrucibleType,BVType,NatRepr,TypeRepr(..))
  import Lang.Crucible.Simulator.RegValue(RegValue)
  import Lang.Crucible.Panic(panic)
  
  import Lang.Crucible.LLVM.Arch.Util((|->))
  
  data AVXOp1 = VShiftL Word8     -- ^ Shift left by this many bytes
                                  -- New bytes are 0.
              | VShufD Word8      -- ^ Shuffle 32-bit words of vector
                                  -- according to pattern in the word8
                deriving (Eq,Ord)
  
  
  data ExtX86 :: (CrucibleType -> Type) -> CrucibleType -> Type where
  
    {- | Unary operation on a vector.  Should have no side effects. -}
    VOp1 :: (1 <= n) =>
       !(NatRepr n)        -> {- width of input/result -}
       !AVXOp1             -> {- do this operation -}
       !(f (BVType n))     -> {- on this thing -}
       ExtX86 f (BVType n)
  
  
  
  eval :: forall sym f tp.
          I.IsSymExprBuilder sym =>
          sym ->
          (forall subT. f subT -> IO (RegValue sym subT)) ->
          ExtX86 f tp ->
          IO (RegValue sym tp)
  eval sym ev ext =
    case ext of
      VOp1 w op e ->
        case op of
          VShiftL amt -> vShiftL sym w amt =<< ev e
          VShufD ixes -> vShufD sym w ixes =<< ev e
  
  
  -- | See @vpslldq@
  vShiftL :: (I.IsSymExprBuilder sym, 1 <= w) =>
             sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
  vShiftL sym w amt v =
    do i <- I.bvLit sym w (BV.mkBV w (8 * fromIntegral amt))
       I.bvShl sym v i
  
  
  -- | See @vpshufd@
  vShufD :: forall sym w.
            I.IsSymExprBuilder sym =>
            sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
  vShufD sym w ixes v
    | Just I.Refl <- testEquality w n128 = mk128 v
    | Just I.Refl <- testEquality w n256 =
      do lower128 <- mk128 =<< I.bvSelect sym n0   n128 v
         upper128 <- mk128 =<< I.bvSelect sym n128 n128 v
         I.bvConcat sym upper128 lower128
    | otherwise = panic "Arch.X86.vShufD"
                          [ "*** Unexpected width: " ++ show (I.natValue w) ]
  
    where
    mk128 :: SymBV sym 128 -> IO (SymBV sym 128)
    mk128 src = do f0 <- getV src 0
                   f1 <- getV src 1
                   f2 <- getV src 2
                   f3 <- getV src 3
                   lower64 <- I.bvConcat sym f1 f0
                   upper64 <- I.bvConcat sym f3 f2
                   I.bvConcat sym upper64 lower64
  
    getV :: SymBV sym 128 -> Int -> IO (SymBV sym 32)
    getV src n = case getIx n of
                   0 -> I.bvSelect sym n0 n32 src
                   1 -> I.bvSelect sym n1 n32 src
                   2 -> I.bvSelect sym n2 n32 src
                   _ -> I.bvSelect sym n3 n32 src
  
    getIx :: Int -> Word8
    getIx n = (ixes `shiftR` (2 * n)) .&. 0x03 -- get 2 bit field
  
  
  
  
  --------------------------------------------------------------------------------
  n0 :: NatRepr 0
  n0 = knownNat
  
  n1 :: NatRepr 1
  n1 = knownNat
  
  n2 :: NatRepr 2
  n2 = knownNat
  
  n3 :: NatRepr 3
  n3 = knownNat
  
  n32 :: NatRepr 32
  n32 = knownNat
  
  n128 :: NatRepr 128
  n128 = knownNat
  
  n256 :: NatRepr 256
  n256 = knownNat
  
  
  --------------------------------------------------------------------------------
  
  $([d| {- New TH Scope -} |])
  
  
  -- This is going to go away
  instance ShowFC ExtX86 where
    showFC _ _ = error "[ShowFC ExtX86] Not implmented."
  
  instance TestEqualityFC ExtX86 where
    testEqualityFC testSubterm =
      $(U.structuralTypeEquality [t| ExtX86 |]
          [ U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType |-> [|testEquality|]
          , U.DataArg 0             `U.TypeApp` U.AnyType |-> [|testSubterm|]
          ])
  
  instance OrdFC ExtX86 where
    compareFC testSubterm =
      $(U.structuralTypeOrd [t| ExtX86 |]
          [ U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType |-> [|compareF|]
          , U.DataArg 0             `U.TypeApp` U.AnyType |-> [|testSubterm|]
          ])
  
  -- This is going away
  instance HashableFC ExtX86 where
    hashWithSaltFC _hash _s _x = error "[HashableFC ExtX86] Not implmented."
  
  instance FunctorFC ExtX86 where
    fmapFC = fmapFCDefault
  
  instance FoldableFC ExtX86 where
    foldMapFC = foldMapFCDefault
  
  instance TraversableFC ExtX86 where
    traverseFC = $(U.structuralTraversal [t|ExtX86|] [])
  
  instance PrettyApp ExtX86 where
    ppApp _pp _x = error "[PrettyApp ExtX86] XXX"
  
  instance TypeApp ExtX86 where
    appType x =
      case x of
        VOp1 w _ _ -> BVRepr w
  
  