mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-29 17:17:05 +03:00
fixed merge conflicts
This commit is contained in:
Ben Perez
commit
d41a58aba2
@ -924,7 +924,7 @@ ppAbsStack m = vcat (pp <$> Map.toDescList m)
|
||||
------------------------------------------------------------------------
|
||||
-- AbsBlockState
|
||||
|
||||
-- | State at beginning of a block.
|
||||
-- | Processor/memory state after at beginning of a block.
|
||||
data AbsBlockState r
|
||||
= AbsBlockState { _absRegState :: !(RegState r (AbsValue (RegAddrWidth r)))
|
||||
, _startAbsStack :: !(AbsBlockStack (RegAddrWidth r))
|
||||
@ -1121,8 +1121,6 @@ transferValue :: forall a ids tp
|
||||
-> Value a ids tp
|
||||
-> ArchAbsValue a tp
|
||||
transferValue c v = do
|
||||
let amap = c^.absAssignments
|
||||
aregs = c^.absInitialRegs
|
||||
case v of
|
||||
BoolValue b -> BoolConst b
|
||||
BVValue w i
|
||||
@ -1140,8 +1138,8 @@ transferValue c v = do
|
||||
-- Invariant: v is in m
|
||||
AssignedValue a ->
|
||||
fromMaybe (error $ "Missing assignment for " ++ show (assignId a))
|
||||
(MapF.lookup (assignId a) amap)
|
||||
Initial r -> aregs ^. boundValue r
|
||||
(MapF.lookup (assignId a) (c^.absAssignments))
|
||||
Initial r -> c^.absInitialRegs ^. boundValue r
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Operations
|
||||
|
||||
@ -125,7 +125,7 @@ addUpperBound :: ( MapF.OrdF (ArchReg arch)
|
||||
-> Either String (IndexBounds (ArchReg arch) ids)
|
||||
addUpperBound v u bnds
|
||||
-- Do nothing if upper bounds equals or exceeds function
|
||||
| u >= maxUnsigned (valueWidth v) = Right bnds
|
||||
| u >= maxUnsigned (typeWidth v) = Right bnds
|
||||
| u < 0 = error "addUpperBound given negative value."
|
||||
| otherwise =
|
||||
case v of
|
||||
|
||||
@ -88,11 +88,17 @@ data ArchitectureInfo arch
|
||||
-> AbsBlockState (ArchReg arch)
|
||||
-- ^ Update the abstract state after a function call returns
|
||||
, identifyCall :: forall ids
|
||||
. Memory (ArchAddrWidth arch)
|
||||
. Memory (ArchAddrWidth arch)
|
||||
-> [Stmt arch ids]
|
||||
-> RegState (ArchReg arch) (Value arch ids)
|
||||
-> Maybe (Seq (Stmt arch ids), ArchSegmentOff arch)
|
||||
|
||||
-- ^ Function for recognizing call statements.
|
||||
--
|
||||
-- Given a memory state, list of statements, and final register
|
||||
-- state, the should determine if this is a call, and if so,
|
||||
-- return the statements with any action to push the return
|
||||
-- value to the stack removed, and provide the explicit return
|
||||
-- address that the function should return to.
|
||||
, identifyReturn :: forall ids
|
||||
. [Stmt arch ids]
|
||||
-> RegState (ArchReg arch) (Value arch ids)
|
||||
|
||||
@ -123,7 +123,9 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
|
||||
-- @BVTestBit x i@ returns true iff bit @i@ of @x@ is true.
|
||||
-- 0 is the index of the least-significant bit.
|
||||
BVTestBit :: !(f (BVType n)) -> !(f (BVType log_n)) -> App f BoolType
|
||||
--
|
||||
-- If the value is larger than the width of n, then the result is false.
|
||||
BVTestBit :: (1 <= n) => !(f (BVType n)) -> !(f (BVType log_n)) -> App f BoolType
|
||||
|
||||
-- Bitwise complement
|
||||
BVComplement :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
@ -33,7 +33,7 @@ module Data.Macaw.CFG.Core
|
||||
, Value(..)
|
||||
, BVValue
|
||||
, valueAsApp
|
||||
, valueWidth
|
||||
, asLiteralAddr
|
||||
, asBaseOffset
|
||||
, asInt64Constant
|
||||
, mkLit
|
||||
@ -105,7 +105,8 @@ import Numeric (showHex)
|
||||
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
|
||||
|
||||
import Data.Macaw.CFG.App
|
||||
import Data.Macaw.Memory (MemWord, MemWidth, MemAddr, MemSegmentOff, Endianness(..))
|
||||
import Data.Macaw.Memory ( MemWord, MemWidth, MemAddr, MemSegmentOff, Endianness(..)
|
||||
, absoluteAddr)
|
||||
import Data.Macaw.Types
|
||||
|
||||
-- Note:
|
||||
@ -323,13 +324,6 @@ instance ( HasRepr (ArchReg arch) TypeRepr
|
||||
typeRepr (AssignedValue a) = typeRepr (assignRhs a)
|
||||
typeRepr (Initial r) = typeRepr r
|
||||
|
||||
valueWidth :: ( HasRepr (ArchReg arch) TypeRepr
|
||||
)
|
||||
=> Value arch ids (BVType n) -> NatRepr n
|
||||
valueWidth v =
|
||||
case typeRepr v of
|
||||
BVTypeRepr n -> n
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Value equality
|
||||
|
||||
@ -395,6 +389,15 @@ valueAsApp :: Value arch ids tp -> Maybe (App (Value arch ids) tp)
|
||||
valueAsApp (AssignedValue (Assignment _ (EvalApp a))) = Just a
|
||||
valueAsApp _ = Nothing
|
||||
|
||||
-- | This returns a segmented address if the value can be interpreted as a literal memory
|
||||
-- address, and returns nothing otherwise.
|
||||
asLiteralAddr :: MemWidth (ArchAddrWidth arch)
|
||||
=> BVValue arch ids (ArchAddrWidth arch)
|
||||
-> Maybe (ArchMemAddr arch)
|
||||
asLiteralAddr (BVValue _ val) = Just $ absoluteAddr (fromInteger val)
|
||||
asLiteralAddr (RelocatableValue _ i) = Just i
|
||||
asLiteralAddr _ = Nothing
|
||||
|
||||
asInt64Constant :: Value arch ids (BVType 64) -> Maybe Int64
|
||||
asInt64Constant (BVValue _ o) = Just (fromInteger o)
|
||||
asInt64Constant _ = Nothing
|
||||
|
||||
@ -147,6 +147,27 @@ rewriteApp app = do
|
||||
UExt (BVValue _ x) w -> do
|
||||
pure $ BVValue w x
|
||||
|
||||
BoolMux (BoolValue b) x y -> do
|
||||
pure $! if b then x else y
|
||||
-- ite c T y = (~c | T) & (c | y)
|
||||
-- = c | y
|
||||
BoolMux c (BoolValue True) y -> do
|
||||
rewriteApp (OrApp c y)
|
||||
-- ite c F y = (~c | F) & (c | y)
|
||||
-- = ~c & y
|
||||
BoolMux c (BoolValue False) y -> do
|
||||
cn <- rewriteApp (NotApp c)
|
||||
rewriteApp (AndApp cn y)
|
||||
-- ite c x T = (~c | x) & (c | T)
|
||||
-- = ~c | x
|
||||
BoolMux c x (BoolValue True) -> do
|
||||
cn <- rewriteApp (NotApp c)
|
||||
rewriteApp (OrApp cn x)
|
||||
-- ite c x F = (~c | x) & (c | F)
|
||||
-- = c & x
|
||||
BoolMux c x (BoolValue False) -> do
|
||||
rewriteApp (AndApp c x)
|
||||
|
||||
AndApp (BoolValue xc) y -> do
|
||||
if xc then
|
||||
pure y
|
||||
@ -161,7 +182,19 @@ rewriteApp app = do
|
||||
pure y
|
||||
OrApp x y@BoolValue{} -> rewriteApp (OrApp y x)
|
||||
NotApp (BoolValue b) ->
|
||||
pure $ boolLitValue (not b)
|
||||
pure $! boolLitValue (not b)
|
||||
NotApp (valueAsApp -> Just (NotApp c)) ->
|
||||
pure $! c
|
||||
XorApp (BoolValue b) x ->
|
||||
if b then
|
||||
rewriteApp (NotApp x)
|
||||
else
|
||||
pure x
|
||||
XorApp x (BoolValue b) ->
|
||||
if b then
|
||||
rewriteApp (NotApp x)
|
||||
else
|
||||
pure x
|
||||
|
||||
BVAdd _ x (BVValue _ 0) -> do
|
||||
pure x
|
||||
@ -196,27 +229,53 @@ rewriteApp app = do
|
||||
r <- rewriteApp (BVSignedLe y x)
|
||||
rewriteApp (NotApp r)
|
||||
BVSignedLe (BVValue w x) (BVValue _ y) -> do
|
||||
pure $ boolLitValue $ toSigned w x <= toSigned w y
|
||||
|
||||
pure $ boolLitValue $ toSigned w x <= toSigned w y
|
||||
BVTestBit (BVValue xw xc) (BVValue _ ic) | ic < min (natValue xw) (toInteger (maxBound :: Int)) -> do
|
||||
let v = xc `testBit` fromInteger ic
|
||||
pure $! boolLitValue v
|
||||
-- If we test the greatest bit turn this to a signed equality
|
||||
BVTestBit x (BVValue _ ic)
|
||||
| w <- typeWidth x
|
||||
, ic + 1 == natValue w -> do
|
||||
rewriteApp (BVSignedLt x (BVValue w 0))
|
||||
BVTestBit (valueAsApp -> Just (UExt x _)) i@(BVValue _ ic) -> do
|
||||
let xw = typeWidth x
|
||||
if ic < natValue xw then
|
||||
rewriteApp (BVTestBit x i)
|
||||
else
|
||||
pure (BoolValue False)
|
||||
BVTestBit (valueAsApp -> Just (BVXor _ x y@BVValue{})) i -> do
|
||||
BVTestBit (valueAsApp -> Just (BVAnd _ x y)) i@BVValue{} -> do
|
||||
xb <- rewriteApp (BVTestBit x i)
|
||||
yb <- rewriteApp (BVTestBit y i)
|
||||
rewriteApp (AndApp xb yb)
|
||||
BVTestBit (valueAsApp -> Just (BVOr _ x y)) i@BVValue{} -> do
|
||||
xb <- rewriteApp (BVTestBit x i)
|
||||
yb <- rewriteApp (BVTestBit y i)
|
||||
rewriteApp (OrApp xb yb)
|
||||
BVTestBit (valueAsApp -> Just (BVXor _ x y)) i -> do
|
||||
xb <- rewriteApp (BVTestBit x i)
|
||||
yb <- rewriteApp (BVTestBit y i)
|
||||
rewriteApp (XorApp xb yb)
|
||||
BVTestBit (valueAsApp -> Just (BVComplement _ x)) i -> do
|
||||
xb <- rewriteApp (BVTestBit x i)
|
||||
rewriteApp (NotApp xb)
|
||||
BVTestBit (valueAsApp -> Just (Mux _ c x y)) i -> do
|
||||
xb <- rewriteApp (BVTestBit x i)
|
||||
yb <- rewriteApp (BVTestBit y i)
|
||||
rewriteApp (BoolMux c xb yb)
|
||||
|
||||
-- (x >> j) testBit i ~> x testBit (j+i)
|
||||
BVTestBit (valueAsApp -> Just (BVShr w x (BVValue _ j))) (BVValue _ i)
|
||||
| j + i < natValue w, j + i <= maxUnsigned w -> do
|
||||
rewriteApp (BVTestBit x (BVValue w (j + i)))
|
||||
|
||||
BVComplement w (BVValue _ x) -> do
|
||||
pure (BVValue w (toUnsigned w (complement x)))
|
||||
|
||||
BVAnd w (BVValue _ x) (BVValue _ y) -> do
|
||||
pure (BVValue w (x .&. y))
|
||||
-- Ensure constant with and is second argument.
|
||||
BVAnd w x@BVValue{} y -> do
|
||||
rewriteApp (BVAnd w y x)
|
||||
BVAnd _ _ y@(BVValue _ 0) -> do
|
||||
@ -272,9 +331,13 @@ rewriteApp app = do
|
||||
Eq x@BVValue{} y -> do
|
||||
rewriteApp (Eq y x)
|
||||
|
||||
-- x + o = y ~> x = (y - o)
|
||||
Eq (valueAsApp -> Just (BVAdd w x (BVValue _ o))) (BVValue _ yc) -> do
|
||||
rewriteApp (Eq x (BVValue w (toUnsigned w (yc - o))))
|
||||
|
||||
Eq (valueAsApp -> Just (BVSub _ x y)) (BVValue _ 0) -> do
|
||||
rewriteApp (Eq x y)
|
||||
|
||||
Eq (valueAsApp -> Just (UExt x _)) (BVValue _ yc) -> do
|
||||
let u = typeWidth x
|
||||
if yc > maxUnsigned u then
|
||||
|
||||
@ -5,6 +5,7 @@ Maintainer : Joe Hendrix <jhendrix@galois.com>, Simon Winwood <sjw@galois.
|
||||
This provides information about code discovered in binaries.
|
||||
-}
|
||||
{-# LANGUAGE ConstraintKinds #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE DoAndIfThenElse #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
@ -77,7 +78,6 @@ import qualified Data.Macaw.AbsDomain.StridedInterval as SI
|
||||
import Data.Macaw.Architecture.Info
|
||||
import Data.Macaw.CFG
|
||||
import Data.Macaw.CFG.DemandSet
|
||||
import Data.Macaw.CFG.Rewriter
|
||||
import Data.Macaw.DebugLogging
|
||||
import Data.Macaw.Discovery.AbsEval
|
||||
import Data.Macaw.Discovery.State as State
|
||||
@ -85,6 +85,11 @@ import Data.Macaw.Memory
|
||||
import qualified Data.Macaw.Memory.Permissions as Perm
|
||||
import Data.Macaw.Types
|
||||
|
||||
#define USE_REWRITER 1
|
||||
|
||||
#ifdef USE_REWRITER
|
||||
import Data.Macaw.CFG.Rewriter
|
||||
#endif
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Utilities
|
||||
@ -152,9 +157,27 @@ cameFromUnsoundReason found_map rsn = do
|
||||
CodePointerInMem{} -> True
|
||||
-}
|
||||
|
||||
------------------------------------------------------------------------
|
||||
--
|
||||
|
||||
-- | This uses an assertion about a given value being true or false to
|
||||
-- refine the information in an abstract processor state.
|
||||
refineProcStateBounds :: ( OrdF (ArchReg arch)
|
||||
, HasRepr (ArchReg arch) TypeRepr
|
||||
)
|
||||
=> Value arch ids BoolType
|
||||
-> Bool
|
||||
-> AbsProcessorState (ArchReg arch) ids
|
||||
-> AbsProcessorState (ArchReg arch) ids
|
||||
refineProcStateBounds v isTrue ps =
|
||||
case indexBounds (Jmp.assertPred v isTrue) ps of
|
||||
Left{} -> ps
|
||||
Right ps' -> ps'
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Rewriting block
|
||||
|
||||
#ifdef USE_REWRITER
|
||||
-- | Apply optimizations to a terminal statement.
|
||||
rewriteTermStmt :: TermStmt arch src -> Rewriter arch src tgt (TermStmt arch tgt)
|
||||
rewriteTermStmt tstmt = do
|
||||
@ -167,7 +190,7 @@ rewriteTermStmt tstmt = do
|
||||
_ | Just (NotApp cn) <- valueAsApp tgtCond -> do
|
||||
Branch cn <$> pure f <*> pure t
|
||||
| otherwise ->
|
||||
Branch tgtCond <$> pure t <*> pure f
|
||||
pure $ Branch tgtCond t f
|
||||
Syscall regs ->
|
||||
Syscall <$> traverseF rewriteValue regs
|
||||
TranslateError regs msg ->
|
||||
@ -187,6 +210,7 @@ rewriteBlock b = do
|
||||
, blockStmts = tgtStmts
|
||||
, blockTerm = tgtTermStmt
|
||||
}
|
||||
#endif
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Demanded subterm utilities
|
||||
@ -268,7 +292,7 @@ data FoundAddr arch
|
||||
------------------------------------------------------------------------
|
||||
-- FunState
|
||||
|
||||
-- | The state for the function explroation monad
|
||||
-- | The state for the function exploration monad (funM)
|
||||
data FunState arch ids
|
||||
= FunState { funNonceGen :: !(NonceGenerator (ST ids) ids)
|
||||
, curFunAddr :: !(ArchSegmentOff arch)
|
||||
@ -332,7 +356,7 @@ liftST = FunM . lift
|
||||
mergeIntraJump :: ArchSegmentOff arch
|
||||
-- ^ Source label that we are jumping from.
|
||||
-> AbsBlockState (ArchReg arch)
|
||||
-- ^ Block state after executing instructions.
|
||||
-- ^ The state of the system after jumping to new block.
|
||||
-> ArchSegmentOff arch
|
||||
-- ^ Address we are trying to reach.
|
||||
-> FunM arch ids ()
|
||||
@ -368,7 +392,7 @@ mergeIntraJump src ab tgt = do
|
||||
-------------------------------------------------------------------------------
|
||||
-- Jump table bounds
|
||||
|
||||
-- See if expression matches form expected by jump tables
|
||||
-- | Figure out if this is a jump table.
|
||||
matchJumpTable :: MemWidth (ArchAddrWidth arch)
|
||||
=> Memory (ArchAddrWidth arch)
|
||||
-> BVValue arch ids (ArchAddrWidth arch) -- ^ Memory address that IP is read from.
|
||||
@ -386,11 +410,14 @@ matchJumpTable mem read_addr
|
||||
matchJumpTable _ _ =
|
||||
Nothing
|
||||
|
||||
-- | This describes why we could not infer the bounds of code that looked like it
|
||||
-- was accessing a jump table.
|
||||
data JumpTableBoundsError arch ids
|
||||
= CouldNotInterpretAbsValue !(AbsValue (ArchAddrWidth arch) (BVType (ArchAddrWidth arch)))
|
||||
| UpperBoundMismatch !(Jmp.UpperBound (BVType (ArchAddrWidth arch))) !Integer
|
||||
| CouldNotFindBound String !(ArchAddrValue arch ids)
|
||||
|
||||
-- | Show the jump table bounds
|
||||
showJumpTableBoundsError :: ArchConstraints arch => JumpTableBoundsError arch ids -> String
|
||||
showJumpTableBoundsError err =
|
||||
case err of
|
||||
@ -405,8 +432,8 @@ showJumpTableBoundsError err =
|
||||
show "Could not find jump table: " ++ msg ++ "\n"
|
||||
++ show (ppValueAssignments jump_index)
|
||||
|
||||
-- Returns the index bounds for a jump table of 'Nothing' if this is not a block
|
||||
-- table.
|
||||
-- | Returns the index bounds for a jump table of 'Nothing' if this is
|
||||
-- not a block table.
|
||||
getJumpTableBounds :: ArchitectureInfo a
|
||||
-> AbsProcessorState (ArchReg a) ids -- ^ Current processor registers.
|
||||
-> ArchMemAddr a -- ^ Base
|
||||
@ -428,24 +455,11 @@ getJumpTableBounds info regs base jump_index = withArchConstraints info $
|
||||
abs_value -> Left (CouldNotInterpretAbsValue abs_value)
|
||||
|
||||
|
||||
------------------------------------------------------------------------
|
||||
--
|
||||
|
||||
refineProcStateBounds :: ( OrdF (ArchReg arch)
|
||||
, HasRepr (ArchReg arch) TypeRepr
|
||||
)
|
||||
=> Value arch ids BoolType
|
||||
-> Bool
|
||||
-> AbsProcessorState (ArchReg arch) ids
|
||||
-> AbsProcessorState (ArchReg arch) ids
|
||||
refineProcStateBounds v isTrue ps =
|
||||
case indexBounds (Jmp.assertPred v isTrue) ps of
|
||||
Left{} -> ps
|
||||
Right ps' -> ps'
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- ParseState
|
||||
|
||||
-- | This describes information learned when analyzing a block to look
|
||||
-- for code pointers and classify exit.
|
||||
data ParseState arch ids =
|
||||
ParseState { _writtenCodeAddrs :: ![ArchSegmentOff arch]
|
||||
-- ^ Addresses marked executable that were written to memory.
|
||||
@ -454,9 +468,11 @@ data ParseState arch ids =
|
||||
, _newFunctionAddrs :: ![ArchSegmentOff arch]
|
||||
}
|
||||
|
||||
-- | Code addresses written to memory.
|
||||
writtenCodeAddrs :: Simple Lens (ParseState arch ids) [ArchSegmentOff arch]
|
||||
writtenCodeAddrs = lens _writtenCodeAddrs (\s v -> s { _writtenCodeAddrs = v })
|
||||
|
||||
-- | Intraprocedural jump targets.
|
||||
intraJumpTargets :: Simple Lens (ParseState arch ids) [(ArchSegmentOff arch, AbsBlockState (ArchReg arch))]
|
||||
intraJumpTargets = lens _intraJumpTargets (\s v -> s { _intraJumpTargets = v })
|
||||
|
||||
@ -483,6 +499,7 @@ recordWriteStmt arch_info mem regs stmt = do
|
||||
------------------------------------------------------------------------
|
||||
-- ParseContext
|
||||
|
||||
-- | Information needed to parse the processor state
|
||||
data ParseContext arch ids = ParseContext { pctxMemory :: !(Memory (ArchAddrWidth arch))
|
||||
, pctxArchInfo :: !(ArchitectureInfo arch)
|
||||
, pctxFunAddr :: !(ArchSegmentOff arch)
|
||||
@ -498,6 +515,34 @@ addrMemRepr arch_info =
|
||||
Addr32 -> BVMemRepr n4 (archEndianness arch_info)
|
||||
Addr64 -> BVMemRepr n8 (archEndianness arch_info)
|
||||
|
||||
identifyCallTargets :: forall arch ids
|
||||
. (RegisterInfo (ArchReg arch))
|
||||
=> AbsProcessorState (ArchReg arch) ids
|
||||
-- ^ Abstract processor state just before call.
|
||||
-> BVValue arch ids (ArchAddrWidth arch)
|
||||
-> [ArchSegmentOff arch]
|
||||
identifyCallTargets absState ip = do
|
||||
-- Code pointers from abstract domains.
|
||||
let mem = absMem absState
|
||||
let def = concretizeAbsCodePointers mem (transferValue absState ip)
|
||||
let segOffAddrs :: Maybe (ArchSegmentOff arch) -> [ArchSegmentOff arch]
|
||||
segOffAddrs (Just addr)
|
||||
| segmentFlags (msegSegment addr) `Perm.hasPerm` Perm.execute =
|
||||
[addr]
|
||||
segOffAddrs _ = []
|
||||
case ip of
|
||||
BVValue _ x -> segOffAddrs $ resolveAbsoluteAddr mem (fromInteger x)
|
||||
RelocatableValue _ a -> segOffAddrs $ asSegmentOff mem a
|
||||
AssignedValue a ->
|
||||
case assignRhs a of
|
||||
-- See if we can get a value out of a concrete memory read.
|
||||
ReadMem addr (BVMemRepr _ end)
|
||||
| Just laddr <- asLiteralAddr addr
|
||||
, Right val <- readAddr mem end laddr ->
|
||||
segOffAddrs (asSegmentOff mem val) ++ def
|
||||
_ -> def
|
||||
Initial _ -> def
|
||||
|
||||
-- | This parses a block that ended with a fetch and execute instruction.
|
||||
parseFetchAndExecute :: forall arch ids
|
||||
. ParseContext arch ids
|
||||
@ -521,15 +566,17 @@ parseFetchAndExecute ctx lbl_idx stmts regs s' = do
|
||||
-- The last statement was a call.
|
||||
-- Note that in some cases the call is known not to return, and thus
|
||||
-- this code will never jump to the return value.
|
||||
_ | Just (prev_stmts, ret) <- identifyCall arch_info mem stmts s' -> do
|
||||
_ | Just (prev_stmts, ret) <- identifyCall arch_info mem stmts s' -> do
|
||||
mapM_ (recordWriteStmt arch_info mem absProcState') prev_stmts
|
||||
let abst = finalAbsBlockState absProcState' s'
|
||||
seq abst $ do
|
||||
-- Merge caller return information
|
||||
intraJumpTargets %= ((ret, postCallAbsState arch_info abst ret):)
|
||||
-- Look for new ips.
|
||||
let addrs = concretizeAbsCodePointers mem (abst^.absRegState^.curIP)
|
||||
-- Use the abstract domain to look for new code pointers for the current IP.
|
||||
let addrs = identifyCallTargets absProcState' (s'^.boundValue ip_reg)
|
||||
newFunctionAddrs %= (++ addrs)
|
||||
-- Use the call-specific code to look for new IPs.
|
||||
|
||||
pure StatementList { stmtsIdent = lbl_idx
|
||||
, stmtsNonterm = toList prev_stmts
|
||||
, stmtsTerm = ParsedCall s' (Just ret)
|
||||
@ -546,14 +593,14 @@ parseFetchAndExecute ctx lbl_idx stmts regs s' = do
|
||||
, stmtsAbsState = absProcState'
|
||||
}
|
||||
|
||||
-- Jump to concrete offset.
|
||||
--
|
||||
-- Note, we disallow jumps back to function entry point thus forcing them to be treated
|
||||
-- as tail calls or unclassified if the stack has changed size.
|
||||
| Just tgt_addr <- asLiteralAddr (s'^.boundValue ip_reg)
|
||||
, Just tgt_mseg <- asSegmentOff mem tgt_addr
|
||||
-- Jump to a block within this function.
|
||||
| Just tgt_mseg <- asSegmentOff mem =<< asLiteralAddr (s'^.boundValue ip_reg)
|
||||
, segmentFlags (msegSegment tgt_mseg) `Perm.hasPerm` Perm.execute
|
||||
-- The target address cannot be this function entry point.
|
||||
--
|
||||
-- This will result in the target being trated as a call or tail call.
|
||||
, tgt_mseg /= pctxFunAddr ctx -> do
|
||||
|
||||
mapM_ (recordWriteStmt arch_info mem absProcState') stmts
|
||||
-- Merge block state and add intra jump target.
|
||||
let abst = finalAbsBlockState absProcState' s'
|
||||
@ -634,7 +681,6 @@ parseFetchAndExecute ctx lbl_idx stmts regs s' = do
|
||||
let addrs = concretizeAbsCodePointers mem (abst^.absRegState^.curIP)
|
||||
newFunctionAddrs %= (++ addrs)
|
||||
|
||||
|
||||
pure StatementList { stmtsIdent = lbl_idx
|
||||
, stmtsNonterm = stmts
|
||||
, stmtsTerm = ParsedCall s' Nothing
|
||||
@ -800,12 +846,16 @@ transfer addr = do
|
||||
curFunBlocks %= Map.insert addr pb
|
||||
else do
|
||||
-- Rewrite returned blocks to simplify expressions
|
||||
#ifdef USE_REWRITER
|
||||
let ctx = RewriteContext { rwctxNonceGen = nonceGen
|
||||
, rwctxArchFn = rewriteArchFn ainfo
|
||||
, rwctxArchStmt = rewriteArchStmt ainfo
|
||||
, rwctxConstraints = \x -> x
|
||||
}
|
||||
bs1 <- liftST $ runRewriter ctx $ traverse rewriteBlock bs0
|
||||
#else
|
||||
let bs1 = bs0
|
||||
#endif
|
||||
-- Comute demand set
|
||||
let demandSet =
|
||||
runDemandComp (archDemandContext ainfo) $ do
|
||||
|
||||
@ -23,7 +23,7 @@ import Data.Macaw.AbsDomain.AbsState
|
||||
import Data.Macaw.Architecture.Info
|
||||
import Data.Macaw.CFG
|
||||
|
||||
-- | Get the absolute value associated with an address.
|
||||
-- | Get the abstract value associated with an address.
|
||||
absEvalReadMem :: RegisterInfo (ArchReg a)
|
||||
=> AbsProcessorState (ArchReg a) ids
|
||||
-> ArchAddrValue a ids
|
||||
@ -31,6 +31,8 @@ absEvalReadMem :: RegisterInfo (ArchReg a)
|
||||
-- ^ Information about the memory layout for the value.
|
||||
-> ArchAbsValue a tp
|
||||
absEvalReadMem r a tp
|
||||
-- If the value is a stack entry, then see if there is a stack
|
||||
-- value associated with it.
|
||||
| StackOffset _ s <- transferValue r a
|
||||
, [o] <- Set.toList s
|
||||
, Just (StackEntry v_tp v) <- Map.lookup o (r^.curAbsStack)
|
||||
|
||||
@ -46,7 +46,6 @@ module Data.Macaw.Discovery.State
|
||||
, CodeAddrReason(..)
|
||||
-- * DiscoveryState utilities
|
||||
, RegConstraint
|
||||
, asLiteralAddr
|
||||
) where
|
||||
|
||||
import Control.Lens
|
||||
@ -240,7 +239,7 @@ data StatementList arch ids
|
||||
-- ^ The terminal statement in the block.
|
||||
, stmtsAbsState :: !(AbsProcessorState (ArchReg arch) ids)
|
||||
-- ^ The abstract state of the block just before terminal
|
||||
}
|
||||
}
|
||||
|
||||
deriving instance ArchConstraints arch
|
||||
=> Show (StatementList arch ids)
|
||||
@ -419,12 +418,3 @@ funInfo = lens _funInfo (\s v -> s { _funInfo = v })
|
||||
|
||||
-- | Constraint on architecture register values needed by code exploration.
|
||||
type RegConstraint r = (OrdF r, HasRepr r TypeRepr, RegisterInfo r, ShowF r)
|
||||
|
||||
-- | This returns a segmented address if the value can be interpreted as a literal memory
|
||||
-- address, and returns nothing otherwise.
|
||||
asLiteralAddr :: MemWidth (ArchAddrWidth arch)
|
||||
=> BVValue arch ids (ArchAddrWidth arch)
|
||||
-> Maybe (ArchMemAddr arch)
|
||||
asLiteralAddr (BVValue _ val) = Just $ absoluteAddr (fromInteger val)
|
||||
asLiteralAddr (RelocatableValue _ i) = Just i
|
||||
asLiteralAddr _ = Nothing
|
||||
|
||||
@ -561,7 +561,6 @@ resolveAbsoluteAddr mem addr = addrWidthClass (memAddrWidth mem) $
|
||||
Just $! MemSegmentOff seg (addr - base)
|
||||
_ -> Nothing
|
||||
|
||||
|
||||
-- | Make a segment offset pair after ensuring the offset is valid
|
||||
resolveSegmentOff :: MemWidth w => MemSegment w -> MemWord w -> Maybe (MemSegmentOff w)
|
||||
resolveSegmentOff seg off
|
||||
|
||||
Loading…
Reference in New Issue
Block a user