mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 08:53:12 +03:00
Migrate abstract state with start of block to block region datatype.
This commit is contained in:
Joe Hendrix
parent
fc2a7a06aa
commit
36d161acd2
@ -278,9 +278,9 @@ tryDisassembleAddr rsn addr ab = do
|
||||
let br = BlockRegion { brReason = rsn
|
||||
, brSize = next_ip^.addrOffset - addr^.addrOffset
|
||||
, brBlocks = block_map
|
||||
, brAbsInitState = ab
|
||||
}
|
||||
put $ s0 & blocks %~ Map.insert addr br
|
||||
& codeInfoMap %~ Map.insert addr (CodeInfo { _addrAbsBlockState = ab })
|
||||
|
||||
-- | Mark address as the start of a code block.
|
||||
markCodeAddrBlock :: PrettyCFGConstraints arch
|
||||
@ -302,8 +302,7 @@ markCodeAddrBlock rsn addr ab = do
|
||||
-- Get block for addr
|
||||
tryDisassembleAddr rsn addr ab
|
||||
-- Get block for old block
|
||||
let Just old_code_info = Map.lookup l (s^.codeInfoMap)
|
||||
tryDisassembleAddr (brReason br) l (old_code_info^.addrAbsBlockState)
|
||||
tryDisassembleAddr (brReason br) l (brAbsInitState br)
|
||||
-- Add function starts to split to frontier
|
||||
-- This will result in us re-exploring l_start and a_start
|
||||
-- once the current function is done.
|
||||
@ -413,7 +412,8 @@ assignmentAbsValues :: forall arch ids
|
||||
=> ArchitectureInfo arch
|
||||
-> Memory (ArchAddrWidth arch)
|
||||
-> CFG arch ids
|
||||
-> Map (ArchSegmentedAddr arch) (CodeInfo arch)
|
||||
-> Map (ArchSegmentedAddr arch) (AbsBlockState (ArchReg arch))
|
||||
-- ^ Maps addresses to the initial state at that address.
|
||||
-> MapF (AssignId ids) (ArchAbsValue arch)
|
||||
assignmentAbsValues info mem g absm =
|
||||
foldl' go MapF.empty (Map.elems (g^.cfgBlocks))
|
||||
@ -426,8 +426,8 @@ assignmentAbsValues info mem g absm =
|
||||
case Map.lookup a absm of
|
||||
Nothing -> do
|
||||
error $ "assignmentAbsValues could not find code infomation for block " ++ show a
|
||||
Just codeInfo -> do
|
||||
let abs_state = initAbsProcessorState mem (codeInfo^.addrAbsBlockState)
|
||||
Just blockState -> do
|
||||
let abs_state = initAbsProcessorState mem blockState
|
||||
insBlock b abs_state m0
|
||||
_ -> m0
|
||||
|
||||
@ -472,16 +472,16 @@ mergeIntraJump src ab tgt = do
|
||||
let rsn = NextIP (labelAddr src)
|
||||
-- Associate a new abstract state with the code region.
|
||||
s0 <- get
|
||||
case Map.lookup tgt (s0^.codeInfoMap) of
|
||||
case Map.lookup tgt (s0^.blocks) of
|
||||
-- We have seen this block before, so need to join and see if
|
||||
-- the results is changed.
|
||||
Just cinfo_old -> do
|
||||
let cinfo_new = CodeInfo { _addrAbsBlockState = ab }
|
||||
case unionCodeInfo cinfo_old cinfo_new of
|
||||
Just old_block -> do
|
||||
case joinD (brAbsInitState old_block) ab of
|
||||
Nothing -> return ()
|
||||
Just new ->
|
||||
modify $ (reverseEdges %~ Map.insertWith Set.union tgt (Set.singleton (labelAddr src)))
|
||||
. (codeInfoMap %~ Map.insert tgt new)
|
||||
Just new -> do
|
||||
let new_block = old_block { brAbsInitState = new }
|
||||
modify $ (blocks %~ Map.insert tgt new_block)
|
||||
. (reverseEdges %~ Map.insertWith Set.union tgt (Set.singleton (labelAddr src)))
|
||||
. (frontier %~ Map.insert tgt rsn)
|
||||
-- We haven't seen this block before
|
||||
Nothing -> do
|
||||
@ -745,12 +745,12 @@ transfer addr = do
|
||||
case mroot of
|
||||
Nothing -> return ()
|
||||
Just root -> do
|
||||
minfo <- use $ codeInfoMap . at addr
|
||||
minfo <- use $ blocks . at addr
|
||||
case minfo of
|
||||
Nothing -> error $ "Could not find block " ++ show addr ++ "."
|
||||
Just info -> do
|
||||
Just br -> do
|
||||
transferBlock root $
|
||||
initAbsProcessorState mem (info^.addrAbsBlockState)
|
||||
initAbsProcessorState mem (brAbsInitState br)
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- Main loop
|
||||
@ -770,8 +770,6 @@ explore_frontier = do
|
||||
-- Delete any entries we previously discovered for function.
|
||||
& reverseEdges %~ deleteMapRange (Just addr) high
|
||||
& blocks %~ deleteMapRange (Just addr) high
|
||||
-- Delete any entries we previously discovered for function.
|
||||
& codeInfoMap %~ deleteMapRange (Just addr) high
|
||||
put st'
|
||||
explore_frontier
|
||||
Just ((addr,_rsn), next_roots) -> do
|
||||
|
||||
@ -37,11 +37,6 @@ module Data.Macaw.Discovery.Info
|
||||
, CodeAddrReason(..)
|
||||
, frontier
|
||||
, function_frontier
|
||||
-- ** Abstract state information
|
||||
, CodeInfo(..)
|
||||
, addrAbsBlockState
|
||||
, codeInfoMap
|
||||
, unionCodeInfo
|
||||
-- ** DiscoveryInfo utilities
|
||||
, getFunctionEntryPoint
|
||||
, inSameFunction
|
||||
@ -74,33 +69,6 @@ import Data.Macaw.Memory
|
||||
import qualified Data.Macaw.Memory.Permissions as Perm
|
||||
import Data.Macaw.Types
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- AbsStateMap
|
||||
|
||||
-- | All information specifc about a discovered code address.
|
||||
data CodeInfo arch = CodeInfo
|
||||
{ _addrAbsBlockState :: !(AbsBlockState (ArchReg arch))
|
||||
}
|
||||
|
||||
-- | The abstract state at the beginning of the code block.
|
||||
addrAbsBlockState :: Simple Lens (CodeInfo arch) (AbsBlockState (ArchReg arch))
|
||||
addrAbsBlockState = lens _addrAbsBlockState (\s v -> s { _addrAbsBlockState = v })
|
||||
|
||||
-- | 'joinCodeInfo x y' returns 'Nothing' if all states represented by 'y' are
|
||||
-- also in 'x', and 'Just z' where 'z' represents an overapproximation
|
||||
-- of the union of the states 'x' and 'y'.
|
||||
unionCodeInfo :: RegisterInfo (ArchReg arch)
|
||||
=> CodeInfo arch
|
||||
-> CodeInfo arch
|
||||
-> Maybe (CodeInfo arch)
|
||||
unionCodeInfo x y =
|
||||
case joinD (x^.addrAbsBlockState) (y^.addrAbsBlockState) of
|
||||
Just z -> Just CodeInfo { _addrAbsBlockState = z }
|
||||
Nothing -> Nothing
|
||||
|
||||
-- | Maps each code address to a set of abstract states
|
||||
--type AbsStateMap arch = Map (ArchSegmentedAddr arch) (CodeInfo arch))
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- BlockRegion
|
||||
|
||||
@ -113,6 +81,8 @@ data BlockRegion arch ids
|
||||
-- ^ The size of the region of memory covered by this.
|
||||
, brBlocks :: !(Map Word64 (Block arch ids))
|
||||
-- ^ Map from labelIndex to associated block.
|
||||
, brAbsInitState :: !(AbsBlockState (ArchReg arch))
|
||||
-- ^ The abstract state at the start of this block.
|
||||
}
|
||||
|
||||
-- | Does a simple lookup in the cfg at a given DecompiledBlock address.
|
||||
@ -212,9 +182,6 @@ data DiscoveryInfo arch ids
|
||||
, archInfo :: !(ArchitectureInfo arch)
|
||||
-- ^ Architecture-specific information needed for discovery.
|
||||
, _blocks :: !(Map (ArchSegmentedAddr arch) (BlockRegion arch ids))
|
||||
, _codeInfoMap :: !(Map (ArchSegmentedAddr arch) (CodeInfo arch))
|
||||
-- ^ Map from code addresses to the abstract state at the start of
|
||||
-- the block.
|
||||
-- ^ Maps an address to the code associated with that address.
|
||||
, _functionEntries :: !(Set (ArchSegmentedAddr arch))
|
||||
-- ^ Maps addresses that are marked as the start of a function
|
||||
@ -255,7 +222,6 @@ emptyDiscoveryInfo ng mem symbols info = DiscoveryInfo
|
||||
, _globalDataMap = Map.empty
|
||||
, _frontier = Map.empty
|
||||
, _function_frontier = Map.empty
|
||||
, _codeInfoMap = Map.empty
|
||||
}
|
||||
|
||||
blocks :: Simple Lens (DiscoveryInfo arch ids)
|
||||
@ -290,10 +256,6 @@ function_frontier :: Simple Lens (DiscoveryInfo arch ids)
|
||||
(CodeAddrReason (ArchAddrWidth arch)))
|
||||
function_frontier = lens _function_frontier (\s v -> s { _function_frontier = v })
|
||||
|
||||
codeInfoMap :: Simple Lens (DiscoveryInfo arch ids)
|
||||
(Map (ArchSegmentedAddr arch) (CodeInfo arch))
|
||||
codeInfoMap = lens _codeInfoMap (\s v -> s { _codeInfoMap = v })
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- DiscoveryInfo utilities
|
||||
|
||||
@ -459,8 +421,8 @@ tryGetStaticSyscallNo interp_state block_addr proc_state
|
||||
| BVValue _ call_no <- proc_state^.boundValue syscall_num_reg =
|
||||
Just call_no
|
||||
| Initial r <- proc_state^.boundValue syscall_num_reg
|
||||
, Just absSt <- interp_state^.codeInfoMap^.at block_addr =
|
||||
asConcreteSingleton (absSt^.addrAbsBlockState^.absRegState^.boundValue r)
|
||||
, Just b <- interp_state^.blocks^.at block_addr =
|
||||
asConcreteSingleton (brAbsInitState b^.absRegState^.boundValue r)
|
||||
| otherwise =
|
||||
Nothing
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user