mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
Merge branch 'master' of github.com:GaloisInc/macaw
This commit is contained in:
Tristan Ravitch
commit
c527a91521
15
.travis.yml
15
.travis.yml
@ -33,21 +33,10 @@ install:
|
||||
fi
|
||||
- travis_retry cabal update -v
|
||||
- sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config
|
||||
# - cabal install --only-dependencies --enable-tests --enable-benchmarks --dry -v > installplan.txt
|
||||
# - stack install macaw-x86 --only-dependencies --test --dry-run -v 2> installplan.txt
|
||||
# - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
|
||||
|
||||
# Here starts the actual work to be performed for the package under test;
|
||||
# any command which exits with a non-zero exit code causes the build to fail.
|
||||
script:
|
||||
- travis_wait stack --no-terminal --skip-ghc-check setup
|
||||
- stack --stack-yaml stack.ghc-8.2.2.yaml build macaw-x86 macaw-x86-symbolic
|
||||
- stack --stack-yaml stack.ghc-8.2.2.yaml test macaw-x86
|
||||
|
||||
# Check that the resulting source distribution can be built & installed.
|
||||
# If there are no other `.tar.gz` files in `dist`, this can be even simpler:
|
||||
# `cabal install --force-reinstalls dist/*-*.tar.gz`
|
||||
# - SRC_TGZ=$(cabal info . | awk '{print $2;exit}').tar.gz &&
|
||||
# (cd dist && cabal install --force-reinstalls "$SRC_TGZ")
|
||||
|
||||
# EOF
|
||||
- stack --stack-yaml stack.ghc-8.6.3.yaml build macaw-x86 macaw-x86-symbolic
|
||||
- stack --stack-yaml stack.ghc-8.6.3.yaml test macaw-x86
|
||||
|
||||
@ -74,6 +74,10 @@ data App (f :: Type -> Kind.Type) (tp :: Type) where
|
||||
-- all @false@.
|
||||
UExt :: (1 <= m, m+1 <= n, 1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
|
||||
|
||||
-- | This casts an expression from one type to another that should
|
||||
-- use the same number of bytes in memory.
|
||||
Bitcast :: f tp -> TypeRepr out -> App f out
|
||||
|
||||
----------------------------------------------------------------------
|
||||
-- Bitvector operations
|
||||
|
||||
@ -257,15 +261,17 @@ ppAppA :: Applicative m
|
||||
-> m Doc
|
||||
ppAppA pp a0 =
|
||||
case a0 of
|
||||
Eq x y -> sexprA "eq" [ pp x, pp y ]
|
||||
Mux _ c x y -> sexprA "mux" [ pp c, pp x, pp y ]
|
||||
Trunc x w -> sexprA "trunc" [ pp x, ppNat w ]
|
||||
TupleField _ x i -> sexprA "tuple_field" [ pp x, prettyPure (P.indexValue i) ]
|
||||
SExt x w -> sexprA "sext" [ pp x, ppNat w ]
|
||||
UExt x w -> sexprA "uext" [ pp x, ppNat w ]
|
||||
AndApp x y -> sexprA "and" [ pp x, pp y ]
|
||||
OrApp x y -> sexprA "or" [ pp x, pp y ]
|
||||
NotApp x -> sexprA "not" [ pp x ]
|
||||
XorApp x y -> sexprA "xor" [ pp x, pp y ]
|
||||
Trunc x w -> sexprA "trunc" [ pp x, ppNat w ]
|
||||
SExt x w -> sexprA "sext" [ pp x, ppNat w ]
|
||||
UExt x w -> sexprA "uext" [ pp x, ppNat w ]
|
||||
Bitcast x tp -> sexprA "bitcast" [ pp x, pure (text (show tp)) ]
|
||||
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
|
||||
BVAdc _ x y c -> sexprA "bv_adc" [ pp x, pp y, pp c ]
|
||||
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
|
||||
@ -283,7 +289,6 @@ ppAppA pp a0 =
|
||||
BVShl _ x y -> sexprA "bv_shl" [ pp x, pp y ]
|
||||
BVShr _ x y -> sexprA "bv_shr" [ pp x, pp y ]
|
||||
BVSar _ x y -> sexprA "bv_sar" [ pp x, pp y ]
|
||||
Eq x y -> sexprA "eq" [ pp x, pp y ]
|
||||
PopCount _ x -> sexprA "popcount" [ pp x ]
|
||||
ReverseBytes _ x -> sexprA "reverse_bytes" [ pp x ]
|
||||
UadcOverflows x y c -> sexprA "uadc_overflows" [ pp x, pp y, pp c ]
|
||||
@ -311,6 +316,7 @@ instance HasRepr (App f) TypeRepr where
|
||||
Trunc _ w -> BVTypeRepr w
|
||||
SExt _ w -> BVTypeRepr w
|
||||
UExt _ w -> BVTypeRepr w
|
||||
Bitcast _ tp -> tp
|
||||
|
||||
AndApp{} -> knownRepr
|
||||
OrApp{} -> knownRepr
|
||||
|
||||
@ -70,70 +70,8 @@ n128 = knownNat
|
||||
n256 :: NatRepr 256
|
||||
n256 = knownNat
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Type
|
||||
|
||||
data Type
|
||||
= -- | A bitvector with the given number of bits.
|
||||
BVType Nat
|
||||
-- | A floating point in the given format.
|
||||
| FloatType FloatInfo
|
||||
-- | A Boolean value
|
||||
| BoolType
|
||||
-- | A tuple of types
|
||||
| TupleType [Type]
|
||||
|
||||
|
||||
-- Return number of bytes in the type.
|
||||
type family TypeBytes (tp :: Type) :: Nat where
|
||||
TypeBytes (BVType 8) = 1
|
||||
TypeBytes (BVType 16) = 2
|
||||
TypeBytes (BVType 32) = 4
|
||||
TypeBytes (BVType 64) = 8
|
||||
TypeBytes (FloatType fi) = FloatInfoBytes fi
|
||||
|
||||
-- Return number of bits in the type.
|
||||
type family TypeBits (tp :: Type) :: Nat where
|
||||
TypeBits (BVType n) = n
|
||||
TypeBits (FloatType fi) = 8 * FloatInfoBytes fi
|
||||
|
||||
type BVType = 'BVType
|
||||
|
||||
type FloatType = 'FloatType
|
||||
|
||||
type BoolType = 'BoolType
|
||||
|
||||
type TupleType = 'TupleType
|
||||
|
||||
-- | A runtime representation of @Type@ for case matching purposes.
|
||||
data TypeRepr (tp :: Type) where
|
||||
BoolTypeRepr :: TypeRepr BoolType
|
||||
BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
|
||||
FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
|
||||
TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
|
||||
|
||||
type_width :: TypeRepr (BVType n) -> NatRepr n
|
||||
type_width (BVTypeRepr n) = n
|
||||
|
||||
instance Show (TypeRepr tp) where
|
||||
show BoolTypeRepr = "bool"
|
||||
show (BVTypeRepr w) = "[" ++ show w ++ "]"
|
||||
show (FloatTypeRepr fi) = show fi ++ "_float"
|
||||
show (TupleTypeRepr P.Nil) = "()"
|
||||
show (TupleTypeRepr (h P.:< z)) =
|
||||
"(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
|
||||
|
||||
instance KnownRepr TypeRepr BoolType where
|
||||
knownRepr = BoolTypeRepr
|
||||
|
||||
instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
|
||||
knownRepr = BVTypeRepr knownNat
|
||||
|
||||
instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
|
||||
knownRepr = FloatTypeRepr knownRepr
|
||||
|
||||
instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr (TupleType l) where
|
||||
knownRepr = TupleTypeRepr knownRepr
|
||||
n512 :: NatRepr 512
|
||||
n512 = knownNat
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Floating point sizes
|
||||
@ -217,18 +155,92 @@ floatInfoBitsIsPos = \case
|
||||
QuadFloatRepr -> LeqProof
|
||||
X86_80FloatRepr -> LeqProof
|
||||
|
||||
$(return [])
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Type
|
||||
|
||||
data Type
|
||||
= -- | A bitvector with the given number of bits.
|
||||
BVType Nat
|
||||
-- | A floating point in the given format.
|
||||
| FloatType FloatInfo
|
||||
-- | A Boolean value
|
||||
| BoolType
|
||||
-- | A tuple of types
|
||||
| TupleType [Type]
|
||||
-- | A vector of types
|
||||
| VecType Nat Type
|
||||
|
||||
|
||||
-- Return number of bytes in the type.
|
||||
type family TypeBytes (tp :: Type) :: Nat where
|
||||
TypeBytes (BVType 8) = 1
|
||||
TypeBytes (BVType 16) = 2
|
||||
TypeBytes (BVType 32) = 4
|
||||
TypeBytes (BVType 64) = 8
|
||||
TypeBytes (FloatType fi) = FloatInfoBytes fi
|
||||
TypeBytes (VecType n tp) = n * TypeBytes tp
|
||||
|
||||
-- Return number of bits in the type.
|
||||
type family TypeBits (tp :: Type) :: Nat where
|
||||
TypeBits (BVType n) = n
|
||||
TypeBits (FloatType fi) = 8 * FloatInfoBytes fi
|
||||
|
||||
type BVType = 'BVType
|
||||
|
||||
type FloatType = 'FloatType
|
||||
|
||||
type BoolType = 'BoolType
|
||||
|
||||
type TupleType = 'TupleType
|
||||
|
||||
-- | The bitvector associated with the given floating-point format.
|
||||
type FloatBVType (fi :: FloatInfo) = BVType (FloatInfoBits fi)
|
||||
|
||||
floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
|
||||
floatBVTypeRepr fi | LeqProof <- floatInfoBitsIsPos fi =
|
||||
BVTypeRepr $ floatInfoBits fi
|
||||
$(pure [])
|
||||
|
||||
$(return [])
|
||||
|
||||
-- | A runtime representation of @Type@ for case matching purposes.
|
||||
data TypeRepr (tp :: Type) where
|
||||
BoolTypeRepr :: TypeRepr BoolType
|
||||
BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
|
||||
FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
|
||||
TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
|
||||
VectorTypeRepr :: NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)
|
||||
|
||||
type_width :: TypeRepr (BVType n) -> NatRepr n
|
||||
type_width (BVTypeRepr n) = n
|
||||
|
||||
instance Show (TypeRepr tp) where
|
||||
show BoolTypeRepr = "bool"
|
||||
show (BVTypeRepr w) = "[" ++ show w ++ "]"
|
||||
show (FloatTypeRepr fi) = show fi ++ "_float"
|
||||
show (TupleTypeRepr P.Nil) = "()"
|
||||
show (TupleTypeRepr (h P.:< z)) =
|
||||
"(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
|
||||
show (VectorTypeRepr c tp) = "(vec " ++ show c ++ " " ++ show tp ++ ")"
|
||||
|
||||
instance ShowF TypeRepr
|
||||
|
||||
instance KnownRepr TypeRepr BoolType where
|
||||
knownRepr = BoolTypeRepr
|
||||
|
||||
instance (KnownNat n, 1 <= n) => KnownRepr TypeRepr (BVType n) where
|
||||
knownRepr = BVTypeRepr knownNat
|
||||
|
||||
instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
|
||||
knownRepr = FloatTypeRepr knownRepr
|
||||
|
||||
instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr (TupleType l) where
|
||||
knownRepr = TupleTypeRepr knownRepr
|
||||
|
||||
$(pure [])
|
||||
|
||||
instance TestEquality TypeRepr where
|
||||
testEquality = $(structuralTypeEquality [t|TypeRepr|]
|
||||
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
|
||||
, (ConType [t|TypeRepr|] `TypeApp` AnyType, [|testEquality|])
|
||||
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
|
||||
, ( ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType
|
||||
, [|testEquality|]
|
||||
@ -238,6 +250,7 @@ instance TestEquality TypeRepr where
|
||||
instance OrdF TypeRepr where
|
||||
compareF = $(structuralTypeOrd [t|TypeRepr|]
|
||||
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
|
||||
, (ConType [t|TypeRepr|] `TypeApp` AnyType, [|compareF|])
|
||||
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
|
||||
, (ConType [t|P.List|] `TypeApp` AnyType `TypeApp` AnyType, [|compareF|])
|
||||
])
|
||||
@ -247,6 +260,10 @@ instance TestEquality FloatInfoRepr where
|
||||
instance OrdF FloatInfoRepr where
|
||||
compareF = $(structuralTypeOrd [t|FloatInfoRepr|] [])
|
||||
|
||||
floatBVTypeRepr :: FloatInfoRepr fi -> TypeRepr (FloatBVType fi)
|
||||
floatBVTypeRepr fi | LeqProof <- floatInfoBitsIsPos fi =
|
||||
BVTypeRepr $ floatInfoBits fi
|
||||
|
||||
------------------------------------------------------------------------
|
||||
--
|
||||
|
||||
|
||||
2
deps/flexdis86
vendored
2
deps/flexdis86
vendored
@ -1 +1 @@
|
||||
Subproject commit 2ac3d616996885f93b66c870520381cb09e783ca
|
||||
Subproject commit 64a3b8154a654e7079a6a5253a00d4fe8dac9934
|
||||
@ -20,4 +20,5 @@ extra-deps:
|
||||
- monadLib-3.7.3
|
||||
- panic-0.4.0.1
|
||||
- IntervalMap-0.6.1.0
|
||||
- itanium-abi-0.1.1.0
|
||||
resolver: lts-11.22
|
||||
|
||||
24
stack.ghc-8.6.3.yaml
Normal file
24
stack.ghc-8.6.3.yaml
Normal file
@ -0,0 +1,24 @@
|
||||
flags:
|
||||
time-locale-compat:
|
||||
old-locale: false
|
||||
|
||||
packages:
|
||||
- base
|
||||
- x86
|
||||
- symbolic
|
||||
- x86_symbolic
|
||||
- deps/crucible/what4
|
||||
- deps/crucible/crucible
|
||||
- deps/crucible/crucible-llvm
|
||||
- deps/dwarf
|
||||
- deps/elf-edit
|
||||
- deps/flexdis86
|
||||
- deps/flexdis86/binary-symbols
|
||||
- deps/llvm-pretty
|
||||
- deps/parameterized-utils
|
||||
extra-deps:
|
||||
- boomerang-1.4.5.6
|
||||
- itanium-abi-0.1.1.0
|
||||
- monadLib-3.9
|
||||
- panic-0.4.0.1
|
||||
resolver: lts-13.7
|
||||
@ -233,7 +233,8 @@ getSomeBVLocation v =
|
||||
F.XMMReg r -> do avx <- isAVX
|
||||
pure $ SomeBV $ if avx then xmm_avx r
|
||||
else xmm_sse r
|
||||
F.YMMReg r -> pure $ SomeBV $ ymm r
|
||||
F.YMMReg r -> do avx <- isAVX
|
||||
pure $ SomeBV $ if avx then ymm_zero r else ymm_preserve r
|
||||
F.SegmentValue s -> pure $ SomeBV $ SegmentReg s
|
||||
F.X87Register i -> mk (X87StackRegister i)
|
||||
F.FarPointer _ -> fail "FarPointer"
|
||||
@ -320,7 +321,7 @@ getSignExtendedValue v out_w =
|
||||
F.Mem128 ar -> mk =<< getBV128Addr ar
|
||||
F.Mem256 ar -> mk =<< getBV256Addr ar
|
||||
F.XMMReg r -> mk (xmm_avx r)
|
||||
F.YMMReg r -> mk (ymm r)
|
||||
F.YMMReg r -> mk (ymm_zero r)
|
||||
|
||||
F.ByteImm i
|
||||
| Just Refl <- testEquality n8 out_w ->
|
||||
@ -474,6 +475,6 @@ readXMMValue _ = fail "XMM Instruction given unexpected value."
|
||||
|
||||
-- | Get a YMM value
|
||||
readYMMValue :: F.Value -> X86Generator st ids (Expr ids (BVType 256))
|
||||
readYMMValue (F.YMMReg r) = get (ymm r)
|
||||
readYMMValue (F.YMMReg r) = get (ymm_zero r)
|
||||
readYMMValue (F.Mem256 a) = readBVAddress a ymmMemRepr
|
||||
readYMMValue _ = fail "YMM Instruction given unexpected value."
|
||||
|
||||
@ -81,7 +81,8 @@ module Data.Macaw.X86.Monad
|
||||
, ax, bx, cx, dx
|
||||
, al, dl
|
||||
, ah
|
||||
, ymm
|
||||
, ymm_preserve
|
||||
, ymm_zero
|
||||
, xmm_sse
|
||||
, xmm_avx
|
||||
, xmmOwner
|
||||
@ -838,17 +839,22 @@ ah = reg_high8 R.RAX
|
||||
rip :: Location addr (BVType 64)
|
||||
rip = fullRegister R.X86_IP
|
||||
|
||||
ymm :: F.YMMReg -> Location addr (BVType 256)
|
||||
ymm = fullRegister . R.YMM . F.ymmRegNo
|
||||
-- | Access the low-order 256-bits in legacy SSE mode (upper 256-bits preserved)
|
||||
ymm_preserve :: F.YMMReg -> Location addr (BVType 256)
|
||||
ymm_preserve r = subRegister n0 n256 (R.ZMM (F.ymmRegNo r))
|
||||
|
||||
-- | Access the low-order 256-bits in legacy SSE mode (upper 256-bits zeroed)
|
||||
ymm_zero :: F.YMMReg -> Location addr (BVType 256)
|
||||
ymm_zero r = constUpperBitsOnWriteRegister n256 ZeroExtendOnWrite (R.ZMM (F.ymmRegNo r))
|
||||
|
||||
xmm_sse :: F.XMMReg -> Location addr (BVType 128)
|
||||
xmm_sse = reg_low128_sse . xmmOwner
|
||||
xmm_sse r = subRegister n0 n128 (R.ZMM (F.xmmRegNo r))
|
||||
|
||||
xmm_avx :: F.XMMReg -> Location addr (BVType 128)
|
||||
xmm_avx = reg_low128_avx . xmmOwner
|
||||
xmm_avx r = constUpperBitsOnWriteRegister n128 ZeroExtendOnWrite (R.ZMM (F.xmmRegNo r))
|
||||
|
||||
xmmOwner :: F.XMMReg -> X86Reg (BVType 256)
|
||||
xmmOwner = R.YMM . F.xmmRegNo
|
||||
xmmOwner :: F.XMMReg -> X86Reg (BVType 512)
|
||||
xmmOwner r = R.ZMM (F.xmmRegNo r)
|
||||
|
||||
------------------------------------------------------------------------
|
||||
|
||||
|
||||
@ -7,14 +7,13 @@ import Control.Monad(forM_)
|
||||
import Data.Parameterized.NatRepr
|
||||
import Data.Parameterized.Some
|
||||
|
||||
import Flexdis86.Register (ymmReg)
|
||||
import qualified Flexdis86 as F
|
||||
|
||||
import Data.Macaw.CFG.Core(Value,bvValue)
|
||||
import Data.Macaw.Types(BVType,typeWidth,n0,n1,n32,n64,n256)
|
||||
import Data.Macaw.Types(BVType,typeWidth,n0,n1,n32,n64,n128, n256)
|
||||
|
||||
import Data.Macaw.X86.InstructionDef
|
||||
import Data.Macaw.X86.Monad((.=), ymm, reg_high128, uext)
|
||||
import Data.Macaw.X86.Monad((.=), uext, subRegister)
|
||||
import Data.Macaw.X86.Getters(SomeBV(..),getSomeBVValue,getSomeBVLocation
|
||||
, truncateBVValue )
|
||||
import Data.Macaw.X86.Generator(X86Generator, Expr(..),inAVX,evalArchFn,eval)
|
||||
@ -181,12 +180,12 @@ all_instructions =
|
||||
defNullary "vzeroall" $
|
||||
inAVX $
|
||||
forM_ [ 0 .. maxReg ] $ \r ->
|
||||
ymm (ymmReg r) .= ValueExpr (bvValue 0)
|
||||
subRegister n0 n256 (ZMM r) .= ValueExpr (bvValue 0)
|
||||
|
||||
, defNullary "vzeroupper" $
|
||||
inAVX $
|
||||
forM_ [ 0 .. maxReg ] $ \r ->
|
||||
reg_high128 (YMM r) .= ValueExpr (bvValue 0)
|
||||
subRegister n128 n128 (ZMM r) .= ValueExpr (bvValue 0)
|
||||
|
||||
, avxMov "vmovaps"
|
||||
, avxMov "vmovups"
|
||||
|
||||
@ -31,6 +31,7 @@ module Data.Macaw.X86.X86Reg
|
||||
, X87_Control
|
||||
, XMM
|
||||
, YMM
|
||||
, ZMM
|
||||
|
||||
-- * X86Reg
|
||||
, X86Reg(..)
|
||||
@ -81,12 +82,12 @@ module Data.Macaw.X86.X86Reg
|
||||
, pattern X87_C2
|
||||
, pattern X87_C3
|
||||
-- * Large registers
|
||||
, pattern YMM
|
||||
, pattern ZMM
|
||||
|
||||
-- * Register lists
|
||||
, gpRegList
|
||||
, flagRegList
|
||||
, ymmRegList
|
||||
, zmmRegList
|
||||
, x87FPURegList
|
||||
, x86StateRegs
|
||||
, x86CalleeSavedRegs
|
||||
@ -125,6 +126,7 @@ type X87_ControlMask = BVType 1
|
||||
type X87_Control = BVType 2
|
||||
type XMM = BVType 128
|
||||
type YMM = BVType 256
|
||||
type ZMM = BVType 512
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- X86Reg
|
||||
@ -144,8 +146,9 @@ data X86Reg tp
|
||||
| (tp ~ BVType 2) => X87_TagReg {-# UNPACK #-} !Int
|
||||
-- One of 8 fpu/mmx registers.
|
||||
| (tp ~ BVType 80) => X87_FPUReg {-#UNPACK #-} !F.MMXReg
|
||||
-- One of 8 XMM/YMM registers
|
||||
| (tp ~ BVType 256) => X86_YMMReg !F.YMMReg
|
||||
-- AVX2 has 32 512-bit registers.
|
||||
| (tp ~ BVType 512) => X86_ZMMReg !Word8
|
||||
|
||||
|
||||
instance Show (X86Reg tp) where
|
||||
show X86_IP = "rip"
|
||||
@ -156,7 +159,7 @@ instance Show (X86Reg tp) where
|
||||
show X87_TopReg = "x87top"
|
||||
show (X87_TagReg n) = "tag" ++ show n
|
||||
show (X87_FPUReg r) = show r
|
||||
show (X86_YMMReg r) = show r
|
||||
show (X86_ZMMReg r) = "zmm" ++ show r
|
||||
|
||||
instance ShowF X86Reg where
|
||||
showF = show
|
||||
@ -209,7 +212,7 @@ instance OrdF X86Reg where
|
||||
compareF X87_FPUReg{} _ = LTF
|
||||
compareF _ X87_FPUReg{} = GTF
|
||||
|
||||
compareF (X86_YMMReg n) (X86_YMMReg n') = fromOrdering (compare n n')
|
||||
compareF (X86_ZMMReg n) (X86_ZMMReg n') = fromOrdering (compare n n')
|
||||
|
||||
instance Ord (X86Reg cl) where
|
||||
a `compare` b = case a `compareF` b of
|
||||
@ -227,7 +230,7 @@ instance HasRepr X86Reg TypeRepr where
|
||||
X87_TopReg -> knownRepr
|
||||
X87_TagReg{} -> knownRepr
|
||||
X87_FPUReg{} -> knownRepr
|
||||
X86_YMMReg{} -> knownRepr
|
||||
X86_ZMMReg{} -> knownRepr
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Exported constructors and their conversion to words
|
||||
@ -359,8 +362,11 @@ pattern X87_C2 = X87_StatusReg 10
|
||||
pattern X87_C3 :: () => (t ~ X87_Status) => X86Reg t
|
||||
pattern X87_C3 = X87_StatusReg 14
|
||||
|
||||
pattern YMM :: () => (t ~ YMM) => Word8 -> X86Reg t
|
||||
pattern YMM w = X86_YMMReg (F.YMMR w)
|
||||
pattern ZMM :: () => (t ~ ZMM) => Word8 -> X86Reg t
|
||||
pattern ZMM w <- X86_ZMMReg w
|
||||
where ZMM w | w < 32 = X86_ZMMReg w
|
||||
| otherwise = error "There are only 32 ZMM registers."
|
||||
|
||||
|
||||
x87StatusNames :: V.Vector String
|
||||
x87StatusNames = V.fromList $
|
||||
@ -392,8 +398,8 @@ x87TagRegList = [X87_TagReg i | i <- [0..7]]
|
||||
x87FPURegList :: [X86Reg (BVType 80)]
|
||||
x87FPURegList = [X87_FPUReg (F.mmxReg i) | i <- [0..7]]
|
||||
|
||||
ymmRegList :: [X86Reg (BVType 256)]
|
||||
ymmRegList = [X86_YMMReg (F.ymmReg i) | i <- [0..15]]
|
||||
zmmRegList :: [X86Reg (BVType 512)]
|
||||
zmmRegList = [X86_ZMMReg i | i <- [0..31]]
|
||||
|
||||
-- | List of registers stored in X86State
|
||||
x86StateRegs :: [Some X86Reg]
|
||||
@ -405,7 +411,7 @@ x86StateRegs
|
||||
++ [Some X87_TopReg]
|
||||
++ (Some <$> x87TagRegList)
|
||||
++ (Some <$> x87FPURegList)
|
||||
++ (Some <$> ymmRegList)
|
||||
++ (Some <$> zmmRegList)
|
||||
|
||||
type instance RegAddrWidth X86Reg = 64
|
||||
|
||||
@ -444,11 +450,11 @@ x86CalleeSavedRegs = Set.fromList $
|
||||
x86ArgumentRegs :: [X86Reg (BVType 64)]
|
||||
x86ArgumentRegs = X86_GP <$> [ F.RDI, F.RSI, F.RDX, F.RCX, F.R8, F.R9 ]
|
||||
|
||||
x86FloatArgumentRegs :: [X86Reg (BVType 256)]
|
||||
x86FloatArgumentRegs = X86_YMMReg . F.ymmReg <$> [0..7]
|
||||
x86FloatArgumentRegs :: [X86Reg (BVType 512)]
|
||||
x86FloatArgumentRegs = X86_ZMMReg <$> [0..7]
|
||||
|
||||
x86ResultRegs :: [X86Reg (BVType 64)]
|
||||
x86ResultRegs = X86_GP <$> [ F.RAX, F.RDX ]
|
||||
|
||||
x86FloatResultRegs :: [X86Reg (BVType 256)]
|
||||
x86FloatResultRegs = [ X86_YMMReg (F.ymmReg 0) ]
|
||||
x86FloatResultRegs :: [X86Reg (BVType 512)]
|
||||
x86FloatResultRegs = [ X86_ZMMReg 0 ]
|
||||
|
||||
@ -105,7 +105,7 @@ withConcreteCountAndDir
|
||||
-> (AtomWrapper (RegEntry sym) M.BoolType)
|
||||
-> (S sym rtp bs r ctx -> (SymBV sym 64) -> IO (S sym rtp bs r ctx))
|
||||
-> IO (RegValue sym UnitType, S sym rtp bs r ctx)
|
||||
withConcreteCountAndDir state val_size wrapped_count wrapped_dir func = do
|
||||
withConcreteCountAndDir state val_size wrapped_count _wrapped_dir func = do
|
||||
let sym = state^.stateSymInterface
|
||||
let val_byte_size = M.repValSizeByteCount val_size
|
||||
bv_count <- toValBV sym wrapped_count
|
||||
|
||||
@ -87,7 +87,7 @@ type instance ArchRegContext M.X86_64
|
||||
<+> (EmptyCtx ::> M.BVType 3) -- X87 top of the stack (x87 status word)
|
||||
<+> CtxRepeat 8 (M.BVType 2) -- X87 tags
|
||||
<+> CtxRepeat 8 (M.BVType 80) -- FP regs
|
||||
<+> CtxRepeat 16 (M.BVType 256) -- YMM regs
|
||||
<+> CtxRepeat 16 (M.BVType 512) -- ZMM regs
|
||||
|
||||
type RegAssign f = Assignment f (ArchRegContext M.X86_64)
|
||||
|
||||
@ -112,7 +112,7 @@ x86RegName' (M.X87_StatusReg r) = show r
|
||||
x86RegName' M.X87_TopReg = "x87Top"
|
||||
x86RegName' (M.X87_TagReg r) = "x87Tag" ++ show r
|
||||
x86RegName' (M.X87_FPUReg r) = show r
|
||||
x86RegName' (M.X86_YMMReg r) = show r
|
||||
x86RegName' (M.X86_ZMMReg r) = "zmm" ++ show r
|
||||
|
||||
x86RegName :: M.X86Reg tp -> C.SolverSymbol
|
||||
x86RegName r = C.systemSymbol $ "r!" ++ x86RegName' r
|
||||
@ -142,7 +142,8 @@ x86RegAssignment =
|
||||
<++> (Empty :> M.X87_TopReg)
|
||||
<++> (repeatAssign (M.X87_TagReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 8 (M.BVType 2)))
|
||||
<++> (repeatAssign (M.X87_FPUReg . F.mmxReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 8 (M.BVType 80)))
|
||||
<++> (repeatAssign (M.X86_YMMReg . F.ymmReg . fromIntegral) :: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 256)))
|
||||
<++> (repeatAssign (M.X86_ZMMReg . fromIntegral)
|
||||
:: Assignment M.X86Reg (CtxRepeat 16 (M.BVType 512)))
|
||||
|
||||
|
||||
x86RegStructType :: C.TypeRepr (ArchRegStruct M.X86_64)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user