interpreter: evaluate const-expr data/elem segment offsets at instantiation - #150
Merged
Conversation
…iation An active data or element segment whose offset is a non-literal constant expression (`global.get`, extended-const arithmetic) was decoded with a `0` placeholder, so the segment landed at offset 0 instead of the computed offset. Keep the parsed const-expr program in a new `offsetExpr` field on `DataSegment` / `ElementSegment` (mirroring `GlobalDecl.initExpr`). `Module.initialStore` defers such segments, and a new instantiation pass `Module.runActiveSegments` — run after `Module.runConstGlobals`, so the offsets see the evaluated (and imported) globals — evaluates each `offsetExpr` and writes the segment at the computed offset. Wired into the testsuite driver and the runner. Testsuite: data.wast/elem.wast lose all 8 offset-related decode errors and 4 downstream assert_return failures; 11 assert_invalid commands that were rejected only because the decoder choked on non-literal offsets now decode and move to the standard not-rejected skip bucket. Closes #101 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
|
Verifier report preview: https://talos-verifier-report-pr-150.vercel.app (This URL is stable for this PR — it always points to the latest build of 9869340.) |
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 #101.
A data or element segment whose offset is a
global.get(or extended-const arithmetic) const-expr was placed at offset0: the decoder folded non-literal offset expressions to a0placeholder, so the offset was never evaluated at instantiation.Change
Wasm.DataSegment/Wasm.ElementSegmentgain anoffsetExpr : Program := []field, mirroringGlobalDecl.initExpr. The WAT decoder keeps the parsed const-expr program (wrapped(offset …)and bare abbreviated forms) instead of collapsing it to0;offset := some 0remains as the active-segment marker.Module.initialStoreskips segments with a pendingoffsetExpr— their offset depends on the store (imported globals), so they cannot be written there.Module.runActiveSegments(Semantics.lean) evaluates each pendingoffsetExpragainst the current store and writes the segment at the computed offset — data bytes into the right (multi-)memory, funcref/GC-item elements into the right table slot. It runs afterModule.runConstGlobals, so offsets see the evaluated and imported globals;runConstElemsskips these segments to avoid double-writing.Testsuite/Exec.lean) and the runner (Runner.lean).Examples/SegmentOffsetExpr.leanis the regression test: the issue's exact scenario (data atglobal.get $o = 4, elem atglobal.get $t = 2) proven end-to-end vianative_decide, including that byte 0 stays zero (segment moved, not duplicated).Testsuite report
testsuite_report.txtregenerated (all three packageslake buildcleanly):module decode_error→pass(data.wast 178/183/188/195, elem.wast 128/135/178/182)assert_return fail→pass(elem.wast 1065/1076/1087/1109 —call_indirectthrough a global-offset elem segment)assert_invalid pass→skipped: not rejected: ill-typed offset const-exprs (e.g.(offset (nop) …), two-value offsets) were previously rejected only because the decoder couldn't parse non-literal offsets at all; they now decode and join the existing not-validated skip bucket (data.wast already carried 25 such skips).🤖 Generated with Claude Code