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

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

Make add_exprs total (on branch).

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