source: src/Cminor/Cminor_semantics.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 16.4 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
86axiom UnknownLocal : String.
87axiom FailedConstant : String.
88axiom FailedOp : String.
89axiom FailedLoad : String.
90
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
93[ Id _ i ⇒ λEnv.
94    let r ≝ lookup_present ?? en i ? in
95    OK ? 〈E0, r〉
96| Cst _ c ⇒ λEnv.
97    do r ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) sp c);
98    OK ? 〈E0, r〉
99| Op1 ty ty' op e' ⇒ λEnv.
100    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
101    do r ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
102    OK ? 〈tr, r〉
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;
106    do r ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
107    OK ? 〈tr1 ⧺ tr2, r〉
108| Mem ty e ⇒ λEnv.
109    do 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
110    do r ← opt_to_res … (msg FailedLoad) (loadv ty m v);
111    OK ? 〈tr, r〉
112| Cond sz sg ty e' e1 e2 ⇒ λEnv.
113    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
114    do b ← eval_bool_of_val v;
115    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en ? sp m;
116    OK ? 〈tr ⧺ tr', r〉
117| Ecost ty l e' ⇒ λEnv.
118    do 〈tr,r〉 ← eval_expr ge ty e' en ? sp m;
119    OK ? 〈Echarge l ⧺ tr, r〉
120] Env.
121try @Env
122try @(π1 Env)
123try @(π2 Env)
124try @(π1 (π1 Env))
125cases b
126try @(π2 (π1 Env))
127try @(π2 Env)
128qed.
129
130axiom BadState : String.
131
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.
140
141let rec find_case (A:Type[0]) (sz:intsize) (i:bvint sz) (cs:list (bvint sz × A)) (default:A) on cs : A ≝
142match cs with
143[ nil ⇒ default
144| cons h t ⇒
145    let 〈hi,a〉 ≝ h in
146    if eq_bv ? i hi then a else find_case A sz i t default
147].
148
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 ??
154    | Some sk ⇒ Some ? sk
155    ]
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 ??
159    | Some sk ⇒ Some ? sk
160    ]
161| St_label l' s' ⇒ λInv.
162    match identifier_eq ? l l' with
163    [ inl _ ⇒ Some ? 〈s',k〉
164    | inr _ ⇒ find_label l s' k f en ??
165    ]
166| St_cost _ s' ⇒ λInv. find_label l s' k f en ??
167| _ ⇒ λ_. None ?
168] Inv.
169//
170try @(π2 Inv)
171try @(π1 (π2 Inv))
172try @(π2 (π2 Inv))
173[ % [ @(π2 (π2 Inv)) | @kInv ]
174| % [ @(π2 Inv) | @kInv ]
175] qed.
176
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 % * (* *) )
182[ #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
183  lapply (IH1 (Kseq s2 k) f en (π1 (π2 Inv)) (conj ?? (π2 (π2 Inv)) kInv))
184  cases (find_label l s1 (Kseq s2 k) f en ??)
185  [ #H1 whd in ⊢ (??%? → ?);
186    lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??)
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  ]
195| #sz #sg #e #s1 #s2 #IH1 #IH2 #k #f #en #Inv #kInv whd in ⊢ (??%? → ?(???%));
196  lapply (IH1 k f en (π1 (π2 Inv)) kInv)
197  cases (find_label l s1 k f en ??)
198  [ #H1 whd in ⊢ (??%? → ?);
199    lapply (IH2 k f en (π2 (π2 Inv)) kInv) cases (find_label l s2 k f en ??)
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;
209  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
210| whd in i:(??%?); cases (identifier_eq Label l a) in i;
211  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | #NE #E cases (c d e f ?? E) #H @H ]
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
227axiom WrongNumberOfParameters : String.
228
229(* TODO: perhaps should do a little type checking? *)
230let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
231match vs with
232[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
233| cons v vt ⇒
234    match ids return λids.res (Σen. All ?? ids) with
235    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
236    | cons idh idt ⇒
237        let 〈id,ty〉 ≝ idh in
238        do en ← bind_params vt idt;
239        OK ? «add ?? en (\fst idh) v, ?»
240    ]
241].
242[ @I
243| % [ whd >lookup_add_hit % #E destruct
244    | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H
245    ]
246] qed.
247
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).
251
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
282axiom FailedStore : String.
283axiom BadFunctionValue : String.
284axiom ReturnMismatch : String.
285
286definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
287λge,st.
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
291    [ St_skip ⇒ λInv.
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〉
295          (* cminor allows functions without an explicit return statement *)
296        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
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
301        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
302    | St_store ty edst e ⇒ λInv.
303        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
304        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
305        ! m' ← opt_to_res … (msg FailedStore) (storev ty m vdst v);
306        return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
307
308    | St_call dst ef args ⇒ λInv.
309        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
310        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct … ge vf);
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 ?;
312        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
313(*
314    | St_tailcall ef args ⇒ λInv.
315        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
316        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
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 ?;
318        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
319*)       
320    | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
321    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
322        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
323        ! b ← eval_bool_of_val v;
324        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
325    | St_return eo ⇒
326        match eo return λeo. stmt_inv f en (St_return eo) → ? with
327        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
328        | Some e ⇒
329            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
330              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
331              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
332            ]
333        ]
334    | St_label l s' ⇒ λInv. return 〈E0, State f s' en fInv ? m sp k ? st〉
335    | St_goto l ⇒ λInv.
336        match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒
337          return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
338        ]
339    | St_cost l s' ⇒ λInv.
340        return 〈Echarge l, State f s' en fInv ? m sp k ? st〉
341    ] Inv)
342| Callstate fd args m st ⇒
343    match fd with
344    [ Internal f ⇒ err_to_io ?? (trace × state) (
345        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) XData in
346        ! en ← bind_params args (f_params f);
347        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
348    | External fn ⇒
349        ! evargs ← err_to_io ??? (check_eventval_list args (sig_args (ef_sig fn)));
350        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
351        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
352        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
353    ]
354| Returnstate result m st ⇒ err_to_io ??? (
355    match st with
356    [ Scall dst f sp en dstP fInv k Inv st' ⇒
357        match result with
358        [ None ⇒ match dst with
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'〉
364                   ] dstP
365        ]
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        ]
375    ])
376| Finalstate r ⇒ Error ? (msg BadState)
377].
378try @(π1 kInv)
379try @(π2 kInv)
380try @(conj ?? I I)
381try @kInv
382try @(π2 (π1 Inv))
383try @kInv
384try @(π1 (π1 Inv))
385try (@cont_inv_update @kInv)
386try @(π2 (π1 (π1 Inv)))
387try @(π1 (π1 (π1 Inv)))
388try @(π2 Inv)
389try @(π1 (π2 Inv))
390[ @fInv
391| @(π2 Inv')
392| @(π1 Inv')
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/
398| @stmt_inv_update @fInv
399| /3/
400| /3/
401| 12,13:
402  @(stmt_P_mp … (f_inv f))
403  #s * #V #L #R %
404  [ 1,3: @(stmt_vars_mp … V) #id #ty #EX cases (Exists_append … EX)
405    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
406      * #id' #ty * #E1 destruct #H @H
407    | *: #H cases (Exists_All … H (init_locals_env … en …))
408      * #id' #ty * #E1 destruct #H @H
409    ]
410  | 2,4: @L
411  ]
412| @I
413| @cont_inv_update @Inv
414| /3/
415| @stmt_inv_update @fInv
416| @Inv
417| /3/
418| @fInv
419] qed.
420
421definition is_final : state → option int ≝
422λs. match s with
423[ Finalstate r ⇒ Some ? r
424| _ ⇒ None ?
425].
426
427definition Cminor_exec : trans_system io_out io_in ≝
428  mk_trans_system … ? (λ_.is_final) eval_step.
429
430axiom MainMissing : String.
431
432definition make_global : Cminor_program → genv ≝
433λp. globalenv … (λx.x) p.
434
435definition make_initial_state : Cminor_program → res state ≝
436λp.
437  let ge ≝ make_global p in
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);
441  OK ? (Callstate f (nil ?) m SStop).
442
443definition Cminor_fullexec : fullexec io_out io_in ≝
444  mk_fullexec … Cminor_exec make_global make_initial_state.
445
446definition make_noinit_global : Cminor_noinit_program → genv ≝
447λp. globalenv … (λx.[Init_space x]) p.
448
449definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
450λp.
451  let ge ≝ make_noinit_global p in
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);
455  OK ? (Callstate f (nil ?) m SStop).
456
457definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
458  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.
Note: See TracBrowser for help on using the repository browser.