Skip to content

Commit 751a47c

Browse files
committed
Make recursive type verification logic better by allowing it to see through multiple levels of indirection. Still can trigger "unexpected OpaqueTy" bugs, but that's better than infinite loops.
1 parent 742b1c5 commit 751a47c

File tree

2 files changed

+18
-12
lines changed

2 files changed

+18
-12
lines changed

src/boot/me/semant.ml

Lines changed: 17 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2134,7 +2134,11 @@ and vec_sty (word_bits:Il.bits) : Il.scalar_ty =
21342134
let ptr = Il.ScalarTy (Il.AddrTy Il.OpaqueTy) in
21352135
Il.AddrTy (Il.StructTy [| word; word; word; ptr |])
21362136

2137-
and referent_type (cx:ctxt) (t:Ast.ty) : Il.referent_ty =
2137+
and referent_type
2138+
?parent_tag:parent_tag
2139+
(cx:ctxt)
2140+
(t:Ast.ty)
2141+
: Il.referent_ty =
21382142
let s t = Il.ScalarTy t in
21392143
let v b = Il.ValTy b in
21402144
let p t = Il.AddrTy t in
@@ -2149,12 +2153,7 @@ and referent_type (cx:ctxt) (t:Ast.ty) : Il.referent_ty =
21492153
let tag ttag =
21502154
let n = get_n_tag_tups cx ttag in
21512155
let union =
2152-
let rty t =
2153-
match t with
2154-
Ast.TY_box (Ast.TY_tag dst_tag) when is_back_edge ttag dst_tag ->
2155-
sp (Il.StructTy [| word; Il.OpaqueTy |])
2156-
| _ -> referent_type cx t
2157-
in
2156+
let rty t = referent_type ~parent_tag:ttag cx t in
21582157
let tup ttup = Il.StructTy (Array.map rty ttup) in
21592158
Array.init n (fun i -> tup (get_nth_tag_tup cx ttag i))
21602159
in
@@ -2194,7 +2193,13 @@ and referent_type (cx:ctxt) (t:Ast.ty) : Il.referent_ty =
21942193
| Ast.TY_fn _ -> fn_rty cx false
21952194
| Ast.TY_obj _ -> obj_rty word_bits
21962195

2197-
| Ast.TY_tag ttag -> tag ttag
2196+
| Ast.TY_tag ttag ->
2197+
begin
2198+
match parent_tag with
2199+
Some parent_tag when is_back_edge ttag parent_tag ->
2200+
Il.OpaqueTy
2201+
| _ -> tag ttag
2202+
end
21982203

21992204
| Ast.TY_chan _
22002205
| Ast.TY_port _
@@ -2205,14 +2210,15 @@ and referent_type (cx:ctxt) (t:Ast.ty) : Il.referent_ty =
22052210
| Ast.TY_native _ -> ptr
22062211

22072212
| Ast.TY_box t ->
2208-
sp (Il.StructTy [| word; referent_type cx t |])
2213+
sp (Il.StructTy
2214+
[| word; referent_type ?parent_tag:parent_tag cx t |])
22092215

2210-
| Ast.TY_mutable t -> referent_type cx t
2216+
| Ast.TY_mutable t -> referent_type ?parent_tag:parent_tag cx t
22112217

22122218
| Ast.TY_param (i, _) -> Il.ParamTy i
22132219

22142220
| Ast.TY_named _ -> bug () "named type in referent_type"
2215-
| Ast.TY_constrained (t, _) -> referent_type cx t
2221+
| Ast.TY_constrained (t, _) -> referent_type ?parent_tag:parent_tag cx t
22162222

22172223
and slot_referent_type (cx:ctxt) (sl:Ast.slot) : Il.referent_ty =
22182224
let s t = Il.ScalarTy t in

src/boot/me/type.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1010,7 +1010,7 @@ let populate_tag_graph_node (cx:Semant.ctxt) (id:Common.opaque_id) (n:int) =
10101010
| Ast.TY_rec ty_rec ->
10111011
Array.iter (fun (_, ty) -> add_ty ty) ty_rec
10121012
| Ast.TY_fn ty_fn -> add_ty_fn ty_fn
1013-
| Ast.TY_vec ty | Ast.TY_chan ty | Ast.TY_port ty | Ast.TY_mutable ty
1013+
| Ast.TY_chan ty | Ast.TY_port ty | Ast.TY_mutable ty
10141014
| Ast.TY_constrained (ty, _) -> add_ty ty
10151015
| Ast.TY_obj (_, ty_fns) ->
10161016
Hashtbl.iter (fun _ ty_fn -> add_ty_fn ty_fn) ty_fns

0 commit comments

Comments
 (0)