Hoopl: построение графа и автоматическое удаление недостижимых блоков

Question

Я работаю над проектом с использованием библиотеки Hoopl, и я столкнулся с загвоздкой, которая указывает мне, что я не полностью понимаю, что происходит под капотом. Вкратце, Hoopl, похоже, считает некоторые блоки в моем графике недостижимыми, чего (ИМО) не должно. Я реализую разреженное условное распространение констант, поэтому я ожидаю, что некоторые блоки станут недоступными, но не все блоки! Ниже приведен пример из набора тестов HUnit, который я использую для создания прототипов. В примере используется несколько функций, которые здесь не определены, но у меня есть отдельные модульные тесты для тех, кто подтверждает, что они работают изолированно, в частности, чтоfromHoopl . toHoopl x работает как положено и так далее.

Я ожидаю, что произойдет то, что block_cprop_out должен быть результатом выполнения этого прохода, но фактический результат - это просто свернутая константой версия block_cprop_in_0: исключаются как истинная, так и ложная ветви. Результат теста HUnit находится под фрагментом кода.

Чтобы обобщить то, что я делаю на высоком уровне, я создаю закрытый / закрытый график Hoopl для каждого блока, а затем объединяю эти графики с Hoopl.|*><*|. Я использую простойData.Map для отслеживания уникальных меток, которые Hoopl назначает для пользовательских меток, чтобы, когда я переписываю Branch userlabel, Я могу изменить метку преемника Hoopl на правильный Hoopl Label. Однако кажется, что Hoopl считает, что блоки ветвления true и false здесь недостижимы, потому что после того, как я запустил этот прямой анализ и перезаписал, я получаю обратно график, содержащий только входной блок.

block_cprop_out здесь немного странно, потому что мой fromHoopl функция просто вызывает Hoopl.foldGraphNodes превратить весь Hoopl Graph a в простой [a] на проверку.

Отдельный тест подтверждает, что обход этого списка блоков одним и тем же методом построения графа (объединение закрытых / закрытых блоков) работает должным образом; похоже, что устранение недостижимых блоков запускается именноHoopl.analyzeAndRewrite{Fwd,Bwd}.

Правильно ли объединить список закрытых / закрытых блоков, как я здесь делаю? Если да, может ли кто-нибудь увидеть здесь что-нибудь подозрительное, что могло бы заставить Hoopl поверить в то, что блоки недоступны?

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
                   ] -- this block is unreachable from the CondBranch in block_cprop_in_0

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
      let p = foldl (H.|*><*|) H.emptyClosedGraph ps
      let hooplLabelFor = fromJust . flip Map.lookup hlm
      let eLabel = hooplLabelFor $ Label "entry"
      let 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"))]

Answer 1

Как оказалось, проблема действительно не в этом фрагменте кода.

Вместо того, чтобы входить в монаду сопоставления меток на верхнем уровне, я разместил отдельные вызовы runLabelMapM на листьях моего преобразования, что означало, что я случайно назначил уникальные метки Hoopl каждой пользовательской метке в моей программе, в отличие от повторного использования Hoopl метки, в которых программа повторно использовала пользовательские метки.

Конечно, это означало, что goto L3 и соответствие L3:в последующем коде отображались на разные метки Hoopl, а не на одну и ту же метку Hoopl; блоки истинной и ложной ветвей были абсолютно недоступны, потому что для Hoopl они выглядели так, как будто я написал это:

block_cprop_in_0 = [ --test for constprop
                     L $ Label "1",
                     O $ Sub (Reg "r0") (Reg "r0"),
                     T $ CondBranch (Reg "r0") (Label "2") (Label "3")
                   ]

block_cprop_in_1 = [ -- test for constprop
                     L $ Label "4",
                     O $ Sub (Reg "r1") (Reg "r0"),
                     T $ Halt
                   ] -- this block is unreachable from the CondBranch in block_cprop_in_0

block_cprop_in_2 = [ -- test for constprop
                     L $ Label "5",
                     O $ Sub (Reg "r2") (Reg "r0"), --should get rewritten as a SubI
                     T $ Halt
                   ]

Просто монадный поток в конце концов!

Для потомков вот правильный код: мне просто нужно было поднять runHooplLabelMapM вне toHoopl функция на высший уровень.

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
    convert prog = do
      ps <- forM prog (toHoopl @[] @Instruction @Label)
      let p = foldl (H.|*><*|) H.emptyClosedGraph ps
      return p

    transform :: (H.CheckpointMonad m, H.FuelMonad m, H.UniqueMonad m) => [[Instruction]] -> m (H.Graph (Node Instruction) H.C H.C)
    transform p = do
      (hlm, prog) <- runHooplLabelMapM Map.empty $ convert p
      let registers = ["r0", "r1", "r2", "r3"]
      let hooplLabelFor = fromJust . flip Map.lookup hlm
      let eLabel = hooplLabelFor $ Label "entry"
      p' <- runConstProp registers hooplLabelFor eLabel prog
      return p'

...