<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><span class=""><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>One is essentially covering input diversity, the other has to cover *output* diversity, and must prove the negative. We fundamentally must gain confidence that the pass *never* produces unreachable IR. This seems much harder than demonstrating that it does handle unreachable IR.</div><div><br></div></div></blockquote></span></div></div></div></blockquote><div>Missed a spot :)</div><div><br></div><div>Except, in this case, output diversity is finite (each pass has a limited set of ways it can produce unreachable code, and unreachable code is not valid input to the next pass) , but input diversity is pretty much infinite, because you need to know *all* possible unreachable code that could be produced by all passes combined (since unreachable code is a valid input into each pass, you are testing the combination of all possible unreachable code transforms by any order of passes that could possibly exist up to that point).</div><div><br></div><div>I would much rather have the former than the latter.</div><div><br></div><div>You are also "proving the negative" either way.<br></div><div>"There is no unreachable code this does not handle vs This does not produce unreachable code"</div><div><br></div><div>BTW, one is formally verifiable, the other is pretty much not.</div><div><br></div><div>(IE i can formally verify that a pass removes all dead blocks it creates, whereas you pretty much cannot formally verify there is no set of dead input cfgs that affects an algorithm)</div><div>  </div></div></div></div>