GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-22 23:32:15 +03:00
Code Issues Projects Releases Wiki Activity

Tr/warning cleanups (#127)

Browse Source 
Warning and style cleanups in macaw-semmc and macaw-aarch32
This commit is contained in:
Tristan Ravitch 2020-04-14 00:07:15 -07:00 committed by GitHub
parent d6de268bbd
commit a824fc4051
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 164 additions and 342 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
macaw-aarch32/macaw-aarch32.cabal
View File

@ -20,7 +20,6 @@ library
, Data.Macaw.ARM.Disassemble , Data.Macaw.ARM.Disassemble
, Data.Macaw.ARM.Eval , Data.Macaw.ARM.Eval
, Data.Macaw.ARM.Identify , Data.Macaw.ARM.Identify
, Data.Macaw.ARM.Operand
, Data.Macaw.ARM.Semantics.ARMSemantics , Data.Macaw.ARM.Semantics.ARMSemantics
, Data.Macaw.ARM.Semantics.ThumbSemantics , Data.Macaw.ARM.Semantics.ThumbSemantics
, Data.Macaw.ARM.Semantics.TH , Data.Macaw.ARM.Semantics.TH

6
macaw-aarch32/src/Data/Macaw/ARM.hs
View File

@ -26,7 +26,6 @@ import Control.Lens ( (^.) )
import qualified Data.Macaw.Architecture.Info as MI import qualified Data.Macaw.Architecture.Info as MI
import qualified Data.Macaw.CFG.DemandSet as MDS import qualified Data.Macaw.CFG.DemandSet as MDS
import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.Memory as MM
import Data.Proxy ( Proxy(..) )
import qualified SemMC.Architecture.AArch32 as ARM import qualified SemMC.Architecture.AArch32 as ARM
@ -41,7 +40,7 @@ arm_linux_info =
, MI.archEndianness = MM.LittleEndian , MI.archEndianness = MM.LittleEndian
, MI.extractBlockPrecond = extractBlockPrecond , MI.extractBlockPrecond = extractBlockPrecond
, MI.initialBlockRegs = initialBlockRegs , MI.initialBlockRegs = initialBlockRegs
, MI.disassembleFn = disassembleFn proxy ARMSem.execInstruction ThumbSem.execInstruction , MI.disassembleFn = disassembleFn ARMSem.execInstruction ThumbSem.execInstruction
, MI.mkInitialAbsState = mkInitialAbsState , MI.mkInitialAbsState = mkInitialAbsState
, MI.absEvalArchFn = absEvalArchFn , MI.absEvalArchFn = absEvalArchFn
, MI.absEvalArchStmt = absEvalArchStmt , MI.absEvalArchStmt = absEvalArchStmt
@ -55,9 +54,6 @@ arm_linux_info =
, MI.archDemandContext = archDemandContext , MI.archDemandContext = archDemandContext
, MI.postArchTermStmtAbsState = postARMTermStmtAbsState preserveRegAcrossSyscall , MI.postArchTermStmtAbsState = postARMTermStmtAbsState preserveRegAcrossSyscall
} }
where
proxy = Proxy @ARM.AArch32
archDemandContext :: MDS.DemandContext ARM.AArch32 archDemandContext :: MDS.DemandContext ARM.AArch32
archDemandContext = archDemandContext =

98
macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
View File

@ -15,10 +15,8 @@
module Data.Macaw.ARM.ARMReg module Data.Macaw.ARM.ARMReg
( ARMReg(..) ( ARMReg(..)
-- , armRegToGPR
, arm_LR , arm_LR
, branchTaken , branchTaken
-- , ArchWidth(..)
, linuxSystemCallPreservedRegisters , linuxSystemCallPreservedRegisters
, locToRegTH , locToRegTH
, integerToReg , integerToReg
@ -29,23 +27,20 @@ module Data.Macaw.ARM.ARMReg
import Data.Parameterized.Classes import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.NatRepr as NR
import Data.Parameterized.Some ( Some(..) ) import Data.Parameterized.Some ( Some(..) )
import Data.Parameterized.SymbolRepr (symbolRepr) import qualified Data.Parameterized.SymbolRepr as PSR
import Data.Parameterized.TraversableFC (toListFC, fmapFC) import qualified Data.Parameterized.TraversableFC as FC
import qualified Data.Parameterized.TH.GADT as TH import qualified Data.Parameterized.TH.GADT as PTH
import qualified Data.Set as Set import qualified Data.Set as Set
import qualified Data.Text as T import qualified Data.Text as T
import Data.Word ( Word32 )
import GHC.TypeLits import GHC.TypeLits
import Language.Haskell.TH import qualified Language.Haskell.TH as TH
import Language.Haskell.TH.Syntax ( lift )
import qualified Text.PrettyPrint.ANSI.Leijen as PP import qualified Text.PrettyPrint.ANSI.Leijen as PP
import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.CFG as MC
import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.Memory as MM
import Data.Macaw.Types as MT import qualified Data.Macaw.Types as MT
-- ( TypeRepr(..), HasRepr, BVType
-- , typeRepr, n32 )
import qualified Language.ASL.Globals as ASL import qualified Language.ASL.Globals as ASL
import qualified SemMC.Architecture.AArch32 as SA import qualified SemMC.Architecture.AArch32 as SA
import qualified SemMC.Architecture.ARM.Location as SA import qualified SemMC.Architecture.ARM.Location as SA
@ -62,25 +57,29 @@ baseToMacawTypeRepr _ = error "ARMReg: unsupported what4 type"
-- | Defines the Register set for the ARM processor. -- | Defines the Register set for the ARM processor.
--
-- Note that the unusual statements of the GADT types in the BV and Bool cases
-- are that way to make it easier to bring type variables into scope and allow
-- us to recover some extra type equalities when pattern matching.
data ARMReg tp where data ARMReg tp where
-- | 'ASL.GlobalRef' that refers to a bitvector. -- | 'ASL.GlobalRef' that refers to a bitvector.
ARMGlobalBV :: ( tp ~ BVType w ARMGlobalBV :: ( tp ~ MT.BVType w
, 1 <= w , 1 <= w
, tp' ~ ASL.GlobalsType s , tp' ~ ASL.GlobalsType s
, tp ~ BaseToMacawType tp') , tp ~ BaseToMacawType tp')
=> ASL.GlobalRef s -> ARMReg tp => ASL.GlobalRef s -> ARMReg tp
-- | 'ASL.GlobalRef' that refers to a boolean. -- | 'ASL.GlobalRef' that refers to a boolean.
ARMGlobalBool :: ( tp ~ BoolType ARMGlobalBool :: ( tp ~ MT.BoolType
, tp' ~ ASL.GlobalsType s , tp' ~ ASL.GlobalsType s
, tp ~ BaseToMacawType tp') , tp ~ BaseToMacawType tp')
=> ASL.GlobalRef s -> ARMReg tp => ASL.GlobalRef s -> ARMReg tp
ARMWriteMode :: tp ~ BVType 2 => ARMReg tp ARMWriteMode :: tp ~ MT.BVType 2 => ARMReg (MT.BVType 2)
-- | GPR14 is the link register for ARM -- | GPR14 is the link register for ARM
arm_LR :: (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => ARMReg (BVType w) arm_LR :: (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => ARMReg (MT.BVType w)
arm_LR = ARMGlobalBV (ASL.knownGlobalRef @"_R14") arm_LR = ARMGlobalBV (ASL.knownGlobalRef @"_R14")
branchTaken :: ARMReg BoolType branchTaken :: ARMReg MT.BoolType
branchTaken = ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken") branchTaken = ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")
instance Show (ARMReg tp) where instance Show (ARMReg tp) where
@ -98,9 +97,9 @@ instance MC.PrettyF ARMReg where
$(return []) -- allow template haskell below to see definitions above $(return []) -- allow template haskell below to see definitions above
instance TestEquality ARMReg where instance TestEquality ARMReg where
testEquality = $(TH.structuralTypeEquality [t| ARMReg |] testEquality = $(PTH.structuralTypeEquality [t| ARMReg |]
[ (TH.ConType [t|ASL.GlobalRef|] [ (PTH.ConType [t|ASL.GlobalRef|]
`TH.TypeApp` TH.AnyType, `PTH.TypeApp` PTH.AnyType,
[|testEquality|]) [|testEquality|])
]) ])
@ -111,9 +110,9 @@ instance Eq (ARMReg tp) where
r1 == r2 = r1 `eqF` r2 r1 == r2 = r1 `eqF` r2
instance OrdF ARMReg where instance OrdF ARMReg where
compareF = $(TH.structuralTypeOrd [t| ARMReg |] compareF = $(PTH.structuralTypeOrd [t| ARMReg |]
[ (TH.ConType [t|ASL.GlobalRef|] [ (PTH.ConType [t|ASL.GlobalRef|]
`TH.TypeApp` TH.AnyType, `PTH.TypeApp` PTH.AnyType,
[|compareF|]) [|compareF|])
]) ])
@ -121,11 +120,12 @@ instance Ord (ARMReg tp) where
r1 `compare` r2 = toOrdering (r1 `compareF` r2) r1 `compare` r2 = toOrdering (r1 `compareF` r2)
instance HasRepr ARMReg TypeRepr where instance MT.HasRepr ARMReg MT.TypeRepr where
typeRepr r = typeRepr r =
case r of case r of
ARMGlobalBV globalRef -> baseToMacawTypeRepr (ASL.globalRefRepr globalRef) ARMGlobalBV globalRef -> baseToMacawTypeRepr (ASL.globalRefRepr globalRef)
ARMGlobalBool globalRef -> baseToMacawTypeRepr (ASL.globalRefRepr globalRef) ARMGlobalBool globalRef -> baseToMacawTypeRepr (ASL.globalRefRepr globalRef)
ARMWriteMode -> MT.BVTypeRepr (NR.knownNat @2)
type instance MC.ArchReg SA.AArch32 = ARMReg type instance MC.ArchReg SA.AArch32 = ARMReg
type instance MC.RegAddrWidth ARMReg = 32 type instance MC.RegAddrWidth ARMReg = 32
@ -134,7 +134,6 @@ instance ( 1 <= MC.RegAddrWidth ARMReg
, KnownNat (MC.RegAddrWidth ARMReg) , KnownNat (MC.RegAddrWidth ARMReg)
, MM.MemWidth (MC.RegAddrWidth (MC.ArchReg SA.AArch32)) , MM.MemWidth (MC.RegAddrWidth (MC.ArchReg SA.AArch32))
, MC.ArchReg SA.AArch32 ~ ARMReg , MC.ArchReg SA.AArch32 ~ ARMReg
-- , ArchWidth arm
) => ) =>
MC.RegisterInfo ARMReg where MC.RegisterInfo ARMReg where
archRegs = armRegs archRegs = armRegs
@ -144,38 +143,16 @@ instance ( 1 <= MC.RegAddrWidth ARMReg
syscallArgumentRegs = error "TODO: MC.RegisterInfo ARMReg syscallArgumentsRegs undefined" syscallArgumentRegs = error "TODO: MC.RegisterInfo ARMReg syscallArgumentsRegs undefined"
armRegs :: forall w. (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => [Some ARMReg] armRegs :: forall w. (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => [Some ARMReg]
armRegs = toListFC asARMReg ( fmapFC ASL.SimpleGlobalRef ASL.simpleGlobalRefs Ctx.<++> armRegs = FC.toListFC asARMReg ( FC.fmapFC ASL.SimpleGlobalRef ASL.simpleGlobalRefs Ctx.<++>
ASL.gprGlobalRefsSym Ctx.<++> ASL.gprGlobalRefsSym Ctx.<++>
ASL.simdGlobalRefsSym ASL.simdGlobalRefsSym
) )
where asARMReg :: ASL.GlobalRef s -> Some ARMReg where asARMReg :: ASL.GlobalRef s -> Some ARMReg
asARMReg gr = case ASL.globalRefRepr gr of asARMReg gr = case ASL.globalRefRepr gr of
WT.BaseBoolRepr -> Some (ARMGlobalBool gr) WT.BaseBoolRepr -> Some (ARMGlobalBool gr)
WT.BaseBVRepr _ -> Some (ARMGlobalBV gr) WT.BaseBVRepr _ -> Some (ARMGlobalBV gr)
tp -> error $ "unsupported global type " <> show tp tp -> error $ "unsupported global type " <> show tp
-- baseToMacawTypeRepr (WT.BaseBVRepr w) = MT.BVTypeRepr w
-- baseToMacawTypeRepr WT.BaseBoolRepr = MT.BoolTypeRepr
-- baseToMacawTypeRepr _ = error "ARMReg: unsupported what4 type"
-- armRegs = [ Some (ARMGlobalBV (ASL.knownGlobalRef @"_R0"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R1"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R2"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R3"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R4"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R5"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R6"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R7"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R8"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R9"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R10"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R11"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R12"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R13"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_R14"))
-- , Some (ARMGlobalBV (ASL.knownGlobalRef @"_PC"))
-- ]
-- | The set of registers preserved across Linux system calls is defined by the ABI. -- | The set of registers preserved across Linux system calls is defined by the ABI.
-- --
-- According to -- According to
@ -199,22 +176,21 @@ linuxSystemCallPreservedRegisters =
-- | Translate a location from the semmc semantics into a location suitable for -- | Translate a location from the semmc semantics into a location suitable for
-- use in macaw -- use in macaw
locToRegTH :: proxy arm locToRegTH :: SA.Location SA.AArch32 ctp
-> SA.Location arm ctp -> TH.Q TH.Exp
-> Q Exp locToRegTH (SA.Location globalRef) = do
locToRegTH _ (SA.Location globalRef) = do let refName = T.unpack (PSR.symbolRepr (ASL.globalRefSymbol globalRef))
let refName = T.unpack (symbolRepr (ASL.globalRefSymbol globalRef))
case ASL.globalRefRepr globalRef of case ASL.globalRefRepr globalRef of
WT.BaseBoolRepr -> WT.BaseBoolRepr ->
[| ARMGlobalBool (ASL.knownGlobalRef :: ASL.GlobalRef $(return (LitT (StrTyLit refName)))) |] [| ARMGlobalBool (ASL.knownGlobalRef :: ASL.GlobalRef $(return (TH.LitT (TH.StrTyLit refName)))) |]
WT.BaseBVRepr _ -> WT.BaseBVRepr _ ->
[| ARMGlobalBV (ASL.knownGlobalRef :: ASL.GlobalRef $(return (LitT (StrTyLit refName)))) |] [| ARMGlobalBV (ASL.knownGlobalRef :: ASL.GlobalRef $(return (TH.LitT (TH.StrTyLit refName)))) |]
tp -> [| error $ "locToRegTH undefined for unrecognized location: " <> $(return $ LitE (StringL refName)) |] _tp -> [| error $ "locToRegTH undefined for unrecognized location: " <> $(return $ TH.LitE (TH.StringL refName)) |]
branchTakenReg :: ARMReg BoolType branchTakenReg :: ARMReg MT.BoolType
branchTakenReg = ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken") branchTakenReg = ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")
integerToReg :: Integer -> Maybe (ARMReg (BVType 32)) integerToReg :: Integer -> Maybe (ARMReg (MT.BVType 32))
integerToReg 0 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R0") integerToReg 0 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R0")
integerToReg 1 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R1") integerToReg 1 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R1")
integerToReg 2 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R2") integerToReg 2 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R2")
@ -232,7 +208,7 @@ integerToReg 13 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R13")
integerToReg 14 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R14") integerToReg 14 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R14")
integerToReg _ = Nothing integerToReg _ = Nothing
integerToSIMDReg :: Integer -> Maybe (ARMReg (BVType 128)) integerToSIMDReg :: Integer -> Maybe (ARMReg (MT.BVType 128))
integerToSIMDReg 0 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V0") integerToSIMDReg 0 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V0")
integerToSIMDReg 1 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V1") integerToSIMDReg 1 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V1")
integerToSIMDReg 2 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V2") integerToSIMDReg 2 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V2")

113
macaw-aarch32/src/Data/Macaw/ARM/Disassemble.hs
View File

@ -74,16 +74,16 @@ import Control.Monad.Trans ( lift )
import Data.Bits import Data.Bits
import qualified Data.ByteString as BS import qualified Data.ByteString as BS
import qualified Data.ByteString.Lazy as LBS import qualified Data.ByteString.Lazy as LBS
import Data.Macaw.ARM.ARMReg import qualified Data.Macaw.ARM.ARMReg as AR
import Data.Macaw.ARM.Arch() import Data.Macaw.ARM.Arch()
import Data.Macaw.CFG import qualified Data.Macaw.CFG as MC
import Data.Macaw.CFG.Block import qualified Data.Macaw.CFG.Block as MCB
import qualified Data.Macaw.CFG.Core as MC
import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.Memory as MM
import qualified Data.Macaw.Memory.Permissions as MMP import qualified Data.Macaw.Memory.Permissions as MMP
import Data.Macaw.SemMC.Generator import qualified Data.Macaw.SemMC.Generator as SG
import Data.Macaw.Types import qualified Data.Macaw.Types as MT
import qualified Data.Parameterized.Map as MapF import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.NatRepr as PN
import qualified Data.Parameterized.Nonce as NC import qualified Data.Parameterized.Nonce as NC
import qualified Data.Text as T import qualified Data.Text as T
import qualified Dismantle.ARM.A32 as ARMD import qualified Dismantle.ARM.A32 as ARMD
@ -103,25 +103,24 @@ data InstructionSet = A32I ARMD.Instruction | T32I ThumbD.Instruction
-- --
-- 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 :: proxy ARM.AArch32 disassembleFn :: (MC.Value ARM.AArch32 ids (MT.BVType 32) -> ARMD.Instruction -> Maybe (SG.Generator ARM.AArch32 ids s ()))
-> (Value ARM.AArch32 ids (BVType (ArchAddrWidth ARM.AArch32)) -> ARMD.Instruction -> Maybe (Generator ARM.AArch32 ids s ()))
-- ^ A function to look up the semantics for an A32 instruction. The -- ^ A function to look up the semantics for an A32 instruction. The
-- lookup is provided with the value of the IP in case IP-relative -- lookup is provided with the value of the IP in case IP-relative
-- addressing is necessary. -- addressing is necessary.
-> (Value ARM.AArch32 ids (BVType (ArchAddrWidth ARM.AArch32)) -> ThumbD.Instruction -> Maybe (Generator ARM.AArch32 ids s ())) -> (MC.Value ARM.AArch32 ids (MT.BVType 32) -> ThumbD.Instruction -> Maybe (SG.Generator ARM.AArch32 ids s ()))
-- ^ A function to look up the semantics for a T32 instruction. The -- ^ A function to look up the semantics for a T32 instruction. The
-- lookup is provided with the value of the IP in case IP-relative -- lookup is provided with the value of the IP in case IP-relative
-- addressing is necessary. -- addressing is necessary.
-> NC.NonceGenerator (ST s) ids -> NC.NonceGenerator (ST s) ids
-- ^ A generator of unique IDs used for assignments -- ^ A generator of unique IDs used for assignments
-> ArchSegmentOff ARM.AArch32 -> MC.ArchSegmentOff ARM.AArch32
-- ^ The address to disassemble from -- ^ The address to disassemble from
-> (RegState (ArchReg ARM.AArch32) (Value ARM.AArch32 ids)) -> (MC.RegState AR.ARMReg (MC.Value ARM.AArch32 ids))
-- ^ The initial registers -- ^ The initial registers
-> Int -> Int
-- ^ Maximum size of the block (a safeguard) -- ^ Maximum size of the block (a safeguard)
-> ST s (Block ARM.AArch32 ids, Int) -> ST s (MCB.Block ARM.AArch32 ids, Int)
disassembleFn _ lookupA32Semantics lookupT32Semantics nonceGen startAddr regState maxSize = do disassembleFn lookupA32Semantics lookupT32Semantics nonceGen startAddr regState maxSize = do
let lookupSemantics ipval instr = case instr of let lookupSemantics ipval instr = case instr of
A32I inst -> lookupA32Semantics ipval inst A32I inst -> lookupA32Semantics ipval inst
T32I inst -> lookupT32Semantics ipval inst T32I inst -> lookupT32Semantics ipval inst
@ -132,14 +131,14 @@ disassembleFn _ lookupA32Semantics lookupT32Semantics nonceGen startAddr regStat
Left (blocks, off, _exn) -> return (blocks, off) Left (blocks, off, _exn) -> return (blocks, off)
Right (blocks, bytes) -> return (blocks, bytes) Right (blocks, bytes) -> return (blocks, bytes)
tryDisassembleBlock :: (Value ARM.AArch32 ids (BVType (ArchAddrWidth ARM.AArch32)) -> InstructionSet -> Maybe (Generator ARM.AArch32 ids s ())) tryDisassembleBlock :: (MC.Value ARM.AArch32 ids (MT.BVType 32) -> InstructionSet -> Maybe (SG.Generator ARM.AArch32 ids s ()))
-> NC.NonceGenerator (ST s) ids -> NC.NonceGenerator (ST s) ids
-> ArchSegmentOff ARM.AArch32 -> MC.ArchSegmentOff ARM.AArch32
-> RegState (ArchReg ARM.AArch32) (Value ARM.AArch32 ids) -> MC.RegState AR.ARMReg (MC.Value ARM.AArch32 ids)
-> Int -> Int
-> DisM ARM.AArch32 ids s (Block ARM.AArch32 ids, Int) -> DisM ids s (MCB.Block ARM.AArch32 ids, Int)
tryDisassembleBlock lookupSemantics nonceGen startAddr regState maxSize = do tryDisassembleBlock lookupSemantics nonceGen startAddr regState maxSize = do
let gs0 = initGenState nonceGen startAddr regState let gs0 = SG.initGenState nonceGen startAddr regState
let startOffset = MM.segoffOffset startAddr let startOffset = MM.segoffOffset startAddr
(nextPCOffset, block) <- disassembleBlock lookupSemantics gs0 startAddr 0 (startOffset + fromIntegral maxSize) (nextPCOffset, block) <- disassembleBlock lookupSemantics gs0 startAddr 0 (startOffset + fromIntegral maxSize)
unless (nextPCOffset > startOffset) $ do unless (nextPCOffset > startOffset) $ do
@ -163,9 +162,9 @@ tryDisassembleBlock lookupSemantics nonceGen startAddr regState maxSize = do
-- In most of those cases, we end the block with a simple terminator. If the IP -- In most of those cases, we end the block with a simple terminator. If the IP
-- becomes a mux, we split execution using 'conditionalBranch'. -- becomes a mux, we split execution using 'conditionalBranch'.
disassembleBlock :: forall ids s . disassembleBlock :: forall ids s .
(Value ARM.AArch32 ids (BVType 32) -> InstructionSet -> Maybe (Generator ARM.AArch32 ids s ())) (MC.Value ARM.AArch32 ids (MT.BVType 32) -> InstructionSet -> Maybe (SG.Generator ARM.AArch32 ids s ()))
-- ^ A function to look up the semantics for an instruction that we disassemble -- ^ A function to look up the semantics for an instruction that we disassemble
-> GenState ARM.AArch32 ids s -> SG.GenState ARM.AArch32 ids s
-> MM.MemSegmentOff 32 -> MM.MemSegmentOff 32
-- ^ The current instruction pointer -- ^ The current instruction pointer
-> MM.MemWord 32 -> MM.MemWord 32
@ -174,7 +173,7 @@ disassembleBlock :: forall ids s .
-- ^ The maximum offset into the bytestring that we should -- ^ The maximum offset into the bytestring that we should
-- disassemble to; in principle, macaw can tell us to limit our -- disassemble to; in principle, macaw can tell us to limit our
-- search with this. -- search with this.
-> DisM ARM.AArch32 ids s (MM.MemWord 32, Block ARM.AArch32 ids) -> DisM ids s (MM.MemWord 32, MCB.Block ARM.AArch32 ids)
disassembleBlock lookupSemantics gs curPCAddr blockOff maxOffset = do disassembleBlock lookupSemantics gs curPCAddr blockOff maxOffset = do
let seg = MM.segoffSegment curPCAddr let seg = MM.segoffSegment curPCAddr
let off = MM.segoffOffset curPCAddr let off = MM.segoffOffset curPCAddr
@ -187,49 +186,49 @@ disassembleBlock lookupSemantics gs curPCAddr blockOff maxOffset = do
-- let curPC = MM.segmentOffAddr seg off -- let curPC = MM.segmentOffAddr seg off
let nextPCOffset = off + bytesRead let nextPCOffset = off + bytesRead
nextPC = MM.segmentOffAddr seg nextPCOffset nextPC = MM.segmentOffAddr seg nextPCOffset
nextPCVal :: Value ARM.AArch32 ids (BVType 32) = MC.RelocatableValue (MM.addrWidthRepr curPCAddr) nextPC nextPCVal :: MC.Value ARM.AArch32 ids (MT.BVType 32) = MC.RelocatableValue (MM.addrWidthRepr curPCAddr) nextPC
-- curPCVal :: Value ARM.AArch32 ids (BVType 32) = MC.RelocatableValue (MM.addrWidthRepr curPCAddr) curPC -- curPCVal :: Value ARM.AArch32 ids (BVType 32) = MC.RelocatableValue (MM.addrWidthRepr curPCAddr) curPC
-- Note: In ARM, the IP is incremented *after* an instruction -- Note: In ARM, the IP is incremented *after* an instruction
-- executes; pass in the physical address of the instruction here. -- executes; pass in the physical address of the instruction here.
ipVal <- case MM.asAbsoluteAddr (MM.segoffAddr curPCAddr) of ipVal <- case MM.asAbsoluteAddr (MM.segoffAddr curPCAddr) of
Nothing -> failAt gs off curPCAddr (InstructionAtUnmappedAddr i) Nothing -> failAt gs off curPCAddr (InstructionAtUnmappedAddr i)
Just addr -> return (BVValue (knownNat :: NatRepr 32) (fromIntegral addr)) Just addr -> return (MC.BVValue (PN.knownNat @32) (fromIntegral addr))
case lookupSemantics ipVal i of case lookupSemantics ipVal i of
Nothing -> failAt gs off curPCAddr (UnsupportedInstruction i) Nothing -> failAt gs off curPCAddr (UnsupportedInstruction i)
Just transformer -> do Just transformer -> do
-- Once we have the semantics for the instruction (represented by a -- Once we have the semantics for the instruction (represented by a
-- state transformer), we apply the state transformer and then extract -- state transformer), we apply the state transformer and then extract
-- a result from the state of the 'Generator'. -- a result from the state of the 'Generator'.
egs1 <- liftST $ ET.runExceptT (runGenerator unfinishedBlock gs $ do egs1 <- liftST $ ET.runExceptT (SG.runGenerator SG.unfinishedBlock gs $ do
let lineStr = printf "%s: %s" (show curPCAddr) (show (case i of let lineStr = printf "%s: %s" (show curPCAddr) (show (case i of
A32I i' -> ARMD.ppInstruction i' A32I i' -> ARMD.ppInstruction i'
T32I i' -> ThumbD.ppInstruction i')) T32I i' -> ThumbD.ppInstruction i'))
addStmt (InstructionStart blockOff (T.pack lineStr)) SG.addStmt (MC.InstructionStart blockOff (T.pack lineStr))
addStmt (Comment (T.pack lineStr)) SG.addStmt (MC.Comment (T.pack lineStr))
setRegVal branchTaken (CValue (BoolCValue False)) SG.setRegVal AR.branchTaken (MC.CValue (MC.BoolCValue False))
asAtomicStateUpdate (MM.segoffAddr curPCAddr) transformer) SG.asAtomicStateUpdate (MM.segoffAddr curPCAddr) transformer)
case egs1 of case egs1 of
Left genErr -> failAt gs off curPCAddr (GenerationError i genErr) Left genErr -> failAt gs off curPCAddr (GenerationError i genErr)
Right gs1 -> do Right gs1 -> do
case gs1 of case gs1 of
UnfinishedPartialBlock preBlock -> SG.UnfinishedPartialBlock preBlock ->
if | CValue (BoolCValue False) <- preBlock ^. (pBlockState . boundValue branchTakenReg) if | MC.CValue (MC.BoolCValue False) <- preBlock ^. (SG.pBlockState . MC.boundValue AR.branchTakenReg)
, Just nextPCSegAddr <- MM.incSegmentOff curPCAddr (fromIntegral bytesRead) -> do , Just nextPCSegAddr <- MM.incSegmentOff curPCAddr (fromIntegral bytesRead) -> do
-- If the branch taken flag is anything besides a -- If the branch taken flag is anything besides a
-- concrete False value, then we are at the end of a -- concrete False value, then we are at the end of a
-- block. -- block.
let preBlock' = (pBlockState . curIP .~ nextPCVal) preBlock let preBlock' = (SG.pBlockState . MC.curIP .~ nextPCVal) preBlock
let gs2 = GenState { assignIdGen = assignIdGen gs let gs2 = SG.GenState { SG.assignIdGen = SG.assignIdGen gs
, _blockState = preBlock' , SG._blockState = preBlock'
, genAddr = nextPCSegAddr , SG.genAddr = nextPCSegAddr
, genRegUpdates = MapF.empty , SG.genRegUpdates = MapF.empty
, _blockStateSnapshot = preBlock' ^. pBlockState , SG._blockStateSnapshot = preBlock' ^. SG.pBlockState
, appCache = appCache gs , SG.appCache = SG.appCache gs
} }
disassembleBlock lookupSemantics gs2 nextPCSegAddr (blockOff + fromIntegral bytesRead) maxOffset disassembleBlock lookupSemantics gs2 nextPCSegAddr (blockOff + fromIntegral bytesRead) maxOffset
-- Otherwise, we are still at the end of a block. -- Otherwise, we are still at the end of a block.
| otherwise -> return (nextPCOffset, finishBlock' preBlock FetchAndExecute) | otherwise -> return (nextPCOffset, SG.finishBlock' preBlock MCB.FetchAndExecute)
FinishedPartialBlock b -> return (nextPCOffset, b) SG.FinishedPartialBlock b -> return (nextPCOffset, b)
-- | Read one instruction from the 'MM.Memory' at the given segmented offset. -- | Read one instruction from the 'MM.Memory' at the given segmented offset.
-- --
@ -268,7 +267,7 @@ readInstruction addr = do
-- bytestrings, at the cost of possibly making it less efficient for -- bytestrings, at the cost of possibly making it less efficient for
-- other clients. -- other clients.
let (bytesRead, minsn) = let (bytesRead, minsn) =
if segoffOffset addr .&. 1 == 0 if MC.segoffOffset addr .&. 1 == 0
then fmap (fmap A32I) $ ARMD.disassembleInstruction (LBS.fromStrict bs) then fmap (fmap A32I) $ ARMD.disassembleInstruction (LBS.fromStrict bs)
else fmap (fmap T32I) $ ThumbD.disassembleInstruction (LBS.fromStrict bs) else fmap (fmap T32I) $ ThumbD.disassembleInstruction (LBS.fromStrict bs)
case minsn of case minsn of
@ -289,16 +288,17 @@ data ARMMemoryError w = ARMInvalidInstruction !(MM.MemAddr w) [MM.MemChunk w]
| ARMInvalidInstructionAddress !(MM.MemSegment w) !(MM.MemWord w) | ARMInvalidInstructionAddress !(MM.MemSegment w) !(MM.MemWord w)
deriving (Show) deriving (Show)
type LocatedError ppc ids = (Block ppc ids type LocatedError ids = ( MCB.Block ARM.AArch32 ids
, Int , Int
, TranslationError (ArchAddrWidth ppc)) , TranslationError 32
)
-- | This is a monad for error handling during disassembly -- | This is a monad for error handling during disassembly
-- --
-- It allows for early failure that reports progress (in the form of blocks -- It allows for early failure that reports progress (in the form of blocks
-- discovered and the latest address examined) along with a reason for failure -- discovered and the latest address examined) along with a reason for failure
-- (a 'TranslationError'). -- (a 'TranslationError').
newtype DisM ppc ids s a = DisM { unDisM :: ET.ExceptT (LocatedError ppc ids) (ST s) a } newtype DisM ids s a = DisM { unDisM :: ET.ExceptT (LocatedError ids) (ST s) a }
deriving (Functor, Applicative, Monad) deriving (Functor, Applicative, Monad)
-- | This funny instance is required because GHC doesn't allow type function -- | This funny instance is required because GHC doesn't allow type function
@ -309,7 +309,7 @@ newtype DisM ppc ids s a = DisM { unDisM :: ET.ExceptT (LocatedError ppc ids) (S
-- --
-- We also can't derive this instance because of that restriction (but deriving -- We also can't derive this instance because of that restriction (but deriving
-- silently fails). -- silently fails).
instance (w ~ ArchAddrWidth ppc) => ET.MonadError (Block ppc ids, Int, TranslationError w) (DisM ppc ids s) where instance ET.MonadError (MCB.Block ARM.AArch32 ids, Int, TranslationError 32) (DisM ids s) where
throwError e = DisM (ET.throwError e) throwError e = DisM (ET.throwError e)
catchError a hdlr = do catchError a hdlr = do
r <- liftST $ ET.runExceptT (unDisM a) r <- liftST $ ET.runExceptT (unDisM a)
@ -330,12 +330,12 @@ data TranslationErrorReason w = InvalidNextPC (MM.MemAddr w) (MM.MemAddr w)
| DecodeError (ARMMemoryError w) | DecodeError (ARMMemoryError w)
| UnsupportedInstruction InstructionSet | UnsupportedInstruction InstructionSet
| InstructionAtUnmappedAddr InstructionSet | InstructionAtUnmappedAddr InstructionSet
| GenerationError InstructionSet GeneratorError | GenerationError InstructionSet SG.GeneratorError
deriving (Show) deriving (Show)
deriving instance (MM.MemWidth w) => Show (TranslationError w) deriving instance (MM.MemWidth w) => Show (TranslationError w)
liftST :: ST s a -> DisM arm ids s a liftST :: ST s a -> DisM ids s a
liftST = DisM . lift liftST = DisM . lift
@ -346,17 +346,16 @@ liftST = DisM . lift
-- that translation of the basic block resulted in an error (with the exception -- that translation of the basic block resulted in an error (with the exception
-- string stored as its argument). This allows macaw to carry errors in the -- string stored as its argument). This allows macaw to carry errors in the
-- instruction stream, which is useful for debugging and diagnostics. -- instruction stream, which is useful for debugging and diagnostics.
failAt :: forall arm ids s a failAt :: forall ids s a
. (ArchReg arm ~ ARMReg, MM.MemWidth (ArchAddrWidth arm)) . SG.GenState ARM.AArch32 ids s
=> GenState arm ids s -> MM.MemWord 32
-> MM.MemWord (ArchAddrWidth arm) -> MM.MemSegmentOff 32
-> MM.MemSegmentOff (ArchAddrWidth arm) -> TranslationErrorReason 32
-> TranslationErrorReason (ArchAddrWidth arm) -> DisM ids s a
-> DisM arm ids s a
failAt gs offset curPCAddr reason = do failAt gs offset curPCAddr reason = do
let exn = TranslationError { transErrorAddr = curPCAddr let exn = TranslationError { transErrorAddr = curPCAddr
, transErrorReason = reason , transErrorReason = reason
} }
let term = (`TranslateError` T.pack (show exn)) let term = (`MCB.TranslateError` T.pack (show exn))
let b = finishBlock' (gs ^. blockState) term let b = SG.finishBlock' (gs ^. SG.blockState) term
ET.throwError (b, fromIntegral offset, exn) ET.throwError (b, fromIntegral offset, exn)

101
macaw-aarch32/src/Data/Macaw/ARM/Eval.hs
View File

@ -20,11 +20,11 @@ module Data.Macaw.ARM.Eval
where where
import Control.Lens ( (&), (^.), (.~) ) import Control.Lens ( (&), (^.), (.~) )
import Data.Macaw.ARM.ARMReg import qualified Data.Macaw.ARM.ARMReg as AR
import Data.Macaw.ARM.Arch import qualified Data.Macaw.ARM.Arch as AA
import Data.Macaw.AbsDomain.AbsState as MA import qualified Data.Macaw.AbsDomain.AbsState as MA
import qualified Data.Macaw.Architecture.Info as MI import qualified Data.Macaw.Architecture.Info as MI
import Data.Macaw.CFG import qualified Data.Macaw.CFG as MC
import qualified Data.Macaw.AbsDomain.JumpBounds as MJ import qualified Data.Macaw.AbsDomain.JumpBounds as MJ
import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.Memory as MM
import qualified Data.Macaw.SemMC.Generator as MSG import qualified Data.Macaw.SemMC.Generator as MSG
@ -33,15 +33,14 @@ import Data.Parameterized.NatRepr (knownNat)
import Data.Parameterized.Some ( Some(..) ) import Data.Parameterized.Some ( Some(..) )
import qualified Data.Parameterized.Map as MapF import qualified Data.Parameterized.Map as MapF
import qualified Data.Set as Set import qualified Data.Set as Set
import GHC.TypeLits
import qualified Language.ASL.Globals as ASL import qualified Language.ASL.Globals as ASL
import qualified SemMC.Architecture.AArch32 as ARM import qualified SemMC.Architecture.AArch32 as ARM
import Data.Macaw.ARM.Simplify () import Data.Macaw.ARM.Simplify ()
callParams :: (forall tp . ARMReg tp -> Bool) callParams :: (forall tp . AR.ARMReg tp -> Bool)
-> MA.CallParams ARMReg -> MA.CallParams AR.ARMReg
callParams preservePred = callParams preservePred =
MA.CallParams { MA.postCallStackDelta = 0 MA.CallParams { MA.postCallStackDelta = 0
, MA.preserveReg = preservePred , MA.preserveReg = preservePred
@ -50,33 +49,33 @@ callParams preservePred =
-- FIXME: initialize some of the globals to FALSE -- FIXME: initialize some of the globals to FALSE
initialBlockRegs :: forall ids . initialBlockRegs :: forall ids .
ArchSegmentOff ARM.AArch32 MC.ArchSegmentOff ARM.AArch32
-- ^ The address of the block -- ^ The address of the block
-> ArchBlockPrecond ARM.AArch32 -> MC.ArchBlockPrecond ARM.AArch32
-> RegState (ArchReg ARM.AArch32) (Value ARM.AArch32 ids) -> MC.RegState (MC.ArchReg ARM.AArch32) (MC.Value ARM.AArch32 ids)
initialBlockRegs addr _preconds = MSG.initRegState addr & initialBlockRegs addr _preconds = MSG.initRegState addr &
-- FIXME: Set all simple globals to 0?? -- FIXME: Set all simple globals to 0??
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ MC.BoolValue False &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__UnpredictableBehavior")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__UnpredictableBehavior")) .~ MC.BoolValue False &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__UndefinedBehavior")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__UndefinedBehavior")) .~ MC.BoolValue False &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__AssertionFailure")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__AssertionFailure")) .~ MC.BoolValue False &
-- FIXME: PSTATE_T is 0 for ARM mode, 1 for Thumb mode. For now, we -- FIXME: PSTATE_T is 0 for ARM mode, 1 for Thumb mode. For now, we
-- are setting this concretely to 0 at the start of a block, but -- are setting this concretely to 0 at the start of a block, but
-- once we get Thumb support, we will want to refer to the semantics -- once we get Thumb support, we will want to refer to the semantics
-- for this. -- for this.
boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ BVValue knownNat 0 & MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ MC.BVValue knownNat 0 &
boundValue ARMWriteMode .~ BVValue knownNat 0 & MC.boundValue AR.ARMWriteMode .~ MC.BVValue knownNat 0 &
boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_IT")) .~ BVValue knownNat 0 & MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_IT")) .~ MC.BVValue knownNat 0 &
boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ BVValue knownNat 0 & MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ MC.BVValue knownNat 0 &
boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_nRW")) .~ BVValue knownNat 1 & MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_nRW")) .~ MC.BVValue knownNat 1 &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__PendingInterrupt")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__PendingInterrupt")) .~ MC.BoolValue False &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__PendingPhysicalSError")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__PendingPhysicalSError")) .~ MC.BoolValue False &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__Sleeping")) .~ BoolValue False & MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__Sleeping")) .~ MC.BoolValue False &
boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ BoolValue False MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ MC.BoolValue False
extractBlockPrecond :: ArchSegmentOff ARM.AArch32 extractBlockPrecond :: MC.ArchSegmentOff ARM.AArch32
-> MA.AbsBlockState (ArchReg ARM.AArch32) -> MA.AbsBlockState (MC.ArchReg ARM.AArch32)
-> Either String (MI.ArchBlockPrecond ARM.AArch32) -> Either String (MI.ArchBlockPrecond ARM.AArch32)
extractBlockPrecond _ _ = Right () extractBlockPrecond _ _ = Right ()
@ -89,53 +88,53 @@ extractBlockPrecond _ _ = Right ()
-- Note that we don't initialize the abstract stack. On ARM, there are no -- Note that we don't initialize the abstract stack. On ARM, there are no
-- initial stack entries (since the return address is in the link register). -- initial stack entries (since the return address is in the link register).
-- --
mkInitialAbsState :: MM.Memory (RegAddrWidth (ArchReg ARM.AArch32)) mkInitialAbsState :: MM.Memory 32
-> ArchSegmentOff ARM.AArch32 -> MC.ArchSegmentOff ARM.AArch32
-> MA.AbsBlockState (ArchReg ARM.AArch32) -> MA.AbsBlockState (MC.ArchReg ARM.AArch32)
mkInitialAbsState _mem startAddr = mkInitialAbsState _mem startAddr =
s0 & MA.absRegState . boundValue arm_LR .~ MA.ReturnAddr s0 & MA.absRegState . MC.boundValue AR.arm_LR .~ MA.ReturnAddr
-- FIXME: Initialize every single global to macaw's "Initial" value -- FIXME: Initialize every single global to macaw's "Initial" value
where initRegVals = MapF.fromList [] where initRegVals = MapF.fromList []
s0 = MA.fnStartAbsBlockState startAddr initRegVals [] s0 = MA.fnStartAbsBlockState startAddr initRegVals []
absEvalArchFn :: AbsProcessorState (ArchReg ARM.AArch32) ids absEvalArchFn :: MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
-> ArchFn ARM.AArch32 (Value ARM.AArch32 ids) tp -> MC.ArchFn ARM.AArch32 (MC.Value ARM.AArch32 ids) tp
-> AbsValue (RegAddrWidth (ArchReg ARM.AArch32)) tp -> MA.AbsValue 32 tp
absEvalArchFn _r f = absEvalArchFn _r f =
case f of case f of
UDiv{} -> MA.TopV AA.UDiv{} -> MA.TopV
SDiv{} -> MA.TopV AA.SDiv{} -> MA.TopV
URem{} -> MA.TopV AA.URem{} -> MA.TopV
SRem{} -> MA.TopV AA.SRem{} -> MA.TopV
-- For now, none of the architecture-specific statements have an effect on the -- For now, none of the architecture-specific statements have an effect on the
-- abstract value. -- abstract value.
absEvalArchStmt :: AbsProcessorState (ArchReg ARM.AArch32) ids absEvalArchStmt :: MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
-> ArchStmt ARM.AArch32 (Value ARM.AArch32 ids) -> MC.ArchStmt ARM.AArch32 (MC.Value ARM.AArch32 ids)
-> AbsProcessorState (ArchReg ARM.AArch32) ids -> MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
absEvalArchStmt s _ = s absEvalArchStmt s _ = s
postARMTermStmtAbsState :: (forall tp . ARMReg tp -> Bool) postARMTermStmtAbsState :: (forall tp . AR.ARMReg tp -> Bool)
-> MM.Memory (RegAddrWidth (ArchReg ARM.AArch32)) -> MM.Memory 32
-> AbsProcessorState ARMReg ids -> MA.AbsProcessorState AR.ARMReg ids
-> MJ.IntraJumpBounds ARM.AArch32 ids -> MJ.IntraJumpBounds ARM.AArch32 ids
-> RegState ARMReg (Value ARM.AArch32 ids) -> MC.RegState AR.ARMReg (MC.Value ARM.AArch32 ids)
-> ARMTermStmt ids -> AA.ARMTermStmt ids
-> Maybe (MM.MemSegmentOff (RegAddrWidth (ArchReg ARM.AArch32)), AbsBlockState ARMReg, MJ.InitJumpBounds ARM.AArch32) -> Maybe (MM.MemSegmentOff 32, MA.AbsBlockState AR.ARMReg, MJ.InitJumpBounds ARM.AArch32)
postARMTermStmtAbsState preservePred mem s0 jumpBounds regState stmt = postARMTermStmtAbsState preservePred mem s0 jumpBounds regState stmt =
case stmt of case stmt of
ARMSyscall _ -> AA.ARMSyscall _ ->
case simplifyValue (regState ^. curIP) of case simplifyValue (regState ^. MC.curIP) of
Just (RelocatableValue _ addr) Just (MC.RelocatableValue _ addr)
| Just nextPC <- MM.asSegmentOff mem (MM.incAddr 4 addr) -> do | Just nextPC <- MM.asSegmentOff mem (MM.incAddr 4 addr) -> do
let params = MA.CallParams { MA.postCallStackDelta = 0 let params = MA.CallParams { MA.postCallStackDelta = 0
, MA.preserveReg = preservePred , MA.preserveReg = preservePred
, MA.stackGrowsDown = True , MA.stackGrowsDown = True
} }
Just (nextPC, MA.absEvalCall params s0 regState nextPC, MJ.postCallBounds params jumpBounds regState) Just (nextPC, MA.absEvalCall params s0 regState nextPC, MJ.postCallBounds params jumpBounds regState)
_ -> error ("Syscall could not interpret next PC: " ++ show (regState ^. curIP)) _ -> error ("Syscall could not interpret next PC: " ++ show (regState ^. MC.curIP))
-- FIXME: Check semantics for SVC. Is there a special function -- FIXME: Check semantics for SVC. Is there a special function
-- that we need to translate? -- that we need to translate?
-- ThumbSyscall _ -> -- ThumbSyscall _ ->
@ -149,6 +148,6 @@ postARMTermStmtAbsState preservePred mem s0 jumpBounds regState stmt =
-- _ -> error ("Syscall could not interpret next PC: " ++ show (regState ^. curIP)) -- _ -> error ("Syscall could not interpret next PC: " ++ show (regState ^. curIP))
preserveRegAcrossSyscall :: ArchReg ARM.AArch32 tp -> Bool preserveRegAcrossSyscall :: MC.ArchReg ARM.AArch32 tp -> Bool
preserveRegAcrossSyscall r = preserveRegAcrossSyscall r =
Some r `Set.member` linuxSystemCallPreservedRegisters Some r `Set.member` AR.linuxSystemCallPreservedRegisters

39
macaw-aarch32/src/Data/Macaw/ARM/Identify.hs
View File

@ -12,24 +12,12 @@ module Data.Macaw.ARM.Identify
) where ) where
import Control.Lens ( (^.) ) import Control.Lens ( (^.) )
import Control.Monad ( guard )
import qualified Data.Macaw.ARM.ARMReg as AR import qualified Data.Macaw.ARM.ARMReg as AR
import Data.Macaw.AbsDomain.AbsState ( AbsProcessorState import qualified Data.Macaw.AbsDomain.AbsState as MA
, AbsValue(..)
, transferValue
, ppAbsValue
, absAssignments
, AbsBlockStack
)
import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.CFG as MC
import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.Memory as MM
import qualified Data.Macaw.SemMC.Simplify as MSS import qualified Data.Macaw.SemMC.Simplify as MSS
import qualified Data.Macaw.Types as MT import qualified Data.Macaw.Types as MT
import Data.Parameterized.Classes
import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.NatRepr as PN
import qualified Data.Parameterized.TraversableFC as FC
import Data.Semigroup
import qualified Data.Sequence as Seq import qualified Data.Sequence as Seq
import qualified SemMC.Architecture.AArch32 as ARM import qualified SemMC.Architecture.AArch32 as ARM
@ -38,13 +26,6 @@ import Data.Macaw.ARM.Simplify ()
import Prelude import Prelude
import qualified Language.ASL.Globals as ASL
debug :: Show a => a -> b -> b
-- debug = trace
debug = flip const
-- | Identifies a call statement, *after* the corresponding statement -- | Identifies a call statement, *after* the corresponding statement
-- has been performed. This can be tricky with ARM because there are -- has been performed. This can be tricky with ARM because there are
-- several instructions that can update R15 and effect a "call", -- several instructions that can update R15 and effect a "call",
@ -75,7 +56,7 @@ identifyCall mem stmts0 rs
-- addresses. -- addresses.
identifyReturn :: Seq.Seq (MC.Stmt ARM.AArch32 ids) identifyReturn :: Seq.Seq (MC.Stmt ARM.AArch32 ids)
-> MC.RegState (MC.ArchReg ARM.AArch32) (MC.Value ARM.AArch32 ids) -> MC.RegState (MC.ArchReg ARM.AArch32) (MC.Value ARM.AArch32 ids)
-> AbsProcessorState (MC.ArchReg ARM.AArch32) ids -> MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
-> Maybe (Seq.Seq (MC.Stmt ARM.AArch32 ids)) -> Maybe (Seq.Seq (MC.Stmt ARM.AArch32 ids))
identifyReturn stmts s finalRegSt8 = identifyReturn stmts s finalRegSt8 =
if isReturnValue finalRegSt8 (s^.MC.boundValue MC.ip_reg) if isReturnValue finalRegSt8 (s^.MC.boundValue MC.ip_reg)
@ -86,18 +67,10 @@ identifyReturn stmts s finalRegSt8 =
-- from Macaw, modulo any ARM semantics operations (lots of ite caused -- from Macaw, modulo any ARM semantics operations (lots of ite caused
-- by the conditional execution bits for most instructions, clearing -- by the conditional execution bits for most instructions, clearing
-- of the low bits (1 in T32 mode, 2 in A32 mode). -- of the low bits (1 in T32 mode, 2 in A32 mode).
isReturnValue :: AbsProcessorState (MC.ArchReg ARM.AArch32) ids isReturnValue :: MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids
-> MC.Value ARM.AArch32 ids (MT.BVType (MC.RegAddrWidth (MC.ArchReg ARM.AArch32))) -> MC.Value ARM.AArch32 ids (MT.BVType (MC.RegAddrWidth (MC.ArchReg ARM.AArch32)))
-> Bool -> Bool
isReturnValue absProcState val = isReturnValue absProcState val =
case transferValue absProcState val of case MA.transferValue absProcState val of
ReturnAddr -> True MA.ReturnAddr -> True
-- TBD: fill in the code here to recognize the expression that _ -> False
-- clears the lower bit(s), along the lines of what is done by PPC
-- Identify.hs for the shifting operations.
o -> debug ("######################## Unrecognized return value: " <>
show (MC.ppValue 0 val) <>
" or " <>
show (ppAbsValue o)
) False

116
macaw-aarch32/src/Data/Macaw/ARM/Operand.hs
View File

@ -1,116 +0,0 @@
-- | Instance definitions to assist in extracting Macaw values from instruction operands
--
-- This module is full of orphans, as the definitions of the classes are in a
-- package that cannot depend on the architecture-specific backends.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Macaw.ARM.Operand
(
)
where
import Control.Lens ( (^. ) )
import qualified Data.Macaw.ARM.ARMReg as Reg
import qualified Data.Macaw.CFG.Core as MC
import Data.Macaw.SemMC.Operands
import Data.Macaw.Types ( BVType )
import qualified Data.Parameterized.NatRepr as NR
import Data.Word ( Word16, Word8 )
import qualified Dismantle.ARM.A32 as A32Operand
import qualified Dismantle.ARM.T32 as T32Operand
import qualified SemMC.Architecture.AArch32 as ARM
-- instance ExtractValue ARM.AArch32 A32Operand.GPR (BVType 32) where
-- extractValue regs r = regs ^. MC.boundValue (Reg.ARM_GP $ fromIntegral $ A32Operand.unGPR r)
-- instance ToRegister A32Operand.GPR Reg.ARMReg (BVType 32) where
-- toRegister = Reg.ARM_GP . fromIntegral . A32Operand.unGPR
-- instance ExtractValue ARM.AArch32 (Maybe A32Operand.GPR) (BVType 32) where
-- extractValue regs mgpr =
-- case mgpr of
-- Just r -> extractValue regs r
-- Nothing -> MC.BVValue NR.knownNat 0
-- instance ExtractValue ARM.AArch32 A32Operand.Pred (BVType 4) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.predToBits
-- instance ExtractValue ARM.AArch32 A32Operand.SBit (BVType 1) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.sBitToBits
-- instance ExtractValue ARM.AArch32 A32Operand.Imm5 (BVType 5) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.imm5ToBits
-- instance ExtractValue ARM.AArch32 A32Operand.BranchTarget (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.branchTargetToBits
-- instance ExtractValue ARM.AArch32 A32Operand.BranchExecuteTarget (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.branchExecuteTargetToBits
-- instance ExtractValue ARM.AArch32 A32Operand.SoRegImm (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.soRegImmToBits
-- instance ExtractValue ARM.AArch32 A32Operand.SoRegReg (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.soRegRegToBits
-- instance ExtractValue ARM.AArch32 A32Operand.LdstSoReg (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . A32Operand.ldstSoRegToBits
-- instance ExtractValue arch Word16 (BVType 16) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger
-- instance ExtractValue ARM.AArch32 Word8 (BVType 8) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger
-- -- instance ExtractValue arch AddrModeImm12 (BVType 12) where
-- -- extractValue i = return $ MC.BVValue NR.knownNat (toInteger $ addrModeImm12ToBits i)
-- -- ----------------------------------------------------------------------
-- instance ExtractValue ARM.AArch32 T32Operand.GPR (BVType 32) where
-- extractValue regs r = regs ^. MC.boundValue (Reg.ARM_GP $ fromIntegral $ T32Operand.unGPR r)
-- instance ToRegister T32Operand.GPR Reg.ARMReg (BVType 32) where
-- toRegister = Reg.ARM_GP . fromIntegral . T32Operand.unGPR
-- instance ExtractValue ARM.AArch32 (Maybe T32Operand.GPR) (BVType 32) where
-- extractValue regs mgpr =
-- case mgpr of
-- Just r -> extractValue regs r
-- Nothing -> MC.BVValue NR.knownNat 0
-- instance ExtractValue ARM.AArch32 T32Operand.Opcode (BVType 3) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . T32Operand.opcodeToBits
-- instance ExtractValue ARM.AArch32 T32Operand.Reglist (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . T32Operand.regListToBits
-- instance ExtractValue ARM.AArch32 T32Operand.TImm01020S4 (BVType 8) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . T32Operand.tImm01020S4ToBits
-- instance ExtractValue ARM.AArch32 T32Operand.AddrModeIs4 (BVType 32) where
-- extractValue _ = MC.BVValue NR.knownNat . toInteger . T32Operand.addrModeIs4ToBits
-- instance ExtractValue ARM.AArch32 T32Operand.LowGPR (BVType 32) where
-- extractValue regs r = regs ^. MC.boundValue (Reg.ARM_GP $ fromIntegral $ T32Operand.unLowGPR r)
-- instance ToRegister T32Operand.LowGPR Reg.ARMReg (BVType 32) where
-- toRegister = Reg.ARM_GP . fromIntegral . T32Operand.unLowGPR
-- instance ExtractValue ARM.AArch32 (Maybe T32Operand.LowGPR) (BVType 32) where
-- extractValue regs mgpr =
-- case mgpr of
-- Just r -> extractValue regs r
-- Nothing -> MC.BVValue NR.knownNat 0

2
macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
View File

@ -38,7 +38,7 @@ execInstruction =
aconv :: (Some (Opcode Operand), BS.ByteString) -> (Some (ARMSem.ARMOpcode ARMSem.ARMOperand), BS.ByteString) aconv :: (Some (Opcode Operand), BS.ByteString) -> (Some (ARMSem.ARMOpcode ARMSem.ARMOperand), BS.ByteString)
aconv (o,b) = (mapSome ARMSem.A32Opcode o, b) aconv (o,b) = (mapSome ARMSem.A32Opcode o, b)
genExecInstruction (Proxy @ARMSem.AArch32) genExecInstruction (Proxy @ARMSem.AArch32)
(locToRegTH (Proxy @ARMSem.AArch32)) locToRegTH
armNonceAppEval armNonceAppEval
(armAppEvaluator MC.LittleEndian) (armAppEvaluator MC.LittleEndian)
'a32InstructionMatcher 'a32InstructionMatcher

2
macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
View File

@ -285,7 +285,7 @@ translateExpr :: M.Endianness
translateExpr endianness interps e = case e of translateExpr endianness interps e = case e of
WB.AppExpr app -> appToExprTH endianness (WB.appExprApp app) interps WB.AppExpr app -> appToExprTH endianness (WB.appExprApp app) interps
WB.BoundVarExpr bvar -> do WB.BoundVarExpr bvar -> do
val <- evalBoundVar endianness interps bvar val <- evalBoundVar interps bvar
liftQ [| G.ValueExpr <$> $(return val) |] liftQ [| G.ValueExpr <$> $(return val) |]
WB.NonceAppExpr n -> do WB.NonceAppExpr n -> do
val <- evalNonceAppTH endianness interps (WB.nonceExprApp n) val <- evalNonceAppTH endianness interps (WB.nonceExprApp n)

1
macaw-ppc/src/Data/Macaw/PPC/Eval.hs
View File

@ -18,7 +18,6 @@ module Data.Macaw.PPC.Eval (
preserveRegAcrossSyscall preserveRegAcrossSyscall
) where ) where
import Data.Proxy
import GHC.TypeLits import GHC.TypeLits
import Control.Lens ( (&), (.~), (^.) ) import Control.Lens ( (&), (.~), (^.) )

27
macaw-semmc/src/Data/Macaw/SemMC/TH.hs
View File

@ -45,10 +45,10 @@ import Control.Monad (void)
import qualified Control.Concurrent.Async as Async import qualified Control.Concurrent.Async as Async
import qualified Data.Functor.Const as C import qualified Data.Functor.Const as C
import Data.Functor.Product import Data.Functor.Product
import qualified Data.Foldable as F import qualified Data.Foldable as F
import qualified Data.List as L import qualified Data.List as L
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Maybe ( fromMaybe )
import Data.Proxy ( Proxy(..) ) import Data.Proxy ( Proxy(..) )
import Data.Semigroup ((<>)) import Data.Semigroup ((<>))
import qualified Data.Text as T import qualified Data.Text as T
@ -176,13 +176,13 @@ libraryDefinitions ltr ena ae archType lib endianness = do
varMap :: Map.Map String Name <- Map.fromList <$> traverse fnName ffs varMap :: Map.Map String Name <- Map.fromList <$> traverse fnName ffs
-- Create lookup functions for names and calls -- Create lookup functions for names and calls
let lookupName name = Map.lookup name varMap let lookupVarName name = Map.lookup name varMap
lookupCall name = (liftQ . varE) <$> lookupName name lookupCall name = (liftQ . varE) <$> lookupVarName name
decs <- traverse (translate lookupName lookupCall) (MapF.elems lib) decs <- traverse (translate lookupVarName lookupCall) (MapF.elems lib)
return (concat decs, lookupCall) return (concat decs, lookupCall)
where where
fnName :: Some (FunctionFormula (Sym t fs)) -> Q (String, Name) fnName :: Some (FunctionFormula (Sym t fs)) -> Q (String, Name)
fnName (Some ff@(FunctionFormula { ffName = name })) = do fnName (Some (FunctionFormula { ffName = name })) = do
var <- newName ("_df_" ++ name) var <- newName ("_df_" ++ name)
return (name, var) return (name, var)
@ -190,8 +190,8 @@ libraryDefinitions ltr ena ae archType lib endianness = do
-> (String -> Maybe (MacawQ arch t fs Exp)) -> (String -> Maybe (MacawQ arch t fs Exp))
-> Some (FunctionFormula (Sym t fs)) -> Some (FunctionFormula (Sym t fs))
-> Q [Dec] -> Q [Dec]
translate lookupName lookupCall (Some ff@(FunctionFormula {})) = do translate lookupVarName lookupCall (Some ff@(FunctionFormula {})) = do
(var, sig, def) <- translateFunction ltr ena ae lookupName lookupCall archType ff endianness (_var, sig, def) <- translateFunction ltr ena ae lookupVarName lookupCall archType ff endianness
return [sig, def] return [sig, def]
-- | Generate a single case for one opcode of the case expression. -- | Generate a single case for one opcode of the case expression.
@ -641,9 +641,8 @@ translateFunction :: forall arch t fs args ret .
-> M.Endianness -> M.Endianness
-> Q (Name, Dec, Dec) -> Q (Name, Dec, Dec)
translateFunction ltr ena ae fnName df archType ff endianness = do translateFunction ltr ena ae fnName df archType ff endianness = do
let var = case fnName (ffName ff) of let funNameErr = error ("Undefined function " ++ ffName ff)
Nothing -> error $ "undefined function " ++ ffName ff let var = fromMaybe funNameErr (fnName (ffName ff))
Just var -> var
argVars :: [Name] argVars :: [Name]
<- sequence $ FC.toListFC (\bv -> newName (bvarName bv)) (ffArgVars ff) <- sequence $ FC.toListFC (\bv -> newName (bvarName bv)) (ffArgVars ff)
let argVarMap :: MapF.MapF (SI.BoundVar (Sym t fs)) (C.Const Name) let argVarMap :: MapF.MapF (SI.BoundVar (Sym t fs)) (C.Const Name)
@ -705,7 +704,7 @@ addEltTH endianness interps elt = do
translatedExpr <- appToExprTH endianness (S.appExprApp appElt) interps translatedExpr <- appToExprTH endianness (S.appExprApp appElt) interps
bindExpr elt [| G.addExpr =<< $(return translatedExpr) |] bindExpr elt [| G.addExpr =<< $(return translatedExpr) |]
S.BoundVarExpr bVar -> do S.BoundVarExpr bVar -> do
translatedBV <- evalBoundVar endianness interps bVar translatedBV <- evalBoundVar interps bVar
bindExpr elt (return translatedBV) bindExpr elt (return translatedBV)
S.NonceAppExpr n -> do S.NonceAppExpr n -> do
translatedExpr <- evalNonceAppTH endianness interps (S.nonceExprApp n) translatedExpr <- evalNonceAppTH endianness interps (S.nonceExprApp n)
@ -713,18 +712,16 @@ addEltTH endianness interps elt = do
S.SemiRingLiteral srTy val _ S.SemiRingLiteral srTy val _
| (SR.SemiRingBVRepr _ w) <- srTy -> | (SR.SemiRingBVRepr _ w) <- srTy ->
bindExpr elt [| genBVValue $(natReprTH w) $(lift val) |] bindExpr elt [| genBVValue $(natReprTH w) $(lift val) |]
-- bindExpr elt [| return (M.BVValue $(natReprTH w) $(lift val)) |]
| otherwise -> liftQ [| error "SemiRingLiteral Elts are not supported" |] | otherwise -> liftQ [| error "SemiRingLiteral Elts are not supported" |]
S.StringExpr {} -> liftQ [| error "StringExpr elts are not supported" |] S.StringExpr {} -> liftQ [| error "StringExpr elts are not supported" |]
S.BoolExpr b _loc -> bindExpr elt [| return (M.BoolValue $(lift b)) |] S.BoolExpr b _loc -> bindExpr elt [| return (M.BoolValue $(lift b)) |]
evalBoundVar :: forall arch t fs ctp . evalBoundVar :: forall arch t fs ctp .
(A.Architecture arch) (A.Architecture arch)
=> M.Endianness => BoundVarInterpretations arch t fs
-> BoundVarInterpretations arch t fs
-> S.ExprBoundVar t ctp -> S.ExprBoundVar t ctp
-> MacawQ arch t fs Exp -> MacawQ arch t fs Exp
evalBoundVar endianness interps bVar = evalBoundVar interps bVar =
if | Just loc <- MapF.lookup bVar (locVars interps) -> withLocToReg $ \ltr -> do if | Just loc <- MapF.lookup bVar (locVars interps) -> withLocToReg $ \ltr -> do
liftQ [| return ($(varE (regsValName interps)) ^. M.boundValue $(ltr loc)) |] liftQ [| return ($(varE (regsValName interps)) ^. M.boundValue $(ltr loc)) |]
| Just (C.Const name) <- MapF.lookup bVar (opVars interps) -> | Just (C.Const name) <- MapF.lookup bVar (opVars interps) ->