Skip to content
This repository was archived by the owner on Nov 3, 2021. It is now read-only.

[exec] Bounds check bulk-memory before execution #123

Merged
merged 2 commits into from
Nov 14, 2019
Merged

[exec] Bounds check bulk-memory before execution #123

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2be0b11
[exec] Bounds check bulk-memory before execution
eqrion Nov 4, 2019
766a295
[spec] Fix prose text for mem/tab.init with dropped segments
eqrion Nov 6, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 20 additions & 20 deletions document/core/exec/instructions.rst
View file
Original file line number Diff line number Diff line change
@@ -730,25 +730,25 @@ Memory Instructions

9. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[\X{da}]`.

10. If :math:`\X{data}^? = \epsilon`, then:
10. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

a. Trap.
11. Pop the value :math:`\I32.\CONST~cnt` from the stack.

11. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
12. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

12. Pop the value :math:`\I32.\CONST~cnt` from the stack.
13. Pop the value :math:`\I32.\CONST~src` from the stack.

13. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
14. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

14. Pop the value :math:`\I32.\CONST~src` from the stack.
15. Pop the value :math:`\I32.\CONST~dst` from the stack.

15. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
16. If :math:`cnt = 0`, then:

16. Pop the value :math:`\I32.\CONST~dst` from the stack.
a. Return.

17. If :math:`cnt = 0`, then:
17. If :math:`\X{data}^? = \epsilon`, then:

a. Return.
a. Trap.

18. If :math:`cnt = 1`, then:

@@ -1091,25 +1091,25 @@ Table Instructions

9. Let :math:`\X{elem}^?` be the optional :ref:`element instance <syntax-eleminst>` :math:`S.\SELEM[\X{ea}]`.

10. If :math:`\X{elem}^? = \epsilon`, then:
10. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

a. Trap.
11. Pop the value :math:`\I32.\CONST~cnt` from the stack.

11. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
12. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

12. Pop the value :math:`\I32.\CONST~cnt` from the stack.
13. Pop the value :math:`\I32.\CONST~src` from the stack.

13. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
14. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

14. Pop the value :math:`\I32.\CONST~src` from the stack.
15. Pop the value :math:`\I32.\CONST~dst` from the stack.

15. Assert: due to :ref:`validation <valid-table.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
16. If :math:`cnt = 0`, then:

16. Pop the value :math:`\I32.\CONST~dst` from the stack.
a. Return.

17. If :math:`cnt = 0`, then:
17. If :math:`\X{elem}^? = \epsilon`, then:

a. Return.
a. Trap.

18. If :math:`cnt = 1`, then:

114 changes: 64 additions & 50 deletions interpreter/exec/eval.ml
View file
Original file line number Diff line number Diff line change
@@ -117,9 +117,27 @@ let drop n (vs : 'a stack) at =
* c : config
*)

let const_i32_add i j at msg =
let k = I32.add i j in
if I32.lt_u k i then Trapping msg else Plain (Const (I32 k @@ at))
let mem_oob frame x i n =
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(Memory.bound (memory frame.inst x))

let data_oob frame x i n =
match !(data frame.inst x) with
| None -> false
| Some bs ->
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64.of_int_u (String.length bs))

let table_oob frame x i n =
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64_convert.extend_i32_u (Table.size (table frame.inst x)))

let elem_oob frame x i n =
match !(elem frame.inst x) with
| None -> false
| Some es ->
I64.gt_u (I64.add (I64_convert.extend_i32_u i) (I64_convert.extend_i32_u n))
(I64.of_int_u (List.length es))

let rec step (c : config) : config =
let {frame; code = vs, es; _} = c in
@@ -205,6 +223,10 @@ let rec step (c : config) : config =
| TableCopy, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

| TableCopy, I32 n :: I32 s :: I32 d :: vs'
when table_oob frame (0l @@ e.at) s n || table_oob frame (0l @@ e.at) d n ->
vs', [Trapping (table_error e.at Table.Bounds) @@ e.at]

(* TODO: turn into small-step, but needs reference values *)
| TableCopy, I32 n :: I32 s :: I32 d :: vs' ->
let tab = table frame.inst (0l @@ e.at) in
@@ -214,6 +236,10 @@ let rec step (c : config) : config =
| TableInit x, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

| TableInit x, I32 n :: I32 s :: I32 d :: vs'
when table_oob frame (0l @@ e.at) d n || elem_oob frame x s n ->
vs', [Trapping (table_error e.at Table.Bounds) @@ e.at]

(* TODO: turn into small-step, but needs reference values *)
| TableInit x, I32 n :: I32 s :: I32 d :: vs' ->
let tab = table frame.inst (0l @@ e.at) in
@@ -233,22 +259,22 @@ let rec step (c : config) : config =

| Load {offset; ty; sz; _}, I32 i :: vs' ->
let mem = memory frame.inst (0l @@ e.at) in
let addr = I64_convert.extend_i32_u i in
let a = I64_convert.extend_i32_u i in
(try
let v =
match sz with
| None -> Memory.load_value mem addr offset ty
| Some (sz, ext) -> Memory.load_packed sz ext mem addr offset ty
| None -> Memory.load_value mem a offset ty
| Some (sz, ext) -> Memory.load_packed sz ext mem a offset ty
in v :: vs', []
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at])

| Store {offset; sz; _}, v :: I32 i :: vs' ->
let mem = memory frame.inst (0l @@ e.at) in
let addr = I64_convert.extend_i32_u i in
let a = I64_convert.extend_i32_u i in
(try
(match sz with
| None -> Memory.store_value mem addr offset v
| Some sz -> Memory.store_packed sz mem addr offset v
| None -> Memory.store_value mem a offset v
| Some sz -> Memory.store_packed sz mem a offset v
);
vs', []
with exn -> vs', [Trapping (memory_error e.at exn) @@ e.at]);
@@ -268,21 +294,17 @@ let rec step (c : config) : config =
| MemoryFill, I32 0l :: v :: I32 i :: vs' ->
vs', []

| MemoryFill, I32 1l :: v :: I32 i :: vs' ->
vs', List.map (at e.at) [
Plain (Const (I32 i @@ e.at));
Plain (Const (v @@ e.at));
Plain (Store
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
]
| MemoryFill, I32 n :: v :: I32 i :: vs'
when mem_oob frame (0l @@ e.at) i n ->
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]

| MemoryFill, I32 n :: v :: I32 i :: vs' ->
vs', List.map (at e.at) [
Plain (Const (I32 i @@ e.at));
Plain (Const (v @@ e.at));
Plain (Const (I32 1l @@ e.at));
Plain (MemoryFill);
const_i32_add i 1l e.at (memory_error e.at Memory.Bounds);
Plain (Store
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
Plain (Const (I32 (I32.add i 1l) @@ e.at));
Plain (Const (v @@ e.at));
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryFill);
@@ -291,71 +313,63 @@ let rec step (c : config) : config =
| MemoryCopy, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

| MemoryCopy, I32 1l :: I32 s :: I32 d :: vs' ->
| MemoryCopy, I32 n :: I32 s :: I32 d :: vs'
when mem_oob frame (0l @@ e.at) s n || mem_oob frame (0l @@ e.at) d n ->
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]

| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when d <= s ->
vs', List.map (at e.at) [
Plain (Const (I32 d @@ e.at));
Plain (Const (I32 s @@ e.at));
Plain (Load
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.(Pack8, ZX)});
Plain (Store
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
]

| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when d <= s ->
vs', List.map (at e.at) [
Plain (Const (I32 d @@ e.at));
Plain (Const (I32 s @@ e.at));
Plain (Const (I32 1l @@ e.at));
Plain (MemoryCopy);
const_i32_add d 1l e.at (memory_error e.at Memory.Bounds);
const_i32_add s 1l e.at (memory_error e.at Memory.Bounds);
Plain (Const (I32 (I32.add d 1l) @@ e.at));
Plain (Const (I32 (I32.add s 1l) @@ e.at));
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryCopy);
]

| MemoryCopy, I32 n :: I32 s :: I32 d :: vs' when s < d ->
vs', List.map (at e.at) [
const_i32_add d (I32.sub n 1l) e.at (memory_error e.at Memory.Bounds);
const_i32_add s (I32.sub n 1l) e.at (memory_error e.at Memory.Bounds);
Plain (Const (I32 1l @@ e.at));
Plain (Const (I32 (I32.add d 1l) @@ e.at));
Plain (Const (I32 (I32.add s 1l) @@ e.at));
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryCopy);
Plain (Const (I32 d @@ e.at));
Plain (Const (I32 s @@ e.at));
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryCopy);
Plain (Load
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.(Pack8, ZX)});
Plain (Store
{ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
]

| MemoryInit x, I32 0l :: I32 s :: I32 d :: vs' ->
vs', []

| MemoryInit x, I32 1l :: I32 s :: I32 d :: vs' ->
| MemoryInit x, I32 n :: I32 s :: I32 d :: vs'
when mem_oob frame (0l @@ e.at) d n || data_oob frame x s n ->
vs', [Trapping (memory_error e.at Memory.Bounds) @@ e.at]

| MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
(match !(data frame.inst x) with
| None ->
vs', [Trapping "data segment dropped" @@ e.at]
| Some bs when Int32.to_int s >= String.length bs ->
vs', [Trapping "out of bounds data segment access" @@ e.at]
| Some bs ->
let b = Int32.of_int (Char.code bs.[Int32.to_int s]) in
vs', List.map (at e.at) [
Plain (Const (I32 d @@ e.at));
Plain (Const (I32 b @@ e.at));
Plain (
Store {ty = I32Type; align = 0; offset = 0l; sz = Some Memory.Pack8});
Plain (Const (I32 (I32.add d 1l) @@ e.at));
Plain (Const (I32 (I32.add s 1l) @@ e.at));
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryInit x);
]
)

| MemoryInit x, I32 n :: I32 s :: I32 d :: vs' ->
vs', List.map (at e.at) [
Plain (Const (I32 d @@ e.at));
Plain (Const (I32 s @@ e.at));
Plain (Const (I32 1l @@ e.at));
Plain (MemoryInit x);
const_i32_add d 1l e.at (memory_error e.at Memory.Bounds);
const_i32_add s 1l e.at (memory_error e.at Memory.Bounds);
Plain (Const (I32 (I32.sub n 1l) @@ e.at));
Plain (MemoryInit x);
]

| DataDrop x, vs ->
let seg = data frame.inst x in
(match !seg with
23 changes: 12 additions & 11 deletions test/core/bulk.wast
View file
Original file line number Diff line number Diff line change
@@ -39,11 +39,11 @@
;; Fill all of memory
(invoke "fill" (i32.const 0) (i32.const 0) (i32.const 0x10000))

;; Out-of-bounds writes trap, but all previous writes succeed.
;; Out-of-bounds writes trap, and nothing is written
(assert_trap (invoke "fill" (i32.const 0xff00) (i32.const 1) (i32.const 0x101))
"out of bounds memory access")
(assert_return (invoke "load8_u" (i32.const 0xff00)) (i32.const 1))
(assert_return (invoke "load8_u" (i32.const 0xffff)) (i32.const 1))
(assert_return (invoke "load8_u" (i32.const 0xff00)) (i32.const 0))
(assert_return (invoke "load8_u" (i32.const 0xffff)) (i32.const 0))

;; Succeed when writing 0 bytes at the end of the region.
(invoke "fill" (i32.const 0x10000) (i32.const 0) (i32.const 0))
@@ -131,11 +131,11 @@
;; Init ending at memory limit and segment limit is ok.
(invoke "init" (i32.const 0xfffc) (i32.const 0) (i32.const 4))

;; Out-of-bounds writes trap, but all previous writes succeed.
;; Out-of-bounds writes trap, and nothing is written.
(assert_trap (invoke "init" (i32.const 0xfffe) (i32.const 0) (i32.const 3))
"out of bounds memory access")
(assert_return (invoke "load8_u" (i32.const 0xfffe)) (i32.const 0xaa))
(assert_return (invoke "load8_u" (i32.const 0xffff)) (i32.const 0xbb))
(assert_return (invoke "load8_u" (i32.const 0xfffe)) (i32.const 0xcc))
(assert_return (invoke "load8_u" (i32.const 0xffff)) (i32.const 0xdd))

;; Succeed when writing 0 bytes at the end of either region.
(invoke "init" (i32.const 0x10000) (i32.const 0) (i32.const 0))
@@ -190,6 +190,12 @@
(local.get 0)))
)

;; Out-of-bounds stores trap, and nothing is written.
(assert_trap (invoke "init" (i32.const 2) (i32.const 0) (i32.const 2))
"out of bounds table access")
(assert_trap (invoke "call" (i32.const 2))
"uninitialized element 2")

(invoke "init" (i32.const 0) (i32.const 1) (i32.const 2))
(assert_return (invoke "call" (i32.const 0)) (i32.const 1))
(assert_return (invoke "call" (i32.const 1)) (i32.const 0))
@@ -198,11 +204,6 @@
;; Init ending at table limit and segment limit is ok.
(invoke "init" (i32.const 1) (i32.const 2) (i32.const 2))

;; Out-of-bounds stores trap, but all previous stores succeed.
(assert_trap (invoke "init" (i32.const 2) (i32.const 0) (i32.const 2))
"out of bounds table access")
(assert_return (invoke "call" (i32.const 2)) (i32.const 0))

;; Succeed when storing 0 elements at the end of either region.
(invoke "init" (i32.const 3) (i32.const 0) (i32.const 0))
(invoke "init" (i32.const 0) (i32.const 4) (i32.const 0))
Loading