Update to the latest macaw

2024-11-23 08:27:24 +03:00 · 2018-04-24 10:55:07 -07:00 · 2018-04-24 10:55:07 -07:00 · 4bed676ca2
commit 4bed676ca2
parent 27b4eaf360
11 changed files with 58 additions and 30 deletions
--- a/cabal.project.dist
+++ b/cabal.project.dist
@ -19,4 +19,5 @@ packages: macaw-ppc/
          submodules/dwarf/
          submodules/elf-edit/
          submodules/flexdis86/
+          submodules/flexdis86/binary-symbols/
          submodules/llvm-pretty/
--- a/macaw-arm/src/Data/Macaw/ARM/Disassemble.hs
+++ b/macaw-arm/src/Data/Macaw/ARM/Disassemble.hs
@ -138,7 +138,7 @@ disassembleBlock lookupSemantics mem gs curPCAddr maxOffset = do
      -- traceM ("II: " ++ show i)
      let nextPCOffset = off + bytesRead
          nextPC = MM.relativeAddr seg nextPCOffset
-          nextPCVal = MC.RelocatableValue (knownNat :: NatRepr (ArchAddrWidth arm)) nextPC
+          nextPCVal = MC.RelocatableValue (MM.addrWidthRepr curPCAddr) nextPC
      -- 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.relativeSegmentAddr curPCAddr) of
@ -196,7 +196,7 @@ disassembleBlock lookupSemantics mem gs curPCAddr maxOffset = do
 -- are no byte regions that could be coalesced.
 readInstruction :: MM.Memory w
                -> MM.MemSegmentOff w
-                -> Either (MM.MemoryError w) (InstructionSet, MM.MemWord w)
+                -> Either (ARMMemoryError w) (InstructionSet, MM.MemWord w)
 readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
  let seg = MM.msegSegment addr
      segRelAddrRaw = MM.relativeSegmentAddr addr
@ -209,13 +209,15 @@ readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
      segRelAddr = segRelAddrRaw { addrOffset = MM.addrOffset segRelAddrRaw `xor` loBit }
  if MM.segmentFlags seg `MMP.hasPerm` MMP.execute
  then do
-      contents <- MM.addrContentsAfter mem segRelAddr
+      contents <- liftMemError $ MM.addrContentsAfter mem segRelAddr
      case contents of
-        [] -> ET.throwError $ MM.AccessViolation segRelAddr
-        MM.SymbolicRef {} : _ ->
-          ET.throwError $ MM.UnexpectedRelocation segRelAddr
+        [] -> ET.throwError $ ARMMemoryError (MM.AccessViolation segRelAddr)
+        MM.BSSRegion {} : _ ->
+          ET.throwError $ ARMMemoryError (MM.UnexpectedBSS segRelAddr)
+        MM.RelocationRegion r : _ ->
+          ET.throwError $ ARMMemoryError (MM.UnexpectedRelocation segRelAddr r "Disassembling from relocation")
        MM.ByteRegion bs : _
-          | BS.null bs -> ET.throwError $ MM.AccessViolation segRelAddr
+          | BS.null bs -> ET.throwError $ ARMMemoryError (MM.AccessViolation segRelAddr)
          | otherwise -> do
            -- FIXME: Having to wrap the bytestring in a lazy wrapper is
            -- unpleasant.  We could alter the disassembler to consume strict
@ -227,8 +229,20 @@ readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
                         else fmap (fmap T32I) $ ThumbD.disassembleInstruction (LBS.fromStrict bs)
            case minsn of
              Just insn -> return (insn, fromIntegral bytesRead)
-              Nothing -> ET.throwError $ MM.InvalidInstruction segRelAddr contents
-  else ET.throwError $ MM.PermissionsError segRelAddr
+              Nothing -> ET.throwError $ ARMInvalidInstruction segRelAddr contents
+  else ET.throwError $ ARMMemoryError (MM.PermissionsError segRelAddr)
+
+liftMemError :: Either (MM.MemoryError w) a -> Either (ARMMemoryError w) a
+liftMemError e =
+  case e of
+    Left err -> Left (ARMMemoryError err)
+    Right a -> Right a
+
+-- | A wrapper around the 'MM.MemoryError' that lets us add in information about
+-- invalid instructions.
+data ARMMemoryError w = ARMInvalidInstruction !(MM.MemAddr w) [MM.SegmentRange w]
+                      | ARMMemoryError !(MM.MemoryError w)
+                      deriving (Show)

 -- | Examine a value and see if it is a mux; if it is, break the mux up and
 -- return its component values (the condition and two alternatives)
@ -284,7 +298,7 @@ data TranslationError w = TranslationError { transErrorAddr :: MM.MemSegmentOff
                                           }

 data TranslationErrorReason w = InvalidNextPC (MM.MemAddr w) (MM.MemAddr w)
-                              | DecodeError (MM.MemoryError w)
+                              | DecodeError (ARMMemoryError w)
                              | UnsupportedInstruction InstructionSet
                              | InstructionAtUnmappedAddr InstructionSet
                              | GenerationError InstructionSet GeneratorError
--- a/macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs
+++ b/macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs
@ -50,19 +50,21 @@ import           Data.Macaw.PPC.PPCReg
 -- are no byte regions that could be coalesced.
 readInstruction :: MM.Memory w
                -> MM.MemSegmentOff w
-                -> Either (MM.MemoryError w) (D.Instruction, MM.MemWord w)
+                -> Either (PPCMemoryError w) (D.Instruction, MM.MemWord w)
 readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
  let seg = MM.msegSegment addr
  case MM.segmentFlags seg `MMP.hasPerm` MMP.execute of
-    False -> ET.throwError (MM.PermissionsError (MM.relativeSegmentAddr addr))
+    False -> ET.throwError (PPCMemoryError (MM.PermissionsError (MM.relativeSegmentAddr addr)))
    True -> do
-      contents <- MM.addrContentsAfter mem (MM.relativeSegmentAddr addr)
+      contents <- liftMemError $ MM.addrContentsAfter mem (MM.relativeSegmentAddr addr)
      case contents of
-        [] -> ET.throwError (MM.AccessViolation (MM.relativeSegmentAddr addr))
-        MM.SymbolicRef {} : _ ->
-          ET.throwError (MM.UnexpectedRelocation (MM.relativeSegmentAddr addr))
+        [] -> ET.throwError (PPCMemoryError (MM.AccessViolation (MM.relativeSegmentAddr addr)))
+        MM.RelocationRegion r : _ ->
+          ET.throwError (PPCMemoryError (MM.UnexpectedRelocation (MM.relativeSegmentAddr addr) r "Disassembling from relocation"))
+        MM.BSSRegion {} : _ ->
+          ET.throwError (PPCMemoryError (MM.UnexpectedBSS (MM.relativeSegmentAddr addr)))
        MM.ByteRegion bs : _rest
-          | BS.null bs -> ET.throwError (MM.AccessViolation (MM.relativeSegmentAddr addr))
+          | BS.null bs -> ET.throwError (PPCMemoryError (MM.AccessViolation (MM.relativeSegmentAddr addr)))
          | otherwise -> do
            -- FIXME: Having to wrap the bytestring in a lazy wrapper is
            -- unpleasant.  We could alter the disassembler to consume strict
@ -71,7 +73,19 @@ readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
            let (bytesRead, minsn) = D.disassembleInstruction (LBS.fromStrict bs)
            case minsn of
              Just insn -> return (insn, fromIntegral bytesRead)
-              Nothing -> ET.throwError (MM.InvalidInstruction (MM.relativeSegmentAddr addr) contents)
+              Nothing -> ET.throwError (PPCInvalidInstruction (MM.relativeSegmentAddr addr) contents)
+
+liftMemError :: Either (MM.MemoryError w) a -> Either (PPCMemoryError w) a
+liftMemError e =
+  case e of
+    Left err -> Left (PPCMemoryError err)
+    Right a -> Right a
+
+-- | A wrapper around the 'MM.MemoryError' that lets us add in information about
+-- invalid instructions.
+data PPCMemoryError w = PPCInvalidInstruction !(MM.MemAddr w) [MM.SegmentRange w]
+                      | PPCMemoryError !(MM.MemoryError w)
+                      deriving (Show)

 -- | Disassemble an instruction and terminate the current block if we run out of
 -- instructions to disassemble.  We can run out if:
@ -108,7 +122,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
 --      traceM ("II: " ++ show i)
      let nextIPOffset = off + bytesRead
          nextIP = MM.relativeAddr seg nextIPOffset
-          nextIPVal = MC.RelocatableValue (pointerNatRepr (Proxy @ppc)) nextIP
+          nextIPVal = MC.RelocatableValue (MM.addrWidthRepr curIPAddr) nextIP
      -- Note: In PowerPC, the IP is incremented *after* an instruction
      -- executes, rather than before as in X86.  We have to pass in the
      -- physical address of the instruction here.
@ -250,7 +264,7 @@ data TranslationError w = TranslationError { transErrorAddr :: MM.MemSegmentOff
                                           }

 data TranslationErrorReason w = InvalidNextIP Word64 Word64
-                              | DecodeError (MM.MemoryError w)
+                              | DecodeError (PPCMemoryError w)
                              | UnsupportedInstruction D.Instruction
                              | InstructionAtUnmappedAddr D.Instruction
                              | GenerationError D.Instruction GeneratorError
--- a/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
@ -67,7 +67,6 @@ import qualified Data.Macaw.Memory as MM
 import           Data.Macaw.Types ( BoolType )
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.Map as MapF
-import qualified Data.Parameterized.NatRepr as NR
 import qualified Data.Parameterized.Nonce as NC

 import           Data.Macaw.SemMC.Simplify ( simplifyValue, simplifyApp )
@ -155,7 +154,7 @@ initRegState :: (KnownNat (RegAddrWidth (ArchReg arch)),
             => MM.MemSegmentOff (RegAddrWidth (ArchReg arch))
             -> RegState (ArchReg arch) (Value arch ids)
 initRegState startIP =
-  mkRegState Initial & curIP .~ RelocatableValue NR.knownNat (MM.relativeSegmentAddr startIP)
+  mkRegState Initial & curIP .~ RelocatableValue (addrWidthRepr startIP) (MM.relativeSegmentAddr startIP)

 blockSeq :: Simple Lens (GenState arch ids s) (BlockSeq arch ids)
 blockSeq = lens _blockSeq (\s v -> s { _blockSeq = v })
--- a/macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs
@ -53,8 +53,8 @@ simplifyApp a =
    BVAdd _ (BVValue _ 0) r           -> Just r
    BVAdd rep l@(BVValue {}) r@(RelocatableValue {}) ->
      simplifyApp (BVAdd rep r l)
-    BVAdd rep (RelocatableValue _ addr) (BVValue _ off) ->
-      Just (RelocatableValue rep (MM.incAddr off addr))
+    BVAdd _rep (RelocatableValue _ addr) (BVValue _ off) ->
+      Just (RelocatableValue (addrWidthRepr addr) (MM.incAddr off addr))
    BVAdd sz l r                      -> binopbv (+) sz l r
    BVMul _ l (BVValue _ 1)           -> Just l
    BVMul _ (BVValue _ 1) r           -> Just r
--- a/submodules/crucible
+++ b/submodules/crucible
@ -1 +1 @@
-Subproject commit 7674f24ede49d169e436b9314ddf1eea313d8d69
+Subproject commit b8b3c0049384f18694e49e2f978982cb4021dcf7
--- a/submodules/elf-edit
+++ b/submodules/elf-edit
@ -1 +1 @@
-Subproject commit 6e79f23efb4d5ff656cf107893d53565df0ba4de
+Subproject commit 81891986f31838cbfe622fb894e643b14ad21a1f
--- a/submodules/flexdis86
+++ b/submodules/flexdis86
@ -1 +1 @@
-Subproject commit 71c32ec99d503f8aae234b3716aff6c3d217bf50
+Subproject commit 497854b1eef4e477a11c808ac21a659dbd757ea5
--- a/submodules/macaw
+++ b/submodules/macaw
@ -1 +1 @@
-Subproject commit 1517bf64b4611f4252de914a0d51153e647746c0
+Subproject commit 9047cb41fb2e62df9dc01fd93e56224ed4b10a60
--- a/submodules/parameterized-utils
+++ b/submodules/parameterized-utils
@ -1 +1 @@
-Subproject commit d70ece92e67e10b2092bc3f062b2447ac3d1b19f
+Subproject commit 3e6a0e87567c7bff8412f451a44bc5b850c3f8ee
--- a/submodules/semmc
+++ b/submodules/semmc
@ -1 +1 @@
-Subproject commit 52366d9201eeffdcdbb8bb7428ec09a927ba01a3
+Subproject commit 66a80ada32e05d05a66074c2281fcfe6243fdfae