search

wasmi-labs / wasmi

WebAssembly (Wasm) interpreter.
https://wasmi-labs.github.io/wasmi/
Apache License 2.0
1.61k stars 286 forks source link

Unexpected behavior with load/store alignment #570

Open erxiaozhou opened 1 year ago

erxiaozhou commented 1 year ago

Description

Current State

Output: 65508521924046110000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000

Expected

An exception indicating that "alignment must not be larger than natural"

Environment

Steps to Reproduce

wasmi.zip

  1. build the wasmi
  2. run the test case by wasmi <test_case_name> to_test
Robbepop commented 1 year ago

Hmmm as with the other issue running Wasmtime results in the same output without your expected exception. Can you elaborate what you used to verify that your expected output is as specified by the Wasm standard?

erxiaozhou commented 1 year ago

Hmmm as with the other issue running Wasmtime results in the same output without your expected exception. Can you elaborate what you used to verify that your expected output is as specified by the Wasm standard?

Thank you four your reply. On Wasmedge, there is a validation error "alignment must not be larger than natural". On iwasm (from https://github.com/bytecodealliance/wasm-micro-runtime), there is an error "alignment must not be larger than natural". There is also an error on wasmer

Robbepop commented 1 year ago

Okay thanks for letting me know about all these other runtimes. Can you verify though that Wasmtime also has this same behavior as wasmi? (Just in case I did something wrong there.)

erxiaozhou commented 1 year ago

Okay thanks for letting me know about all these other runtimes. Can you verify though that Wasmtime also has this same behavior as wasmi? (Just in case I did something wrong there.)

On my computer, the wasmtime can output the same thing. as wasmi·

Robbepop commented 1 year ago

I was reading about memory load and store operation alignment semantics in Wasm and found this explanation: https://rsms.me/wasm-intro#addressing-memory

So according to this source it seems to me that wasmi and Wasmtime behavior is actually correct.

Robbepop commented 1 year ago

@erxiaozhou it would be nice to know if you agree with my interpretation or disagree so we can either close this or find an agreement.

erxiaozhou commented 1 year ago

@erxiaozhou it would be nice to know if you agree with my interpretation or disagree so we can either close this or find an agreement.

Thank you for your nice reply. I'm reading the explanation link, and I'll decide my opinion in a few hours. So I wish you could wait for me for hours, thank you!

erxiaozhou commented 1 year ago

@erxiaozhou it would be nice to know if you agree with my interpretation or disagree so we can either close this or find an agreement.

reply_wasmi_570.zip Thank you for your patient reply. I prepare a shorter test case in the zip. The wat code corresponding to the function to_test in wasmi_unexpected.wasm is as follows. (The steps to generate this test case is also attached)

    (local i32 f32 i64 f64)
    f64.const 1.0
    br 0
    unreachable
    i64.store offset=0 align=0x40
    drop

There is no error when I execute wasmi_cli wasmi_unexpected.wasm to_test. However, it seems there is supposed to be an error because the memarg.align of i64.store is 0x40. Because according to the specification, the alignment must not be larger than the bit width of 𝑡 divided by 8 and 0x40 is greater than 64/8. https://webassembly.github.io/spec/core/valid/instructions.html#memory-instructions

image

I am looking forward to your reply, thank you!

Robbepop commented 1 year ago

Hmmm, if this is true then it might imply a bug in the wasmparser crate with its Wasm validation infrastructure that we are also using in wasmi. Seems to be a check that should exist at Wasm validation time indeed. Maybe it is not checked due to being unreachable? At least in wasmi we tend to ignore code that we know is unreachable. However, unreachable code is still validated.

For i64.store as in your example the maximum allowed value for the alignment parameter is 3 since alignment is given as 2^align therefore a value of 3 is 2^3 = 8. I just checked the wasmparser code and can verify that it looks as if they do not miss any alignment checks.

erxiaozhou commented 1 year ago

Hmmm, if this is true then it might imply a bug in the wasmparser crate with its Wasm validation infrastructure that we are also using in wasmi. Seems to be a check that should exist at Wasm validation time indeed. Maybe it is not checked due to being unreachable? At least in wasmi we tend to ignore code that we know is unreachable. However, unreachable code is still validated.

For i64.store as in your example the maximum allowed value for the alignment parameter is 3 since alignment is given as 2^align therefore a value of 3 is 2^3 = 8. I just checked the wasmparser code and can verify that it looks as if they do not miss any alignment checks.

reply_wasmi_570_2.zip

Thank you for your insights and patient reply! I have tried different values for the byte which represents memarg.align. I found an interesting phenomenon when I set the value of this byte to 4 (i.e., the test case reply_570_2_expected_cannot_execution.wasm), the program throws an exception as expected and when I set the value of that byte to 0x40 (i.e., the test case replay_570_2_unexpected_execution.wasm), no exception is thrown.

Robbepop commented 1 year ago

Interestingly trying to turn the Wasm file into a .wat file is also not possible due to the following error:

> wasm2wat replay_570_2_unexpected_execution.wasm -o replay_570_2_unexpected_execution.wat
0000046: error: invalid store alignment: 64

In this case 64 refers to the given 0x40 argument in decimal formatting. This really looks like something in Wasm validation is wrong somewhere. Note that Wasm validation is not done by wasmi but by the wasmparser crate used by wasmi.

Robbepop commented 1 year ago

@erxiaozhou I just tried your provided wasmi_unexpected.wasm with the most recent version of wasmi_cli and now it properly fails as expected denying the invalid alignment value. I guess the bug in wasmparser has been fixed and we updated to the fixed version in the meantime.

@erxiaozhou Can you confirm this so that we can close this issue?

I tested with version 0.26.0 of wasmi_cli. Get it with:

cargo install wasmi_cli

And also the current wasmi_cli on master.

Robbepop commented 1 year ago

Strongly connected to this Wasmtime issue: https://github.com/bytecodealliance/wasmtime/issues/5344

Robbepop commented 1 month ago

The linked Wasmtime issue was just triaged and found to be fixed. (https://github.com/bytecodealliance/wasmtime/issues/5344#issuecomment-2395603696)

Thus, once we update to the new wasmparser version we should have this fix ready for Wasmi as well. (if it isn't already fixed)