Skip to content

Commit

Permalink
Add br_on_non_null (WebAssembly#48)
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed May 19, 2021
1 parent b158867 commit 25d26e7
Show file tree
Hide file tree
Showing 14 changed files with 117 additions and 20 deletions.
7 changes: 3 additions & 4 deletions document/core/appendix/algorithm.rst
Original file line number Diff line number Diff line change
Expand Up @@ -290,10 +290,9 @@ Other instructions are checked in a similar manner.
let rt = pop_ref()
if (rt.heap =/= Bot)
error_if(not is_def(rt.heap))
let t1*->t2* = lookup_def(rt.heap.def) // TODO
pop_vals(t1*)
push_vals(t2*)
let ft = lookup_func_type(rt.heap.idx) // TODO
pop_vals(ft.params)
push_vals(ft.results)
.. note::
It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack.
Expand Down
2 changes: 2 additions & 0 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -500,6 +500,8 @@ let rec instr s =
| 0xd2 -> ref_func (at var s)
| 0xd3 -> ref_as_non_null
| 0xd4 -> br_on_null (at var s)
| 0xd5 as b -> illegal s pos b
| 0xd6 -> br_on_non_null (at var s)

| 0xfc as b ->
(match vu32 s with
Expand Down
1 change: 1 addition & 0 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,7 @@ struct
| BrIf x -> op 0x0d; var x
| BrTable (xs, x) -> op 0x0e; vec var xs; var x
| BrOnNull x -> op 0xd4; var x
| BrOnNonNull x -> op 0xd6; var x
| Return -> op 0x0f
| Call x -> op 0x10; var x
| CallRef -> op 0x14
Expand Down
8 changes: 8 additions & 0 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,14 @@ let rec step (c : config) : config =
Ref r :: vs', []
)

| BrOnNonNull x, Ref r :: vs' ->
(match r with
| NullRef _ ->
vs', []
| _ ->
Ref r :: vs', [Plain (Br x) @@ e.at]
)

| Return, vs ->
[], [Returning vs @@ e.at]

Expand Down
1 change: 1 addition & 0 deletions interpreter/syntax/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,7 @@ and instr' =
| BrIf of idx (* conditional break *)
| BrTable of idx list * idx (* indexed break *)
| BrOnNull of idx (* break on null *)
| BrOnNonNull of idx (* break on non-null *)
| Return (* break from function body *)
| Call of idx (* call function *)
| CallRef (* call function through reference *)
Expand Down
2 changes: 1 addition & 1 deletion interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ let rec instr (e : instr) =
| Let (bt, ts, es) ->
let free = block_type bt ++ block es in
{free with locals = Lib.Fun.repeat (List.length ts) shift free.locals}
| Br x | BrIf x | BrOnNull x -> labels (idx x)
| Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
| BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
| Return | CallRef | ReturnCallRef -> empty
| Call x -> funcs (idx x)
Expand Down
1 change: 1 addition & 0 deletions interpreter/syntax/operators.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ let br x = Br x
let br_if x = BrIf x
let br_table xs x = BrTable (xs, x)
let br_on_null x = BrOnNull x
let br_on_non_null x = BrOnNonNull x

let return = Return
let call x = Call x
Expand Down
1 change: 1 addition & 0 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -250,6 +250,7 @@ let rec instr e =
| BrTable (xs, x) ->
"br_table " ^ String.concat " " (list var (xs @ [x])), []
| BrOnNull x -> "br_on_null " ^ var x, []
| BrOnNonNull x -> "br_on_non_null " ^ var x, []
| Return -> "return", []
| Call x -> "call " ^ var x, []
| CallRef -> "call_ref", []
Expand Down
1 change: 1 addition & 0 deletions interpreter/text/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,7 @@ rule token = parse
| "br_if" { BR_IF }
| "br_table" { BR_TABLE }
| "br_on_null" { BR_ON_NULL }
| "br_on_non_null" { BR_ON_NON_NULL }
| "return" { RETURN }
| "if" { IF }
| "then" { THEN }
Expand Down
3 changes: 2 additions & 1 deletion interpreter/text/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -210,7 +210,7 @@ let inline_func_type_explicit (c : context) x ft at =
%token NUM_TYPE FUNCREF EXTERNREF REF EXTERN NULL MUT
%token UNREACHABLE NOP DROP SELECT
%token BLOCK END IF THEN ELSE LOOP LET
%token BR BR_IF BR_TABLE BR_ON_NULL
%token BR BR_IF BR_TABLE BR_ON_NULL BR_ON_NON_NULL
%token CALL CALL_REF CALL_INDIRECT RETURN RETURN_CALL_REF FUNC_BIND
%token LOCAL_GET LOCAL_SET LOCAL_TEE GLOBAL_GET GLOBAL_SET
%token TABLE_GET TABLE_SET
Expand Down Expand Up @@ -398,6 +398,7 @@ plain_instr :
{ fun c -> let xs, x = Lib.List.split_last ($2 c label :: $3 c label) in
br_table xs x }
| BR_ON_NULL var { fun c -> br_on_null ($2 c label) }
| BR_ON_NON_NULL var { fun c -> br_on_non_null ($2 c label) }
| RETURN { fun c -> return }
| CALL var { fun c -> call ($2 c func) }
| CALL_REF { fun c -> call_ref }
Expand Down
12 changes: 12 additions & 0 deletions interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -353,6 +353,18 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
(label c x @ [RefType (Nullable, t)]) -->
(label c x @ [RefType (NonNullable, t)])

| BrOnNonNull x ->
let (_, ht) as rt = peek_ref 0 s e.at in
let t' = RefType (NonNullable, ht) in
require (label c x <> []) e.at
("type mismatch: instruction requires type " ^ string_of_value_type t' ^
" but label has " ^ string_of_result_type (label c x));
let ts0, t = Lib.List.split_last (label c x) in
require (match_value_type c.types [] t' t) e.at
("type mismatch: instruction requires type " ^ string_of_value_type t' ^
" but label has " ^ string_of_result_type (label c x));
(ts0 @ [RefType rt]) --> ts0

| Return ->
c.results -->... []

Expand Down
11 changes: 9 additions & 2 deletions proposals/function-references/Overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ Note: In a Wasm engine, function references (whether first-class or as table ent

* Add an instruction `ref.as_non_null` that converts a nullable reference to a non-nullable one or traps if null

* Add an instruction `br_on_null` that converts a nullable reference to a non-nullable one or branches if null
* Add an instruction `br_on_null` that converts a nullable reference to a non-nullable one or branches if null, as well as the inverted `br_on_non_null`

* Add an instruction `call_ref` for calling a function through a `ref $t`

Expand Down Expand Up @@ -228,12 +228,18 @@ The following rules, now defined in terms of heap types, replace and extend the
- iff `ht ok`
- traps on `null`

* `br_on_null $l` checks for null and branches
* `br_on_null $l` checks for null and branches if present
- `br_on_null $l : [t* (ref null ht)] -> [t* (ref ht)]`
- iff `$l : [t*]`
- and `ht ok`
- branches to `$l` on `null`, otherwise returns operand as non-null

* `br_on_non_null $l` checks for null and branches if not present
- `br_on_non_null $l : [t* (ref null ht)] -> [t*]`
- iff `$l : [t* (ref ht)]`
- and `ht ok`
- branches to `$l` if operand is not `null`, passing the operand itself under non-null type (along with potential additional operands)

* Note: `ref.is_null` already exists via the [reference types proposal](https://github.com/WebAssembly/reference-types)


Expand Down Expand Up @@ -299,6 +305,7 @@ The opcode for heap types is encoded as an `s33`.
| 0x17 | `let <bt> <locals>` | `bt : blocktype, locals : (as in functions)` |
| 0xd3 | `ref.as_non_null` | |
| 0xd4 | `br_on_null $l` | `$l : u32` |
| 0xd6 | `br_on_non_null $l` | `$l : u32` |

### Tables

Expand Down
72 changes: 72 additions & 0 deletions test/core/br_on_non_null.wast
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
(module
(type $t (func (result i32)))

(func $nn (param $r (ref $t)) (result i32)
(call_ref
(block $l (result (ref $t))
(br_on_non_null $l (local.get $r))
(return (i32.const -1))
)
)
)
(func $n (param $r (ref null $t)) (result i32)
(call_ref
(block $l (result (ref $t))
(br_on_non_null $l (local.get $r))
(return (i32.const -1))
)
)
)

(elem func $f)
(func $f (result i32) (i32.const 7))

(func (export "nullable-null") (result i32) (call $n (ref.null $t)))
(func (export "nonnullable-f") (result i32) (call $nn (ref.func $f)))
(func (export "nullable-f") (result i32) (call $n (ref.func $f)))

(func (export "unreachable") (result i32)
(block $l
(return (call_ref (br_on_null $l (unreachable))))
)
(i32.const -1)
)
)

(assert_trap (invoke "unreachable") "unreachable")

(assert_return (invoke "nullable-null") (i32.const -1))
(assert_return (invoke "nonnullable-f") (i32.const 7))
(assert_return (invoke "nullable-f") (i32.const 7))

(module
(type $t (func))
(func (param $r (ref null $t)) (drop (block (result (ref $t)) (br_on_non_null 0 (local.get $r)) (unreachable))))
(func (param $r (ref null func)) (drop (block (result (ref func)) (br_on_non_null 0 (local.get $r)) (unreachable))))
(func (param $r (ref null extern)) (drop (block (result (ref extern)) (br_on_non_null 0 (local.get $r)) (unreachable))))
)


(module
(type $t (func (param i32) (result i32)))
(elem func $f)
(func $f (param i32) (result i32) (i32.mul (local.get 0) (local.get 0)))

(func $a (param $n i32) (param $r (ref null $t)) (result i32)
(call_ref
(block $l (result i32 (ref $t))
(return (br_on_non_null $l (local.get $n) (local.get $r)))
)
)
)

(func (export "args-null") (param $n i32) (result i32)
(call $a (local.get $n) (ref.null $t))
)
(func (export "args-f") (param $n i32) (result i32)
(call $a (local.get $n) (ref.func $f))
)
)

(assert_return (invoke "args-null" (i32.const 3)) (i32.const 3))
(assert_return (invoke "args-f" (i32.const 3)) (i32.const 9))
15 changes: 3 additions & 12 deletions test/core/br_on_null.wast
Original file line number Diff line number Diff line change
Expand Up @@ -35,20 +35,11 @@
(assert_return (invoke "nonnullable-f") (i32.const 7))
(assert_return (invoke "nullable-f") (i32.const 7))

(assert_invalid
(module
(type $t (func (result i32)))
(func $g (param $r (ref $t)) (drop (br_on_null 0 (local.get $r))))
(func (call $g (ref.null $t)))
)
"type mismatch"
)

(module
(type $t (func))
(func (param $r (ref $t)) (drop (br_on_null 0 (local.get $r))))
(func (param $r (ref func)) (drop (br_on_null 0 (local.get $r))))
(func (param $r (ref extern)) (drop (br_on_null 0 (local.get $r))))
(func (param $r (ref null $t)) (drop (br_on_null 0 (local.get $r))))
(func (param $r (ref null func)) (drop (br_on_null 0 (local.get $r))))
(func (param $r (ref null extern)) (drop (br_on_null 0 (local.get $r))))
)


Expand Down

0 comments on commit 25d26e7

Please sign in to comment.