{-# 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 (AVXOp1 -> AVXOp1 -> Bool
(AVXOp1 -> AVXOp1 -> Bool)
-> (AVXOp1 -> AVXOp1 -> Bool) -> Eq AVXOp1
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AVXOp1 -> AVXOp1 -> Bool
== :: AVXOp1 -> AVXOp1 -> Bool
$c/= :: AVXOp1 -> AVXOp1 -> Bool
/= :: AVXOp1 -> AVXOp1 -> Bool
Eq,Eq AVXOp1
Eq AVXOp1 =>
(AVXOp1 -> AVXOp1 -> Ordering)
-> (AVXOp1 -> AVXOp1 -> Bool)
-> (AVXOp1 -> AVXOp1 -> Bool)
-> (AVXOp1 -> AVXOp1 -> Bool)
-> (AVXOp1 -> AVXOp1 -> Bool)
-> (AVXOp1 -> AVXOp1 -> AVXOp1)
-> (AVXOp1 -> AVXOp1 -> AVXOp1)
-> Ord AVXOp1
AVXOp1 -> AVXOp1 -> Bool
AVXOp1 -> AVXOp1 -> Ordering
AVXOp1 -> AVXOp1 -> AVXOp1
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AVXOp1 -> AVXOp1 -> Ordering
compare :: AVXOp1 -> AVXOp1 -> Ordering
$c< :: AVXOp1 -> AVXOp1 -> Bool
< :: AVXOp1 -> AVXOp1 -> Bool
$c<= :: AVXOp1 -> AVXOp1 -> Bool
<= :: AVXOp1 -> AVXOp1 -> Bool
$c> :: AVXOp1 -> AVXOp1 -> Bool
> :: AVXOp1 -> AVXOp1 -> Bool
$c>= :: AVXOp1 -> AVXOp1 -> Bool
>= :: AVXOp1 -> AVXOp1 -> Bool
$cmax :: AVXOp1 -> AVXOp1 -> AVXOp1
max :: AVXOp1 -> AVXOp1 -> AVXOp1
$cmin :: AVXOp1 -> AVXOp1 -> AVXOp1
min :: AVXOp1 -> AVXOp1 -> AVXOp1
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 :: forall sym (f :: CrucibleType -> Type) (tp :: CrucibleType).
IsSymExprBuilder sym =>
sym
-> (forall (subT :: CrucibleType).
    f subT -> IO (RegValue sym subT))
-> ExtX86 f tp
-> IO (RegValue sym tp)
eval sym
sym forall (subT :: CrucibleType). f subT -> IO (RegValue sym subT)
ev ExtX86 f tp
ext =
  case ExtX86 f tp
ext of
    VOp1 NatRepr n
w AVXOp1
op f ('BaseToType (BaseBVType n))
e ->
      case AVXOp1
op of
        VShiftL Word8
amt -> sym
-> NatRepr n
-> Word8
-> SymExpr sym (BaseBVType n)
-> IO (SymExpr sym (BaseBVType n))
forall sym (w :: Natural).
(IsSymExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
vShiftL sym
sym NatRepr n
w Word8
amt (SymExpr sym (BaseBVType n) -> IO (SymExpr sym (BaseBVType n)))
-> IO (SymExpr sym (BaseBVType n))
-> IO (SymExpr sym (BaseBVType n))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType (BaseBVType n))
-> IO (RegValue sym ('BaseToType (BaseBVType n)))
forall (subT :: CrucibleType). f subT -> IO (RegValue sym subT)
ev f ('BaseToType (BaseBVType n))
e
        VShufD Word8
ixes -> sym
-> NatRepr n
-> Word8
-> SymExpr sym (BaseBVType n)
-> IO (SymExpr sym (BaseBVType n))
forall sym (w :: Natural).
IsSymExprBuilder sym =>
sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
vShufD sym
sym NatRepr n
w Word8
ixes (SymExpr sym (BaseBVType n) -> IO (SymExpr sym (BaseBVType n)))
-> IO (SymExpr sym (BaseBVType n))
-> IO (SymExpr sym (BaseBVType n))
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< f ('BaseToType (BaseBVType n))
-> IO (RegValue sym ('BaseToType (BaseBVType n)))
forall (subT :: CrucibleType). f subT -> IO (RegValue sym subT)
ev f ('BaseToType (BaseBVType n))
e


-- | See @vpslldq@
vShiftL :: (I.IsSymExprBuilder sym, 1 <= w) =>
           sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
vShiftL :: forall sym (w :: Natural).
(IsSymExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
vShiftL sym
sym NatRepr w
w Word8
amt SymBV sym w
v =
  do SymBV sym w
i <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
I.bvLit sym
sym NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (Integer
8 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Word8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
amt))
     sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
I.bvShl sym
sym SymBV sym w
v SymBV sym w
i


-- | See @vpshufd@
vShufD :: forall sym w.
          I.IsSymExprBuilder sym =>
          sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
vShufD :: forall sym (w :: Natural).
IsSymExprBuilder sym =>
sym -> NatRepr w -> Word8 -> SymBV sym w -> IO (SymBV sym w)
vShufD sym
sym NatRepr w
w Word8
ixes SymBV sym w
v
  | Just w :~: 128
I.Refl <- NatRepr w -> NatRepr 128 -> Maybe (w :~: 128)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w NatRepr 128
n128 = SymBV sym 128 -> IO (SymBV sym 128)
mk128 SymBV sym w
SymBV sym 128
v
  | Just w :~: 256
I.Refl <- NatRepr w -> NatRepr 256 -> Maybe (w :~: 256)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr w
w NatRepr 256
n256 =
    do SymBV sym 128
lower128 <- SymBV sym 128 -> IO (SymBV sym 128)
mk128 (SymBV sym 128 -> IO (SymBV sym 128))
-> IO (SymBV sym 128) -> IO (SymBV sym 128)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr 0 -> NatRepr 128 -> SymBV sym 256 -> IO (SymBV sym 128)
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
I.bvSelect sym
sym NatRepr 0
n0   NatRepr 128
n128 SymBV sym w
SymBV sym 256
v
       SymBV sym 128
upper128 <- SymBV sym 128 -> IO (SymBV sym 128)
mk128 (SymBV sym 128 -> IO (SymBV sym 128))
-> IO (SymBV sym 128) -> IO (SymBV sym 128)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym
-> NatRepr 128
-> NatRepr 128
-> SymBV sym 256
-> IO (SymBV sym 128)
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
I.bvSelect sym
sym NatRepr 128
n128 NatRepr 128
n128 SymBV sym w
SymBV sym 256
v
       sym -> SymBV sym 128 -> SymBV sym 128 -> IO (SymBV sym (128 + 128))
forall (u :: Natural) (v :: Natural).
(1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
I.bvConcat sym
sym SymBV sym 128
upper128 SymBV sym 128
lower128
  | Bool
otherwise = String -> [String] -> IO (SymBV sym w)
forall a. HasCallStack => String -> [String] -> a
panic String
"Arch.X86.vShufD"
                        [ String
"*** Unexpected width: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (NatRepr w -> Natural
forall (n :: Natural). NatRepr n -> Natural
I.natValue NatRepr w
w) ]

  where
  mk128 :: SymBV sym 128 -> IO (SymBV sym 128)
  mk128 :: SymBV sym 128 -> IO (SymBV sym 128)
mk128 SymBV sym 128
src = do SymExpr sym (BaseBVType 32)
f0 <- SymBV sym 128 -> Int -> IO (SymExpr sym (BaseBVType 32))
getV SymBV sym 128
src Int
0
                 SymExpr sym (BaseBVType 32)
f1 <- SymBV sym 128 -> Int -> IO (SymExpr sym (BaseBVType 32))
getV SymBV sym 128
src Int
1
                 SymExpr sym (BaseBVType 32)
f2 <- SymBV sym 128 -> Int -> IO (SymExpr sym (BaseBVType 32))
getV SymBV sym 128
src Int
2
                 SymExpr sym (BaseBVType 32)
f3 <- SymBV sym 128 -> Int -> IO (SymExpr sym (BaseBVType 32))
getV SymBV sym 128
src Int
3
                 SymExpr sym (BaseBVType (32 + 32))
lower64 <- sym
-> SymExpr sym (BaseBVType 32)
-> SymExpr sym (BaseBVType 32)
-> IO (SymExpr sym (BaseBVType (32 + 32)))
forall (u :: Natural) (v :: Natural).
(1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
I.bvConcat sym
sym SymExpr sym (BaseBVType 32)
f1 SymExpr sym (BaseBVType 32)
f0
                 SymExpr sym (BaseBVType (32 + 32))
upper64 <- sym
-> SymExpr sym (BaseBVType 32)
-> SymExpr sym (BaseBVType 32)
-> IO (SymExpr sym (BaseBVType (32 + 32)))
forall (u :: Natural) (v :: Natural).
(1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
I.bvConcat sym
sym SymExpr sym (BaseBVType 32)
f3 SymExpr sym (BaseBVType 32)
f2
                 sym -> SymBV sym 64 -> SymBV sym 64 -> IO (SymBV sym (64 + 64))
forall (u :: Natural) (v :: Natural).
(1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
I.bvConcat sym
sym SymBV sym 64
SymExpr sym (BaseBVType (32 + 32))
upper64 SymBV sym 64
SymExpr sym (BaseBVType (32 + 32))
lower64

  getV :: SymBV sym 128 -> Int -> IO (SymBV sym 32)
  getV :: SymBV sym 128 -> Int -> IO (SymExpr sym (BaseBVType 32))
getV SymBV sym 128
src Int
n = case Int -> Word8
getIx Int
n of
                 Word8
0 -> sym
-> NatRepr 0
-> NatRepr 32
-> SymBV sym 128
-> IO (SymExpr sym (BaseBVType 32))
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
I.bvSelect sym
sym NatRepr 0
n0 NatRepr 32
n32 SymBV sym 128
src
                 Word8
1 -> sym
-> NatRepr 1
-> NatRepr 32
-> SymBV sym 128
-> IO (SymExpr sym (BaseBVType 32))
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
I.bvSelect sym
sym NatRepr 1
n1 NatRepr 32
n32 SymBV sym 128
src
                 Word8
2 -> sym
-> NatRepr 2
-> NatRepr 32
-> SymBV sym 128
-> IO (SymExpr sym (BaseBVType 32))
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
I.bvSelect sym
sym NatRepr 2
n2 NatRepr 32
n32 SymBV sym 128
src
                 Word8
_ -> sym
-> NatRepr 3
-> NatRepr 32
-> SymBV sym 128
-> IO (SymExpr sym (BaseBVType 32))
forall (idx :: Natural) (n :: Natural) (w :: Natural).
(1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
I.bvSelect sym
sym NatRepr 3
n3 NatRepr 32
n32 SymBV sym 128
src

  getIx :: Int -> Word8
  getIx :: Int -> Word8
getIx Int
n = (Word8
ixes Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
`shiftR` (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n)) Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.&. Word8
0x03 -- get 2 bit field




--------------------------------------------------------------------------------
n0 :: NatRepr 0
n0 :: NatRepr 0
n0 = NatRepr 0
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

n1 :: NatRepr 1
n1 :: NatRepr 1
n1 = NatRepr 1
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

n2 :: NatRepr 2
n2 :: NatRepr 2
n2 = NatRepr 2
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

n3 :: NatRepr 3
n3 :: NatRepr 3
n3 = NatRepr 3
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

n32 :: NatRepr 32
n32 :: NatRepr 32
n32 = NatRepr 32
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

n128 :: NatRepr 128
n128 :: NatRepr 128
n128 = NatRepr 128
forall (n :: Natural). KnownNat n => NatRepr n
knownNat

n256 :: NatRepr 256
n256 :: NatRepr 256
n256 = NatRepr 256
forall (n :: Natural). KnownNat n => NatRepr n
knownNat


--------------------------------------------------------------------------------

$([d| {- New TH Scope -} |])


-- This is going to go away
instance ShowFC ExtX86 where
  showFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> String)
-> forall (x :: CrucibleType). ExtX86 f x -> String
showFC forall (x :: CrucibleType). f x -> String
_ ExtX86 f x
_ = String -> String
forall a. HasCallStack => String -> a
error String
"[ShowFC ExtX86] Not implmented."

instance TestEqualityFC ExtX86 where
  testEqualityFC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> forall (x :: CrucibleType) (y :: CrucibleType).
   ExtX86 f x -> ExtX86 f y -> Maybe (x :~: y)
testEqualityFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
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 :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> OrderingF x y)
-> forall (x :: CrucibleType) (y :: CrucibleType).
   ExtX86 f x -> ExtX86 f y -> OrderingF x y
compareFC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> OrderingF x y
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 :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType). Int -> f x -> Int)
-> forall (x :: CrucibleType). Int -> ExtX86 f x -> Int
hashWithSaltFC forall (x :: CrucibleType). Int -> f x -> Int
_hash Int
_s ExtX86 f x
_x = String -> Int
forall a. HasCallStack => String -> a
error String
"[HashableFC ExtX86] Not implmented."

instance FunctorFC ExtX86 where
  fmapFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). ExtX86 f x -> ExtX86 g x
fmapFC = (forall (x :: CrucibleType). f x -> g x)
-> ExtX86 f x -> ExtX86 g x
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). ExtX86 f x -> ExtX86 g x
forall {k} {l} (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
TraversableFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> forall (x :: CrucibleType). ExtX86 f x -> ExtX86 g x
fmapFCDefault

instance FoldableFC ExtX86 where
  foldMapFC :: forall (f :: CrucibleType -> Type) m.
Monoid m =>
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). ExtX86 f x -> m
foldMapFC = (forall (x :: CrucibleType). f x -> m) -> ExtX86 f x -> m
(forall (x :: CrucibleType). f x -> m)
-> forall (x :: CrucibleType). ExtX86 f x -> m
forall {k} {l} (t :: (k -> Type) -> l -> Type) m (f :: k -> Type).
(TraversableFC t, Monoid m) =>
(forall (x :: k). f x -> m) -> forall (x :: l). t f x -> m
foldMapFCDefault

instance TraversableFC ExtX86 where
  traverseFC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: CrucibleType). ExtX86 f x -> m (ExtX86 g x)
traverseFC = $(U.structuralTraversal [t|ExtX86|] [])

instance PrettyApp ExtX86 where
  ppApp :: forall (f :: CrucibleType -> Type) ann.
(forall (x :: CrucibleType). f x -> Doc ann)
-> forall (x :: CrucibleType). ExtX86 f x -> Doc ann
ppApp forall (x :: CrucibleType). f x -> Doc ann
_pp ExtX86 f x
_x = String -> Doc ann
forall a. HasCallStack => String -> a
error String
"[PrettyApp ExtX86] XXX"

instance TypeApp ExtX86 where
  appType :: forall (f :: CrucibleType -> Type) (x :: CrucibleType).
ExtX86 f x -> TypeRepr x
appType ExtX86 f x
x =
    case ExtX86 f x
x of
      VOp1 NatRepr n
w AVXOp1
_ f ('BaseToType (BaseBVType n))
_ -> NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
forall (n :: Natural).
(1 <= n) =>
NatRepr n -> TypeRepr ('BaseToType (BaseBVType n))
BVRepr NatRepr n
w