From a824fc4051bb673f7bb595b1de01c457fc6d1b29 Mon Sep 17 00:00:00 2001 From: Tristan Ravitch Date: Tue, 14 Apr 2020 00:07:15 -0700 Subject: [PATCH] Tr/warning cleanups (#127) Warning and style cleanups in macaw-semmc and macaw-aarch32 --- macaw-aarch32/macaw-aarch32.cabal | 1 - macaw-aarch32/src/Data/Macaw/ARM.hs | 6 +- macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs | 98 ++++++--------- .../src/Data/Macaw/ARM/Disassemble.hs | 113 +++++++++-------- macaw-aarch32/src/Data/Macaw/ARM/Eval.hs | 101 ++++++++------- macaw-aarch32/src/Data/Macaw/ARM/Identify.hs | 39 +----- macaw-aarch32/src/Data/Macaw/ARM/Operand.hs | 116 ------------------ .../Data/Macaw/ARM/Semantics/ARMSemantics.hs | 2 +- .../src/Data/Macaw/ARM/Semantics/TH.hs | 2 +- macaw-ppc/src/Data/Macaw/PPC/Eval.hs | 1 - macaw-semmc/src/Data/Macaw/SemMC/TH.hs | 27 ++-- 11 files changed, 164 insertions(+), 342 deletions(-) delete mode 100644 macaw-aarch32/src/Data/Macaw/ARM/Operand.hs diff --git a/macaw-aarch32/macaw-aarch32.cabal b/macaw-aarch32/macaw-aarch32.cabal index c30c6ace..0434e46f 100644 --- a/macaw-aarch32/macaw-aarch32.cabal +++ b/macaw-aarch32/macaw-aarch32.cabal @@ -20,7 +20,6 @@ library , Data.Macaw.ARM.Disassemble , Data.Macaw.ARM.Eval , Data.Macaw.ARM.Identify - , Data.Macaw.ARM.Operand , Data.Macaw.ARM.Semantics.ARMSemantics , Data.Macaw.ARM.Semantics.ThumbSemantics , Data.Macaw.ARM.Semantics.TH diff --git a/macaw-aarch32/src/Data/Macaw/ARM.hs b/macaw-aarch32/src/Data/Macaw/ARM.hs index 43be9089..0251c552 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM.hs @@ -26,7 +26,6 @@ import Control.Lens ( (^.) ) import qualified Data.Macaw.Architecture.Info as MI import qualified Data.Macaw.CFG.DemandSet as MDS import qualified Data.Macaw.Memory as MM -import Data.Proxy ( Proxy(..) ) import qualified SemMC.Architecture.AArch32 as ARM @@ -41,7 +40,7 @@ arm_linux_info = , MI.archEndianness = MM.LittleEndian , MI.extractBlockPrecond = extractBlockPrecond , MI.initialBlockRegs = initialBlockRegs - , MI.disassembleFn = disassembleFn proxy ARMSem.execInstruction ThumbSem.execInstruction + , MI.disassembleFn = disassembleFn ARMSem.execInstruction ThumbSem.execInstruction , MI.mkInitialAbsState = mkInitialAbsState , MI.absEvalArchFn = absEvalArchFn , MI.absEvalArchStmt = absEvalArchStmt @@ -55,9 +54,6 @@ arm_linux_info = , MI.archDemandContext = archDemandContext , MI.postArchTermStmtAbsState = postARMTermStmtAbsState preserveRegAcrossSyscall } - where - proxy = Proxy @ARM.AArch32 - archDemandContext :: MDS.DemandContext ARM.AArch32 archDemandContext = diff --git a/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs b/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs index 81e8f819..0eed22c9 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs @@ -15,10 +15,8 @@ module Data.Macaw.ARM.ARMReg ( ARMReg(..) - -- , armRegToGPR , arm_LR , branchTaken - -- , ArchWidth(..) , linuxSystemCallPreservedRegisters , locToRegTH , integerToReg @@ -29,23 +27,20 @@ module Data.Macaw.ARM.ARMReg import Data.Parameterized.Classes import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.NatRepr as NR import Data.Parameterized.Some ( Some(..) ) -import Data.Parameterized.SymbolRepr (symbolRepr) -import Data.Parameterized.TraversableFC (toListFC, fmapFC) -import qualified Data.Parameterized.TH.GADT as TH +import qualified Data.Parameterized.SymbolRepr as PSR +import qualified Data.Parameterized.TraversableFC as FC +import qualified Data.Parameterized.TH.GADT as PTH import qualified Data.Set as Set import qualified Data.Text as T -import Data.Word ( Word32 ) import GHC.TypeLits -import Language.Haskell.TH -import Language.Haskell.TH.Syntax ( lift ) +import qualified Language.Haskell.TH as TH import qualified Text.PrettyPrint.ANSI.Leijen as PP import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Memory as MM -import Data.Macaw.Types as MT --- ( TypeRepr(..), HasRepr, BVType --- , typeRepr, n32 ) +import qualified Data.Macaw.Types as MT import qualified Language.ASL.Globals as ASL import qualified SemMC.Architecture.AArch32 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. +-- +-- 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 -- | 'ASL.GlobalRef' that refers to a bitvector. - ARMGlobalBV :: ( tp ~ BVType w + ARMGlobalBV :: ( tp ~ MT.BVType w , 1 <= w , tp' ~ ASL.GlobalsType s , tp ~ BaseToMacawType tp') => ASL.GlobalRef s -> ARMReg tp -- | 'ASL.GlobalRef' that refers to a boolean. - ARMGlobalBool :: ( tp ~ BoolType + ARMGlobalBool :: ( tp ~ MT.BoolType , tp' ~ ASL.GlobalsType s , tp ~ BaseToMacawType 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 -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") -branchTaken :: ARMReg BoolType +branchTaken :: ARMReg MT.BoolType branchTaken = ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken") instance Show (ARMReg tp) where @@ -98,9 +97,9 @@ instance MC.PrettyF ARMReg where $(return []) -- allow template haskell below to see definitions above instance TestEquality ARMReg where - testEquality = $(TH.structuralTypeEquality [t| ARMReg |] - [ (TH.ConType [t|ASL.GlobalRef|] - `TH.TypeApp` TH.AnyType, + testEquality = $(PTH.structuralTypeEquality [t| ARMReg |] + [ (PTH.ConType [t|ASL.GlobalRef|] + `PTH.TypeApp` PTH.AnyType, [|testEquality|]) ]) @@ -111,9 +110,9 @@ instance Eq (ARMReg tp) where r1 == r2 = r1 `eqF` r2 instance OrdF ARMReg where - compareF = $(TH.structuralTypeOrd [t| ARMReg |] - [ (TH.ConType [t|ASL.GlobalRef|] - `TH.TypeApp` TH.AnyType, + compareF = $(PTH.structuralTypeOrd [t| ARMReg |] + [ (PTH.ConType [t|ASL.GlobalRef|] + `PTH.TypeApp` PTH.AnyType, [|compareF|]) ]) @@ -121,11 +120,12 @@ instance Ord (ARMReg tp) where r1 `compare` r2 = toOrdering (r1 `compareF` r2) -instance HasRepr ARMReg TypeRepr where +instance MT.HasRepr ARMReg MT.TypeRepr where typeRepr r = case r of ARMGlobalBV 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.RegAddrWidth ARMReg = 32 @@ -134,7 +134,6 @@ instance ( 1 <= MC.RegAddrWidth ARMReg , KnownNat (MC.RegAddrWidth ARMReg) , MM.MemWidth (MC.RegAddrWidth (MC.ArchReg SA.AArch32)) , MC.ArchReg SA.AArch32 ~ ARMReg - -- , ArchWidth arm ) => MC.RegisterInfo ARMReg where archRegs = armRegs @@ -144,37 +143,15 @@ instance ( 1 <= MC.RegAddrWidth ARMReg syscallArgumentRegs = error "TODO: MC.RegisterInfo ARMReg syscallArgumentsRegs undefined" armRegs :: forall w. (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => [Some ARMReg] -armRegs = toListFC asARMReg ( fmapFC ASL.SimpleGlobalRef ASL.simpleGlobalRefs Ctx.<++> - ASL.gprGlobalRefsSym Ctx.<++> - ASL.simdGlobalRefsSym - ) +armRegs = FC.toListFC asARMReg ( FC.fmapFC ASL.SimpleGlobalRef ASL.simpleGlobalRefs Ctx.<++> + ASL.gprGlobalRefsSym Ctx.<++> + ASL.simdGlobalRefsSym + ) where asARMReg :: ASL.GlobalRef s -> Some ARMReg asARMReg gr = case ASL.globalRefRepr gr of WT.BaseBoolRepr -> Some (ARMGlobalBool gr) WT.BaseBVRepr _ -> Some (ARMGlobalBV gr) 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. -- @@ -199,22 +176,21 @@ linuxSystemCallPreservedRegisters = -- | Translate a location from the semmc semantics into a location suitable for -- use in macaw -locToRegTH :: proxy arm - -> SA.Location arm ctp - -> Q Exp -locToRegTH _ (SA.Location globalRef) = do - let refName = T.unpack (symbolRepr (ASL.globalRefSymbol globalRef)) +locToRegTH :: SA.Location SA.AArch32 ctp + -> TH.Q TH.Exp +locToRegTH (SA.Location globalRef) = do + let refName = T.unpack (PSR.symbolRepr (ASL.globalRefSymbol globalRef)) case ASL.globalRefRepr globalRef of WT.BaseBoolRepr -> - [| ARMGlobalBool (ASL.knownGlobalRef :: ASL.GlobalRef $(return (LitT (StrTyLit refName)))) |] + [| ARMGlobalBool (ASL.knownGlobalRef :: ASL.GlobalRef $(return (TH.LitT (TH.StrTyLit refName)))) |] WT.BaseBVRepr _ -> - [| ARMGlobalBV (ASL.knownGlobalRef :: ASL.GlobalRef $(return (LitT (StrTyLit refName)))) |] - tp -> [| error $ "locToRegTH undefined for unrecognized location: " <> $(return $ LitE (StringL refName)) |] + [| ARMGlobalBV (ASL.knownGlobalRef :: ASL.GlobalRef $(return (TH.LitT (TH.StrTyLit 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") -integerToReg :: Integer -> Maybe (ARMReg (BVType 32)) +integerToReg :: Integer -> Maybe (ARMReg (MT.BVType 32)) integerToReg 0 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R0") integerToReg 1 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_R1") 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 _ = Nothing -integerToSIMDReg :: Integer -> Maybe (ARMReg (BVType 128)) +integerToSIMDReg :: Integer -> Maybe (ARMReg (MT.BVType 128)) integerToSIMDReg 0 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V0") integerToSIMDReg 1 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V1") integerToSIMDReg 2 = Just $ ARMGlobalBV (ASL.knownGlobalRef @"_V2") diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Disassemble.hs b/macaw-aarch32/src/Data/Macaw/ARM/Disassemble.hs index a85f8460..a8d3aa59 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Disassemble.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Disassemble.hs @@ -74,16 +74,16 @@ import Control.Monad.Trans ( lift ) import Data.Bits import qualified Data.ByteString as BS 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.CFG -import Data.Macaw.CFG.Block -import qualified Data.Macaw.CFG.Core as MC +import qualified Data.Macaw.CFG as MC +import qualified Data.Macaw.CFG.Block as MCB import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.Memory.Permissions as MMP -import Data.Macaw.SemMC.Generator -import Data.Macaw.Types +import qualified Data.Macaw.SemMC.Generator as SG +import qualified Data.Macaw.Types as MT import qualified Data.Parameterized.Map as MapF +import qualified Data.Parameterized.NatRepr as PN import qualified Data.Parameterized.Nonce as NC import qualified Data.Text as T 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 -- occupied by those blocks. -disassembleFn :: proxy ARM.AArch32 - -> (Value ARM.AArch32 ids (BVType (ArchAddrWidth ARM.AArch32)) -> ARMD.Instruction -> Maybe (Generator ARM.AArch32 ids s ())) +disassembleFn :: (MC.Value ARM.AArch32 ids (MT.BVType 32) -> ARMD.Instruction -> Maybe (SG.Generator ARM.AArch32 ids s ())) -- ^ 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 -- 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 -- lookup is provided with the value of the IP in case IP-relative -- addressing is necessary. -> NC.NonceGenerator (ST s) ids -- ^ A generator of unique IDs used for assignments - -> ArchSegmentOff ARM.AArch32 + -> MC.ArchSegmentOff ARM.AArch32 -- ^ 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 -> Int -- ^ Maximum size of the block (a safeguard) - -> ST s (Block ARM.AArch32 ids, Int) -disassembleFn _ lookupA32Semantics lookupT32Semantics nonceGen startAddr regState maxSize = do + -> ST s (MCB.Block ARM.AArch32 ids, Int) +disassembleFn lookupA32Semantics lookupT32Semantics nonceGen startAddr regState maxSize = do let lookupSemantics ipval instr = case instr of A32I inst -> lookupA32Semantics ipval inst T32I inst -> lookupT32Semantics ipval inst @@ -132,14 +131,14 @@ disassembleFn _ lookupA32Semantics lookupT32Semantics nonceGen startAddr regStat Left (blocks, off, _exn) -> return (blocks, off) 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 - -> ArchSegmentOff ARM.AArch32 - -> RegState (ArchReg ARM.AArch32) (Value ARM.AArch32 ids) + -> MC.ArchSegmentOff ARM.AArch32 + -> MC.RegState AR.ARMReg (MC.Value ARM.AArch32 ids) -> 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 - let gs0 = initGenState nonceGen startAddr regState + let gs0 = SG.initGenState nonceGen startAddr regState let startOffset = MM.segoffOffset startAddr (nextPCOffset, block) <- disassembleBlock lookupSemantics gs0 startAddr 0 (startOffset + fromIntegral maxSize) 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 -- becomes a mux, we split execution using 'conditionalBranch'. 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 - -> GenState ARM.AArch32 ids s + -> SG.GenState ARM.AArch32 ids s -> MM.MemSegmentOff 32 -- ^ The current instruction pointer -> MM.MemWord 32 @@ -174,7 +173,7 @@ disassembleBlock :: forall ids s . -- ^ The maximum offset into the bytestring that we should -- disassemble to; in principle, macaw can tell us to limit our -- 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 let seg = MM.segoffSegment curPCAddr let off = MM.segoffOffset curPCAddr @@ -187,49 +186,49 @@ disassembleBlock lookupSemantics gs curPCAddr blockOff maxOffset = do -- let curPC = MM.segmentOffAddr seg off let nextPCOffset = off + bytesRead 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 -- Note: In ARM, the IP is incremented *after* an instruction -- executes; pass in the physical address of the instruction here. ipVal <- case MM.asAbsoluteAddr (MM.segoffAddr curPCAddr) of 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 Nothing -> failAt gs off curPCAddr (UnsupportedInstruction i) Just transformer -> do -- Once we have the semantics for the instruction (represented by a -- state transformer), we apply the state transformer and then extract -- 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 A32I i' -> ARMD.ppInstruction i' T32I i' -> ThumbD.ppInstruction i')) - addStmt (InstructionStart blockOff (T.pack lineStr)) - addStmt (Comment (T.pack lineStr)) - setRegVal branchTaken (CValue (BoolCValue False)) - asAtomicStateUpdate (MM.segoffAddr curPCAddr) transformer) + SG.addStmt (MC.InstructionStart blockOff (T.pack lineStr)) + SG.addStmt (MC.Comment (T.pack lineStr)) + SG.setRegVal AR.branchTaken (MC.CValue (MC.BoolCValue False)) + SG.asAtomicStateUpdate (MM.segoffAddr curPCAddr) transformer) case egs1 of Left genErr -> failAt gs off curPCAddr (GenerationError i genErr) Right gs1 -> do case gs1 of - UnfinishedPartialBlock preBlock -> - if | CValue (BoolCValue False) <- preBlock ^. (pBlockState . boundValue branchTakenReg) + SG.UnfinishedPartialBlock preBlock -> + if | MC.CValue (MC.BoolCValue False) <- preBlock ^. (SG.pBlockState . MC.boundValue AR.branchTakenReg) , Just nextPCSegAddr <- MM.incSegmentOff curPCAddr (fromIntegral bytesRead) -> do -- If the branch taken flag is anything besides a -- concrete False value, then we are at the end of a -- block. - let preBlock' = (pBlockState . curIP .~ nextPCVal) preBlock - let gs2 = GenState { assignIdGen = assignIdGen gs - , _blockState = preBlock' - , genAddr = nextPCSegAddr - , genRegUpdates = MapF.empty - , _blockStateSnapshot = preBlock' ^. pBlockState - , appCache = appCache gs - } + let preBlock' = (SG.pBlockState . MC.curIP .~ nextPCVal) preBlock + let gs2 = SG.GenState { SG.assignIdGen = SG.assignIdGen gs + , SG._blockState = preBlock' + , SG.genAddr = nextPCSegAddr + , SG.genRegUpdates = MapF.empty + , SG._blockStateSnapshot = preBlock' ^. SG.pBlockState + , SG.appCache = SG.appCache gs + } disassembleBlock lookupSemantics gs2 nextPCSegAddr (blockOff + fromIntegral bytesRead) maxOffset -- Otherwise, we are still at the end of a block. - | otherwise -> return (nextPCOffset, finishBlock' preBlock FetchAndExecute) - FinishedPartialBlock b -> return (nextPCOffset, b) + | otherwise -> return (nextPCOffset, SG.finishBlock' preBlock MCB.FetchAndExecute) + SG.FinishedPartialBlock b -> return (nextPCOffset, b) -- | 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 -- other clients. let (bytesRead, minsn) = - if segoffOffset addr .&. 1 == 0 + if MC.segoffOffset addr .&. 1 == 0 then fmap (fmap A32I) $ ARMD.disassembleInstruction (LBS.fromStrict bs) else fmap (fmap T32I) $ ThumbD.disassembleInstruction (LBS.fromStrict bs) case minsn of @@ -289,16 +288,17 @@ data ARMMemoryError w = ARMInvalidInstruction !(MM.MemAddr w) [MM.MemChunk w] | ARMInvalidInstructionAddress !(MM.MemSegment w) !(MM.MemWord w) deriving (Show) -type LocatedError ppc ids = (Block ppc ids - , Int - , TranslationError (ArchAddrWidth ppc)) +type LocatedError ids = ( MCB.Block ARM.AArch32 ids + , Int + , TranslationError 32 + ) -- | This is a monad for error handling during disassembly -- -- 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 -- (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) -- | 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 -- 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) catchError a hdlr = do r <- liftST $ ET.runExceptT (unDisM a) @@ -330,12 +330,12 @@ data TranslationErrorReason w = InvalidNextPC (MM.MemAddr w) (MM.MemAddr w) | DecodeError (ARMMemoryError w) | UnsupportedInstruction InstructionSet | InstructionAtUnmappedAddr InstructionSet - | GenerationError InstructionSet GeneratorError + | GenerationError InstructionSet SG.GeneratorError deriving (Show) 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 @@ -346,17 +346,16 @@ liftST = DisM . lift -- 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 -- instruction stream, which is useful for debugging and diagnostics. -failAt :: forall arm ids s a - . (ArchReg arm ~ ARMReg, MM.MemWidth (ArchAddrWidth arm)) - => GenState arm ids s - -> MM.MemWord (ArchAddrWidth arm) - -> MM.MemSegmentOff (ArchAddrWidth arm) - -> TranslationErrorReason (ArchAddrWidth arm) - -> DisM arm ids s a +failAt :: forall ids s a + . SG.GenState ARM.AArch32 ids s + -> MM.MemWord 32 + -> MM.MemSegmentOff 32 + -> TranslationErrorReason 32 + -> DisM ids s a failAt gs offset curPCAddr reason = do let exn = TranslationError { transErrorAddr = curPCAddr , transErrorReason = reason } - let term = (`TranslateError` T.pack (show exn)) - let b = finishBlock' (gs ^. blockState) term + let term = (`MCB.TranslateError` T.pack (show exn)) + let b = SG.finishBlock' (gs ^. SG.blockState) term ET.throwError (b, fromIntegral offset, exn) diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs b/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs index 38f7a0ec..882f9354 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs @@ -20,11 +20,11 @@ module Data.Macaw.ARM.Eval where import Control.Lens ( (&), (^.), (.~) ) -import Data.Macaw.ARM.ARMReg -import Data.Macaw.ARM.Arch -import Data.Macaw.AbsDomain.AbsState as MA +import qualified Data.Macaw.ARM.ARMReg as AR +import qualified Data.Macaw.ARM.Arch as AA +import qualified Data.Macaw.AbsDomain.AbsState as MA 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.Memory as MM import qualified Data.Macaw.SemMC.Generator as MSG @@ -33,15 +33,14 @@ import Data.Parameterized.NatRepr (knownNat) import Data.Parameterized.Some ( Some(..) ) import qualified Data.Parameterized.Map as MapF import qualified Data.Set as Set -import GHC.TypeLits import qualified Language.ASL.Globals as ASL import qualified SemMC.Architecture.AArch32 as ARM import Data.Macaw.ARM.Simplify () -callParams :: (forall tp . ARMReg tp -> Bool) - -> MA.CallParams ARMReg +callParams :: (forall tp . AR.ARMReg tp -> Bool) + -> MA.CallParams AR.ARMReg callParams preservePred = MA.CallParams { MA.postCallStackDelta = 0 , MA.preserveReg = preservePred @@ -50,33 +49,33 @@ callParams preservePred = -- FIXME: initialize some of the globals to FALSE initialBlockRegs :: forall ids . - ArchSegmentOff ARM.AArch32 + MC.ArchSegmentOff ARM.AArch32 -- ^ The address of the block - -> ArchBlockPrecond ARM.AArch32 - -> RegState (ArchReg ARM.AArch32) (Value ARM.AArch32 ids) + -> MC.ArchBlockPrecond ARM.AArch32 + -> MC.RegState (MC.ArchReg ARM.AArch32) (MC.Value ARM.AArch32 ids) initialBlockRegs addr _preconds = MSG.initRegState addr & -- FIXME: Set all simple globals to 0?? - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ BoolValue False & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__UnpredictableBehavior")) .~ BoolValue False & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__UndefinedBehavior")) .~ BoolValue False & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__AssertionFailure")) .~ BoolValue False & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ MC.BoolValue False & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__UnpredictableBehavior")) .~ MC.BoolValue False & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__UndefinedBehavior")) .~ MC.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 -- 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 -- for this. - boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ BVValue knownNat 0 & - boundValue ARMWriteMode .~ BVValue knownNat 0 & - boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_IT")) .~ BVValue knownNat 0 & - boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ BVValue knownNat 0 & - boundValue (ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_nRW")) .~ BVValue knownNat 1 & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__PendingInterrupt")) .~ BoolValue False & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__PendingPhysicalSError")) .~ BoolValue False & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__Sleeping")) .~ BoolValue False & - boundValue (ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ BoolValue False + MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ MC.BVValue knownNat 0 & + MC.boundValue AR.ARMWriteMode .~ MC.BVValue knownNat 0 & + MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_IT")) .~ MC.BVValue knownNat 0 & + MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ MC.BVValue knownNat 0 & + MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_nRW")) .~ MC.BVValue knownNat 1 & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__PendingInterrupt")) .~ MC.BoolValue False & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__PendingPhysicalSError")) .~ MC.BoolValue False & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__Sleeping")) .~ MC.BoolValue False & + MC.boundValue (AR.ARMGlobalBool (ASL.knownGlobalRef @"__BranchTaken")) .~ MC.BoolValue False -extractBlockPrecond :: ArchSegmentOff ARM.AArch32 - -> MA.AbsBlockState (ArchReg ARM.AArch32) +extractBlockPrecond :: MC.ArchSegmentOff ARM.AArch32 + -> MA.AbsBlockState (MC.ArchReg ARM.AArch32) -> Either String (MI.ArchBlockPrecond ARM.AArch32) extractBlockPrecond _ _ = Right () @@ -89,53 +88,53 @@ extractBlockPrecond _ _ = Right () -- 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). -- -mkInitialAbsState :: MM.Memory (RegAddrWidth (ArchReg ARM.AArch32)) - -> ArchSegmentOff ARM.AArch32 - -> MA.AbsBlockState (ArchReg ARM.AArch32) +mkInitialAbsState :: MM.Memory 32 + -> MC.ArchSegmentOff ARM.AArch32 + -> MA.AbsBlockState (MC.ArchReg ARM.AArch32) 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 where initRegVals = MapF.fromList [] s0 = MA.fnStartAbsBlockState startAddr initRegVals [] -absEvalArchFn :: AbsProcessorState (ArchReg ARM.AArch32) ids - -> ArchFn ARM.AArch32 (Value ARM.AArch32 ids) tp - -> AbsValue (RegAddrWidth (ArchReg ARM.AArch32)) tp +absEvalArchFn :: MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids + -> MC.ArchFn ARM.AArch32 (MC.Value ARM.AArch32 ids) tp + -> MA.AbsValue 32 tp absEvalArchFn _r f = case f of - UDiv{} -> MA.TopV - SDiv{} -> MA.TopV - URem{} -> MA.TopV - SRem{} -> MA.TopV + AA.UDiv{} -> MA.TopV + AA.SDiv{} -> MA.TopV + AA.URem{} -> MA.TopV + AA.SRem{} -> MA.TopV -- For now, none of the architecture-specific statements have an effect on the -- abstract value. -absEvalArchStmt :: AbsProcessorState (ArchReg ARM.AArch32) ids - -> ArchStmt ARM.AArch32 (Value ARM.AArch32 ids) - -> AbsProcessorState (ArchReg ARM.AArch32) ids +absEvalArchStmt :: MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids + -> MC.ArchStmt ARM.AArch32 (MC.Value ARM.AArch32 ids) + -> MA.AbsProcessorState (MC.ArchReg ARM.AArch32) ids absEvalArchStmt s _ = s -postARMTermStmtAbsState :: (forall tp . ARMReg tp -> Bool) - -> MM.Memory (RegAddrWidth (ArchReg ARM.AArch32)) - -> AbsProcessorState ARMReg ids +postARMTermStmtAbsState :: (forall tp . AR.ARMReg tp -> Bool) + -> MM.Memory 32 + -> MA.AbsProcessorState AR.ARMReg ids -> MJ.IntraJumpBounds ARM.AArch32 ids - -> RegState ARMReg (Value ARM.AArch32 ids) - -> ARMTermStmt ids - -> Maybe (MM.MemSegmentOff (RegAddrWidth (ArchReg ARM.AArch32)), AbsBlockState ARMReg, MJ.InitJumpBounds ARM.AArch32) + -> MC.RegState AR.ARMReg (MC.Value ARM.AArch32 ids) + -> AA.ARMTermStmt ids + -> Maybe (MM.MemSegmentOff 32, MA.AbsBlockState AR.ARMReg, MJ.InitJumpBounds ARM.AArch32) postARMTermStmtAbsState preservePred mem s0 jumpBounds regState stmt = case stmt of - ARMSyscall _ -> - case simplifyValue (regState ^. curIP) of - Just (RelocatableValue _ addr) + AA.ARMSyscall _ -> + case simplifyValue (regState ^. MC.curIP) of + Just (MC.RelocatableValue _ addr) | Just nextPC <- MM.asSegmentOff mem (MM.incAddr 4 addr) -> do let params = MA.CallParams { MA.postCallStackDelta = 0 , MA.preserveReg = preservePred , MA.stackGrowsDown = True } 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 -- that we need to translate? -- ThumbSyscall _ -> @@ -149,6 +148,6 @@ postARMTermStmtAbsState preservePred mem s0 jumpBounds regState stmt = -- _ -> 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 = - Some r `Set.member` linuxSystemCallPreservedRegisters + Some r `Set.member` AR.linuxSystemCallPreservedRegisters diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Identify.hs b/macaw-aarch32/src/Data/Macaw/ARM/Identify.hs index 9a8c0818..6973f7a9 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Identify.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Identify.hs @@ -12,24 +12,12 @@ module Data.Macaw.ARM.Identify ) where import Control.Lens ( (^.) ) -import Control.Monad ( guard ) import qualified Data.Macaw.ARM.ARMReg as AR -import Data.Macaw.AbsDomain.AbsState ( AbsProcessorState - , AbsValue(..) - , transferValue - , ppAbsValue - , absAssignments - , AbsBlockStack - ) +import qualified Data.Macaw.AbsDomain.AbsState as MA import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Memory as MM import qualified Data.Macaw.SemMC.Simplify as MSS 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 SemMC.Architecture.AArch32 as ARM @@ -38,13 +26,6 @@ import Data.Macaw.ARM.Simplify () 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 -- has been performed. This can be tricky with ARM because there are -- several instructions that can update R15 and effect a "call", @@ -75,7 +56,7 @@ identifyCall mem stmts0 rs -- addresses. identifyReturn :: Seq.Seq (MC.Stmt 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)) identifyReturn stmts s finalRegSt8 = 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 -- by the conditional execution bits for most instructions, clearing -- 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))) -> Bool isReturnValue absProcState val = - case transferValue absProcState val of - ReturnAddr -> True - -- TBD: fill in the code here to recognize the expression that - -- 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 - + case MA.transferValue absProcState val of + MA.ReturnAddr -> True + _ -> False diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Operand.hs b/macaw-aarch32/src/Data/Macaw/ARM/Operand.hs deleted file mode 100644 index f4cface1..00000000 --- a/macaw-aarch32/src/Data/Macaw/ARM/Operand.hs +++ /dev/null @@ -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 diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs index fce9a1aa..49eee523 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs @@ -38,7 +38,7 @@ execInstruction = aconv :: (Some (Opcode Operand), BS.ByteString) -> (Some (ARMSem.ARMOpcode ARMSem.ARMOperand), BS.ByteString) aconv (o,b) = (mapSome ARMSem.A32Opcode o, b) genExecInstruction (Proxy @ARMSem.AArch32) - (locToRegTH (Proxy @ARMSem.AArch32)) + locToRegTH armNonceAppEval (armAppEvaluator MC.LittleEndian) 'a32InstructionMatcher diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs index e1b59779..fe82c471 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs @@ -285,7 +285,7 @@ translateExpr :: M.Endianness translateExpr endianness interps e = case e of WB.AppExpr app -> appToExprTH endianness (WB.appExprApp app) interps WB.BoundVarExpr bvar -> do - val <- evalBoundVar endianness interps bvar + val <- evalBoundVar interps bvar liftQ [| G.ValueExpr <$> $(return val) |] WB.NonceAppExpr n -> do val <- evalNonceAppTH endianness interps (WB.nonceExprApp n) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs index 53b181ac..e7ebb1e5 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Eval.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Eval.hs @@ -18,7 +18,6 @@ module Data.Macaw.PPC.Eval ( preserveRegAcrossSyscall ) where -import Data.Proxy import GHC.TypeLits import Control.Lens ( (&), (.~), (^.) ) diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs index 6aee3d17..084d63ce 100644 --- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs +++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs @@ -45,10 +45,10 @@ import Control.Monad (void) import qualified Control.Concurrent.Async as Async import qualified Data.Functor.Const as C import Data.Functor.Product - import qualified Data.Foldable as F import qualified Data.List as L import qualified Data.Map as Map +import Data.Maybe ( fromMaybe ) import Data.Proxy ( Proxy(..) ) import Data.Semigroup ((<>)) 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 -- Create lookup functions for names and calls - let lookupName name = Map.lookup name varMap - lookupCall name = (liftQ . varE) <$> lookupName name - decs <- traverse (translate lookupName lookupCall) (MapF.elems lib) + let lookupVarName name = Map.lookup name varMap + lookupCall name = (liftQ . varE) <$> lookupVarName name + decs <- traverse (translate lookupVarName lookupCall) (MapF.elems lib) return (concat decs, lookupCall) where 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) return (name, var) @@ -190,8 +190,8 @@ libraryDefinitions ltr ena ae archType lib endianness = do -> (String -> Maybe (MacawQ arch t fs Exp)) -> Some (FunctionFormula (Sym t fs)) -> Q [Dec] - translate lookupName lookupCall (Some ff@(FunctionFormula {})) = do - (var, sig, def) <- translateFunction ltr ena ae lookupName lookupCall archType ff endianness + translate lookupVarName lookupCall (Some ff@(FunctionFormula {})) = do + (_var, sig, def) <- translateFunction ltr ena ae lookupVarName lookupCall archType ff endianness return [sig, def] -- | Generate a single case for one opcode of the case expression. @@ -641,9 +641,8 @@ translateFunction :: forall arch t fs args ret . -> M.Endianness -> Q (Name, Dec, Dec) translateFunction ltr ena ae fnName df archType ff endianness = do - let var = case fnName (ffName ff) of - Nothing -> error $ "undefined function " ++ ffName ff - Just var -> var + let funNameErr = error ("Undefined function " ++ ffName ff) + let var = fromMaybe funNameErr (fnName (ffName ff)) argVars :: [Name] <- sequence $ FC.toListFC (\bv -> newName (bvarName bv)) (ffArgVars ff) 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 bindExpr elt [| G.addExpr =<< $(return translatedExpr) |] S.BoundVarExpr bVar -> do - translatedBV <- evalBoundVar endianness interps bVar + translatedBV <- evalBoundVar interps bVar bindExpr elt (return translatedBV) S.NonceAppExpr n -> do translatedExpr <- evalNonceAppTH endianness interps (S.nonceExprApp n) @@ -713,18 +712,16 @@ addEltTH endianness interps elt = do S.SemiRingLiteral srTy val _ | (SR.SemiRingBVRepr _ w) <- srTy -> bindExpr elt [| genBVValue $(natReprTH w) $(lift val) |] --- bindExpr elt [| return (M.BVValue $(natReprTH w) $(lift val)) |] | otherwise -> liftQ [| error "SemiRingLiteral Elts are not supported" |] S.StringExpr {} -> liftQ [| error "StringExpr elts are not supported" |] S.BoolExpr b _loc -> bindExpr elt [| return (M.BoolValue $(lift b)) |] evalBoundVar :: forall arch t fs ctp . (A.Architecture arch) - => M.Endianness - -> BoundVarInterpretations arch t fs + => BoundVarInterpretations arch t fs -> S.ExprBoundVar t ctp -> MacawQ arch t fs Exp -evalBoundVar endianness interps bVar = +evalBoundVar interps bVar = if | Just loc <- MapF.lookup bVar (locVars interps) -> withLocToReg $ \ltr -> do liftQ [| return ($(varE (regsValName interps)) ^. M.boundValue $(ltr loc)) |] | Just (C.Const name) <- MapF.lookup bVar (opVars interps) ->