runtimeverification / wasm-semantics

A Prototype Formal Semantics of WebAssembly in K
Other
77 stars 19 forks source link

Try to use the bison parser for `kwasm kast` #671

Closed gtrepta closed 1 month ago

gtrepta commented 1 month ago

Some of the unparseable tests in the wasm conformance tests are failing because the java parser invoked by kast runs out of memory while trying to parse them.

This changes the command kwasm kast to try to use the bison generated parser_PGM to parse in the webassembly file into kore first, which is able to handle most of the OOM cases. This gets us a few more wasm tests passing.

The only test that still OOMs even with the bison parser is br_table.wast