mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-26 23:52:48 +03:00
Use a ConstraintKind to simplify a number of constraint contexts
This commit is contained in:
parent
adf8a46f91
commit
c751e02e6c
@ -68,7 +68,7 @@ readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
|
|||||||
Nothing -> ET.throwError (MM.InvalidInstruction (MM.relativeSegmentAddr addr) contents)
|
Nothing -> ET.throwError (MM.InvalidInstruction (MM.relativeSegmentAddr addr) contents)
|
||||||
|
|
||||||
disassembleBlock :: forall ppc s
|
disassembleBlock :: forall ppc s
|
||||||
. (ArchWidth ppc, ArchReg ppc ~ PPCReg ppc, MM.MemWidth (ArchAddrWidth ppc))
|
. (PPCWidth ppc)
|
||||||
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
||||||
-> MM.Memory (ArchAddrWidth ppc)
|
-> MM.Memory (ArchAddrWidth ppc)
|
||||||
-> GenState ppc s
|
-> GenState ppc s
|
||||||
@ -81,9 +81,6 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
|||||||
case readInstruction mem curIPAddr of
|
case readInstruction mem curIPAddr of
|
||||||
Left err -> failAt gs off curIPAddr (DecodeError err)
|
Left err -> failAt gs off curIPAddr (DecodeError err)
|
||||||
Right (i, bytesRead) -> do
|
Right (i, bytesRead) -> do
|
||||||
-- let nextIP = MM.relativeAddr seg (off + bytesRead)
|
|
||||||
-- let nextIPVal = MC.RelocatableValue undefined nextIP
|
|
||||||
|
|
||||||
-- Note: In PowerPC, the IP is incremented *after* an instruction
|
-- Note: In PowerPC, the IP is incremented *after* an instruction
|
||||||
-- executes, rather than before as in X86. We have to pass in the
|
-- executes, rather than before as in X86. We have to pass in the
|
||||||
-- physical address of the instruction here.
|
-- physical address of the instruction here.
|
||||||
@ -93,9 +90,6 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
|||||||
case lookupSemantics ipVal i of
|
case lookupSemantics ipVal i of
|
||||||
Nothing -> failAt gs off curIPAddr (UnsupportedInstruction i)
|
Nothing -> failAt gs off curIPAddr (UnsupportedInstruction i)
|
||||||
Just transformer -> do
|
Just transformer -> do
|
||||||
-- FIXME: Do we need to add failure modes here? Probably. There are
|
|
||||||
-- some invalid encodings that we could encounter that would be worth
|
|
||||||
-- failing for.
|
|
||||||
egs1 <- liftST $ execGenerator gs $ do
|
egs1 <- liftST $ execGenerator gs $ do
|
||||||
let line = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
|
let line = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
|
||||||
addStmt (Comment (T.pack line))
|
addStmt (Comment (T.pack line))
|
||||||
@ -104,7 +98,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
|||||||
Left genErr -> failAt gs off curIPAddr (GenerationError i genErr)
|
Left genErr -> failAt gs off curIPAddr (GenerationError i genErr)
|
||||||
Right gs1 -> undefined
|
Right gs1 -> undefined
|
||||||
|
|
||||||
tryDisassembleBlock :: (ArchWidth ppc, ArchReg ppc ~ PPCReg ppc, MM.MemWidth (ArchAddrWidth ppc), KnownNat (RegAddrWidth (PPCReg ppc)))
|
tryDisassembleBlock :: (PPCWidth ppc)
|
||||||
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
||||||
-> MM.Memory (ArchAddrWidth ppc)
|
-> MM.Memory (ArchAddrWidth ppc)
|
||||||
-> NC.NonceGenerator (ST s) s
|
-> NC.NonceGenerator (ST s) s
|
||||||
@ -126,7 +120,7 @@ tryDisassembleBlock lookupSemantics mem nonceGen startAddr maxSize = do
|
|||||||
--
|
--
|
||||||
-- Return a list of disassembled blocks as well as the total number of bytes
|
-- Return a list of disassembled blocks as well as the total number of bytes
|
||||||
-- occupied by those blocks.
|
-- occupied by those blocks.
|
||||||
disassembleFn :: (ArchWidth ppc, ArchReg ppc ~ PPCReg ppc, MM.MemWidth (RegAddrWidth (ArchReg ppc)), KnownNat (RegAddrWidth (PPCReg ppc)))
|
disassembleFn :: (PPCWidth ppc)
|
||||||
=> proxy ppc
|
=> proxy ppc
|
||||||
-> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
-> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
||||||
-- ^ A function to look up the semantics for an instruction. The
|
-- ^ A function to look up the semantics for an instruction. The
|
||||||
|
@ -1,3 +1,4 @@
|
|||||||
|
{-# LANGUAGE ConstraintKinds #-}
|
||||||
{-# LANGUAGE DataKinds #-}
|
{-# LANGUAGE DataKinds #-}
|
||||||
{-# LANGUAGE FlexibleContexts #-}
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
{-# LANGUAGE GADTs #-}
|
{-# LANGUAGE GADTs #-}
|
||||||
@ -12,6 +13,7 @@
|
|||||||
module Data.Macaw.PPC.PPCReg (
|
module Data.Macaw.PPC.PPCReg (
|
||||||
PPCReg(..),
|
PPCReg(..),
|
||||||
linuxSystemCallPreservedRegisters,
|
linuxSystemCallPreservedRegisters,
|
||||||
|
PPCWidth,
|
||||||
ArchWidth(..)
|
ArchWidth(..)
|
||||||
) where
|
) where
|
||||||
|
|
||||||
@ -99,8 +101,13 @@ instance (ArchWidth ppc) => HasRepr (PPCReg ppc) TypeRepr where
|
|||||||
PPC_CTR -> BVTypeRepr (pointerNatRepr (Proxy @ppc))
|
PPC_CTR -> BVTypeRepr (pointerNatRepr (Proxy @ppc))
|
||||||
PPC_CR -> BVTypeRepr n32
|
PPC_CR -> BVTypeRepr n32
|
||||||
|
|
||||||
instance (MM.MemWidth w, ArchWidth ppc, w ~ MC.RegAddrWidth (PPCReg ppc), 1 <= w)
|
type PPCWidth ppc = (ArchWidth ppc,
|
||||||
=> MC.RegisterInfo (PPCReg ppc) where
|
MC.ArchReg ppc ~ PPCReg ppc,
|
||||||
|
MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc)),
|
||||||
|
1 <= MC.RegAddrWidth (PPCReg ppc),
|
||||||
|
KnownNat (MC.RegAddrWidth (PPCReg ppc)))
|
||||||
|
|
||||||
|
instance (PPCWidth ppc) => MC.RegisterInfo (PPCReg ppc) where
|
||||||
archRegs = ppcRegs
|
archRegs = ppcRegs
|
||||||
sp_reg = PPC_GP (D.GPR 1)
|
sp_reg = PPC_GP (D.GPR 1)
|
||||||
ip_reg = PPC_IP
|
ip_reg = PPC_IP
|
||||||
|
Loading…
Reference in New Issue
Block a user