GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-27 03:13:43 +03:00
Code Issues Projects Releases Wiki Activity

Update the calls to asAtomicStateUpdate

Browse Source 
The type of the instruction address changed
This commit is contained in:
Tristan Ravitch 2018-03-30 10:52:58 -07:00
parent dd655680f7
commit b7c3118070
4 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -141,9 +141,9 @@ disassembleBlock lookupSemantics mem gs curPCAddr maxOffset = do
nextPCVal = MC.RelocatableValue (knownNat :: NatRepr (ArchAddrWidth arm)) nextPC
-- Note: In ARM, the IP is incremented *after* an instruction
-- executes; pass in the physical address of the instruction here.
(ipAddr, ipVal) <- case MM.asAbsoluteAddr (MM.relativeSegmentAddr curPCAddr) of
ipVal <- case MM.asAbsoluteAddr (MM.relativeSegmentAddr curPCAddr) of
Nothing -> failAt gs off curPCAddr (InstructionAtUnmappedAddr i)
Just addr -> return (addr, BVValue (knownNat :: NatRepr (ArchAddrWidth arm)) (fromIntegral addr))
Just addr -> return (BVValue (knownNat :: NatRepr (ArchAddrWidth arm)) (fromIntegral addr))
case lookupSemantics ipVal i of
Nothing -> failAt gs off curPCAddr (UnsupportedInstruction i)
Just transformer -> do
@ -155,7 +155,7 @@ disassembleBlock lookupSemantics mem gs curPCAddr maxOffset = do
A32I i' -> ARMD.ppInstruction i'
T32I i' -> ThumbD.ppInstruction i'))
addStmt (Comment (T.pack lineStr))
asAtomicStateUpdate ipAddr transformer
asAtomicStateUpdate (MM.relativeSegmentAddr curPCAddr) transformer
-- Check to see if the PC has become conditionally-defined (by e.g.,
-- a mux). If it has, we need to split execution using a primitive

6
macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs
View File

@ -112,9 +112,9 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
-- 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.
(ipWord, ipVal) <- case MM.asAbsoluteAddr (MM.relativeSegmentAddr curIPAddr) of
ipVal <- case MM.asAbsoluteAddr (MM.relativeSegmentAddr curIPAddr) of
Nothing -> failAt gs off curIPAddr (InstructionAtUnmappedAddr i)
Just addr -> return (addr, BVValue (pointerNatRepr (Proxy @ppc)) (fromIntegral addr))
Just addr -> return (BVValue (pointerNatRepr (Proxy @ppc)) (fromIntegral addr))
case lookupSemantics ipVal i of
Nothing -> failAt gs off curIPAddr (UnsupportedInstruction i)
Just transformer -> do
@ -124,7 +124,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
egs1 <- liftST $ ET.runExceptT (runGenerator genResult gs $ do
let lineStr = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
addStmt (Comment (T.pack lineStr))
asAtomicStateUpdate ipWord transformer
asAtomicStateUpdate (MM.relativeSegmentAddr curIPAddr) transformer
-- Check to see if the IP has become conditionally-defined (by e.g.,
-- a mux). If it has, we need to split execution using a primitive

2
macaw-semmc/src/Data/Macaw/SemMC/Generator.hs
View File

@ -178,7 +178,7 @@ curRegState = blockState . pBlockState
-- transformer is executed. Note: if the transformer splits the state, it isn't
-- obvious what will happen here. The mechanism is not designed with that use
-- case in mind.
asAtomicStateUpdate :: ArchAddrWord arch
asAtomicStateUpdate :: ArchMemAddr arch
-- ^ Instruction address
-> Generator arch ids s a
-- ^ An action recording the state transformations of the instruction

2
submodules/macaw

@ -1 +1 @@
Subproject commit ce96c5589683b8ab8a545a2defa6f83423cade86
Subproject commit 4bd307e41d114d824300e08d7e9953a728663ee3