Remove unused debug reg code.

This commit is contained in:
Joe Hendrix 2019-09-09 00:55:28 -07:00
parent 3dc9463b8d
commit 7aee0cd803
No known key found for this signature in database
GPG Key ID: 8DFA5FF784098C4F
3 changed files with 2 additions and 15 deletions

View File

@ -139,8 +139,7 @@ instance PrettyF X86TermStmt where
-- X86 architecture model.
-- Primitive locations are not modeled as registers, but rather as implicit state.
data X86PrimLoc tp
= (tp ~ BVType 64) => DebugLoc !F.DebugReg
| (tp ~ BVType 16) => FS
= (tp ~ BVType 16) => FS
-- ^ This refers to the selector of the 'FS' register.
| (tp ~ BVType 16) => GS
-- ^ This refers to the selector of the 'GS' register.
@ -148,7 +147,6 @@ data X86PrimLoc tp
-- ^ One of the x87 control registers
instance HasRepr X86PrimLoc TypeRepr where
typeRepr DebugLoc{} = knownRepr
typeRepr FS = knownRepr
typeRepr GS = knownRepr
typeRepr (X87_ControlLoc r) =
@ -156,7 +154,6 @@ instance HasRepr X86PrimLoc TypeRepr where
LeqProof -> BVTypeRepr (typeRepr r)
instance Pretty (X86PrimLoc tp) where
pretty (DebugLoc r) = text (show r)
pretty FS = text "fs"
pretty GS = text "gs"
pretty (X87_ControlLoc r) = text (show r)

View File

@ -233,7 +233,7 @@ getSomeBVLocation :: F.Value -> X86Generator st ids (SomeBV (Location (Addr ids)
getSomeBVLocation v =
case v of
F.ControlReg _ -> fail "ControlReg"
F.DebugReg dr -> pure $ SomeBV $ DebugReg dr
F.DebugReg _ -> fail "DebugReg"
F.MMXReg mmx -> pure $ SomeBV $ x87reg_mmx $ X87_FPUReg mmx
F.XMMReg r -> do avx <- isAVX
pure $ SomeBV $ if avx then xmm_avx r

View File

@ -502,9 +502,6 @@ data Location addr (tp :: Type) where
Register :: !(RegisterView m b n)
-> Location addr (BVType n)
DebugReg :: !F.DebugReg
-> Location addr (BVType 64)
SegmentReg :: !F.Segment
-> Location addr (BVType 16)
@ -560,9 +557,6 @@ setLoc loc v =
MemoryAddr w tp -> do
addr <- eval w
addStmt $ WriteMem addr tp v
DebugReg r ->
addWriteLoc (DebugLoc r) v
SegmentReg s
| s == F.FS -> addWriteLoc FS v
| s == F.GS -> addWriteLoc GS v
@ -614,7 +608,6 @@ ppLocation ppAddr loc = case loc of
MemoryAddr addr _tr -> ppAddr addr
Register rv -> ppReg rv
FullRegister r -> text $ "%" ++ show r
DebugReg r -> text (show r)
SegmentReg r -> text (show r)
X87ControlReg r -> text ("x87_" ++ show r)
X87StackRegister i -> text $ "x87_stack@" ++ show i
@ -680,7 +673,6 @@ instance HasRepr (Location addr) TypeRepr where
typeRepr (MemoryAddr _ tp) = typeRepr tp
typeRepr (FullRegister r) = typeRepr r
typeRepr (Register rv@RegisterView{}) = BVTypeRepr $ _registerViewSize rv
typeRepr (DebugReg _) = knownRepr
typeRepr (SegmentReg _) = knownRepr
typeRepr (X87ControlReg r) =
case x87ControlRegWidthIsPos r of
@ -1555,8 +1547,6 @@ get l0 =
MemoryAddr w tp -> do
addr <- eval w
evalAssignRhs (ReadMem addr tp)
DebugReg _ ->
fail $ "Do not support reading debug registers."
SegmentReg s
| s == F.FS -> readLoc FS
| s == F.GS -> readLoc GS