Hoopl图构建与不可达块误判问题排查求助

数据老陈

2026-5-6

排查Hoopl稀疏条件常量传播的可达性错误

我看你在用Hoopl实现稀疏条件常量传播时碰到了一个棘手的问题：Hoopl错误地将实际可达的代码块判定为不可达，测试案例里预期保留entry和fb块并完成常量折叠，但最终只留下了entry块，分支块全被删掉了。结合你给出的代码，我整理几个排查方向，你可以一步步验证：

1. 先确认图构建的正确性

你通过合并多个closed/closed Hoopl Graph来构建整体图，这里有几个关键点要检查：

合并操作的正确性：你用foldl (H.|*><*|) H.emptyClosedGraph ps合并子图，|*><*|用于合并两个独立的closed图，但如果子图之间有跳转关系（比如entry跳转到tb和fb），要确保合并后的图正确建立了跳转的标签关联。可以用Hoopl的showGraph函数打印构建后的完整图，查看entry块的CondBranch是否真的指向了正确的fb和tb的Hoopl内部标签，而不是无效标签。
标签映射的准确性：你用Data.Map维护用户标签和Hoopl标签的映射，要确保hooplLabelFor (Label "fb")能正确拿到对应的Hoopl标签——比如可以在构建完映射后，打印hlm的内容，确认所有用户标签都有对应的Hoopl标签。另外，fromJust在这里如果遇到未找到的标签会直接崩溃，测试案例里虽然不存在这个问题，但可以加个安全判断（比如用Map.lookup后处理Maybe）避免隐藏问题。
终止节点的跳转列表：你的NodeTerm构造函数里，第二个参数应该是该节点指向的Hoopl标签列表。如果toHoopl函数生成终止节点时，没有把用户标签转换成Hoopl标签并放入这个列表，Hoopl就无法识别跳转目标，自然会认为后续块不可达。

2. 检查数据流分析的逻辑

传递函数的问题

你的传递函数regIsConstant处理CondBranch时，不管条件的常量值，都同时返回两个分支的事实：

rc (NodeTerm (T (CondBranch (Reg x) tl fl)) _) f = 
  H.mkFactBase constLattice [(hooplLabelFor tl, f), (hooplLabelFor fl, Map.insert x (H.PElem 0) f)]

但在这个测试案例里，entry块执行后r0的值是0，所以CondBranch (Reg "r0") tl fl的true分支（tl）是不可达的。稀疏条件常量传播的核心就是在数据流分析阶段过滤不可达分支，你现在的传递函数会让Hoopl认为两个分支都可达，但实际上true分支的条件永远不满足，后续分析可能会因为事实冲突导致异常。

另外，你给false分支的事实是Map.insert x (H.PElem 0) f，但此时f里的x已经是PElem 0了，这个操作是冗余的，但不影响结果，不过可以优化。

初始事实的传递

你的初始事实initFact把所有寄存器设为Top，这没问题，但要确认entry块执行后，传递给后续分支的事实是否正确：比如entry块的Sub (Reg "r0") (Reg "r0")执行后，r0的事实应该被更新为PElem 0，你可以在传递函数里加日志（比如liftIO $ print f）来验证这一点。

3. 重写阶段的逻辑验证

你的重写函数constProp会把常量条件的CondBranch改成Branch，这个逻辑是对的，但要注意：

重写后的Branch必须指向正确的Hoopl标签，也就是hooplLabelFor fl，如果这里的标签映射错误，会导致Hoopl认为跳转目标不存在，进而删除fb块。
重写操作是否在分析阶段之后正确执行？analyzeAndRewriteFwd会先做数据流分析，再应用重写，你可以检查重写后的图是否正确替换了CondBranch为Branch，并且跳转目标正确。

4. 调试技巧

打印图结构：在构建图后、分析后分别用H.showGraph打印图的内容，查看每个块的标签、跳转关系和节点内容，确认fb块是否真的被包含在初始图里，以及分析后是否被错误标记为不可达。
添加日志：在传递函数和重写函数里加入liftIO $ print语句，输出每个节点处理时的事实、标签等信息，比如查看entry块处理后的r0值，CondBranch处理时的条件值，以及fb块是否接收到了正确的事实。
简化测试案例：先单独测试entry和fb块，去掉tb块，看看Hoopl是否能正确保留这两个块，逐步缩小问题范围。

测试代码与HUnit结果

测试代码

block_cprop_in_0 = [ --test for constprop
    L $ Label "entry",
    O $ Sub (Reg "r0") (Reg "r0"),
    T $ CondBranch (Reg "r0") (Label "tb") (Label "fb")
  ]
block_cprop_in_1 = [ -- test for constprop
    L $ Label "tb",
    O $ Sub (Reg "r1") (Reg "r0"),
    T $ Halt
  ]
block_cprop_in_2 = [ -- test for constprop
    L $ Label "fb",
    O $ Sub (Reg "r2") (Reg "r0"), --should get rewritten as a SubI
    T $ Halt
  ]
block_cprop_out = [ --test for constprop
    L $ Label "entry",
    O $ Sub (Reg "r0") (Reg "r0"),
    T $ Branch (Label "fb"),
    L $ Label "fb",
    O $ SubI 0 (Reg "r2"),
    T $ Halt
  ]
test_hoopl_6 = let
    p = [block_cprop_in_0, block_cprop_in_1, block_cprop_in_2]
    p' :: (H.Graph (Node Instruction) H.C H.C) = 
      H.runSimpleUniqueMonad $ H.runWithFuel H.infiniteFuel $ 
        (transform p :: H.SimpleFuelMonad (H.Graph (Node Instruction) H.C H.C))
    unP' :: [Instruction] = fromHoopl p'
  in unP' @?= block_cprop_out
  where
    transform :: (H.CheckpointMonad m, H.FuelMonad m, H.UniqueMonad m) => [[Instruction]] -> m (H.Graph (Node Instruction) H.C H.C)
    transform prog = do
      (hlms, ps) <- liftM unzip $ forM prog toHoopl
      let hlm = Map.unions hlms
          p = foldl (H.|*><*|) H.emptyClosedGraph ps
          hooplLabelFor = fromJust . flip Map.lookup hlm
          eLabel = hooplLabelFor $ Label "entry"
          registers = ["r0", "r1", "r2", "r3"]
      p' <- runConstProp registers hooplLabelFor eLabel p
      return p'

    constLattice :: H.DataflowLattice ConstFact
    constLattice = H.DataflowLattice {
        H.fact_name = "Register Contents",
        H.fact_bot = Map.empty,
        H.fact_join = H.joinMaps (H.extendJoinDomain constFactAdd)
      }
      where
        constFactAdd _ (H.OldFact old) (H.NewFact new) =
          if new == old then (H.NoChange, H.PElem new) else (H.SomeChange, H.Top)

    -- initially all registers have unknown contents
    initFact :: [Register] -> ConstFact
    initFact regs = Map.fromList $ [(r, H.Top) | r <- regs]

    -- transfer function: register value is a constant
    regIsConstant :: (Label -> H.Label) -> H.FwdTransfer (Node Instruction) ConstFact
    regIsConstant hooplLabelFor = H.mkFTransfer rc
      where
        rc :: Node Instruction e x -> ConstFact -> H.Fact x ConstFact
        rc (NodeInit _ _) f = f
        -- subtracting a register from itself yields zero
        rc (NodeCont (O (Sub (Reg a) (Reg b)))) f =
          if a == b then Map.insert a (H.PElem 0) f else f
        rc (NodeCont (O (Sub _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O (SubI _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O (SubM _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O (Load _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O (Store _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O (CmpEq _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O (CmpLt _ (Reg x)))) f = Map.insert x H.Top f
        rc (NodeCont (O _)) f = f
        rc (NodeTerm (T Halt) _) f = H.mkFactBase constLattice []
        rc (NodeTerm (T (Branch l)) _) f = H.mapSingleton (hooplLabelFor l) f
        -- if we take the false branch of a CondBranch then the condition register contains zero
        rc (NodeTerm (T (CondBranch (Reg x) tl fl)) _) f =
          H.mkFactBase constLattice [(hooplLabelFor tl, f), (hooplLabelFor fl, Map.insert x (H.PElem 0) f)]

    -- rewrite function: replace use of reg with constant contents
    constProp :: forall m. H.FuelMonad m => (Label -> H.Label) -> H.FwdRewrite m (Node Instruction) ConstFact
    constProp hooplLabelFor = H.mkFRewrite cp
      where
        cp :: Node Instruction e x -> ConstFact -> m (Maybe (H.Graph (Node Instruction) e x))
        cp node f = return $ rw hooplLabelFor (lookup f) node
        rw :: (Label -> H.Label) -> (Register -> Maybe Integer) -> Node Instruction e x -> (Maybe (H.Graph (Node Instruction) e x))
        rw hooplLabelFor valueOf inst = case inst of
          -- if we see a subtract with constant, turn it into a SubI
          (NodeCont (O (Sub (Reg x) (Reg y)))) ->
            case (valueOf x, valueOf y) of
              (Just xi, _) -> Just $ H.mkMiddle $ NodeCont $ O $ SubI xi (Reg y)
              (_, Just yi) -> Just $ H.mkMiddle $ NodeCont $ O $ SubI yi (Reg x)
              _ -> Nothing
          -- if we see a CondBranch on a constant, turn it into a Branch
          (NodeTerm (T (CondBranch (Reg x) tl fl)) _) ->
            case (valueOf x) of
              (Just xi) -> if 0 == xi
                then Just $ H.mkLast $ NodeTerm (T $ Branch fl) [hooplLabelFor fl]
                else Just $ H.mkLast $ NodeTerm (T $ Branch tl) [hooplLabelFor tl]
              _ -> Nothing
          _ -> Nothing
        lookup :: ConstFact -> Register -> Maybe Integer
        lookup f x = case Map.lookup x f of
          Just (H.PElem v) -> Just v
          _ -> Nothing

    constPropPass :: H.FuelMonad m => (Label -> H.Label) -> H.FwdPass m (Node Instruction) ConstFact
    constPropPass hooplLabelFor = H.FwdPass {
        H.fp_lattice = constLattice,
        H.fp_transfer = regIsConstant hooplLabelFor,
        H.fp_rewrite = constProp hooplLabelFor
      }

    runConstProp :: (H.CheckpointMonad m, H.FuelMonad m) => [Register] -> (Label -> H.Label) -> H.Label -> (H.Graph (Node Instruction) H.C H.C) -> m (H.Graph (Node Instruction) H.C H.C)
    runConstProp registers hooplLabelFor entry graph = do
      (graph', _, _) <- H.analyzeAndRewriteFwd (constPropPass hooplLabelFor) (H.JustC [entry]) graph (H.mapSingleton entry $ initFact registers)
      return graph'

HUnit输出

hoopl_6: [Failed] expected: [L (Label "entry"),O (Sub (Reg "r0") (Reg "r0")),T (Branch (Label "fb")),L (Label "fb"),O (SubI 0 (Reg "r2")),T Halt] but got: [L (Label "entry"),O (Sub (Reg "r0") (Reg "r0")),T (Branch (Label "fb"))]

内容的提问来源于stack exchange，提问作者andrew-wja

Hoopl图构建与不可达块误判问题排查求助

1. 先确认图构建的正确性 #

2. 检查数据流分析的逻辑 #

传递函数的问题 #

初始事实的传递 #

3. 重写阶段的逻辑验证 #

4. 调试技巧 #

测试代码与HUnit结果 #

测试代码 #

HUnit输出 #