Unexpected behavior of the instruction `memory.init` #3020

erxiaozhou · 2024-01-15T17:40:39Z

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 892a94f.
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

The text was updated successfully, but these errors were encountered:

wenyongh · 2024-01-16T03:45:11Z

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 · 2024-01-16T05:31:23Z

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 · 2024-01-21T18:01:26Z

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 · 2024-01-24T07:53:47Z

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 · 2024-01-25T01:53:46Z

@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 · 2024-01-25T18:08:55Z

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

According to the wasm core spec, the checks for the table segments in `table.init` opcode are similar to the checks for `memory.init` opcode: - The size of a passive segment is shrunk to zero after `data.drop` (or `elem.drop`) opcode is executed, and the segment can be used to do `memory.init` (or `table.init`) again - The `memory.init` only traps when `s+n > len(data.data)` or `d+n > len(mem.data)` and `table.init` only traps when `s+n > len(elem.elem)` or `d+n > len(tab.elem)` - The active segment can also be used to do `memory.init` (or `table.init`), while it behaves like a dropped passive segment https://github.com/WebAssembly/bulk-memory-operations/blob/master/proposals/bulk-memory-operations/Overview.md ``` Segments can also be shrunk to size zero by using the following new instructions: - data.drop: discard the data in an data segment - elem.drop: discard the data in an element segment 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. ``` ps. https://webassembly.github.io/spec/core/bikeshed/#-hrefsyntax-instr-memorymathsfmemoryinitx%E2%91%A0 https://webassembly.github.io/spec/core/bikeshed/#-hrefsyntax-instr-tablemathsftableinitxy%E2%91%A0 #3020

wenyongh · 2024-01-26T01:47:08Z

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

erxiaozhou · 2024-02-04T17:55:29Z

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

…lliance#3081) According to the wasm core spec, the checks for the table segments in `table.init` opcode are similar to the checks for `memory.init` opcode: - The size of a passive segment is shrunk to zero after `data.drop` (or `elem.drop`) opcode is executed, and the segment can be used to do `memory.init` (or `table.init`) again - The `memory.init` only traps when `s+n > len(data.data)` or `d+n > len(mem.data)` and `table.init` only traps when `s+n > len(elem.elem)` or `d+n > len(tab.elem)` - The active segment can also be used to do `memory.init` (or `table.init`), while it behaves like a dropped passive segment https://github.com/WebAssembly/bulk-memory-operations/blob/master/proposals/bulk-memory-operations/Overview.md ``` Segments can also be shrunk to size zero by using the following new instructions: - data.drop: discard the data in an data segment - elem.drop: discard the data in an element segment 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. ``` ps. https://webassembly.github.io/spec/core/bikeshed/#-hrefsyntax-instr-memorymathsfmemoryinitx%E2%91%A0 https://webassembly.github.io/spec/core/bikeshed/#-hrefsyntax-instr-tablemathsftableinitxy%E2%91%A0 bytecodealliance#3020

wenyongh mentioned this issue Jan 16, 2024

Unexpected behavior of the instruction table.init #3023

Closed

erxiaozhou closed this as completed Jan 17, 2024

erxiaozhou reopened this Jan 21, 2024

wenyongh mentioned this issue Jan 25, 2024

Fix memory/table segment checks in memory.init/table.init #3081

Merged

wenyongh closed this as completed Apr 29, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Unexpected behavior of the instruction `memory.init` #3020

Unexpected behavior of the instruction `memory.init` #3020

erxiaozhou commented Jan 15, 2024

wenyongh commented Jan 16, 2024

erxiaozhou commented Jan 16, 2024

erxiaozhou commented Jan 21, 2024

erxiaozhou commented Jan 24, 2024

wenyongh commented Jan 25, 2024

erxiaozhou commented Jan 25, 2024

wenyongh commented Jan 26, 2024

erxiaozhou commented Feb 4, 2024

Unexpected behavior of the instruction memory.init #3020

Unexpected behavior of the instruction memory.init #3020

Comments

erxiaozhou commented Jan 15, 2024

Introduction

Build commands

Case

Actual output:

Expected output:

wenyongh commented Jan 16, 2024

erxiaozhou commented Jan 16, 2024

erxiaozhou commented Jan 21, 2024

erxiaozhou commented Jan 24, 2024

wenyongh commented Jan 25, 2024

erxiaozhou commented Jan 25, 2024

wenyongh commented Jan 26, 2024

erxiaozhou commented Feb 4, 2024

Unexpected behavior of the instruction `memory.init` #3020

Unexpected behavior of the instruction `memory.init` #3020