source: Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma @ 1102

Last change on this file since 1102 was 1102, checked in by campbell, 9 years ago

Tidy up branch

File size: 17.0 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5include "utilities/pair.ma".
6include "utilities/deppair.ma".
7
8definition env ≝ identifier_map SymbolTag register.
9definition label_env ≝ identifier_map Label label.
10definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
11λen,gen. foldr ??
12 (λidt,rsengen.
13   let 〈id,ty〉 ≝ idt in
14   let 〈rs,en,gen〉 ≝ rsengen in
15   let 〈r,gen'〉 ≝ fresh … gen in
16     〈〈r,ty〉::rs, add ?? en id r, gen'〉) 〈[ ], en, gen〉.
17
18lemma populates_env : ∀l,e,u,l',e',u'.
19  populate_env e u l = 〈l',e',u'〉 →
20  ∀i. Exists ? (λx.\fst x = i) l →
21      present ?? e' i.
22#l elim l
23[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
24| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
25  * [ whd in ⊢ (??%? → ?) #E1 <E1
26      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
27      whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
28      whd in E:(??%?);
29      >(?:e' = add ?? y id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
30      whd >lookup_add_hit % #A destruct
31    | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
32      lapply (refl ? (populate_env e u tl))
33      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
34      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
35      whd in ⊢ (??%? → ?) #E
36      >(?:e' = add ?? e1 id r) [ 2: destruct (E) @refl ] (* XXX workaround because destruct overnormalises *)
37      @lookup_add_oblivious
38      @(IH … E1 ? H)
39    ]
40] qed.
41
42lemma populate_extends : ∀l,e,u,l',e',u'.
43  populate_env e u l = 〈l',e',u'〉 →
44  ∀i. present ?? e i → present ?? e' i.
45#l elim l
46[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
47| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
48  change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
49  lapply (refl ? (populate_env e u tl))
50  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
51  >E0 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u0) #i1 #u1 #E
52  whd in E:(??%?)
53  >(?:e' = add ?? e0 id i1) [ 2: destruct (E) @refl ]
54  #i #H @lookup_add_oblivious @(IH … E0) @H
55] qed.
56
57definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
58λen,gen. foldr ??
59 (λid,engen.
60   let 〈en,gen〉 ≝ engen in
61   let 〈r,gen'〉 ≝ fresh … gen in
62     〈add ?? en id r, gen'〉) 〈en, gen〉.
63
64lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
65  populate_label_env lbls u ls = 〈lbls',u'〉 →
66  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
67#ls elim ls
68[ #lbls #u #lbls' #u' #E #l *
69| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
70  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
71  lapply (refl ? (populate_label_env lbls u t))
72  cases (populate_label_env lbls u t) in ⊢ (???% → %)
73  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
74  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
75  #l *
76  [ #El <El whd >lookup_add_hit % #Er destruct
77  | #H @lookup_add_oblivious @(IH … E1 ? H)
78  ]
79] qed.
80
81definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
82λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
83cases H #H'  cases (H' (refl ??)) qed.
84
85definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝
86λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
87cases H #H'  cases (H' (refl ??)) qed.
88
89
90(* Add a statement to the graph, *without* updating the entry label. *)
91definition fill_in_statement : label → statement → internal_function → internal_function ≝
92λl,s,f.
93  mk_internal_function (f_labgen f) (f_reggen f)
94                       (f_result f) (f_params f) (f_locals f)
95                       (f_stacksize f) (add ?? (f_graph f) l s)
96                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
97@lookup_add_oblivious @use_sig
98qed.
99
100(* Add a statement to the graph, making it the entry label. *)
101definition add_to_graph : label → statement → internal_function → internal_function ≝
102λl,s,f.
103  mk_internal_function (f_labgen f) (f_reggen f)
104                       (f_result f) (f_params f) (f_locals f)
105                       (f_stacksize f) (add ?? (f_graph f) l s)
106                       (dp ?? l ?) (dp ?? (f_exit f) ?).
107[ >lookup_add_hit % #E destruct
108| @lookup_add_oblivious @use_sig
109] qed.
110
111(* Add a statement with a fresh label to the start of the function.  The
112   statement is parametrised by the *next* instruction's label. *)
113definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝
114λs,f.
115  let 〈l,g〉 ≝ fresh … (f_labgen f) in
116  let s' ≝ s (f_entry f) in
117    (mk_internal_function g (f_reggen f)
118                       (f_result f) (f_params f) (f_locals f)
119                       (f_stacksize f) (add ?? (f_graph f) l s')
120                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
121[ >lookup_add_hit % #E destruct
122| @lookup_add_oblivious @use_sig
123] qed.
124
125definition fresh_reg : internal_function → typ → register × internal_function ≝
126λf,ty.
127  let 〈r,g〉 ≝ fresh … (f_reggen f) in
128    〈r, mk_internal_function (f_labgen f) g
129                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
130                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
131
132axiom UnknownVariable : String.
133
134definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function ≝
135λenv,ty,e,f.
136  match e return λty,e. expr_vars ty e (present ?? env) → register × internal_function with
137  [ Id _ i ⇒ λEnv. 〈lookup' env i Env, f〉
138  | _ ⇒ λ_.fresh_reg f ty
139  ].
140 
141let rec foldr_all (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → B → B) (b:B) (l:list A) (H:All ? P l) on l :B ≝ 
142 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
143
144definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
145
146definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t).
147                         internal_function → All ? (exprtyp_present env) es →
148                         list register × internal_function ≝
149λenv,es,f,Env.
150  foldr_all (Σt:typ.expr t) ??
151    (λe,p,acc. let 〈rs,f〉 ≝ acc in
152             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in
153             〈r::rs,f'〉) 〈[ ], f〉 es Env.
154@p qed.
155
156lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
157((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
158∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
159#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
160
161
162lemma choose_regs_length : ∀env,es,f,p,rs,f'.
163  choose_regs env es f p = 〈rs,f'〉 → |es| = |rs|.
164#env #es #f elim es
165[ #p #rs #f normalize #E destruct @refl
166| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
167  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
168  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
169  destruct (E4) skip (E1 E3) @eq_f @IH
170  [ @(proj2 … p)
171  | 3: @sym_eq @E1
172  | 2: skip
173  ]
174] qed.
175
176axiom BadCminorProgram : String.
177
178let rec add_expr (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:internal_function) on e: internal_function ≝
179match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
180[ Id _ i ⇒ λEnv.
181    let r ≝ lookup' env i Env in
182    match register_eq r dst with
183    [ inl _ ⇒ f
184    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
185    ]
186| Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f
187| Op1 _ _ op e' ⇒ λEnv.
188    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
189    let f ≝ add_fresh_to_graph (St_op1 op dst r) f in
190    add_expr env ? e' Env r f
191| Op2 _ _ _ op e1 e2 ⇒ λEnv.
192    let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
193    let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
194    let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in
195    let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in
196    add_expr env ? e1 (proj1 … Env) r1 f
197| Mem _ _ q e' ⇒ λEnv.
198    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
199    let f ≝ add_fresh_to_graph (St_load q r dst) f in
200    add_expr env ? e' Env r f
201| Cond _ _ _ e' e1 e2 ⇒ λEnv.
202    let resume_at ≝ f_entry f in
203    let f ≝ add_expr env ? e2 (proj2 … Env) dst f in
204    let lfalse ≝ f_entry f in
205    let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in
206    let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in
207    let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in
208    let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in
209    add_expr env ? e' (proj1 … (proj1 … Env)) r f
210| Ecost _ l e' ⇒ λEnv.
211    let f ≝ add_expr env ? e' Env dst f in
212    add_fresh_to_graph (St_cost l) f
213] Env.
214
215let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
216                  (dsts:list register) (pf:|es|=|dsts|) (f:internal_function) on es: internal_function ≝
217match es return λes.All ?? es → |es|=|dsts| → ? with
218[ nil ⇒ λ_. match dsts return λx. ?=|x| → ? with [ nil ⇒ λ_. f | cons _ _ ⇒ λpf.⊥ ]
219| cons e et ⇒ λEnv.
220    match dsts return λx. ?=|x| → ? with
221    [ nil ⇒ λpf.⊥
222    | cons r rt ⇒ λpf.
223        let f ≝ add_exprs env et ? rt ? f in
224        match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env)
225    ]
226] Env pf.
227[ 1,2,3: normalize in pf; destruct //
228| whd in Env @(proj2 … Env)
229| normalize in pf; destruct @e0 ] qed.
230
231axiom UnknownLabel : String.
232axiom ReturnMismatch : String.
233
234definition stmt_inv : env → label_env → stmt → Prop ≝
235λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
236
237let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (exits:list label) (f:internal_function) on s : res internal_function ≝
238match s return λs.stmt_inv env label_env s → res internal_function with
239[ St_skip ⇒ λ_. OK ? f
240| St_assign _ x e ⇒ λEnv.
241    let dst ≝ lookup' env x (π1 (π1 Env)) in
242    OK ? (add_expr env ? e (π2 (π1 Env)) dst f)
243| St_store _ _ q e1 e2 ⇒ λEnv.
244    let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (π2 (π1 Env)) in
245    let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (π1 (π1 Env)) in
246    let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in
247    let f ≝ add_expr env ? e1 (π1 (π1 Env)) addr_reg f in
248    OK ? (add_expr env ? e2 (π2 (π1 Env)) val_reg f)
249| St_call return_opt_id e args ⇒ λEnv.
250    let return_opt_reg ≝
251      match return_opt_id return λo. ? → ? with
252      [ None ⇒ λ_. None ?
253      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
254      ] Env in
255    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
256    let f ≝
257      match e with
258      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
259      | _ ⇒
260        let 〈fnr, f〉 ≝ choose_reg env ? e f (π2 (π1 (π1 Env))) in
261        let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in
262        add_expr env ? e (π2 (π1 (π1 Env))) fnr f
263      ] in
264    OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)
265| St_tailcall e args ⇒ λEnv.
266    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
267    let f ≝
268      match e with
269      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
270      | _ ⇒
271        let 〈fnr, f〉 ≝ choose_reg env ? e f (π1 (π1 Env)) in
272        let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
273        add_expr env ? e (π1 (π1 Env)) fnr f
274      ] in
275    OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)
276| St_seq s1 s2 ⇒ λEnv.
277    do f ← add_stmt env label_env s2 ? exits f;
278    add_stmt env label_env s1 ? exits f
279| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
280    let l_next ≝ f_entry f in
281    do f ← add_stmt env label_env s2 (π2 Env) exits f;
282    let l2 ≝ f_entry f in
283    let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in
284    do f ← add_stmt env label_env s1 (π2 (π1 Env)) exits f;
285    let 〈r,f〉 ≝ choose_reg env ? e f (π1 (π1 (π1 Env))) in
286    let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in
287    OK ? (add_expr env ? e (π1 (π1 (π1 Env))) r f)
288| St_loop s ⇒ λEnv.
289    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
290    let l_loop ≝ f_entry f in
291    do f ← add_stmt env label_env s (π2 Env) exits f;
292    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
293| St_block s ⇒ λEnv.
294    add_stmt env label_env s (π2 Env) ((f_entry f)::exits) f
295| St_exit n ⇒ λEnv.
296    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
297    OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
298| St_switch sz sg e tab n ⇒ λEnv.
299    let 〈r,f〉 ≝ choose_reg env ? e f ? in
300    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
301    let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
302    do f ← foldr ?? (λcs,f.
303      do f ← f;
304      let 〈i,n〉 ≝ cs in
305      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
306      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
307      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
308      let f ≝ add_fresh_to_graph (St_cond br l_case) f in
309      let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
310        OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
311    OK ? (add_expr env ? e (π1 Env) r f)
312| St_return opt_e ⇒
313    let f ≝ add_fresh_to_graph (λ_. St_return) f in
314    match opt_e return λo. ? → ? with
315    [ None ⇒ λEnv. OK ? f
316    | Some e ⇒
317        match f_result f with
318        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
319        | Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ]
320        ]
321    ]
322| St_label l s' ⇒ λEnv.
323    do f ← add_stmt env label_env s' (π2 Env) exits f;
324    let l' ≝ lookup_label label_env l ? in
325    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
326| St_goto l ⇒ λEnv.
327    let l' ≝ lookup_label label_env l ? in
328    OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
329| St_cost l s' ⇒ λEnv.
330    do f ← add_stmt env label_env s' (π2 Env) exits f;
331    OK ? (add_fresh_to_graph (St_cost l) f)
332] Env.
333try @(π1 Env)
334try @(π2 Env)
335try @(π1 (π1 Env))
336try @(π2 (π1 Env))
337[ -f @(choose_regs_length … (sym_eq … Eregs))
338| whd in Env @(π1 (π1 (π1 Env)))
339| -f @(choose_regs_length … (sym_eq … Eregs))
340| @(λ_. St_skip l_next)
341| @(St_skip (f_entry f))
342| @St_skip
343| @(λ_. St_skip l)
344| @(λ_. St_skip l_default)
345| @(St_skip (f_entry f))
346| @(λ_.St_skip l')
347] qed.
348
349
350definition c2ra_function (*: internal_function → internal_function*) ≝
351λf.
352let labgen0 ≝ new_universe LabelTag in
353let reggen0 ≝ new_universe RegisterTag in
354let cminor_labels ≝ labels_of (f_body f) in
355let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
356let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
357let 〈result, locals, reggen〉 ≝
358  match f_return f with
359  [ None ⇒ 〈None ?, locals0, reggen2〉
360  | Some ty ⇒
361      let 〈r,gen〉 ≝ fresh … reggen2 in
362        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
363let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
364let 〈l,labgen〉 ≝ fresh … labgen1 in
365let emptyfn ≝
366  mk_internal_function
367    labgen
368    reggen
369    result
370    params
371    locals
372    (f_stacksize f)
373    (add ?? (empty_map …) l St_return)
374    l
375    l in
376do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn;
377do u1 ← check_universe_ok ? (f_labgen f);
378do u2 ← check_universe_ok ? (f_reggen f);
379OK ? f
380.
381[ @(stmt_P_mp … (f_inv f))
382  #s * #V #L %
383  [ @(stmt_vars_mp … V)
384    #i #H cases (Exists_append … H)
385    [ #H1 @(populate_extends ?????? (sym_eq … E2))
386          @(populates_env … (sym_eq … E1)) @H1
387    | #H1 @(populates_env … (sym_eq … E2)) @H1
388    ]
389  | @(stmt_labels_mp … L)
390    #l #H @(populates_label_env … (sym_eq … El)) @H
391  ]
392| *: >lookup_add_hit % #E destruct
393]
394qed.
395
396definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
397transform_partial_program ???
398  (transf_partial_fundef ?? c2ra_function).
399
400include "Cminor/initialisation.ma".
401
402definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
403λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.