From c8b679877a1d33858327cc184cfa0a5b44164b80 Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Fri, 20 Dec 2024 17:17:27 +0000 Subject: [PATCH 1/8] extend signatures to record pre and post when required --- doc/md/examples/grammar.txt | 1 + src/lowering/desugar.ml | 34 ++++++++++++------- src/mo_def/syntax.ml | 6 +++- src/mo_frontend/parser.mly | 17 +++++++++- src/mo_frontend/stability.ml | 18 +++++----- src/mo_frontend/stability.mli | 2 +- src/mo_frontend/typing.ml | 48 +++++++++++++++------------ src/mo_frontend/typing.mli | 2 +- src/mo_types/type.ml | 62 ++++++++++++++++++++++++++--------- src/mo_types/type.mli | 11 +++++-- 10 files changed, 138 insertions(+), 63 deletions(-) diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt index 5d20ddf28e0..9e20af6a947 100644 --- a/doc/md/examples/grammar.txt +++ b/doc/md/examples/grammar.txt @@ -336,5 +336,6 @@ ::= , ';')> , ';')> + , ';')> 'actor' '(' '{' , ';')> '}' ',' '{' , ';')> '}' ')' diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index f77eb62963d..5c4f1f7ae0c 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -541,7 +541,7 @@ and build_actor at ts exp_opt self_id es obj_typ = let pairs = List.map2 stabilize stabs ds in let idss = List.map fst pairs in let ids = List.concat idss in - let sig_ = List.sort T.compare_field + let sig_post = List.sort T.compare_field (List.map (fun (i,t) -> T.{lab = i; typ = t; src = empty_src}) ids) in let fields = List.map (fun (i,t) -> T.{lab = i; typ = T.Opt (T.as_immut t); src = T.empty_src}) ids in @@ -550,8 +550,9 @@ and build_actor at ts exp_opt self_id es obj_typ = let state = fresh_var "state" (T.Mut (T.Opt ty)) in let get_state = fresh_var "getState" (T.Func(T.Local, T.Returns, [], [], [ty])) in let ds = List.map (fun mk_d -> mk_d get_state) mk_ds in - let stable_type, migration = match exp_opt with + let sig_, stable_type, migration = match exp_opt with | None -> + T.Single sig_post, I.{pre = ty; post = ty}, primE (I.ICStableRead ty) [] (* as before *) | Some exp0 -> @@ -559,21 +560,30 @@ and build_actor at ts exp_opt self_id es obj_typ = let [@warning "-8"] (_s,_c, [], [dom], [rng]) = T.as_func (exp0.note.S.note_typ) in let [@warning "-8"] (T.Object, dom_fields) = T.as_obj dom in let [@warning "-8"] (T.Object, rng_fields) = T.as_obj rng in + let sig_pre = + List.sort T.compare_field + (dom_fields @ + (List.filter_map + (fun (i,t) -> + match T.lookup_val_field_opt i dom_fields with + | Some t -> + (* ignore overriden *) + None + | None -> + (* retain others *) + Some T.{lab = i; typ = t; src = T.empty_src}) ids)) + in let fields' = List.map - (fun (i,t) -> - T.{lab = i; typ = T.Opt (T.as_immut t); src = T.empty_src}) - ((List.map (fun T.{lab;typ;_} -> (lab,typ)) dom_fields) @ - (List.filter_map - (fun (i,t) -> - match T.lookup_val_field_opt i dom_fields with - | Some t -> None (* ignore overriden *) - | None -> Some (i, t) (* retain others *)) - ids)) in - let ty' = T.Obj (T.Memory, List.sort T.compare_field fields') in + (fun tf -> + { tf with T.typ = T.Opt (T.as_immut tf.T.typ) }) + sig_pre + in + let ty' = T.Obj (T.Memory, fields') in let v = fresh_var "v" ty' in let v_dom = fresh_var "v_dom" dom in let v_rng = fresh_var "v_rng" rng in + T.PrePost (sig_pre, sig_post), I.{pre = ty'; post = ty}, ifE (primE (I.OtherPrim "rts_in_install") []) (primE (I.ICStableRead ty) []) diff --git a/src/mo_def/syntax.ml b/src/mo_def/syntax.ml index 87cf9b5485d..c8aac7b0d26 100644 --- a/src/mo_def/syntax.ml +++ b/src/mo_def/syntax.ml @@ -235,7 +235,11 @@ and prog' = dec list (* Signatures (stable variables) *) type stab_sig = (stab_sig', prog_note) Source.annotated_phrase -and stab_sig' = (dec list * typ_field list) (* type declarations & stable actor fields *) +and stab_sig' = (dec list * stab_body) (* type declarations & stable actor fields *) +and stab_body = stab_body' Source.phrase (* type declarations & stable actor fields *) +and stab_body' = + | Single of typ_field list + | PrePost of typ_field list * typ_field list (* Compilation units *) diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index 24f54aed881..faa7429647f 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -997,7 +997,22 @@ stab_field : parse_stab_sig : | start ds=seplist(typ_dec, semicolon) ACTOR LCURLY sfs=seplist(stab_field, semicolon) RCURLY { let trivia = !triv_table in - fun filename -> { it = (ds, sfs); at = at $sloc; note = { filename; trivia }} + let sigs = Single sfs in + fun filename -> { + it = (ds, {it=sigs; at = at $sloc; note = ()}); + at = at $sloc; + note = + { filename; trivia }} + } + | start ds=seplist(typ_dec, semicolon) + ACTOR LPAR LCURLY sfs_pre=seplist(stab_field, semicolon) RCURLY COMMA + LCURLY sfs_post=seplist(stab_field, semicolon) RCURLY RPAR + { let trivia = !triv_table in + let sigs = PrePost(sfs_pre, sfs_post) in (* FIX ME*) + fun filename -> { + it = (ds, {it=sigs; at = at $sloc; note = ()}); + at = at $sloc; + note = { filename; trivia }} } %% diff --git a/src/mo_frontend/stability.ml b/src/mo_frontend/stability.ml index b3069f5e307..d074cf8f2f5 100644 --- a/src/mo_frontend/stability.ml +++ b/src/mo_frontend/stability.ml @@ -31,16 +31,18 @@ let error_sub s tf1 tf2 = (* Relaxed rules with enhanced orthogonal persistence for more flexible upgrades. - Mutability of stable fields can be changed because they are never aliased. - - Stable fields can be dropped, however, with a warning of potential data loss. + - Stable fields can be dropped, however, with a warning of potential data loss. For this, we give up the transitivity property of upgrades. - Upgrade transitivity means that an upgrade from a program A to B and then from B to C - should have the same effect as directly upgrading from A to C. If B discards a field - and C re-adds it, this transitivity is no longer maintained. However, rigorous upgrade + Upgrade transitivity means that an upgrade from a program A to B and then from B to C + should have the same effect as directly upgrading from A to C. If B discards a field + and C re-adds it, this transitivity is no longer maintained. However, rigorous upgrade transitivity was also not guaranteed before, since B may contain initialization logic or pre-/post-upgrade hooks that alter the stable data. *) -let match_stab_sig tfs1 tfs2 : unit Diag.result = +let match_stab_sig sig1 sig2 : unit Diag.result = + let tfs1 = post sig1 in + let tfs2 = pre sig2 in (* Assume that tfs1 and tfs2 are sorted. *) let res = Diag.with_message_store (fun s -> let rec go tfs1 tfs2 = match tfs1, tfs2 with @@ -59,7 +61,7 @@ let match_stab_sig tfs1 tfs2 : unit Diag.result = | -1 -> (* dropped field is allowed with warning, recurse on tfs1' *) warning_discard s tf1; - go tfs1' tfs2 + go tfs1' tfs2 | _ -> go tfs1 tfs2' (* new field ok, recurse on tfs2' *) ) @@ -68,8 +70,8 @@ let match_stab_sig tfs1 tfs2 : unit Diag.result = (* cross check with simpler definition *) match res with | Ok _ -> - assert (Type.match_stab_sig tfs1 tfs2); + assert (Type.match_stab_sig sig1 sig2); res | Error _ -> - assert (not (Type.match_stab_sig tfs1 tfs2)); + assert (not (Type.match_stab_sig sig1 sig2)); res diff --git a/src/mo_frontend/stability.mli b/src/mo_frontend/stability.mli index 8568f20103b..620fb4de244 100644 --- a/src/mo_frontend/stability.mli +++ b/src/mo_frontend/stability.mli @@ -6,4 +6,4 @@ open Mo_types c.f. (simpler) Types.match_sig. *) -val match_stab_sig : Type.field list -> Type.field list -> unit Diag.result +val match_stab_sig : Type.stab_sig -> Type.stab_sig -> unit Diag.result diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 35f90d81718..9e819aaca86 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -3214,7 +3214,7 @@ let check_lib scope pkg_opt lib : Scope.t Diag.result = ) lib ) -let check_stab_sig scope sig_ : (T.field list) Diag.result = +let check_stab_sig scope sig_ : T.stab_sig Diag.result = Diag.with_message_store (fun msgs -> recover_opt @@ -3222,25 +3222,31 @@ let check_stab_sig scope sig_ : (T.field list) Diag.result = let env = env_of_scope msgs scope in let scope = infer_block_decs env decs sig_.at in let env1 = adjoin env scope in - check_ids env "object type" "field" - (List.filter_map (fun (field : typ_field) -> - match field.it with ValF (id, _, _) -> Some id | _ -> None) - sfs); - check_ids env "object type" "type field" - (List.filter_map (fun (field : typ_field) -> - match field.it with TypF (id, _, _) -> Some id | _ -> None) - sfs); - let _ = List.map (check_typ_field {env1 with pre = true} T.Object) sfs in - let fs = List.map (check_typ_field {env1 with pre = false} T.Object) sfs in - List.iter (fun (field : Syntax.typ_field) -> - match field.it with - | TypF _ -> () - | ValF (id, typ, _) -> - if not (T.stable typ.note) then - error env id.at "M0131" "variable %s is declared stable but has non-stable type%a" - id.it - display_typ typ.note) - sfs; - List.sort T.compare_field fs + let check_fields sfs = + check_ids env "object type" "field" + (List.filter_map (fun (field : typ_field) -> + match field.it with ValF (id, _, _) -> Some id | _ -> None) + sfs); + check_ids env "object type" "type field" + (List.filter_map (fun (field : typ_field) -> + match field.it with TypF (id, _, _) -> Some id | _ -> None) + sfs); + let _ = List.map (check_typ_field {env1 with pre = true} T.Object) sfs in + let fs = List.map (check_typ_field {env1 with pre = false} T.Object) sfs in + List.iter (fun (field : Syntax.typ_field) -> + match field.it with + | TypF _ -> () + | ValF (id, typ, _) -> + if not (T.stable typ.note) then + error env id.at "M0131" "variable %s is declared stable but has non-stable type%a" + id.it + display_typ typ.note) + sfs; + List.sort T.compare_field fs + in + match sfs.it with + | Single sfs -> T.Single (check_fields sfs) + | PrePost (pre,post) -> + T.PrePost (check_fields pre, check_fields post) ) sig_.it ) diff --git a/src/mo_frontend/typing.mli b/src/mo_frontend/typing.mli index be0d8b40b7e..2bb01f47ea7 100644 --- a/src/mo_frontend/typing.mli +++ b/src/mo_frontend/typing.mli @@ -10,6 +10,6 @@ val infer_prog : ?viper_mode:bool -> scope -> string option -> Async_cap.async_c val check_lib : scope -> string option -> Syntax.lib -> scope Diag.result val check_actors : ?viper_mode:bool -> ?check_actors:bool -> scope -> Syntax.prog list -> unit Diag.result -val check_stab_sig : scope -> Syntax.stab_sig -> (field list) Diag.result +val check_stab_sig : scope -> Syntax.stab_sig -> Type.stab_sig Diag.result val heartbeat_type : typ diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index 3c0b25609ff..c9165285400 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -72,6 +72,11 @@ and kind = let empty_src = {depr = None; region = Source.no_region} +(* Stable signatures *) +type stab_sig = + | Single of field list + | PrePost of field list * field list + (* Efficient comparison *) let tag_prim = function | Null -> 0 @@ -1754,11 +1759,15 @@ and pp_kind ppf k = pp_kind' vs ppf k and pp_stab_sig ppf sig_ = + let all_fields = match sig_ with + | Single tfs -> tfs + | PrePost (pre, post) -> pre @ post + in let cs = List.fold_right (cons_field false) (* false here ^ means ignore unreferenced Typ c components that would produce unreferenced bindings when unfolded *) - sig_ ConSet.empty in + all_fields ConSet.empty in let vs = vs_of_cs cs in let ds = let cs' = ConSet.filter (fun c -> @@ -1776,15 +1785,22 @@ and pp_stab_sig ppf sig_ = typ = Typ c; src = empty_src }) ds) in - let pp_stab_fields ppf sig_ = - fprintf ppf "@[%s{@;<0 0>%a@;<0 -2>}@]" - (string_of_obj_sort Actor) - (pp_print_list ~pp_sep:semi (pp_stab_field vs)) sig_ + let pp_stab_actor ppf sig_ = + match sig_ with + | Single tfs -> + fprintf ppf "@[%s{@;<0 0>%a@;<0 -2>}@]" + (string_of_obj_sort Actor) + (pp_print_list ~pp_sep:semi (pp_stab_field vs)) tfs + | PrePost (pre, post) -> + fprintf ppf "@[%s({@;<0 0>%a@;<0 -2>}, {@;<0 0>%a@;<0 -2>} @]" + (string_of_obj_sort Actor) + (pp_print_list ~pp_sep:semi (pp_stab_field vs)) pre + (pp_print_list ~pp_sep:semi (pp_stab_field vs)) post in - fprintf ppf "@[%a%a%a;@]" - (pp_print_list ~pp_sep:semi (pp_field vs)) fs - (if fs = [] then fun ppf () -> () else semi) () - pp_stab_fields sig_ + fprintf ppf "@[%a%a%a;@]" + (pp_print_list ~pp_sep:semi (pp_field vs)) fs + (if fs = [] then fun ppf () -> () else semi) () + pp_stab_actor sig_ let rec pp_typ_expand' vs ppf t = match t with @@ -1850,7 +1866,20 @@ let _ = str := string_of_typ (* Stable signatures *) -let rec match_stab_sig tfs1 tfs2 = +let pre = function + | Single tfs -> tfs + | PrePost (tfs, _) -> tfs + +let post = function + | Single tfs -> tfs + | PrePost (_, tfs) -> tfs + +let rec match_stab_sig sig1 sig2 = + let tfs1 = post sig1 in + let tfs2 = pre sig2 in + match_stab_fields tfs1 tfs2 + +and match_stab_fields tfs1 tfs2 = (* Assume that tfs1 and tfs2 are sorted. *) match tfs1, tfs2 with | [], _ | _, [] -> @@ -1860,16 +1889,17 @@ let rec match_stab_sig tfs1 tfs2 = (match compare_field tf1 tf2 with | 0 -> sub (as_immut tf1.typ) (as_immut tf2.typ) && - match_stab_sig tfs1' tfs2' + match_stab_fields tfs1' tfs2' | -1 -> (* dropped field ok *) - match_stab_sig tfs1' tfs2 + match_stab_fields tfs1' tfs2 | _ -> (* new field ok *) - match_stab_sig tfs1 tfs2' + match_stab_fields tfs1 tfs2' ) -let string_of_stab_sig fields : string = +let string_of_stab_sig stab_sig : string = let module Pretty = MakePretty(ParseableStamps) in - "// Version: 1.0.0\n" ^ - Format.asprintf "@[%a@]@\n" (fun ppf -> Pretty.pp_stab_sig ppf) fields + "// Version: 2.0\n" ^ + Format.asprintf "@[%a@]@\n" (fun ppf -> Pretty.pp_stab_sig ppf) stab_sig + diff --git a/src/mo_types/type.mli b/src/mo_types/type.mli index b94c9eb7468..cba21c47984 100644 --- a/src/mo_types/type.mli +++ b/src/mo_types/type.mli @@ -262,9 +262,16 @@ val scope_bind : bind (* Signatures *) -val match_stab_sig : field list -> field list -> bool +type stab_sig = + | Single of field list + | PrePost of field list * field list -val string_of_stab_sig : field list -> string +val pre : stab_sig -> field list +val post : stab_sig -> field list + +val match_stab_sig : stab_sig -> stab_sig -> bool + +val string_of_stab_sig : stab_sig -> string val motoko_runtime_information_type : typ From a73956d7e00b53ee30089517a07ed3fb55b22d7a Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Fri, 20 Dec 2024 17:59:10 +0000 Subject: [PATCH 2/8] fix printer --- src/mo_types/type.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index c9165285400..31386be100c 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -1792,7 +1792,7 @@ and pp_stab_sig ppf sig_ = (string_of_obj_sort Actor) (pp_print_list ~pp_sep:semi (pp_stab_field vs)) tfs | PrePost (pre, post) -> - fprintf ppf "@[%s({@;<0 0>%a@;<0 -2>}, {@;<0 0>%a@;<0 -2>} @]" + fprintf ppf "@[%s({@;<0 0>%a@;<0 -2>}, {@;<0 0>%a@;<0 -2>}) @]" (string_of_obj_sort Actor) (pp_print_list ~pp_sep:semi (pp_stab_field vs)) pre (pp_print_list ~pp_sep:semi (pp_stab_field vs)) post From f65d3f00a91e7f204143c523cb50b8969bd29a84 Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Fri, 20 Dec 2024 18:02:21 +0000 Subject: [PATCH 3/8] fix printer --- src/mo_types/type.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index 31386be100c..1197c045f0a 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -1789,18 +1789,18 @@ and pp_stab_sig ppf sig_ = match sig_ with | Single tfs -> fprintf ppf "@[%s{@;<0 0>%a@;<0 -2>}@]" - (string_of_obj_sort Actor) - (pp_print_list ~pp_sep:semi (pp_stab_field vs)) tfs + (string_of_obj_sort Actor) + (pp_print_list ~pp_sep:semi (pp_stab_field vs)) tfs | PrePost (pre, post) -> fprintf ppf "@[%s({@;<0 0>%a@;<0 -2>}, {@;<0 0>%a@;<0 -2>}) @]" - (string_of_obj_sort Actor) - (pp_print_list ~pp_sep:semi (pp_stab_field vs)) pre - (pp_print_list ~pp_sep:semi (pp_stab_field vs)) post + (string_of_obj_sort Actor) + (pp_print_list ~pp_sep:semi (pp_stab_field vs)) pre + (pp_print_list ~pp_sep:semi (pp_stab_field vs)) post in - fprintf ppf "@[%a%a%a;@]" - (pp_print_list ~pp_sep:semi (pp_field vs)) fs - (if fs = [] then fun ppf () -> () else semi) () - pp_stab_actor sig_ + fprintf ppf "@[%a%a%a;@]" + (pp_print_list ~pp_sep:semi (pp_field vs)) fs + (if fs = [] then fun ppf () -> () else semi) () + pp_stab_actor sig_ let rec pp_typ_expand' vs ppf t = match t with From 9f4ab927cdef049aaea4c9459c32f7427a8e0a76 Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Wed, 8 Jan 2025 10:23:13 +0000 Subject: [PATCH 4/8] refine versioning --- src/mo_types/type.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index 1197c045f0a..0c59b141f33 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -1900,6 +1900,8 @@ and match_stab_fields tfs1 tfs2 = let string_of_stab_sig stab_sig : string = let module Pretty = MakePretty(ParseableStamps) in - "// Version: 2.0\n" ^ + (match stab_sig with + | Single _ -> "// Version: 1.0.0\n" + | PrePost _-> "// Version: 2.0.0\n") ^ Format.asprintf "@[%a@]@\n" (fun ppf -> Pretty.pp_stab_sig ppf) stab_sig From 047e153002f5794d88d7b970ad71a2f6b47fa11c Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Wed, 8 Jan 2025 10:41:25 +0000 Subject: [PATCH 5/8] fix grammar --- doc/md/examples/grammar.txt | 1 - src/gen-grammar/grammar.sed | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/md/examples/grammar.txt b/doc/md/examples/grammar.txt index 9e20af6a947..5d20ddf28e0 100644 --- a/doc/md/examples/grammar.txt +++ b/doc/md/examples/grammar.txt @@ -336,6 +336,5 @@ ::= , ';')> , ';')> - , ';')> 'actor' '(' '{' , ';')> '}' ',' '{' , ';')> '}' ')' diff --git a/src/gen-grammar/grammar.sed b/src/gen-grammar/grammar.sed index 45d4698f044..4f8be9b2b70 100644 --- a/src/gen-grammar/grammar.sed +++ b/src/gen-grammar/grammar.sed @@ -12,7 +12,7 @@ s//ID/g /^ ::=/,+2d /^ ::=/,+2d /^ ::=/,+2d -/^ ::=/,+2d +/^ ::=/,+5d /.*PRIM.*/d /^ ::=/,+2d /^ ::=/,+2d From df60b8189ba0d62149414401abc33d1b15cb3c3f Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Wed, 8 Jan 2025 11:01:29 +0000 Subject: [PATCH 6/8] remove fix me --- src/mo_frontend/parser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mo_frontend/parser.mly b/src/mo_frontend/parser.mly index faa7429647f..f19d8b65918 100644 --- a/src/mo_frontend/parser.mly +++ b/src/mo_frontend/parser.mly @@ -1008,7 +1008,7 @@ parse_stab_sig : ACTOR LPAR LCURLY sfs_pre=seplist(stab_field, semicolon) RCURLY COMMA LCURLY sfs_post=seplist(stab_field, semicolon) RCURLY RPAR { let trivia = !triv_table in - let sigs = PrePost(sfs_pre, sfs_post) in (* FIX ME*) + let sigs = PrePost(sfs_pre, sfs_post) in fun filename -> { it = (ds, {it=sigs; at = at $sloc; note = ()}); at = at $sloc; From 9d26155c1a8d15087808a8c585af2e9dea763df3 Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Wed, 8 Jan 2025 18:52:37 +0000 Subject: [PATCH 7/8] Claudio/migration eop sigs refactor (#4842) * refactoring (buggy) * fix bug * renaming * use blockE to avoid nested letE --- src/lowering/desugar.ml | 136 ++++++++++++++++++++++------------------ 1 file changed, 74 insertions(+), 62 deletions(-) diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index 5c4f1f7ae0c..112587f9d91 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -541,87 +541,99 @@ and build_actor at ts exp_opt self_id es obj_typ = let pairs = List.map2 stabilize stabs ds in let idss = List.map fst pairs in let ids = List.concat idss in - let sig_post = List.sort T.compare_field - (List.map (fun (i,t) -> T.{lab = i; typ = t; src = empty_src}) ids) + let stab_fields = List.sort T.compare_field + (List.map (fun (i, t) -> T.{lab = i; typ = t; src = empty_src}) ids) in - let fields = List.map (fun (i,t) -> T.{lab = i; typ = T.Opt (T.as_immut t); src = T.empty_src}) ids in + let mem_fields = + List.map + (fun tf -> {tf with T.typ = T.Opt (T.as_immut tf.T.typ) } ) + stab_fields in let mk_ds = List.map snd pairs in - let ty = T.Obj (T.Memory, List.sort T.compare_field fields) in - let state = fresh_var "state" (T.Mut (T.Opt ty)) in - let get_state = fresh_var "getState" (T.Func(T.Local, T.Returns, [], [], [ty])) in + let mem_ty = T.Obj (T.Memory, mem_fields) in + let state = fresh_var "state" (T.Mut (T.Opt mem_ty)) in + let get_state = fresh_var "getState" (T.Func(T.Local, T.Returns, [], [], [mem_ty])) in let ds = List.map (fun mk_d -> mk_d get_state) mk_ds in let sig_, stable_type, migration = match exp_opt with | None -> - T.Single sig_post, - I.{pre = ty; post = ty}, - primE (I.ICStableRead ty) [] (* as before *) + T.Single stab_fields, + I.{pre = mem_ty; post = mem_ty}, + primE (I.ICStableRead mem_ty) [] (* as before *) | Some exp0 -> let e = exp exp0 in let [@warning "-8"] (_s,_c, [], [dom], [rng]) = T.as_func (exp0.note.S.note_typ) in let [@warning "-8"] (T.Object, dom_fields) = T.as_obj dom in let [@warning "-8"] (T.Object, rng_fields) = T.as_obj rng in - let sig_pre = - List.sort T.compare_field - (dom_fields @ - (List.filter_map - (fun (i,t) -> - match T.lookup_val_field_opt i dom_fields with - | Some t -> - (* ignore overriden *) - None - | None -> - (* retain others *) - Some T.{lab = i; typ = t; src = T.empty_src}) ids)) + let stab_fields_pre = + List.sort T.compare_field + (dom_fields @ + (List.filter_map + (fun tf -> + match T.lookup_val_field_opt tf.T.lab dom_fields with + | Some t -> + (* ignore overriden *) + None + | None -> + (* retain others *) + Some tf) + stab_fields)) in - let fields' = - List.map - (fun tf -> - { tf with T.typ = T.Opt (T.as_immut tf.T.typ) }) - sig_pre + let mem_fields_pre = + List.map + (fun tf -> { tf with T.typ = T.Opt (T.as_immut tf.T.typ) }) + stab_fields_pre in - let ty' = T.Obj (T.Memory, fields') in - let v = fresh_var "v" ty' in + let mem_ty_pre = T.Obj (T.Memory, mem_fields_pre) in + let v = fresh_var "v" mem_ty_pre in let v_dom = fresh_var "v_dom" dom in let v_rng = fresh_var "v_rng" rng in - T.PrePost (sig_pre, sig_post), - I.{pre = ty'; post = ty}, + T.PrePost (stab_fields_pre, stab_fields), + I.{pre = mem_ty_pre; post = mem_ty}, ifE (primE (I.OtherPrim "rts_in_install") []) - (primE (I.ICStableRead ty) []) - (letE v (primE (I.ICStableRead ty') []) - (letE v_dom + (primE (I.ICStableRead mem_ty) []) + (blockE [ + letD v (primE (I.ICStableRead mem_ty_pre) []); + letD v_dom (objectE T.Object - (List.map (fun T.{lab=i;typ=t;_} -> - let vi = fresh_var ("v_"^i) (T.as_immut t) in - (i, switch_optE (dotE (varE v) i (T.Opt (T.as_immut t))) + (List.map + (fun T.{lab=i;typ=t;_} -> + let vi = fresh_var ("v_"^i) (T.as_immut t) in + (i, + switch_optE (dotE (varE v) i (T.Opt (T.as_immut t))) (primE (Ir.OtherPrim "trap") - [textE (Printf.sprintf - "stable variable `%s` of type `%s` expected but not found" i (T.string_of_typ t))]) - (varP vi) (varE vi) - (T.as_immut t))) dom_fields) dom_fields) - (letE v_rng (callE e [] (varE v_dom)) - (objectE T.Memory - (List.map (fun T.{lab=i;typ=t;_} -> - i, - match T.lookup_val_field_opt i rng_fields with - (* produced by migration *) - | Some t -> optE (dotE (varE v_rng) i (T.as_immut t)) (* wrap in ?_*) - | None -> - (* not produced by migration *) - match T.lookup_val_field_opt i dom_fields with - | Some t -> nullE() (* consumed by migration (not produced) *) - (*TBR: could also reuse if compatible *) - | None -> dotE (varE v) i t) - fields) fields)))) + [textE (Printf.sprintf + "stable variable `%s` of type `%s` expected but not found" + i (T.string_of_typ t))]) + (varP vi) (varE vi) + (T.as_immut t))) + dom_fields) + dom_fields); + letD v_rng (callE e [] (varE v_dom)) + ] + (objectE T.Memory + (List.map + (fun T.{lab=i;typ=t;_} -> + i, + match T.lookup_val_field_opt i rng_fields with + | Some t -> (* produced by migration *) + optE (dotE (varE v_rng) i (T.as_immut t)) (* wrap in ?_*) + | None -> (* not produced by migration *) + match T.lookup_val_field_opt i dom_fields with + | Some t -> + (* consumed by migration (not produced) *) + nullE() (* TBR: could also reuse if compatible *) + | None -> dotE (varE v) i t) + mem_fields) + mem_fields)) in let ds = varD state (optE migration) :: nary_funcD get_state [] - (let v = fresh_var "v" ty in + (let v = fresh_var "v" mem_ty in switch_optE (immuteE (varE state)) (unreachableE ()) (varP v) (varE v) - ty) + mem_ty) :: ds @ @@ -629,32 +641,32 @@ and build_actor at ts exp_opt self_id es obj_typ = in let ds' = match self_id with | Some n -> - with_self n.it obj_typ ds + with_self n.it obj_typ ds | None -> ds in let meta = I.{ candid = candid; sig_ = T.string_of_stab_sig sig_} in let with_stable_vars wrap = - let vs = fresh_vars "v" (List.map (fun f -> f.T.typ) fields) in + let vs = fresh_vars "v" (List.map (fun f -> f.T.typ) mem_fields) in blockE ((match call_system_func_opt "preupgrade" es obj_typ with | Some call -> [ expD call] | None -> []) @ [letP (seqP (List.map varP vs)) (* dereference any mutable vars, option 'em all *) - (seqE (List.map (fun (i,t) -> optE (varE (var i t))) ids))]) + (seqE (List.map (fun tf -> optE (varE (var tf.T.lab tf.T.typ))) stab_fields))]) (wrap (newObjE T.Memory (List.map2 (fun f v -> { it = I.{name = f.T.lab; var = id_of_var v}; at = no_region; note = f.T.typ } - ) fields vs) - ty)) in + ) mem_fields vs) + mem_ty)) in let footprint_d, footprint_f = export_footprint self_id (with_stable_vars Fun.id) in let runtime_info_d, runtime_info_f = export_runtime_information self_id in I.(ActorE (footprint_d @ runtime_info_d @ ds', footprint_f @ runtime_info_f @ fs, { meta; - preupgrade = (primE (I.ICStableWrite ty) []); + preupgrade = (primE (I.ICStableWrite mem_ty) []); postupgrade = (match call_system_func_opt "postupgrade" es obj_typ with | Some call -> call From 8328adf6144057d2a78e26115affd42f607f259f Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Wed, 8 Jan 2025 19:18:05 +0000 Subject: [PATCH 8/8] simplify; delete trailing whitespace --- src/lowering/desugar.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/lowering/desugar.ml b/src/lowering/desugar.ml index 112587f9d91..f8d317cff8d 100644 --- a/src/lowering/desugar.ml +++ b/src/lowering/desugar.ml @@ -477,7 +477,7 @@ and export_runtime_information self_id = let scope_con2 = Cons.fresh "T2" (Abs ([], Any)) in let bind1 = typ_arg scope_con1 Scope scope_bound in let bind2 = typ_arg scope_con2 Scope scope_bound in - let gc_strategy = + let gc_strategy = let open Mo_config in let strategy = match !Flags.gc_strategy with | Flags.Default -> "default" @@ -513,19 +513,19 @@ and export_runtime_information self_id = (asyncE T.Fut bind2 (blockE ([ letD caller (primE I.ICCallerPrim []); - expD (ifE (orE + expD (ifE (orE (primE (I.RelPrim (principal, Operator.EqOp)) [varE caller; selfRefE principal]) (primE (I.OtherPrim "is_controller") [varE caller])) - (unitE()) + (unitE()) (primE (Ir.OtherPrim "trap") [textE "Unauthorized call of __motoko_runtime_information"])) ] @ - (List.map2 (fun field (_, load_info, _) -> + (List.map2 (fun field (_, load_info, _) -> letD field load_info ) fields information)) (newObjE T.Object - (List.map2 (fun field (name, _, typ) -> - { it = Ir.{name; var = id_of_var field}; at = no_region; note = typ }) + (List.map2 (fun field (name, _, typ) -> + { it = Ir.{name; var = id_of_var field}; at = no_region; note = typ }) fields information ) ret_typ)) (Con (scope_con1, [])))) @@ -560,9 +560,9 @@ and build_actor at ts exp_opt self_id es obj_typ = primE (I.ICStableRead mem_ty) [] (* as before *) | Some exp0 -> let e = exp exp0 in - let [@warning "-8"] (_s,_c, [], [dom], [rng]) = T.as_func (exp0.note.S.note_typ) in - let [@warning "-8"] (T.Object, dom_fields) = T.as_obj dom in - let [@warning "-8"] (T.Object, rng_fields) = T.as_obj rng in + let dom, rng = T.as_mono_func_sub (exp0.note.S.note_typ) in + let (_dom_sort, dom_fields) = T.as_obj (T.normalize dom) in + let (_rng_sort, rng_fields) = T.as_obj (T.promote rng) in let stab_fields_pre = List.sort T.compare_field (dom_fields @ @@ -1138,7 +1138,7 @@ let import_compiled_class (lib : S.comp_unit) wasm : import_declaration = (callE (varE install_actor_helper) cs' (tupE [ install_arg; - boolE ((!Mo_config.Flags.enhanced_orthogonal_persistence)); + boolE ((!Mo_config.Flags.enhanced_orthogonal_persistence)); varE wasm_blob; primE (Ir.SerializePrim ts1') [seqE (List.map varE vs)]]))) (primE (Ir.CastPrim (T.principal, t_actor)) [varE principal]))