[refinement] Implement determination of block transfer target addr(s).

refinement/src/Data/Macaw/Refinement/FuncBlockUtils.hs

@@ -9,10 +9,12 @@ module Data.Macaw.Refinement.FuncBlockUtils
 where
 
 import           Control.Lens
+import qualified Data.Foldable as F
 import           Data.Macaw.CFG.AssignRhs ( ArchSegmentOff )
 import           Data.Macaw.Discovery.State ( DiscoveryFunInfo
                                             , DiscoveryState
                                             , ParsedBlock(..)
+                                            , ParsedTermStmt(..)
                                             , funInfo
                                             , parsedBlocks
                                             , stmtsTerm
@@ -58,12 +60,33 @@ funIncludesBlock :: BlockIdentifier arch
 funIncludesBlock blkID (Some fi) =
   isJust ((fi ^. parsedBlocks) Map.!? blkID)
 
+-- | This function identifies the possible target addresses (of other
+-- blocks within this function) from the terminal statement in the
+-- input block.  Note that this function is responsible for returning
+-- the under-approximation of target blocks *within* the current
+-- function; it may return target addresses that lie outside of the
+-- function, but it is not required to, nor will it return other
+-- external targets.
 blockTransferTo :: DiscoveryFunInfo arch ids
                 -> BlockIdentifier arch
                 -> [ArchSegmentOff arch]
 blockTransferTo fi frm =
   let frmBlk = (fi ^. parsedBlocks) Map.!? frm
+      lclTgtAddrs termStmt =
+        case termStmt of
+          ParsedCall _ mbTgt | Just tgt <- mbTgt -> [tgt]
+                             | otherwise -> []
+          ParsedJump _ tgt -> [tgt]
+          ParsedLookupTable _ _ tgts -> F.toList tgts
+          ParsedReturn {} -> []
+          ParsedIte _ thenS elseS -> lclTgtAddrs (stmtsTerm thenS) <>
+                                    lclTgtAddrs (stmtsTerm elseS)
+          PLTStub _ tgt _ -> undefined -- KWQ tgt?
+          ParsedArchTermStmt _ _ mbTgt | Just tgt <- mbTgt -> [tgt]
+                                       | otherwise -> []
+          ParsedTranslateError {} -> []
+          ClassifyFailure {} -> []
+          _ -> undefined
   in case frmBlk of
-       Just fBlk -> case stmtsTerm $ blockStatementList fBlk of
-                      _ -> undefined
+       Just fBlk -> lclTgtAddrs $ stmtsTerm $ blockStatementList fBlk
        Nothing -> error "block ID not valid" -- impossible

refinement/src/Data/Macaw/Refinement/Path.hs

@@ -76,7 +76,9 @@ bldFPath :: DiscoveryFunInfo arch ids
 bldFPath _fi x@(_, []) = x
 bldFPath fi (fs, b:bs) =
   let nextBlkAddrs = blockTransferTo fi b
-      updPath = foldr (bldFPath' fi b) fs nextBlkAddrs
+      updPath = if null nextBlkAddrs
+                then Path b [] [] : fs
+                else foldr (bldFPath' fi b) fs nextBlkAddrs
   in bldFPath fi (updPath, bs)
 
 
@@ -117,7 +119,7 @@ bldFPath' fi b nextAddr fs =
            else Path b [] [] : p  -- new terminal entry
 
   in case nextBlkID of
-       Nothing -> fs -- should never happen (block not in function)
+       Nothing -> fs -- target addr was external to this function; ignore it
        Just cb -> addAncestor cb fs