[refinement] updates for merge of Some removal and updateDiscovery.

This commit is contained in:
Kevin Quick 2019-02-06 17:58:21 -08:00
parent 36a8be1c4e
commit 13224a91ce
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
2 changed files with 11 additions and 10 deletions

View File

@ -53,6 +53,9 @@ library
, crucible-llvm
, lens
, macaw-base
, macaw-loader
-- , macaw-loader-ppc
, macaw-loader-x86
, macaw-symbolic
, mtl
, parameterized-utils

View File

@ -138,7 +138,7 @@ import Data.Macaw.Discovery ( DiscoveryFunInfo
, stmtsTerm
)
import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier(..), blockID
, funForBlock, getBlock )
, getBlock )
import Data.Macaw.Refinement.Path ( FuncBlockPath(..)
, buildFuncPath, pathDepth, pathForwardTrails
, pathTo, takePath )
@ -243,7 +243,7 @@ refineBlockTransfer bin inpDS fi blk =
case pathTo (blockID blk) $ buildFuncPath fi of
Nothing -> error "unable to find function path for block" -- internal error
Just p -> do soln <- refinePath bin inpDS fi p (pathDepth p) 1
return $ maybe Nothing (Just . updateDiscovery inpDS blk) soln
return $ maybe Nothing (Just . updateDiscovery inpDS fi blk) soln
@ -252,17 +252,15 @@ updateDiscovery :: ( MC.RegisterInfo (MC.ArchReg arch)
, MC.ArchConstraints arch
) =>
DiscoveryState arch
-> DiscoveryFunInfo arch ids
-> ParsedBlock arch ids
-> Solution arch
-> DiscoveryState arch
updateDiscovery inpDS b@(Some pblk) soln =
case funForBlock b inpDS of
Just (Some finfo) ->
let funAddr = discoveredFunAddr finfo
blkAddr = pblockAddr pblk
in addDiscoveredFunctionBlockTargets inpDS funAddr $
guideTargets blkAddr soln
Nothing -> error "Cannot updateDiscovery for block with no function"
updateDiscovery inpDS finfo pblk soln =
let funAddr = discoveredFunAddr finfo
blkAddr = pblockAddr pblk
in addDiscoveredFunctionBlockTargets inpDS funAddr $
guideTargets blkAddr soln
guideTargets :: ( MC.RegisterInfo (MC.ArchReg arch)
, KnownNat (MC.ArchAddrWidth arch)