Skip to content

[interpreter] Descriptor type validation #66

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

[interpreter] Descriptor type validation #66

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
58 changes: 49 additions & 9 deletions interpreter/valid/valid.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,17 +157,55 @@ let check_comptype (c : context) (ct : comptype) at =
check_resulttype c ts1 at;
check_resulttype c ts2 at

(* TODO: Make sure the describes and descriptor clauses match. *)
let check_desctype (c : context) (dt : desctype) at =
match dt with
| DescT (ht1, ht2, ct) -> check_comptype c ct at
let DescT (_, _, ct) = dt in
check_comptype c ct at

let check_desctype_sub (c : context) (dt : desctype) (dti : desctype) x xi at =
let check_desctype_sub (c : context) (dt : desctype) (dt' : desctype) x x' at =
(* TODO: check rules *)
let DescT (_, _, ct) = dt in
let DescT (_, _, cti) = dti in
require (match_comptype c.types ct cti) at ("sub type " ^ I32.to_string_u x ^
" does not match super type " ^ I32.to_string_u xi)
let DescT (ut1, ut2, ct) = dt in
let DescT (ut1', ut2', ct') = dt' in
match ut1, ut1' with
| (Some ut1, Some ut1') ->
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rossberg, I'm trying to validate that if dt <: dt', then we also have ut1 <: ut1', where ut1 and ut1' are the types described by dt and dt'.

I have this working in some cases, but it's super ugly and it breaks in other cases. Specifically, the idx_of_typeuse ut on line 178 fails when the four types are all in the same rec group because in that case it is a Rec rather than an idx.

Do you have a suggestion about how to do these checks more generally and cleanly?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh yes, defining that isn't going to be straightforward, due to all the mutual recursion going on. I'll probably have to think about it. Unfortunately, I just arrived at ICFP/OOPSLA today, so might lack the quiet moment this week and the next. But yeah, assuming you can extract indices is not going to work.

let dt1' = deftype_of_typeuse ut1' in
let x1 = idx_of_typeuse ut1 in
let SubT (_, uts, _) = unroll_deftype (type_ c (x1 @@ at)) in
(match uts with
| [] ->
require false at ("described type " ^ I32.to_string_u x1 ^
" does not have required supertype")
| ut :: [] ->
let dt1'' = (type_ c ((idx_of_typeuse ut) @@ at)) in
require (dt1' = dt1'') at "oogabooga"
| _ -> assert false)
| (None, None) -> ()
| _ -> require false at "blah";
(* TODO: match ut2, ut2' *)
require (match_comptype c.types ct ct') at ("sub type " ^ I32.to_string_u x ^
" does not match super type " ^ I32.to_string_u x')

let check_descriptors (dts : deftype list) at =
List.iter (fun dt ->
let DefT ((RecT dts), x) = dt in
let SubT (_, _, DescT (ut1, ut2, _)) = Lib.List32.nth dts x in
Option.iter (fun ut ->
match ut with
| Rec x' ->
let SubT (_, _, DescT (_, ut', _)) = Lib.List32.nth dts x' in
require (ut' = Some (Rec x)) at
"described type is not described by descriptor";
require (x' < x) at "forward use of described type"
| _ -> require false at "described type is outside rec group"
) ut1;
Option.iter (fun ut ->
match ut with
| Rec x' ->
let SubT (_, _, DescT (ut', _, _)) = Lib.List32.nth dts x' in
require (ut' = Some (Rec x)) at
"type is not described by its descriptor";
| _ -> require false at "descriptor type is outside rec group"
) ut2
) dts

let check_subtype (c : context) (sut : subtype) at =
let SubT (_fin, uts, dt) = sut in
Expand All @@ -189,7 +227,9 @@ let check_subtype_sub (c : context) (sut : subtype) x at =
let check_rectype (c : context) (rt : rectype) at : context =
let RecT sts = rt in
let x = Lib.List32.length c.types in
let c' = {c with types = c.types @ roll_deftypes x rt} in
let dts = roll_deftypes x rt in
check_descriptors dts at;
let c' = {c with types = c.types @ dts} in
List.iter (fun st -> check_subtype c' st at) sts;
Lib.List32.iteri
(fun i st -> check_subtype_sub c' st (Int32.add x i) at) sts;
Expand Down
110 changes: 110 additions & 0 deletions test/core/custom-descriptors/descriptors.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,3 +72,113 @@
)
"unexpected token"
)

;; Type validation

(assert_invalid
(module
(type (descriptor 1) (struct))
)
"descriptor type is outside rec group"
)

(assert_invalid
(module
(type (describes 1) (struct))
)
"described type is outside rec group"
)

(assert_invalid
(module
(type (descriptor 1) (struct))
(type (struct))
)
"descriptor type is outside rec group"
)

(assert_invalid
(module
(type (describes 1) (struct))
(type (struct))
)
"described type is outside rec group"
)

(assert_invalid
(module
(type (struct))
(type (descriptor 0) (struct))
)
"descriptor type is outside rec group"
)

(assert_invalid
(module
(type (struct))
(type (describes 0) (struct))
)
"described type is outside rec group"
)

(assert_invalid
(module
(rec
(type (descriptor 1) (struct))
(type (struct))
)
)
"type is not described by its descriptor"
)

(assert_invalid
(module
(rec
(type (struct))
(type (describes 0) (struct))
)
)
"described type is not described by descriptor"
)

(assert_invalid
(module
(rec
(type (describes 1) (struct))
(type (descriptor 0) (struct))
)
)
"forward use of described type"
)

(assert_invalid
(module
(type (describes 0) (descriptor 0) (struct))
)
"forward use of described type"
)

;; Subtyping

(module
(rec
(type $A (sub (descriptor $A.desc) (struct)))
(type $A.desc (sub (describes $A) (struct)))
)
(rec
(type $B (sub $A (descriptor $B.desc) (struct)))
(type $B.desc (sub $A.desc (describes $B) (struct)))
)
)

;; TODO: this fails!
(module
(rec
(type $A (sub (descriptor $A.desc) (struct)))
(type $A.desc (sub (describes $A) (struct)))
(type $B (sub $A (descriptor $B.desc) (struct)))
(type $B.desc (sub $A.desc (describes $B) (struct)))
)
)

;; TODO: structs only
Loading