source: src/Cminor/semantics.ma @ 1352

Last change on this file since 1352 was 1352, checked in by sacerdot, 9 years ago

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File size: 16.9 KB
Line 
1include "common/Events.ma".
2include "common/Mem.ma".
3include "common/IO.ma".
4include "common/Globalenvs.ma".
5include "common/SmallstepExec.ma".
6
7include "Cminor/syntax.ma".
8include alias "basics/logic.ma".
9
10definition env ≝ identifier_map SymbolTag val.
11definition genv ≝ (genv_t Genv) (fundef internal_function).
12
13definition stmt_inv : internal_function → env → stmt → Prop ≝ λf,en,s.
14  stmt_P (λs.stmt_vars (present ?? en) s ∧
15             stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of (f_body f))) s) s.
16
17lemma stmt_inv_update : ∀f,en,s,l,v.
18  stmt_inv f en s →
19  ∀H:present ?? en l.
20  stmt_inv f (update_present ?? en l H v) s.
21#f #en #s #l #v #Inv #H
22@(stmt_P_mp … Inv)
23#s * #H1 #H2 %
24[ @(stmt_vars_mp … H1)
25  #l #H @update_still_present @H
26| @H2
27] qed.
28
29(* continuations within a function. *)
30inductive cont : Type[0] ≝
31| Kend : cont
32| Kseq : stmt → cont → cont
33| Kblock : cont → cont.
34
35let rec cont_inv (f:internal_function) (en:env) (k:cont) on k : Prop ≝
36match k with
37[ Kend ⇒ True
38| Kseq s k' ⇒ stmt_inv f en s ∧ cont_inv f en k'
39| Kblock k' ⇒ cont_inv f en k'
40].
41
42lemma cont_inv_update : ∀f,en,k,l,v.
43  cont_inv f en k →
44  ∀H:present ?? en l.
45  cont_inv f (update_present ?? en l H v) k.
46#f #en #k elim k /2/
47#s #k #IH #l #v #Inv #H whd %
48[ @stmt_inv_update @(π1 Inv)
49| @IH @(π2 Inv)
50] qed.
51
52(* a stack of function calls *)
53inductive stack : Type[0] ≝
54| SStop : stack
55| Scall : ∀dest:option ident. ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some id ⇒ present ?? en id] → stmt_inv f en (f_body f) → ∀k:cont. cont_inv f en k → stack → stack.
56
57inductive state : Type[0] ≝
58| State:
59    ∀    f: internal_function.
60    ∀    s: stmt.
61    ∀   en: env.
62    ∀ fInv: stmt_inv f en (f_body f).
63    ∀  Inv: stmt_inv f en s.
64    ∀    m: mem.
65    ∀   sp: block.
66    ∀    k: cont.
67    ∀ kInv: cont_inv f en k.
68    ∀   st: stack.
69            state
70| Callstate:
71    ∀   fd: fundef internal_function.
72    ∀ args: list val.
73    ∀    m: mem.
74    ∀   st: stack.
75            state
76| Returnstate:
77    ∀    v: option val.
78    ∀    m: mem.
79    ∀   st: stack.
80            state.
81
82definition mem_of_state : state → mem ≝
83λst. match st with
84[ State _ _ _ _ _ m _ _ _ _ ⇒ m
85| Callstate _ _ m _ ⇒ m
86| Returnstate _ m _ ⇒ m
87].
88
89axiom UnknownLocal : String.
90axiom FailedConstant : String.
91axiom FailedOp : String.
92axiom FailedLoad : String.
93
94let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (Env:expr_vars ty0 e (present ?? en)) (sp:block) (m:mem) on e : res (trace × val) ≝
95match e return λt,e.expr_vars t e (present ?? en) → res (trace × val) with
96[ Id _ i ⇒ λEnv.
97    let r ≝ lookup_present ?? en i ? in
98    OK ? 〈E0, r〉
99| Cst _ c ⇒ λEnv.
100    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
101    OK ? 〈E0, r〉
102| Op1 ty ty' op e' ⇒ λEnv.
103    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
104    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
105    OK ? 〈tr, r〉
106| Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv.
107    do 〈tr1,v1〉 ← eval_expr ge ? e1 en ? sp m;
108    do 〈tr2,v2〉 ← eval_expr ge ? e2 en ? sp m;
109    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
110    OK ? 〈tr1 ⧺ tr2, r〉
111| Mem rg ty chunk e ⇒ λEnv.
112    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
113    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
114    OK ? 〈tr, r〉
115| Cond sz sg ty e' e1 e2 ⇒ λEnv.
116    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
117    do b ← eval_bool_of_val v;
118    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en ? sp m;
119    OK ? 〈tr ⧺ tr', r〉
120| Ecost ty l e' ⇒ λEnv.
121    do 〈tr,r〉 ← eval_expr ge ty e' en ? sp m;
122    OK ? 〈Echarge l ⧺ tr, r〉
123] Env.
124try @Env
125try @(π1 Env)
126try @(π2 Env)
127try @(π1 (π1 Env))
128cases b
129try @(π2 (π1 Env))
130try @(π2 Env)
131qed.
132
133axiom BadState : String.
134
135let rec k_exit (n:nat) (k:cont) f en (kInv:cont_inv f en k) on k : res (Σk':cont. cont_inv f en k') ≝
136match k return λk.cont_inv f en k → ? with
137[ Kend ⇒ λ_. Error ? (msg BadState)
138| Kseq _ k' ⇒ λkInv. k_exit n k' f en ?
139| Kblock k' ⇒ λkInv. match n with [ O ⇒ OK ? «k',?» | S m ⇒ k_exit m k' f en ? ]
140] kInv.
141[ @(π2 kInv) | @kInv | @kInv ]
142qed.
143
144let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
145match cs with
146[ nil ⇒ default
147| cons h t ⇒
148    let 〈hi,a〉 ≝ h in
149    if eq_bv ? i hi then a else find_case A sz i t default
150].
151
152let rec find_label (l:identifier Label) (s:stmt) (k:cont) f en (Inv:stmt_inv f en s) (kInv:cont_inv f en k) on s : option (Σsk:(stmt × cont). stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk)) ≝
153match s return λs. stmt_inv f en s → ? with
154[ St_seq s1 s2 ⇒ λInv.
155    match find_label l s1 (Kseq s2 k) f en ?? with
156    [ None ⇒ find_label l s2 k f en ??
157    | Some sk ⇒ Some ? sk
158    ]
159| St_ifthenelse _ _ _ s1 s2 ⇒ λInv.
160    match find_label l s1 k f en ?? with
161    [ None ⇒ find_label l s2 k f en ??
162    | Some sk ⇒ Some ? sk
163    ]
164| St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
165| St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
166| St_label l' s' ⇒ λInv.
167    match identifier_eq ? l l' with
168    [ inl _ ⇒ Some ? 〈s',k〉
169    | inr _ ⇒ find_label l s' k f en ??
170    ]
171| St_cost _ s' ⇒ λInv. find_label l s' k f en ??
172| _ ⇒ λ_. None ?
173] Inv.
174//
175try @(π2 Inv)
176try @(π2 (π1 Inv))
177[ % [ @(π2 Inv) | @kInv ]
178| % [ @Inv | @kInv ]
179| % [ @(π2 Inv) | @kInv ]
180] qed.
181
182lemma find_label_none : ∀l,s,k,f,en,Inv,kInv.
183  find_label l s k f en Inv kInv = None ? →
184  ¬Exists ? (λl'.l' = l) (labels_of s).
185#l #s elim s
186try (try #a try #b try #c try #d try #e try #f try #g try #h try #i try #j try #m % * (* *) )
187[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
188  lapply (IH1 (Kseq s2 k) f en (π2 (π1 Inv)) (conj ?? (π2 Inv) kInv))
189  cases (find_label l s1 (Kseq s2 k) f en ??)
190  [ #H1 whd in ⊢ (??%? → ?)
191    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
192    [ #H2 #_ % #H cases (Exists_append … H)
193      [ #H' cases (H1 (refl ??)) /2/
194      | #H' cases (H2 (refl ??)) /2/
195      ]
196    | #sk #_ #E destruct
197    ]
198  | #sk #_ #E whd in E:(??%?); destruct
199  ]
200| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%))
201  lapply (IH1 k f en (π2 (π1 Inv)) kInv)
202  cases (find_label l s1 k f en ??)
203  [ #H1 whd in ⊢ (??%? → ?)
204    lapply (IH2 k f en (π2 Inv) kInv) cases (find_label l s2 k f en ??)
205    [ #H2 #_ % #H cases (Exists_append … H)
206      [ #H' cases (H1 (refl ??)) /2/
207      | #H' cases (H2 (refl ??)) /2/
208      ]
209    | #sk #_ #E destruct
210    ]
211  | #sk #_ #E whd in E:(??%?); destruct
212  ]
213| #s1 #IH #k #f #en #Inv #kInv @IH
214| #s1 #IH #k #f #en #Inv #kInv @IH
215| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
216  whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
217| whd in i:(??%?); cases (identifier_eq Label l a) in i;
218  whd in ⊢ (? → ??%? → ?) [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
219| #cl #s1 #IH #k #f #en #Inv #kInv @IH
220] qed.
221
222definition find_label_always : ∀l,s,k. Exists ? (λl'.l' = l) (labels_of s) →
223  ∀f,en. stmt_inv f en s → cont_inv f en k →
224  Σsk:stmt × cont. stmt_inv f en (\fst sk) ∧ cont_inv f en (\snd sk) ≝
225λl,s,k,H,f,en,Inv,kInv.
226  match find_label l s k f en Inv kInv return λx.find_label l s k f en Inv kInv = x → ? with
227  [ Some sk ⇒ λ_. sk
228  | None ⇒ λE. ⊥
229  ] (refl ? (find_label l s k f en Inv kInv)).
230cases (find_label_none … E)
231#H1 @(H1 H)
232qed.
233
234axiom WrongNumberOfParameters : String.
235
236(* TODO: perhaps should do a little type checking? *)
237let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
238match vs with
239[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
240| cons v vt ⇒
241    match ids return λids.res (Σen. All ?? ids) with
242    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
243    | cons idh idt ⇒
244        let 〈id,ty〉 ≝ idh in
245        do en ← bind_params vt idt;
246        OK ? «add ?? en (\fst idh) v, ?»
247    ]
248].
249[ @I
250| % [ whd >lookup_add_hit % #E destruct
251    | @(All_mp … (use_sig ?? en)) #a #H whd @lookup_add_oblivious @H
252    ]
253] qed.
254
255(* TODO: perhaps should do a little type checking? *)
256definition init_locals : env → list (ident×typ) → env ≝
257foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
258
259lemma init_locals_preserves : ∀en,vars,l.
260  present ?? en l →
261  present ?? (init_locals en vars) l.
262#en #vars elim vars
263[ #l #H @H
264| #idt #tl #IH #l #H whd
265  @lookup_add_oblivious @IH @H
266] qed.
267
268lemma init_locals_env : ∀en,vars.
269  All ? (λidt. present ?? (init_locals en vars) (\fst idt)) vars.
270#en #vars elim vars
271[ @I
272| #idt #tl #IH %
273  [ whd >lookup_add_hit % #E destruct
274  | @(All_mp … IH) #a #H @lookup_add_oblivious @H
275  ]
276] qed.
277
278let rec trace_map_inv (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → res (trace × B))
279                  (l:list A) (p:All A P l) on l : res (trace × (list B)) ≝
280match l return λl. All A P l → ? with
281[ nil ⇒ λ_. OK ? 〈E0, [ ]〉
282| cons h t ⇒ λp.
283    do 〈tr,h'〉 ← f h ?;
284    do 〈tr',t'〉 ← trace_map_inv … f t ?;
285    OK ? 〈tr ⧺ tr',h'::t'〉
286] p.
287[ @(π1 p) | @(π2 p) ] qed.
288
289axiom FailedStore : String.
290axiom BadFunctionValue : String.
291axiom BadSwitchValue : String.
292axiom UnknownLabel : String.
293axiom ReturnMismatch : String.
294
295definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
296λge,st.
297match st with
298[ State f s en fInv Inv m sp k kInv st ⇒
299    match s return λs. stmt_inv f en s → ? with
300    [ St_skip ⇒ λInv.
301        match k return λk. cont_inv f en k → ? with
302        [ Kseq s' k' ⇒ λkInv. ret ? 〈E0, State f s' en fInv ? m sp k' ? st〉
303        | Kblock k' ⇒ λkInv. ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
304          (* cminor allows functions without an explicit return statement *)
305        | Kend ⇒ λkInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
306        ] kInv
307    | St_assign _ id e ⇒ λInv.
308        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
309        let en' ≝ update_present ?? en id ? v in
310        ret ? 〈tr, State f St_skip en' ? ? m sp k ? st〉
311    | St_store _ _ chunk edst e ⇒ λInv.
312        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
313        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
314        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
315        ret ? 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
316
317    | St_call dst ef args ⇒ λInv.
318        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
319        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
320        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
321        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
322    | St_tailcall ef args ⇒ λInv.
323        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
324        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
325        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
326        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
327       
328    | St_seq s1 s2 ⇒ λInv. ret ? 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
329    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
330        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
331        ! b ← eval_bool_of_val v;
332        ret ? 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
333    | St_loop s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
334    | St_block s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
335    | St_exit n ⇒ λInv.
336        ! k' ← k_exit n k ?? kInv;
337        ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
338    | St_switch sz _ e cs default ⇒ λInv.
339        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
340        match v with
341        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
342            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
343            ret ? 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
344            (Wrong ??? (msg BadSwitchValue))
345        | _ ⇒ Wrong ??? (msg BadSwitchValue)
346        ]
347    | St_return eo ⇒
348        match eo return λeo. stmt_inv f en (St_return eo) → ? with
349        [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
350        | Some e ⇒
351            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ dp ty e ⇒ λInv.
352              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
353              ret ? 〈tr, Returnstate (Some ? v) (free m sp) st〉
354            ]
355        ]
356    | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
357    | St_goto l ⇒ λInv.
358        match find_label_always l (f_body f) Kend ? f en ?? with [ dp sk Inv' ⇒
359          ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
360        ]
361    | St_cost l s' ⇒ λInv.
362        ret ? 〈Echarge l, State f s' en fInv ? m sp k ? st〉
363    ] Inv
364| Callstate fd args m st ⇒
365    match fd with
366    [ Internal f ⇒
367        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
368        ! en ← bind_params args (f_params f);
369        ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉
370    | External fn ⇒
371        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
372        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
373        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
374        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
375    ]
376| Returnstate res m st ⇒
377    match st with
378    [ Scall dst f sp en dstP fInv k Inv st' ⇒
379        match res with
380        [ None ⇒ match dst with
381                 [ None ⇒ ret ? 〈E0, State f St_skip en ? ? m sp k ? st'〉
382                 | Some _ ⇒ Wrong ??? (msg ReturnMismatch)]
383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
384                   [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
385                   | Some id ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en id dstP v) ? ? m sp k ? st'〉
386                   ] dstP
387        ]
388    | _ ⇒ Wrong ??? (msg BadState)
389    ]
390].
391try @(π1 kInv)
392try @(π2 kInv)
393try @(conj ?? I I)
394try @kInv
395try @(π2 (π1 Inv))
396try @kInv
397try @(π1 (π1 Inv))
398try (@cont_inv_update @kInv)
399try @(π2 (π1 (π1 Inv)))
400try @(π1 (π1 (π1 Inv)))
401try @(π1 Inv)
402try @(π2 Inv)
403[ @stmt_inv_update @fInv
404| % [ @(π2 Inv) | @kInv ]
405| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
406| % [ @Inv | @kInv ]
407| @(use_sig … k')
408| @(use_sig … k')
409| @(π1 Inv')
410| @(π2 Inv')
411| @fInv
412| @I
413| 11,12:
414  @(stmt_P_mp … (f_inv f))
415  #s * #V #L %
416  [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
417    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (use_sig … en))
418      * #id' #ty * #E1 #H <E1 @H
419    | *: #H cases (Exists_All … H (init_locals_env … en …))
420      * #id' #ty * #E1 #H <E1 @H
421    ]
422  | 2,4: @L
423  ]
424| @fInv
425| @Inv
426| @stmt_inv_update @fInv
427| @cont_inv_update @Inv
428] qed.
429
430definition is_final : state → option int ≝
431λs. match s with
432[ Returnstate res m st ⇒
433    match st with
434    [ SStop ⇒
435        match res with
436        [ None ⇒ None ?
437        | Some v ⇒
438            match v with
439            [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
440            | _ ⇒ None ?
441            ]
442        ]
443    | _ ⇒ None ?
444    ]
445| _ ⇒ None ?
446].
447
448definition Cminor_exec : trans_system io_out io_in ≝
449  mk_trans_system … ? (λ_.is_final) eval_step.
450
451axiom MainMissing : String.
452
453definition make_global : Cminor_program → genv ≝
454λp. globalenv Genv ?? (λx.x) p.
455
456definition make_initial_state : Cminor_program → res state ≝
457λp.
458  let ge ≝ make_global p in
459  do m ← init_mem Genv ?? (λx.x) p;
460  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
461  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
462  OK ? (Callstate f (nil ?) m SStop).
463
464definition Cminor_fullexec : fullexec io_out io_in ≝
465  mk_fullexec … Cminor_exec make_global make_initial_state.
466
467definition make_noinit_global : Cminor_noinit_program → genv ≝
468λp. globalenv Genv ?? (λx.[Init_space x]) p.
469
470definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
471λp.
472  let ge ≝ make_noinit_global p in
473  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
474  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
475  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
476  OK ? (Callstate f (nil ?) m SStop).
477
478definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
479  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.
Note: See TracBrowser for help on using the repository browser.