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

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

A little more tidying.

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