Unexpected behavior of the instruction `memory.init`

[erxiaozhou]

trafficstars

Introduction

I executed the test case containing a memory.init instruction and found that warm failed to raise an exception as expected.

Build commands

I compile the code with commit id 892a94fd05f2e95fc68535d763bf67ab1b8e6263. Platform: Ubuntu 20.04 CPU: amd64

Here we take the warm on JIT mode for example. This issue also exists in warm on other modes (classic interpreter mode, fast interpreter mode, fast JIT mode, multi JIT mode).

compile:

export CC=/usr/lib/llvm-16/bin/clang
export CXX=/usr/lib/llvm-16/bin/clang++
cd product-mini/platforms/linux/;rm -rf build
cmake -DWAMR_BUILD_AOT=1 -DWAMR_BUILD_FAST_JIT=1   -DWAMR_BUILD_REF_TYPES=1 -DCMAKE_BUILD_TYPE=Release  -DWASM_ENABLE_BULK_MEMORY=1 -DWAMR_BUILD_LIBC_WASI=0 -DWAMR_BUILD_LIBC_BUILTIN=1 -DWAMR_BUILD_SIMD=1  -Bbuild

iwasm --heap-size=0  --fast-jit -f to_test <tc_name>

Case

all_wamr_memory.init_no_exception2.zip

Actual output:

No exception

Expected output:

There is an exception indicating "out of bounds memory access".

According to line 16 in the specification, there should be an exception because the d+s in the test case is 9, and is greater than the length of data.data.

https://webassembly.github.io/spec/core/bikeshed/#memory-instructions%E2%91%A4

[wenyongh]

Hi, thanks for spotting this, it really makes confusing, here s is 9, n is 0, and the length of data.data is 9 (note that the data segment index is 2, see below), so s+n = 9 + 0 = 9, it isn't larger than 9 and doesn't violate the spec. I guess that some runtimes may think that s = 9 is out of range of data.data, no matter whether n is 0 or not. Since the algorithm may affect opcode memory.fill/memory.copy/memory.init/table.fill/table.copy/table.init, we had better check it carefully.

Data[3]:
 - segment[0] memory=0 size=8 - init i32=8
  - 0000008: 0102 0304 0506 0708                      ........
 - segment[1] memory=0 size=9 - init i32=16
  - 0000010: 0102 0304 0506 0708 ff                   .........
 - segment[2] memory=0 size=9 - init i32=32
  - 0000020: 0102 0304 0506 0708 ff                   .........

Code Disassembly:

00011d func[0] <to_test>:
 00011e: 01 7f                      | local[4] type=i32
 000120: 01 7d                      | local[5] type=f32
 000122: 01 7e                      | local[6] type=i64
 000124: 01 7c                      | local[7] type=f64
 000126: 41 00                      | i32.const 0
 000128: 41 09                      | i32.const 9
 00012a: 41 00                      | i32.const 0
 00012c: fc 08 02 00                | memory.init 2 0
 000130: 0b                         | end

[erxiaozhou]

Hi, thanks for spotting this, it really makes confusing, here s is 9, n is 0, and the length of data.data is 9 (note that the data segment index is 2, see below), so s+n = 9 + 0 = 9, it isn't larger than 9 and doesn't violate the spec. I guess that some runtimes may think that s = 9 is out of range of data.data, no matter whether n is 0 or not. Since the algorithm may affect opcode memory.fill/memory.copy/memory.init/table.fill/table.copy/table.init, we had better check it carefully.

Data[3]:
 - segment[0] memory=0 size=8 - init i32=8
  - 0000008: 0102 0304 0506 0708                      ........
 - segment[1] memory=0 size=9 - init i32=16
  - 0000010: 0102 0304 0506 0708 ff                   .........
 - segment[2] memory=0 size=9 - init i32=32
  - 0000020: 0102 0304 0506 0708 ff                   .........

Code Disassembly:

00011d func[0] <to_test>:
 00011e: 01 7f                      | local[4] type=i32
 000120: 01 7d                      | local[5] type=f32
 000122: 01 7e                      | local[6] type=i64
 000124: 01 7c                      | local[7] type=f64
 000126: 41 00                      | i32.const 0
 000128: 41 09                      | i32.const 9
 00012a: 41 00                      | i32.const 0
 00012c: fc 08 02 00                | memory.init 2 0
 000130: 0b                         | end

Thank you for your nice reply. You are right, n+d is not larger than the length of data[2]. I will continue to determine the root cause, thank you!

[erxiaozhou]

https://github.com/WebAssembly/bulk-memory-operations/blob/master/proposals/bulk-memory-operations/Overview.md

Hi, I found another possible root cause for the difference. I found the instruction memory.init is designed to copy the passive data to the linear memory. However, in my case, the data section is defined as active. Therefore, the data section defined in my case should be dropped. Interesting ...

An active segment is equivalent to a passive segment, but with an implicit memory.init followed by a data.drop (or table.init followed by a elem.drop) that is prepended to the module's start function.

[erxiaozhou]

https://github.com/WebAssembly/bulk-memory-operations/blob/master/proposals/bulk-memory-operations/Overview.md

Hi, I found another possible root cause for the difference. I found the instruction memory.init is designed to copy the passive data to the linear memory. However, in my case, the data section is defined as active. Therefore, the data section defined in my case should be dropped. Interesting ...

An active segment is equivalent to a passive segment, but with an implicit memory.init followed by a data.drop (or table.init followed by a elem.drop) that is prepended to the module's start function.

@wenyongh Hi, will WAMR drop the active data section after triggering the start function in the future?

[wenyongh]

@erxiaozhou thanks for the detailed investigation, it is really an issue, I submitted PR #3081 and added my understanding in the comments, please help check whether my understanding is correct. The PR makes the wasm file in this issue also throw exception like other runtimes. There may be more scenarios to test, it will be highly appreciated if you can help test them with more cases.

[erxiaozhou]

Thank you for your reply! I will try to test it these days.

[wenyongh]

Thanks, as the spec tests pass and this case works, I merged the PR.

[erxiaozhou]

Hi, the bug has not been triggered again in my testing. It looks good.