source: src/Cminor/semantics.ma @ 2588

Last change on this file since 2588 was 2395, checked in by campbell, 8 years ago

Proper handling of comparison of pointers off-the-end of an object.
We might need to drop this if the proofs/back-end work is too involved.

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