Drop dangling holes in EliminateHoles#862
Conversation
In elimStmtList, holes that are non-last statements in a block are now dropped instead of being processed. Only the last statement in a block is allowed to be a hole (and gets the normal elimination treatment). Closes #860
|
Can you add an option in |
Add a dropDanglingHoles flag (default false) to LaurelTranslateOptions that controls whether non-last Hole statements in a block are dropped during eliminateHoles. Enable it in the PythonToLaurel pipeline.
|
Done — pushed in 645104d. Here's what changed:
Full build passes including |
| counter : Nat := 0 | ||
| currentInputs : List Parameter := [] | ||
| generatedFunctions : List Procedure := [] | ||
| dropDanglingHoles : Bool := false |
There was a problem hiding this comment.
How can dropping holes be sound? I don't understand. Are these just values that are never returned?
There was a problem hiding this comment.
Good question. The "dangling holes" being dropped here are holes that appear as non-last statements in a block — i.e., they're in statement position but not in tail position. Since a Hole in statement position doesn't produce a value that's used by anything (it's not assigned to a variable, not returned, not passed as an argument), it has no observable effect on the program's semantics.
Concretely, consider a block like:
{
Hole // ← dangling: statement position, value unused
x := 1
return x
}
The hole here is dead code — its "value" is discarded. Normally elimStmt would still replace it with a call to a fresh uninterpreted function, which is harmless but adds noise (an extra function that the verifier has to reason about for no benefit).
When dropDanglingHoles is true, these dead-code holes are simply removed. The last statement in a block is always kept and processed normally, since that's the one whose value may actually matter (e.g., as the block's return value).
This is only enabled in the PythonToLaurel pipeline (translateCombinedLaurelWithLowered), where the translation from Python can produce these dangling holes as artifacts. It's off by default for other uses.
I didn't author the original issue requirement (#860) though — @keyboardDrummer can confirm whether there are additional soundness considerations I'm missing.
There was a problem hiding this comment.
Great explanation, thanks @keyboardDrummer-bot ^^^
There was a problem hiding this comment.
Happy to help! Let me know if there's anything else to address on this PR — I noticed it has a git conflicts label, so I can rebase onto main if you'd like.
3 participants
In
elimStmtList, holes that are non-last statements in a block are now dropped instead of being processed. Only the last statement in a block is allowed to be a hole (and gets the normal elimination treatment).The change is in
elimStmtListwithin the mutual block. Instead ofstmts.mapM elimStmt, it now pattern-matches on the list:This integrates naturally with the mutual recursion termination proof since each recursive call is on a structurally smaller list.
Closes #860