source: src/Cminor/Cminor_semantics.ma @ 2645

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