From c8b679877a1d33858327cc184cfa0a5b44164b80 Mon Sep 17 00:00:00 2001 From: Claudio Russo Date: Fri, 20 Dec 2024 17:17:27 +0000 Subject: [PATCH] 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