Fix table imports and checks for data segments

runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K

Other

77 stars 19 forks source link

Fix table imports and checks for data segments #680

Closed gtrepta closed 1 month ago

gtrepta commented 1 month ago

When instantiating a data segment, we weren't checking that the segment doesn't go out of bounds of the memory in the module.

When importing a table, we weren't using the <nextTabIdx> cell to allow multiple imports.

This change fixes these two issues.

gtrepta commented 1 month ago

FWIW, tests would be nice.

The linking.wast test revealed these two issues and I'm removing it from the unsupported-llvm list in this PR. Introducing some more unit-like tests with pytest would be good, but I probably can't start that effort now since I'll be moving to soroban soon.