diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index a6631d7c65..b3787fb864 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -34,18 +34,6 @@ let flatten_rec def = | Ast.RecD defs -> defs | _ -> [ def ] -(* List of relation names that appear in the prose of the validation rules *) -let validation_helper_relations = [ - "Expand"; - "Expand_use"; - "ImmutReachable"; - "NotImmutReachable" -] -let is_validation_helper_relation def = - match def.it with - | Ast.RelD (id, _, _, _, _) -> - List.mem id.it validation_helper_relations - | _ -> false (* NOTE: Assume validation relation is `|-` *) let is_validation_relation def = match def.it with @@ -53,17 +41,112 @@ let is_validation_relation def = List.exists (List.exists (fun atom -> atom.it = Atom.Turnstile)) (Mixop.flatten mixop) | _ -> false -let extract_validation_il il = - il - |> List.concat_map flatten_rec - |> List.filter - (fun rel -> is_validation_relation rel || is_validation_helper_relation rel) +let pairwise_concat xyss = + (* [(xs1, ys1); (xs2, ys2)] ==> (xs1@xs2, ys1@ys2) *) + let xss, yss = List.split xyss in + List.concat xss, List.concat yss + +let pairwise_concat_map f xs = List.map f xs |> pairwise_concat + +(* dependent_rei_id_of_X: (x:X) -> (rel_id list, func_id list) *) + +let dependent_rel_id_of_exp exp = + let func_ids = ref [] in + let collect_func_call e = + (match e.it with + | Ast.CallE (id, _) -> func_ids := id :: !func_ids + | _ -> () + ); + e + in + + let open Il2al.Il_walk in + let transformer = { base_transformer with + transform_exp = collect_func_call; + } in + ignore (transform_exp transformer exp); + + [], !func_ids + +let rec dependent_rel_id_of_prem prem = + match prem.it with + | Ast.IfPr exp -> dependent_rel_id_of_exp exp + | Ast.LetPr (exp1, exp2, _) -> pairwise_concat_map dependent_rel_id_of_exp [exp1; exp2] + | Ast.RulePr (id, _, _, exp) -> pairwise_concat [([id], []); dependent_rel_id_of_exp exp] + | Ast.IterPr (prem', _) -> dependent_rel_id_of_prem prem' + | _ -> ([], []) + +let dependent_ids_of_rule rule = + match rule.it with + | Ast.RuleD (_, _, _, _, prems) -> pairwise_concat_map dependent_rel_id_of_prem prems + +let dependent_ids_of_clause clause = + match clause.it with + | Ast.DefD (_, _, _, prems) -> pairwise_concat_map dependent_rel_id_of_prem prems + +let dependent_ids_of_def def = + match def.it with + | Ast.RelD (_, _, _, _, rules) -> pairwise_concat_map dependent_ids_of_rule rules + | Ast.DecD (_, _, _, clauses) -> pairwise_concat_map dependent_ids_of_clause clauses + | _ -> ([], []) let rel_has_id id rel = match rel.it with - | Ast.RelD (id', _, _, _, _) -> id.it = id'.it + | Ast.RelD (id', _, _, _, _) -> Eq.eq_id id id' + | _ -> false + +let func_has_id id func = + match func.it with + | Ast.DecD (id', _, _, _) -> Eq.eq_id id id' | _ -> false +let id_to_rel defs id = + List.find (rel_has_id id) defs + +let id_to_func funcs id = + List.find (func_has_id id) funcs + +let rec dedup ids = + match ids with + | [] -> [] + | hd :: tl -> + let tl' = List.filter (fun id -> not (Eq.eq_id hd id)) tl in + hd :: dedup tl' + +let extract_validation_il il = + let all_defs = List.concat_map flatten_rec il in + let validation_rels = List.filter is_validation_relation all_defs in + + (* Expand according to the premise dependency *) + let rec expand (prev_rels, prev_funcs) (new_rels, new_funcs) = + let rels = new_rels @ prev_rels in + let is_new_rel_id id = List.for_all (Fun.negate (rel_has_id id)) rels in + let funcs = new_funcs @ prev_funcs in + let is_new_func_id id = List.for_all (Fun.negate (func_has_id id)) funcs in + + match new_rels @ new_funcs with + | [] -> rels + | defs -> + let (rel_ids, func_ids) = pairwise_concat_map dependent_ids_of_def defs in + + let prem_rels = + rel_ids + |> dedup + |> List.filter is_new_rel_id + |> List.map (id_to_rel all_defs) + in + let prem_funcs = + func_ids + |> dedup + |> List.filter is_new_func_id + |> List.map (id_to_func all_defs) + in + + expand (rels, funcs) (prem_rels, prem_funcs) + in + + expand ([], []) (validation_rels, []) + let extract_prose_hint hintexp = match hintexp.it with | El.Ast.TextE hint -> Some hint @@ -293,7 +376,8 @@ let rec prem_to_instrs prem = let rel = match List.find_opt (rel_has_id id) !Langs.validation_il with | Some rel -> rel - | None -> failwith ("Unknown relation id: " ^ id.it) + | None -> failwith ( + Printf.sprintf "The relation %s is supposed to be included in `validation_il`. Hint: Plese fix `extract_validation_il`." id.it) in let frees = (Free.free_prem prem).varid in let args = exp_to_argexpr e in diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md index 6e7df6d0f0..ffb5bc2c55 100644 --- a/spectec/test-prose/TEST.md +++ b/spectec/test-prose/TEST.md @@ -13748,27 +13748,108 @@ spectec 0.5 generator -The number type :math:`{\mathit{numtype}}` is always :ref:`valid `. +:math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}}_1` if: + * Either: + * :math:`{\mathit{fv}'}` is immutably reachable from :math:`{\mathit{fv}}_1`. -The vector type :math:`{\mathit{vectype}}` is always :ref:`valid `. + * :math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}'}`. + * Or: + * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}struct}~a)`. + * The field value :math:`{\mathit{fv}}_2` is of the form :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]`. -The packed type :math:`{\mathit{packtype}}` is always :ref:`valid `. + * The field value :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]` exists. + * The structure instance :math:`s{.}\mathsf{structs}{}[a]` exists. + * The :ref:`expansion ` of :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{struct}~{{\mathit{ft}}^\ast})`. + * The length of :math:`{{\mathit{ft}}^\ast}` is greater than :math:`i`. -The packed type :math:`{\mathit{packtype}}` :ref:`matches ` only itself. + * The field type :math:`{{\mathit{ft}}^\ast}{}[i]` is of the form :math:`(\epsilon~{\mathit{zt}})`. + * Or: + + * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}array}~a)`. + * The field value :math:`{\mathit{fv}}_2` is of the form :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]`. + * The field value :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]` exists. + * The array instance :math:`s{.}\mathsf{arrays}{}[a]` exists. -The number type :math:`{\mathit{numtype}}` :ref:`matches ` only itself. + * The :ref:`expansion ` of :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{array}~(\epsilon~{\mathit{zt}}))`. + * Or: + + * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}exn}~a)`. + + * The field value :math:`{\mathit{fv}}_2` is of the form :math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]`. + + * The value :math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]` exists. + + * The exception instance :math:`s{.}\mathsf{exns}{}[a]` exists. + * Or: + + * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}extern}~{\mathit{ref}})`. + + * The field value :math:`{\mathit{fv}}_2` is of the form :math:`{\mathit{ref}}`. + + + + +:math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}}_1` if: + + + * :math:`{\mathit{fv}'}` is immutably reachable from :math:`{\mathit{fv}}_1`. + + * :math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}'}`. + + + + +:math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]` is immutably reachable from :math:`(\mathsf{ref{.}struct}~a)` if: + + + * The field value :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]` exists. + + * The structure instance :math:`s{.}\mathsf{structs}{}[a]` exists. + + * The :ref:`expansion ` of :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{struct}~{{\mathit{ft}}^\ast})`. + + * The length of :math:`{{\mathit{ft}}^\ast}` is greater than :math:`i`. + + * The field type :math:`{{\mathit{ft}}^\ast}{}[i]` is of the form :math:`(\epsilon~{\mathit{zt}})`. + + + + +:math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]` is immutably reachable from :math:`(\mathsf{ref{.}array}~a)` if: + + + * The field value :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]` exists. + + * The array instance :math:`s{.}\mathsf{arrays}{}[a]` exists. + + * The :ref:`expansion ` of :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{array}~(\epsilon~{\mathit{zt}}))`. + + + + +:math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]` is immutably reachable from :math:`(\mathsf{ref{.}exn}~a)` if: + + + * The value :math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]` exists. + + * The exception instance :math:`s{.}\mathsf{exns}{}[a]` exists. + + + + +:math:`{\mathit{ref}}` is immutably reachable from :math:`(\mathsf{ref{.}extern}~{\mathit{ref}})`. @@ -13781,6 +13862,77 @@ The :ref:`expansion ` of :math:`{\mathit{deftype}}` is :math +The :ref:`expansion ` of :math:`C` is :math:`{\mathit{comptype}}` if: + + + * Either: + + * The type use :math:`{\mathit{typeuse}}` is of the form :math:`{\mathit{deftype}}`. + + * The :ref:`expansion ` of :math:`{\mathit{deftype}}` is :math:`{\mathit{comptype}}`. + + * Or: + + * The type use :math:`{\mathit{typeuse}}` is of the form :math:`{\mathit{typeidx}}`. + + * The type :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` exists. + + * The :ref:`expansion ` of :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` is :math:`{\mathit{comptype}}`. + + + + +The :ref:`expansion ` of :math:`C` is :math:`{\mathit{comptype}}` if: + + + * The :ref:`expansion ` of :math:`{\mathit{deftype}}` is :math:`{\mathit{comptype}}`. + + + + +The :ref:`expansion ` of :math:`C` is :math:`{\mathit{comptype}}` if: + + + * The type :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` exists. + + * The :ref:`expansion ` of :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` is :math:`{\mathit{comptype}}`. + + + + +:math:`{\mathit{fv}}_2` is not immutably reachable from :math:`{\mathit{fv}}_1` if: + + + * NotImmutReachable(:math:`{\mathit{fv}}_1`, :math:`s`, :math:`{\mathit{fv}}_2`) is true. + + + + +The number type :math:`{\mathit{numtype}}` is always :ref:`valid `. + + + + +The vector type :math:`{\mathit{vectype}}` is always :ref:`valid `. + + + + +The packed type :math:`{\mathit{packtype}}` is always :ref:`valid `. + + + + +The packed type :math:`{\mathit{packtype}}` :ref:`matches ` only itself. + + + + +The number type :math:`{\mathit{numtype}}` :ref:`matches ` only itself. + + + + The vector type :math:`{\mathit{vectype}}` :ref:`matches ` only itself. @@ -14685,44 +14837,6 @@ The instruction type :math:`{t_1^\ast}~{\rightarrow}_{{x^\ast}}\,{t_2^\ast}` is -The :ref:`expansion ` of :math:`C` is :math:`{\mathit{comptype}}` if: - - - * Either: - - * The type use :math:`{\mathit{typeuse}}` is of the form :math:`{\mathit{deftype}}`. - - * The :ref:`expansion ` of :math:`{\mathit{deftype}}` is :math:`{\mathit{comptype}}`. - - * Or: - - * The type use :math:`{\mathit{typeuse}}` is of the form :math:`{\mathit{typeidx}}`. - - * The type :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` exists. - - * The :ref:`expansion ` of :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` is :math:`{\mathit{comptype}}`. - - - - -The :ref:`expansion ` of :math:`C` is :math:`{\mathit{comptype}}` if: - - - * The :ref:`expansion ` of :math:`{\mathit{deftype}}` is :math:`{\mathit{comptype}}`. - - - - -The :ref:`expansion ` of :math:`C` is :math:`{\mathit{comptype}}` if: - - - * The type :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` exists. - - * The :ref:`expansion ` of :math:`C{.}\mathsf{types}{}[{\mathit{typeidx}}]` is :math:`{\mathit{comptype}}`. - - - - The sub type :math:`(\mathsf{sub}~{\mathsf{final}^?}~{x^\ast}~{\mathit{comptype}})` is :ref:`valid ` for the type index :math:`x_0` if: @@ -18182,120 +18296,6 @@ The exception instance :math:`\{ \mathsf{tag}~{\mathit{ta}},\;\allowbreak \maths -:math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}}_1` if: - - - * Either: - - * :math:`{\mathit{fv}'}` is immutably reachable from :math:`{\mathit{fv}}_1`. - - * :math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}'}`. - - * Or: - - * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}struct}~a)`. - - * The field value :math:`{\mathit{fv}}_2` is of the form :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]`. - - * The field value :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]` exists. - - * The structure instance :math:`s{.}\mathsf{structs}{}[a]` exists. - - * The :ref:`expansion ` of :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{struct}~{{\mathit{ft}}^\ast})`. - - * The length of :math:`{{\mathit{ft}}^\ast}` is greater than :math:`i`. - - * The field type :math:`{{\mathit{ft}}^\ast}{}[i]` is of the form :math:`(\epsilon~{\mathit{zt}})`. - * Or: - - * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}array}~a)`. - - * The field value :math:`{\mathit{fv}}_2` is of the form :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]`. - - * The field value :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]` exists. - - * The array instance :math:`s{.}\mathsf{arrays}{}[a]` exists. - - * The :ref:`expansion ` of :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{array}~(\epsilon~{\mathit{zt}}))`. - * Or: - - * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}exn}~a)`. - - * The field value :math:`{\mathit{fv}}_2` is of the form :math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]`. - - * The value :math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]` exists. - - * The exception instance :math:`s{.}\mathsf{exns}{}[a]` exists. - * Or: - - * The field value :math:`{\mathit{fv}}_1` is of the form :math:`(\mathsf{ref{.}extern}~{\mathit{ref}})`. - - * The field value :math:`{\mathit{fv}}_2` is of the form :math:`{\mathit{ref}}`. - - - - -:math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}}_1` if: - - - * :math:`{\mathit{fv}'}` is immutably reachable from :math:`{\mathit{fv}}_1`. - - * :math:`{\mathit{fv}}_2` is immutably reachable from :math:`{\mathit{fv}'}`. - - - - -:math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]` is immutably reachable from :math:`(\mathsf{ref{.}struct}~a)` if: - - - * The field value :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{fields}{}[i]` exists. - - * The structure instance :math:`s{.}\mathsf{structs}{}[a]` exists. - - * The :ref:`expansion ` of :math:`s{.}\mathsf{structs}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{struct}~{{\mathit{ft}}^\ast})`. - - * The length of :math:`{{\mathit{ft}}^\ast}` is greater than :math:`i`. - - * The field type :math:`{{\mathit{ft}}^\ast}{}[i]` is of the form :math:`(\epsilon~{\mathit{zt}})`. - - - - -:math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]` is immutably reachable from :math:`(\mathsf{ref{.}array}~a)` if: - - - * The field value :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{fields}{}[i]` exists. - - * The array instance :math:`s{.}\mathsf{arrays}{}[a]` exists. - - * The :ref:`expansion ` of :math:`s{.}\mathsf{arrays}{}[a]{.}\mathsf{type}` is :math:`(\mathsf{array}~(\epsilon~{\mathit{zt}}))`. - - - - -:math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]` is immutably reachable from :math:`(\mathsf{ref{.}exn}~a)` if: - - - * The value :math:`s{.}\mathsf{exns}{}[a]{.}\mathsf{fields}{}[i]` exists. - - * The exception instance :math:`s{.}\mathsf{exns}{}[a]` exists. - - - - -:math:`{\mathit{ref}}` is immutably reachable from :math:`(\mathsf{ref{.}extern}~{\mathit{ref}})`. - - - - -:math:`{\mathit{fv}}_2` is not immutably reachable from :math:`{\mathit{fv}}_1` if: - - - * NotImmutReachable(:math:`{\mathit{fv}}_1`, :math:`s`, :math:`{\mathit{fv}}_2`) is true. - - - - The store :math:`s` is :ref:`valid ` if: @@ -27624,6 +27624,88 @@ spectec 0.5 generator == IL Validation after pass sideconditions... == Translating to AL... == Prose Generation... +ImmutReachable +- fv_2 is immutably reachable from fv_1 if: + - Either: + - fv' is immutably reachable from fv_1. + - fv_2 is immutably reachable from fv'. + - Or: + - the field value fv_1 is (REF.STRUCT_ADDR a). + - the field value fv_2 is s.STRUCTS[a].FIELDS[i]. + - the field value s.STRUCTS[a].FIELDS[i] exists. + - the structure instance s.STRUCTS[a] exists. + - The :ref:`expansion ` of s.STRUCTS[a].TYPE is (STRUCT ft*). + - |ft*| is greater than i. + - the field type ft*[i] is (?() zt). + - Or: + - fv_1 is (REF.ARRAY_ADDR a). + - fv_2 is s.ARRAYS[a].FIELDS[i]. + - the field value s.ARRAYS[a].FIELDS[i] exists. + - the array instance s.ARRAYS[a] exists. + - The :ref:`expansion ` of s.ARRAYS[a].TYPE is (ARRAY (?() zt)). + - Or: + - fv_1 is (REF.EXN_ADDR a). + - fv_2 is s.EXNS[a].FIELDS[i]. + - the value s.EXNS[a].FIELDS[i] exists. + - the exception instance s.EXNS[a] exists. + - Or: + - fv_1 is (REF.EXTERN ref). + - fv_2 is ref. + +ImmutReachable/trans +- fv_2 is immutably reachable from fv_1 if: + - fv' is immutably reachable from fv_1. + - fv_2 is immutably reachable from fv'. + +ImmutReachable/ref.struct +- s.STRUCTS[a].FIELDS[i] is immutably reachable from (REF.STRUCT_ADDR a) if: + - the field value s.STRUCTS[a].FIELDS[i] exists. + - the structure instance s.STRUCTS[a] exists. + - The :ref:`expansion ` of s.STRUCTS[a].TYPE is (STRUCT ft*). + - |ft*| is greater than i. + - the field type ft*[i] is (?() zt). + +ImmutReachable/ref.array +- s.ARRAYS[a].FIELDS[i] is immutably reachable from (REF.ARRAY_ADDR a) if: + - the field value s.ARRAYS[a].FIELDS[i] exists. + - the array instance s.ARRAYS[a] exists. + - The :ref:`expansion ` of s.ARRAYS[a].TYPE is (ARRAY (?() zt)). + +ImmutReachable/ref.exn +- s.EXNS[a].FIELDS[i] is immutably reachable from (REF.EXN_ADDR a) if: + - the value s.EXNS[a].FIELDS[i] exists. + - the exception instance s.EXNS[a] exists. + +ImmutReachable/ref.extern +- ref is immutably reachable from (REF.EXTERN ref). + +Expand +- The :ref:`expansion ` of deftype is comptype if: + - the sub type $unrolldt(deftype) is (SUB final? typeuse* comptype). + +Expand_use +- The :ref:`expansion ` of C is comptype if: + - Either: + - the type use typeuse is deftype. + - The :ref:`expansion ` of deftype is comptype. + - Or: + - typeuse is (_IDX typeidx). + - the type C.TYPES[typeidx] exists. + - The :ref:`expansion ` of C.TYPES[typeidx] is comptype. + +Expand_use/deftype +- The :ref:`expansion ` of C is comptype if: + - The :ref:`expansion ` of deftype is comptype. + +Expand_use/typeidx +- The :ref:`expansion ` of C is comptype if: + - the type C.TYPES[typeidx] exists. + - The :ref:`expansion ` of C.TYPES[typeidx] is comptype. + +NotImmutReachable +- fv_2 is not immutably reachable from fv_1 if: + - $NotImmutReachable(fv_1, s, fv_2) is true. + Numtype_ok - the number type numtype is always valid. @@ -27639,12 +27721,8 @@ Packtype_sub Numtype_sub - numtype matches only itself. -Expand -- The :ref:`expansion ` of deftype is comptype if: - - the sub type $unrolldt(deftype) is (SUB final? typeuse* comptype). - Vectype_sub -- the vector type vectype matches only itself. +- vectype matches only itself. Heaptype_ok - the heap type heaptype is valid if: @@ -28113,25 +28191,6 @@ Instrtype_ok - For all x in x*: - the local C.LOCALS[x] exists. -Expand_use -- The :ref:`expansion ` of C is comptype if: - - Either: - - the type use typeuse is deftype. - - The :ref:`expansion ` of deftype is comptype. - - Or: - - typeuse is (_IDX typeidx). - - the type C.TYPES[typeidx] exists. - - The :ref:`expansion ` of C.TYPES[typeidx] is comptype. - -Expand_use/deftype -- The :ref:`expansion ` of C is comptype if: - - The :ref:`expansion ` of deftype is comptype. - -Expand_use/typeidx -- The :ref:`expansion ` of C is comptype if: - - the type C.TYPES[typeidx] exists. - - The :ref:`expansion ` of C.TYPES[typeidx] is comptype. - Subtype_ok - the sub type (SUB FINAL? (_IDX x)* comptype) is valid for the type index (OK x_0) if: - |x*| is less than or equal to 1. @@ -29913,65 +29972,6 @@ Exninst_ok - For all t in t*, and corresponding val in val*: - the value val is valid with the value type t. -ImmutReachable -- fv_2 is immutably reachable from fv_1 if: - - Either: - - fv' is immutably reachable from fv_1. - - fv_2 is immutably reachable from fv'. - - Or: - - the field value fv_1 is (REF.STRUCT_ADDR a). - - the field value fv_2 is s.STRUCTS[a].FIELDS[i]. - - the field value s.STRUCTS[a].FIELDS[i] exists. - - the structure instance s.STRUCTS[a] exists. - - The :ref:`expansion ` of s.STRUCTS[a].TYPE is (STRUCT ft*). - - |ft*| is greater than i. - - the field type ft*[i] is (?() zt). - - Or: - - fv_1 is (REF.ARRAY_ADDR a). - - fv_2 is s.ARRAYS[a].FIELDS[i]. - - the field value s.ARRAYS[a].FIELDS[i] exists. - - the array instance s.ARRAYS[a] exists. - - The :ref:`expansion ` of s.ARRAYS[a].TYPE is (ARRAY (?() zt)). - - Or: - - fv_1 is (REF.EXN_ADDR a). - - fv_2 is s.EXNS[a].FIELDS[i]. - - the value s.EXNS[a].FIELDS[i] exists. - - the exception instance s.EXNS[a] exists. - - Or: - - fv_1 is (REF.EXTERN ref). - - fv_2 is ref. - -ImmutReachable/trans -- fv_2 is immutably reachable from fv_1 if: - - fv' is immutably reachable from fv_1. - - fv_2 is immutably reachable from fv'. - -ImmutReachable/ref.struct -- s.STRUCTS[a].FIELDS[i] is immutably reachable from (REF.STRUCT_ADDR a) if: - - the field value s.STRUCTS[a].FIELDS[i] exists. - - the structure instance s.STRUCTS[a] exists. - - The :ref:`expansion ` of s.STRUCTS[a].TYPE is (STRUCT ft*). - - |ft*| is greater than i. - - the field type ft*[i] is (?() zt). - -ImmutReachable/ref.array -- s.ARRAYS[a].FIELDS[i] is immutably reachable from (REF.ARRAY_ADDR a) if: - - the field value s.ARRAYS[a].FIELDS[i] exists. - - the array instance s.ARRAYS[a] exists. - - The :ref:`expansion ` of s.ARRAYS[a].TYPE is (ARRAY (?() zt)). - -ImmutReachable/ref.exn -- s.EXNS[a].FIELDS[i] is immutably reachable from (REF.EXN_ADDR a) if: - - the value s.EXNS[a].FIELDS[i] exists. - - the exception instance s.EXNS[a] exists. - -ImmutReachable/ref.extern -- ref is immutably reachable from (REF.EXTERN ref). - -NotImmutReachable -- fv_2 is not immutably reachable from fv_1 if: - - $NotImmutReachable(fv_1, s, fv_2) is true. - Store_ok - the store s is valid if: - For all :