interpreter: accept folded GC allocator global initializers in the WAT decoder - #148
Merged
Merged
Conversation
…T decoder The global-decl parser detected GC heap-allocating initializers (struct.new / array.new*) by scanning only the top-level atoms of the initializer sexpr, so the folded leaf form (struct.new $s (i32.const 100)) slipped past the check, fell through to the literal-folding shape match, and was rejected with 'global init expression must be i32.const or i64.const'. The same allocation wrapped in extended-const arithmetic was accepted, because the extended-const scan does recurse into folded operands. Generalize the recursive sexpr scan into initExprMentions and use it for both the extended-const detection and a new initExprAllocates predicate, so GC allocators are detected in both the flat form emitted by wasm-tools print and the folded form. Adds regression theorems in Examples/GlobalInitExpr exercising the exact repro from the issue: the leaf and arithmetic-wrapped struct.new initializers both decode and evaluate to a struct whose field reads back as 100. Fixes #109 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
|
Verifier report preview: https://talos-verifier-report-pr-148.vercel.app (This URL is stable for this PR — it always points to the latest build of 182e808.) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #109.
Problem
A global initialized with a plain folded GC allocation was rejected:
The global-decl parser detected GC heap-allocating initializers (
struct.new/array.new*) by scanning only the top-level atoms of the initializer sexpr — which matches the flat form emitted bywasm-tools printbut not the folded leaf form, where the allocator atom sits inside a(...)list. The folded form fell through to the literal-folding shape match and errored. The arithmetic-wrapped variant was accepted only because the extended-const scan does recurse into folded operands and routed it to the const-expr path.Fix
Generalize the existing recursive sexpr scan into
initExprMentions (p : String → Bool)and use it for both:initExprNeedsEval(extended-const /global.get) — unchanged behaviour, now defined via the shared scanner, andinitExprAllocates(struct.new,struct.new_default,array.new,array.new_default,array.new_fixed,array.new_data,array.new_elem) that replaces the top-level-only check, so GC allocators are detected in both the flat and the folded form and kept as a const-expr program forModule.runConstGlobals.Tests
New regression theorems in
Interpreter/Wasm/Examples/GlobalInitExpr.leanusing the exact repro modules from the issue:leaf_struct_new_keeps_initExpr— the leaf form decodes (no error) and keeps itsinitExpr,leaf_struct_new_returns_100/arith_struct_new_returns_100— end-to-end,struct.geton the global returns100for both forms.lake buildof theinterpreterpackage passes (3056 jobs, includes thenative_decidechecks above).🤖 Generated with Claude Code