Fix with-block variable scoping in Python-to-Laurel translation#680
Fix with-block variable scoping in Python-to-Laurel translation#680MikaelMayer merged 5 commits intomainfrom
Conversation
Python with-blocks placed variable declarations inside a Laurel Block, which scopes them in Core. Multiple with-blocks reusing the same variable name caused a 'Cannot havoc undeclared variable' type-checking error because the second block generated a havoc for a variable not declared at the outer Core scope. Hoist manager and as-variable declarations out of the Block, matching Python scoping where with-block variables remain visible after the block ends. Add test for multiple with-blocks with the same variable.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Clean fix that correctly hoists with-block variable declarations to the outer scope, matching Python's scoping semantics and the pattern already used by try/except. The separation into declStmts (outside block) vs setupStmts (inside block) is clear and well-structured. Test covers the exact failure scenario.
One potential follow-up noted inline (not blocking).
This comment was marked as resolved.
This comment was marked as resolved.
|
Could you please check whether this PR overlaps with this one #639. |
|
Checked — PR #639 also fixes this bug. I checked out #639, added this PR's test, and it passes. #639 takes a more comprehensive approach (hoisting all declarations to function top), while this PR is a targeted fix for the |
4 participants
Fix
withstatement variable scoping in Python-to-Laurel translationPython
withblocks (e.g.,with open(...) as f:) were placing variable declarations inside a LaurelBlock, which scopes them in Core. When a function contained multiplewithblocks reusing the same variable name, the second block would generate ahavocfor a variable that wasn't declared at the outer Core scope, causing a "Cannot havoc undeclared variable" type-checking error.The fix hoists the manager and
as-variable declarations out of theBlock, matching Python's scoping semantics wherewith-block variables remain visible after the block ends.New test added in
VerifyPythonTest.leanexercising multiplewithblocks with the same variable name.