[refinement] Provide list of forward path blocks to smt solving.

Currently smt solving just uses the first block of the first path,
which is not correct, but the framework for providing the list of
paths is now present.

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

@@ -4,6 +4,7 @@ module Data.Macaw.Refinement.Path
   ( FuncBlockPath(..)
   , buildFuncPath
   , pathDepth
+  , pathForwardTrails
   , pathTo
   , takePath
   )
@@ -161,3 +162,32 @@ takePath n (Path blkid anc loop) =
 pathDepth :: FuncBlockPath arch -> Int
 pathDepth (Path _ [] _) = 0
 pathDepth (Path _ anc _) = 1 + maximum (pathDepth <$> anc)
+
+
+-- | Converts a Path tree into a list of the distinct paths, where
+-- each path is represented by a list of block IDs in the order that
+-- they would be executed (i.e. the back-path is converted to a
+-- forward-chain list.
+--
+-- For example:
+--
+-- > Path 1
+-- >   [ Path 2 [ Path 3 ] []
+-- >   , Path 4 [ Path 5 [ Path 6 [] []
+-- >                     , Path 7 [ Path 3 [] []] []
+-- >                     ] []
+-- >            ] []
+-- >   ] []
+--
+-- Is converted to:
+--
+-- >  [ [ 3, 2, 1 ]
+-- >  , [ 6, 5, 4, 1 ]
+-- >  , [ 3, 7, 5, 4, 1 ]
+-- >  ]
+--
+pathForwardTrails :: FuncBlockPath arch -> [ [BlockIdentifier arch] ]
+pathForwardTrails (Path i [] _) = [[i]]
+pathForwardTrails (Path i anc _) = let ft = concatMap pathForwardTrails anc
+                                       appendTo v l = l <> [v]
+                                   in map (appendTo i) ft

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

@@ -130,8 +130,11 @@ import Data.Macaw.Discovery.State ( DiscoveryFunInfo
                                   , parsedBlocks
                                   , stmtsTerm
                                   )
-import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, blockID, funForBlock, getBlock )
+import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, blockID
-import Data.Macaw.Refinement.Path ( FuncBlockPath(..), buildFuncPath, pathDepth, pathTo, takePath )
+                                            , funForBlock, getBlock )
+import Data.Macaw.Refinement.Path ( FuncBlockPath(..)
+                                  , buildFuncPath, pathDepth, pathForwardTrails
+                                  , pathTo, takePath )
 import qualified Data.Macaw.Symbolic as MS
 import Data.Map (Map)
 import Data.Maybe
@@ -278,21 +281,16 @@ refinePath inpDS path maxlevel numlevels prevResult =
                        then return bestResult
                        else refinePath inpDS path maxlevel nextlevel bestResult
 
-data Equation arch = Equation (DiscoveryState arch) (Some (ParsedBlock arch))
+data Equation arch = Equation (DiscoveryState arch) [[Some (ParsedBlock arch)]]
 type Solution arch = [ArchSegmentOff arch]  -- identified transfers
 
 equationFor :: DiscoveryState arch -> FuncBlockPath arch -> Equation arch
-equationFor inpDS (Path bid anc _loop) =
+equationFor inpDS p =
-  let curBlk = getBlock inpDS bid
+  let pTrails = pathForwardTrails p
-  in case curBlk of
+      pTrailBlocks = map (getBlock inpDS) <$> pTrails
-       Nothing -> error "did not find requested block in discovery results!" -- internal
+  in if and (any (not . isJust) <$> pTrailBlocks)
-       Just b ->
+     then error "did not find requested block in discovery results!" -- internal
-         if null anc
+       else Equation inpDS (catMaybes <$> pTrailBlocks)
-         then Equation inpDS b
-         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
          , 16 <= MC.ArchAddrWidth arch
@@ -401,6 +399,21 @@ initRegs arch_vals sym ip_val = do
     (MS.updateReg arch_vals) reg_struct MC.ip_reg ip_val
 
 smtSolveTransfer
+  :: forall arch t solver fp m
+   . ( MS.SymArchConstraints arch
+     , C.IsSymInterface (C.OnlineBackend t solver fp)
+     , W.OnlineSolver t solver
+     , MonadIO m
+     )
+  => RefinementContext arch t solver fp
+  -> DiscoveryState arch
+  -> [[Some (ParsedBlock arch)]]
+  -> m [ArchSegmentOff arch]
+smtSolveTransfer rc ds blockPaths =
+  -- wrong thing: fix the handling of blockPaths
+  smtSolveTransfer' rc ds $ head $ head blockPaths
+
+smtSolveTransfer'
   :: forall arch t solver fp m
    . ( MS.SymArchConstraints arch
      , C.IsSymInterface (C.OnlineBackend t solver fp)
@@ -411,7 +424,7 @@ smtSolveTransfer
   -> DiscoveryState arch
   -> Some (ParsedBlock arch)
   -> m [ArchSegmentOff arch]
-smtSolveTransfer RefinementContext{..} discovery_state (Some block) = do
+smtSolveTransfer' RefinementContext{..} discovery_state (Some block) = do
   let arch = Proxy @arch
   block_ip_val <- case MC.segoffAsAbsoluteAddr (pblockAddr block) of
     Just addr -> liftIO $ LLVM.llvmPointer_bv symbolicBackend