Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 4 additions & 4 deletions interpreter/binary/decode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -664,8 +664,8 @@ let rec instr s =
(match opcode with
| 0x18l -> br_on_cast x rt1 rt2
| 0x19l -> br_on_cast_fail x rt1 rt2
| 0x25l -> br_on_cast_desc x rt1 rt2
| 0x26l -> br_on_cast_desc_fail x rt1 rt2
| 0x25l -> br_on_cast_desc_eq x rt1 rt2
| 0x26l -> br_on_cast_desc_eq_fail x rt1 rt2
| _ -> assert false
)

Expand All @@ -677,8 +677,8 @@ let rec instr s =
| 0x1el -> i31_get_u

| 0x22l -> let x = at idx s in ref_get_desc x
| 0x23l -> let ht = heaptype s in ref_cast_desc (NoNull, ht)
| 0x24l -> let ht = heaptype s in ref_cast_desc (Null, ht)
| 0x23l -> let ht = heaptype s in ref_cast_desc_eq (NoNull, ht)
| 0x24l -> let ht = heaptype s in ref_cast_desc_eq (Null, ht)

| n -> illegal2 s pos b n
)
Expand Down
8 changes: 4 additions & 4 deletions interpreter/binary/encode.ml
Original file line number Diff line number Diff line change
Expand Up @@ -277,10 +277,10 @@ struct
| BrOnCastFail (x, (nul1, t1), (nul2, t2)) ->
let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in
op 0xfb; op 0x19; byte flags; idx x; heaptype t1; heaptype t2
| BrOnCastDesc (x, (nul1, t1), (nul2, t2)) ->
| BrOnCastDescEq (x, (nul1, t1), (nul2, t2)) ->
let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in
op 0xfb; op 0x25; byte flags; idx x; heaptype t1; heaptype t2
| BrOnCastDescFail (x, (nul1, t1), (nul2, t2)) ->
| BrOnCastDescEqFail (x, (nul1, t1), (nul2, t2)) ->
let flags = bit 0 (nul1 = Null) + bit 1 (nul2 = Null) in
op 0xfb; op 0x26; byte flags; idx x; heaptype t1; heaptype t2
| Return -> op 0x0f
Expand Down Expand Up @@ -436,8 +436,8 @@ struct
| RefTest (Null, t) -> op 0xfb; op 0x15; heaptype t
| RefCast (NoNull, t) -> op 0xfb; op 0x16; heaptype t
| RefCast (Null, t) -> op 0xfb; op 0x17; heaptype t
| RefCastDesc (NoNull, t) -> op 0xfb; op 0x23; heaptype t
| RefCastDesc (Null, t) -> op 0xfb; op 0x24; heaptype t
| RefCastDescEq (NoNull, t) -> op 0xfb; op 0x23; heaptype t
| RefCastDescEq (Null, t) -> op 0xfb; op 0x24; heaptype t

| RefGetDesc x -> op 0xfb; op 0x22; idx x

Expand Down
24 changes: 12 additions & 12 deletions interpreter/exec/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -258,31 +258,31 @@ let rec step (c : config) : config =
else
Ref r :: vs', [Plain (Br x) @@ e.at]

| BrOnCastDesc (x, _rt1, _rt2), Ref (NullRef _) :: vs' ->
| BrOnCastDescEq (x, _rt1, _rt2), Ref (NullRef _) :: vs' ->
vs', [Trapping "null descriptor reference" @@ e.at]

| BrOnCastDesc (x, _rt1, (Null, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
| BrOnCastDescEq (x, _rt1, (Null, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
Ref r :: vs', [Plain (Br x) @@ e.at]

| BrOnCastDesc (x, _rt1, (NoNull, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
| BrOnCastDescEq (x, _rt1, (NoNull, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
Ref r :: vs', []

| BrOnCastDesc (x, _rt1, _rt2), Ref desc :: Ref r :: vs' ->
| BrOnCastDescEq (x, _rt1, _rt2), Ref desc :: Ref r :: vs' ->
(match Aggr.read_desc r with
| Some desc' when eq_ref desc desc' -> Ref r :: vs', [Plain (Br x) @@ e.at]
| _ -> Ref r :: vs', []
)

| BrOnCastDescFail (x, _rt1, _rt2), Ref (NullRef _) :: vs' ->
| BrOnCastDescEqFail (x, _rt1, _rt2), Ref (NullRef _) :: vs' ->
vs', [Trapping "null descriptor reference" @@ e.at]

| BrOnCastDescFail (x, _rt1, (Null, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
| BrOnCastDescEqFail (x, _rt1, (Null, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
Ref r :: vs', []

| BrOnCastDescFail (x, _rt1, (NoNull, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
| BrOnCastDescEqFail (x, _rt1, (NoNull, _)), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
Ref r :: vs', [Plain (Br x) @@ e.at]

| BrOnCastDescFail (x, _rt1, _rt2), Ref desc :: Ref r :: vs' ->
| BrOnCastDescEqFail (x, _rt1, _rt2), Ref desc :: Ref r :: vs' ->
(match Aggr.read_desc r with
| Some desc' when eq_ref desc desc' -> Ref r :: vs', []
| _ -> Ref r :: vs', [Plain (Br x) @@ e.at]
Expand Down Expand Up @@ -689,16 +689,16 @@ let rec step (c : config) : config =
string_of_reftype rt ^ " but got " ^
string_of_reftype (type_of_ref r)) @@ e.at]

| RefCastDesc _rt, Ref (NullRef _) :: vs' ->
| RefCastDescEq _rt, Ref (NullRef _) :: vs' ->
vs', [Trapping "null descriptor reference" @@ e.at]

| RefCastDesc (NoNull, _), Ref _desc :: Ref (NullRef _) :: vs' ->
| RefCastDescEq (NoNull, _), Ref _desc :: Ref (NullRef _) :: vs' ->
vs', [Trapping "descriptor cast failure" @@ e.at]

| RefCastDesc (Null, _), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
| RefCastDescEq (Null, _), Ref _desc :: Ref ((NullRef _) as r) :: vs' ->
Ref r :: vs', []

| RefCastDesc rt, Ref desc :: Ref r :: vs' ->
| RefCastDescEq rt, Ref desc :: Ref r :: vs' ->
(match Aggr.read_desc r with
| Some desc' when eq_ref desc desc' -> Ref r :: vs', []
| _ -> vs', [Trapping "descriptor cast failure" @@ e.at]
Expand Down
6 changes: 3 additions & 3 deletions interpreter/syntax/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -182,8 +182,8 @@ and instr' =
| BrOnNonNull of labelidx (* break on type inverted *)
| BrOnCast of labelidx * reftype * reftype (* break on type *)
| BrOnCastFail of labelidx * reftype * reftype (* break on type inverted *)
| BrOnCastDesc of labelidx * reftype * reftype (* break on descriptor cast *)
| BrOnCastDescFail of labelidx * reftype * reftype (* break on descriptor cast inverted *)
| BrOnCastDescEq of labelidx * reftype * reftype (* break on descriptor cast *)
| BrOnCastDescEqFail of labelidx * reftype * reftype (* break on descriptor cast inverted *)
| Return (* break from function body *)
| Call of funcidx (* call function *)
| CallRef of typeidx (* call function through reference *)
Expand Down Expand Up @@ -225,7 +225,7 @@ and instr' =
| RefAsNonNull (* type cast *)
| RefTest of reftype (* type test *)
| RefCast of reftype (* type cast *)
| RefCastDesc of reftype (* descriptor type cast *)
| RefCastDescEq of reftype (* descriptor type cast *)
| RefGetDesc of typeidx (* read descriptor *)
| RefEq (* reference equality *)
| RefI31 (* scalar reference *)
Expand Down
4 changes: 2 additions & 2 deletions interpreter/syntax/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ let rec instr (e : instr) =
| If (bt, es1, es2) -> blocktype bt ++ block es1 ++ block es2
| Br x | BrIf x | BrOnNull x | BrOnNonNull x -> labels (idx x)
| BrOnCast (x, t1, t2) | BrOnCastFail (x, t1, t2)
| BrOnCastDesc (x, t1, t2) | BrOnCastDescFail (x, t1, t2) ->
| BrOnCastDescEq (x, t1, t2) | BrOnCastDescEqFail (x, t1, t2) ->
labels (idx x) ++ reftype t1 ++ reftype t2
| BrTable (xs, x) -> list (fun x -> labels (idx x)) (x::xs)
| Return -> empty
Expand All @@ -169,7 +169,7 @@ let rec instr (e : instr) =
| MemoryInit (x, y) -> memories (idx x) ++ datas (idx y)
| DataDrop x -> datas (idx x)
| RefIsNull | RefAsNonNull -> empty
| RefTest t | RefCast t | RefCastDesc t -> reftype t
| RefTest t | RefCast t | RefCastDescEq t -> reftype t
| RefGetDesc x -> types (idx x)
| RefEq -> empty
| RefNull t -> heaptype t
Expand Down
6 changes: 3 additions & 3 deletions interpreter/syntax/mnemonics.ml
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ let br_on_null x = BrOnNull x
let br_on_non_null x = BrOnNonNull x
let br_on_cast x t1 t2 = BrOnCast (x, t1, t2)
let br_on_cast_fail x t1 t2 = BrOnCastFail (x, t1, t2)
let br_on_cast_desc x t1 t2 = BrOnCastDesc (x, t1, t2)
let br_on_cast_desc_fail x t1 t2 = BrOnCastDescFail (x, t1, t2)
let br_on_cast_desc_eq x t1 t2 = BrOnCastDescEq (x, t1, t2)
let br_on_cast_desc_eq_fail x t1 t2 = BrOnCastDescEqFail (x, t1, t2)

let catch x1 x2 = Catch (x1, x2)
let catch_ref x1 x2 = CatchRef (x1, x2)
Expand Down Expand Up @@ -175,7 +175,7 @@ let ref_is_null = RefIsNull
let ref_as_non_null = RefAsNonNull
let ref_test t = RefTest t
let ref_cast t = RefCast t
let ref_cast_desc t = RefCastDesc t
let ref_cast_desc_eq t = RefCastDescEq t
let ref_get_desc x = RefGetDesc x
let ref_eq = RefEq

Expand Down
10 changes: 5 additions & 5 deletions interpreter/text/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -521,10 +521,10 @@ let rec instr e =
"br_on_cast " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
| BrOnCastFail (x, t1, t2) ->
"br_on_cast_fail " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
| BrOnCastDesc (x, t1, t2) ->
"br_on_cast_desc " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
| BrOnCastDescFail (x, t1, t2) ->
"br_on_cast_desc_fail " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
| BrOnCastDescEq (x, t1, t2) ->
"br_on_cast_desc_eq " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
| BrOnCastDescEqFail (x, t1, t2) ->
"br_on_cast_desc_eq_fail " ^ idx x, [Atom (reftype t1); Atom (reftype t2)]
| Return -> "return", []
| Call x -> "call " ^ idx x, []
| CallRef x -> "call_ref " ^ idx x, []
Expand Down Expand Up @@ -569,7 +569,7 @@ let rec instr e =
| RefAsNonNull -> "ref.as_non_null", []
| RefTest t -> "ref.test", [Atom (reftype t)]
| RefCast t -> "ref.cast", [Atom (reftype t)]
| RefCastDesc t -> "ref.cast_desc", [Atom (reftype t)]
| RefCastDescEq t -> "ref.cast_desc_eq", [Atom (reftype t)]
| RefGetDesc x -> "ref.get_desc " ^ idx x, []
| RefEq -> "ref.eq", []
| RefI31 -> "ref.i31", []
Expand Down
6 changes: 3 additions & 3 deletions interpreter/text/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -204,8 +204,8 @@ rule token = parse
| "br_on_non_null" -> BR_ON_NULL br_on_non_null
| "br_on_cast" -> BR_ON_CAST br_on_cast
| "br_on_cast_fail" -> BR_ON_CAST br_on_cast_fail
| "br_on_cast_desc" -> BR_ON_CAST br_on_cast_desc
| "br_on_cast_desc_fail" -> BR_ON_CAST br_on_cast_desc_fail
| "br_on_cast_desc_eq" -> BR_ON_CAST br_on_cast_desc_eq
| "br_on_cast_desc_eq_fail" -> BR_ON_CAST br_on_cast_desc_eq_fail
| "return" -> RETURN
| "if" -> IF
| "then" -> THEN
Expand Down Expand Up @@ -340,7 +340,7 @@ rule token = parse
| "ref.as_non_null" -> REF_AS_NON_NULL
| "ref.test" -> REF_TEST
| "ref.cast" -> REF_CAST
| "ref.cast_desc" -> REF_CAST_DESC
| "ref.cast_desc_eq" -> REF_CAST_DESC
| "ref.get_desc" -> REF_GET_DESC
| "ref.eq" -> REF_EQ

Expand Down
2 changes: 1 addition & 1 deletion interpreter/text/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -640,7 +640,7 @@ plaininstr :
| REF_AS_NON_NULL { fun c -> ref_as_non_null }
| REF_TEST reftype { fun c -> ref_test ($2 c) }
| REF_CAST reftype { fun c -> ref_cast ($2 c) }
| REF_CAST_DESC reftype { fun c -> ref_cast_desc ($2 c) }
| REF_CAST_DESC reftype { fun c -> ref_cast_desc_eq ($2 c) }
| REF_GET_DESC idx { fun c -> ref_get_desc ($2 c type_) }
| REF_EQ { fun c -> ref_eq }
| REF_I31 { fun c -> ref_i31 }
Expand Down
6 changes: 3 additions & 3 deletions interpreter/valid/valid.ml
Original file line number Diff line number Diff line change
Expand Up @@ -591,7 +591,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
" but label has " ^ string_of_resulttype (label c x));
(ts0 @ [RefT rt1]) --> (ts0 @ [RefT rt2]), []

| BrOnCastDesc (x, rt1, rt2) ->
| BrOnCastDescEq (x, rt1, rt2) ->
check_reftype c rt1 e.at;
check_reftype c rt2 e.at;
let (_, ht1), (_, ht2) = rt1, rt2 in
Expand All @@ -609,7 +609,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
let rt = desc_cast_ref c rt2 e.at in
(ts0 @ [RefT rt1; RefT rt]) --> (ts0 @ [RefT (diff_reftype rt1 rt2)]), []

| BrOnCastDescFail (x, rt1, rt2) ->
| BrOnCastDescEqFail (x, rt1, rt2) ->
check_reftype c rt1 e.at;
check_reftype c rt2 e.at;
let rt1' = diff_reftype rt1 rt2 in
Expand Down Expand Up @@ -847,7 +847,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_ins
check_reftype c rt e.at;
[RefT (Null, top_of_heaptype c.types ht)] --> [RefT (nul, ht)], []

| RefCastDesc rt ->
| RefCastDescEq rt ->
let (nul, ht) = rt in
check_reftype c rt e.at;
let rt' = desc_cast_ref c rt e.at in
Expand Down
22 changes: 11 additions & 11 deletions proposals/custom-descriptors/Overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -501,18 +501,18 @@ then the type of the cast output can also be exact.
If the provided descriptor is a null value, these instructions trap.

```
ref.cast_desc reftype
ref.cast_desc_eq reftype

C |- ref.cast_desc rt : (ref null ht) (ref null (exact_1 y)) -> rt
C |- ref.cast_desc_eq rt : (ref null ht) (ref null (exact_1 y)) -> rt
-- rt = (ref null? (exact_1 x))
-- C |- C.types[x] <: ht
-- C.types[x] ~ descriptor y ct
```

```
br_on_cast_desc labelidx reftype reftype
br_on_cast_desc_eq labelidx reftype reftype

C |- br_on_cast_desc l rt_1 rt_2 : t* rt_1 (ref null (exact_1 y)) -> t* (rt_1 \ rt_2)
C |- br_on_cast_desc_eq l rt_1 rt_2 : t* rt_1 (ref null (exact_1 y)) -> t* (rt_1 \ rt_2)
-- C.labels[l] = t* rt
-- C |- rt_2 <: rt
-- C |- rt_1 <: rt'
Expand All @@ -523,9 +523,9 @@ C |- br_on_cast_desc l rt_1 rt_2 : t* rt_1 (ref null (exact_1 y)) -> t* (rt_1 \
```

```
br_on_cast_desc_fail labelidx reftype reftype
br_on_cast_desc_eq_fail labelidx reftype reftype

C |- br_on_cast_desc_fail l rt_1 rt_2 : t* rt_1 (ref null (exact_1 y)) -> t* rt_2
C |- br_on_cast_desc_eq_fail l rt_1 rt_2 : t* rt_1 (ref null (exact_1 y)) -> t* rt_2
-- C.labels[l] = t* rt
-- C |- rt_1 \ rt_2 <: rt
-- C |- rt_1 <: rt'
Expand All @@ -538,7 +538,7 @@ C |- br_on_cast_desc_fail l rt_1 rt_2 : t* rt_1 (ref null (exact_1 y)) -> t* rt_
Note that the constraint `C |- rt_2 <: rt_1` on branching cast instructions before this proposal
is relaxed to the constraint that `rt_1` and `rt_2` share some arbitrary valid supertype `rt'`,
i.e. that `rt_1` and `rt_2` must be in the same heap type hierarchy.
This relaxation is applied not only to the new `br_on_cast_desc` and `br_on_cast_desc_fail` instructions,
This relaxation is applied not only to the new `br_on_cast_desc_eq` and `br_on_cast_desc_eq_fail` instructions,
but also the existing `br_on_cast` and `br_on_cast_fail` instructions.

## JS Prototypes
Expand Down Expand Up @@ -1015,12 +1015,12 @@ instr ::= ...
| 0xFB 32:u32 x:typeidx => struct.new_desc x
| 0xFB 33:u32 x:typeidx => struct.new_default_desc x
| 0xFB 34:u32 x:typeidx => ref.get_desc x
| 0xFB 35:u32 ht:heaptype => ref.cast_desc (ref ht)
| 0xFB 36:u32 ht:heaptype => ref.cast_desc (ref null ht)
| 0xFB 35:u32 ht:heaptype => ref.cast_desc_eq (ref ht)
| 0xFB 36:u32 ht:heaptype => ref.cast_desc_eq (ref null ht)
| 0xFB 37:u32 (null_1?, null_2?):castflags
l:labelidx ht_1:heaptype ht_2:heaptype =>
br_on_cast_desc l (ref null_1? ht_1) (ref null_2? ht_2)
br_on_cast_desc_eq l (ref null_1? ht_1) (ref null_2? ht_2)
| 0xFB 38:u32 (null_1?, null_2?):castflags
l:labelidx ht_1:heaptype ht_2:heaptype =>
br_on_cast_desc_fail l (ref null_1? ht_1) (ref null_2? ht_2)
br_on_cast_desc_eq_fail l (ref null_1? ht_1) (ref null_2? ht_2)
```
Loading