source: src/Cminor/semantics.ma @ 1655

Last change on this file since 1655 was 1655, checked in by campbell, 7 years ago

Update Cminor and RTLabs semantics to use new monad definitions.

File size: 17.2 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 (λid,ty. present ?? en id) 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 #ty #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×typ). ∀f:internal_function. block (* sp *) → ∀en:env. match dest with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty)] → 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 (λid,ty. present ?? en id)) (sp:block) (m:mem) on e : res (trace × val) ≝
95match e return λt,e.expr_vars t e (λid,ty. present ?? en id) → 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 … (pi2 ?? 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 return λ_. IO ??? with
298[ State f s en fInv Inv m sp k kInv st ⇒ err_to_io ??? (
299    match s return λs. stmt_inv f en s → res (trace × state) with
300    [ St_skip ⇒ λInv.
301        match k return λk. cont_inv f en k → res ? with
302        [ Kseq s' k' ⇒ λkInv. return 〈E0, State f s' en fInv ? m sp k' ? st〉
303        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
304          (* cminor allows functions without an explicit return statement *)
305        | Kend ⇒ λkInv. return 〈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        return 〈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        return 〈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 [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
321        return 〈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 [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
326        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
327       
328    | St_seq s1 s2 ⇒ λInv. return 〈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        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
333    | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
334    | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
335    | St_exit n ⇒ λInv.
336        ! k' ← k_exit n k ?? kInv;
337        return 〈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            return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
344            (Error ? (msg BadSwitchValue))
345        | _ ⇒ Error ? (msg BadSwitchValue)
346        ]
347    | St_return eo ⇒
348        match eo return λeo. stmt_inv f en (St_return eo) → ? with
349        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
350        | Some e ⇒
351            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
352              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
353              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
354            ]
355        ]
356    | St_label l s' ⇒ λInv. return 〈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 [ mk_Sig sk Inv' ⇒
359          return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
360        ]
361    | St_cost l s' ⇒ λInv.
362        return 〈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 ⇒ err_to_io ?? (trace × state) (
367        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
368        ! en ← bind_params args (f_params f);
369        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
370    | External fn ⇒
371        ! evargs ← err_to_io ??? (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        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
375    ]
376| Returnstate result m st ⇒ err_to_io ??? (
377    match st with
378    [ Scall dst f sp en dstP fInv k Inv st' ⇒
379        match result with
380        [ None ⇒ match dst with
381                 [ None ⇒ return 〈E0, State f St_skip en ? ? m sp k ? st'〉
382                 | Some _ ⇒ Error ? (msg ReturnMismatch)]
383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty) ] → res (trace × state) with
384                   [ None ⇒ λ_. Error ? (msg ReturnMismatch)
385                   | Some idty ⇒ λdstP. return 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
386                   ] dstP
387        ]
388    | _ ⇒ Error ? (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[ @fInv
404| @(π2 Inv')
405| @(π1 Inv')
406| @(pi2 … k')
407| @(pi2 … k')
408| % [ @Inv | @kInv ]
409| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
410| % [ @(π2 Inv) | @kInv ]
411| @stmt_inv_update @fInv
412| 10,11:
413  @(stmt_P_mp … (f_inv f))
414  #s * #V #L %
415  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
416    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
417      * #id' #ty * #E1 destruct #H @H
418    | *: #H cases (Exists_All … H (init_locals_env … en …))
419      * #id' #ty * #E1 destruct #H @H
420    ]
421  | 2,4: @L
422  ]
423| @I
424| @cont_inv_update @Inv
425| @stmt_inv_update @fInv
426| @Inv
427| @fInv
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.