GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-28 08:34:23 +03:00
Code Issues Projects Releases Wiki Activity

arm: Update macaw-arm to compile with the latest macaw (and macaw-semmc)

Browse Source
This commit is contained in:
Tristan Ravitch 2018-03-30 09:08:49 -07:00
parent 51023263c4
commit d7b0ad9862
2 changed files with 11 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
macaw-arm/src/Data/Macaw/ARM/Disassemble.hs
View File

@ -35,6 +35,7 @@ import Data.Macaw.SemMC.Generator
import Data.Macaw.SemMC.Simplify ( simplifyValue )
import Data.Macaw.Types -- ( BVType, BoolType )
import Data.Maybe ( fromMaybe )
import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.Nonce as NC
import Data.Proxy ( Proxy(..) )
import qualified Data.Sequence as Seq
@ -97,7 +98,7 @@ tryDisassembleBlock lookupSemantics mem nonceGen startAddr maxSize = do
let startOffset = MM.msegOffset startAddr
(nextPCOffset, blocks) <- disassembleBlock lookupSemantics mem gs0 startAddr (startOffset + maxSize)
unless (nextPCOffset > startOffset) $ do
let reason = InvalidNextPC (fromIntegral nextPCOffset) (fromIntegral startOffset)
let reason = InvalidNextPC (MM.absoluteAddr nextPCOffset) (MM.absoluteAddr startOffset)
failAt gs0 nextPCOffset startAddr reason
return (F.toList (blocks ^. frontierBlocks), nextPCOffset - startOffset)
@ -134,7 +135,7 @@ disassembleBlock lookupSemantics mem gs curPCAddr maxOffset = do
let off = MM.msegOffset curPCAddr
case readInstruction mem curPCAddr of
Left err -> failAt gs off curPCAddr (DecodeError err)
Right (_, 0) -> failAt gs off curPCAddr (InvalidNextPC curPCAddr curPCAddr)
Right (_, 0) -> failAt gs off curPCAddr (InvalidNextPC (MM.relativeSegmentAddr curPCAddr) (MM.relativeSegmentAddr curPCAddr))
Right (i, bytesRead) -> do
-- traceM ("II: " ++ show i)
let nextPCOffset = off + bytesRead
@ -183,6 +184,7 @@ disassembleBlock lookupSemantics mem gs curPCAddr maxOffset = do
, _blockState = preBlock'
, genAddr = nextPCSegAddr
, genMemory = mem
, genRegUpdates = MapF.empty
}
disassembleBlock lookupSemantics mem gs2 nextPCSegAddr maxOffset
@ -283,7 +285,7 @@ data TranslationError w = TranslationError { transErrorAddr :: MM.MemSegmentOff
, transErrorReason :: TranslationErrorReason w
}
data TranslationErrorReason w = InvalidNextPC Word32 Word32
data TranslationErrorReason w = InvalidNextPC (MM.MemAddr w) (MM.MemAddr w)
| DecodeError (MM.MemoryError w)
| UnsupportedInstruction InstructionSet
| InstructionAtUnmappedAddr InstructionSet

12
macaw-arm/src/Data/Macaw/ARM/Identify.hs
View File

@ -9,7 +9,6 @@ module Data.Macaw.ARM.Identify
) where
import Control.Lens ( (^.) )
import Data.Macaw.ARM.ARMReg
import Data.Macaw.ARM.Arch
import Data.Macaw.AbsDomain.AbsState ( AbsProcessorState
, AbsValue(..)
@ -32,7 +31,7 @@ identifyCall :: ARMArchConstraints arm =>
-> [MC.Stmt arm ids]
-> MC.RegState (MC.ArchReg arm) (MC.Value arm ids)
-> Maybe (Seq.Seq (MC.Stmt arm ids), MC.ArchSegmentOff arm)
identifyCall _ mem stmts0 rs = Nothing -- KWQ: for now, nothing is identified as a call
identifyCall _ _mem _stmts0 _rs = Nothing -- KWQ: for now, nothing is identified as a call
-- | Intended to identify a return statement.
@ -45,11 +44,12 @@ identifyCall _ mem stmts0 rs = Nothing -- KWQ: for now, nothing is identified a
-- (A32 mode) when writing to the PC to discard the mode bit in target
-- addresses.
identifyReturn :: ARMArchConstraints arm =>
proxy ppc
proxy arm
-> [MC.Stmt arm ids]
-> AbsProcessorState (MC.ArchReg ppc) ids
-> Maybe (Seq.Seq (MC.Stmt ppc ids))
-> MC.RegState (MC.ArchReg arm) (MC.Value arm ids)
-> AbsProcessorState (MC.ArchReg arm) ids
-> Maybe (Seq.Seq (MC.Stmt arm ids))
identifyReturn _ stmts s finalRegSt8 =
case transferValue finalRegSt8 (s^.MC.boundValue PPC_IP) of
case transferValue finalRegSt8 (s^.MC.boundValue MC.ip_reg) of
ReturnAddr -> Just $ Seq.fromList stmts
_ -> Nothing