mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-18 03:21:49 +03:00
[refinement] implement getBlock block lookup function.
This commit is contained in:
parent
bd0e57cfc1
commit
5c2e0edeaa
@ -62,10 +62,15 @@ funIncludesBlock :: BlockIdentifier arch
|
|||||||
funIncludesBlock blkID (Some fi) =
|
funIncludesBlock blkID (Some fi) =
|
||||||
isJust ((fi ^. parsedBlocks) Map.!? blkID)
|
isJust ((fi ^. parsedBlocks) Map.!? blkID)
|
||||||
|
|
||||||
|
-- | Returns the actual block (if it exists) from the Discovery State
|
||||||
|
-- (in the first function for which it exists).
|
||||||
getBlock :: DiscoveryState arch
|
getBlock :: DiscoveryState arch
|
||||||
-> BlockIdentifier arch
|
-> BlockIdentifier arch
|
||||||
-> Some (ParsedBlock arch)
|
-> Maybe (Some (ParsedBlock arch))
|
||||||
getBlock ds blkID = undefined
|
getBlock ds blkID =
|
||||||
|
case filter (funIncludesBlock blkID) (ds ^. funInfo ^.. folded) of
|
||||||
|
((Some fi):_) -> Some <$> (fi ^. parsedBlocks) Map.!? blkID
|
||||||
|
[] -> Nothing
|
||||||
|
|
||||||
-- | This function identifies the possible target addresses (of other
|
-- | This function identifies the possible target addresses (of other
|
||||||
-- blocks within this function) from the terminal statement in the
|
-- blocks within this function) from the terminal statement in the
|
||||||
|
@ -284,12 +284,15 @@ type Solution arch = [ArchSegmentOff arch] -- identified transfers
|
|||||||
equationFor :: DiscoveryState arch -> FuncBlockPath arch -> Equation arch
|
equationFor :: DiscoveryState arch -> FuncBlockPath arch -> Equation arch
|
||||||
equationFor inpDS (Path bid anc _loop) =
|
equationFor inpDS (Path bid anc _loop) =
|
||||||
let curBlk = getBlock inpDS bid
|
let curBlk = getBlock inpDS bid
|
||||||
in if null anc
|
in case curBlk of
|
||||||
then Equation inpDS curBlk
|
Nothing -> error "did not find requested block in discovery results!" -- internal
|
||||||
else undefined
|
Just b ->
|
||||||
-- Should linearly combine the anc statements with the
|
if null anc
|
||||||
-- current block's statements and asserts that state that
|
then Equation inpDS b
|
||||||
-- the IP from one to the next is expected.
|
else undefined
|
||||||
|
-- Should linearly combine the anc statements with the
|
||||||
|
-- current block's statements and asserts that state that
|
||||||
|
-- the IP from one to the next is expected.
|
||||||
|
|
||||||
solve :: ( MS.SymArchConstraints arch
|
solve :: ( MS.SymArchConstraints arch
|
||||||
, 16 <= MC.ArchAddrWidth arch
|
, 16 <= MC.ArchAddrWidth arch
|
||||||
|
Loading…
Reference in New Issue
Block a user