mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-25 23:23:18 +03:00
Add a helper to set register values
This helper additionally simplifies constants. This is very useful for dealing with simplifying the instruction pointer. That is required by the rest of macaw, which expects IP values it wants to explore to be fully reduced.
This commit is contained in:
parent
71a432ed18
commit
6308df3a8f
@ -112,7 +112,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
||||
|
||||
nextIPExpr <- getRegValue PPC_IP
|
||||
case matchConditionalBranch nextIPExpr of
|
||||
Just (cond, t_ip, f_ip) -> conditionalBranch cond (setIP t_ip) (setIP f_ip)
|
||||
Just (cond, t_ip, f_ip) -> conditionalBranch cond (setRegVal PPC_IP t_ip) (setRegVal PPC_IP f_ip)
|
||||
Nothing -> return ())
|
||||
case egs1 of
|
||||
Left genErr -> failAt gs off curIPAddr (GenerationError i genErr)
|
||||
|
@ -35,7 +35,7 @@ module Data.Macaw.PPC.Generator (
|
||||
addExpr,
|
||||
bvconcat,
|
||||
bvselect,
|
||||
setIP,
|
||||
setRegVal,
|
||||
-- * Lenses
|
||||
blockState,
|
||||
curPPCState,
|
||||
@ -189,8 +189,12 @@ curPPCState = blockState . pBlockState
|
||||
------------------------------------------------------------------------
|
||||
-- Factored-out Operations for PPCGenerator
|
||||
|
||||
setIP :: (PPCArchConstraints ppc, RegAddrWidth (PPCReg ppc) ~ w) => Value ppc ids (BVType w) -> PPCGenerator ppc ids s ()
|
||||
setIP val = curPPCState . boundValue PPC_IP .= val
|
||||
setRegVal :: (PPCArchConstraints ppc, RegAddrWidth (PPCReg ppc) ~ w)
|
||||
=> PPCReg ppc tp
|
||||
-> Value ppc ids tp
|
||||
-> PPCGenerator ppc ids s ()
|
||||
setRegVal reg val =
|
||||
curPPCState . boundValue reg .= fromMaybe val (simplifyValue val)
|
||||
|
||||
-- | The implementation of bitvector concatenation
|
||||
--
|
||||
|
@ -19,7 +19,7 @@ module Data.Macaw.PPC.Semantics.TH
|
||||
import qualified Data.ByteString as BS
|
||||
import qualified Data.Constraint as C
|
||||
|
||||
import Control.Lens ( (.=), (^.) )
|
||||
import Control.Lens ( (^.) )
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.List as L
|
||||
import qualified Data.Text as T
|
||||
@ -313,12 +313,12 @@ translateFormula ipVarName semantics interps varNames = do
|
||||
let FreeParamF name = varNames `SL.indexShapedList` idx
|
||||
[| do val <- $(addEltTH interps expr)
|
||||
let reg = toPPCReg $(varE name)
|
||||
curPPCState . M.boundValue reg .= val
|
||||
setRegVal reg val
|
||||
|]
|
||||
LiteralParameter APPC.LocMem -> writeMemTH interps expr
|
||||
LiteralParameter loc -> do
|
||||
[| do val <- $(addEltTH interps expr)
|
||||
curPPCState . M.boundValue $(locToRegTH (Proxy @arch) loc) .= val
|
||||
setRegVal $(locToRegTH (Proxy @arch) loc) val
|
||||
|]
|
||||
FunctionParameter str (WrappedOperand _ opIx) _w -> do
|
||||
let FreeParamF boundOperandName = SL.indexShapedList varNames opIx
|
||||
@ -328,7 +328,7 @@ translateFormula ipVarName semantics interps varNames = do
|
||||
[| do case $(varE (A.exprInterpName fi)) $(varE boundOperandName) of
|
||||
Just reg -> do
|
||||
val <- $(addEltTH interps expr)
|
||||
curPPCState . M.boundValue (toPPCReg reg) .= val
|
||||
setRegVal (toPPCReg reg) val
|
||||
Nothing -> error ("Invalid instruction form at " ++ show $(varE ipVarName))
|
||||
|]
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user