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

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

Experimental branch where lookups of local variables in Cminor code always
succeed.

File size: 15.7 KB
RevLine 
[766]1include "utilities/lists.ma".
[764]2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag register.
[766]7definition label_env ≝ identifier_map SymbolTag label.
[1056]8definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
[764]9λen,gen. foldr ??
[887]10 (λidt,rsengen.
11   let 〈id,ty〉 ≝ idt in
[1056]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〉.
[764]15
[1087]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) ≝
[766]56λen,gen. foldr ??
57 (λid,engen.
[1056]58   let 〈en,gen〉 ≝ engen in
59   let 〈r,gen'〉 ≝ fresh … gen in
60     〈add ?? en id r, gen'〉) 〈en, gen〉.
[764]61
[1072]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
[1087]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
[766]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.
[887]75  mk_internal_function (f_labgen f) (f_reggen f)
76                       (f_result f) (f_params f) (f_locals f)
[1070]77                       (f_stacksize f) (add ?? (f_graph f) l s)
78                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
[1072]79@lookup_add_oblivious @lookup_sigma
[1070]80qed.
[764]81
[766]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.
[887]85  mk_internal_function (f_labgen f) (f_reggen f)
86                       (f_result f) (f_params f) (f_locals f)
[1070]87                       (f_stacksize f) (add ?? (f_graph f) l s)
88                       (dp ?? l ?) (dp ?? (f_exit f) ?).
[1072]89[ >lookup_add_hit % #E destruct
90| @lookup_add_oblivious @lookup_sigma
[1070]91] qed.
[764]92
[766]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. *)
[1056]95definition add_fresh_to_graph : (label → statement) → internal_function → internal_function ≝
[766]96λs,f.
[1056]97  let 〈l,g〉 ≝ fresh … (f_labgen f) in
[766]98  let s' ≝ s (f_entry f) in
[1056]99    (mk_internal_function g (f_reggen f)
[887]100                       (f_result f) (f_params f) (f_locals f)
[1070]101                       (f_stacksize f) (add ?? (f_graph f) l s')
102                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
[1072]103[ >lookup_add_hit % #E destruct
104| @lookup_add_oblivious @lookup_sigma
[1070]105] qed.
[1072]106
[1056]107definition fresh_reg : internal_function → typ → register × internal_function ≝
[887]108λf,ty.
[1056]109  let 〈r,g〉 ≝ fresh … (f_reggen f) in
110    〈r, mk_internal_function (f_labgen f) g
[887]111                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
[766]112                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
113
[797]114axiom UnknownVariable : String.
115
[1087]116definition choose_reg : ∀env:env.∀ty.∀e:expr ty. internal_function → expr_vars ty e (present ?? env) → register × internal_function ≝
[887]117λenv,ty,e,f.
[1087]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
[766]121  ].
[1087]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.
[766]125
[1087]126definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
[766]127
[1087]128definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). internal_function → All ? (exprtyp_present env) es → list register × internal_function ≝
129λenv,es,f,Env.
130  foldr_all (Σt:typ.expr t) ??
131    (λe,p,acc. let 〈rs,f〉 ≝ acc in
132             let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg env t e f ? ] p in
133             〈r::rs,f'〉) 〈[ ], f〉 es Env.
134@p qed.
135
[797]136axiom BadCminorProgram : String.
137
[1087]138let 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 ≝
139match e return λty,e.expr_vars ty e (present ?? env) → internal_function with
140[ Id _ i ⇒ λEnv.
141    let r ≝ lookup' env i Env in
[766]142    match register_eq r dst with
[1087]143    [ inl _ ⇒ f
144    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
[766]145    ]
[1087]146| Cst _ c ⇒ λ_. add_fresh_to_graph (St_const dst c) f
147| Op1 _ _ op e' ⇒ λEnv.
148    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
[1056]149    let f ≝ add_fresh_to_graph (St_op1 op dst r) f in
[1087]150    add_expr env ? e' Env r f
151| Op2 _ _ _ op e1 e2 ⇒ λEnv.
152    let 〈r1,f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
153    let 〈r2,f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
[1056]154    let f ≝ add_fresh_to_graph (St_op2 op dst r1 r2) f in
[1087]155    let f ≝ add_expr env ? e2 (proj2 … Env) r2 f in
156    add_expr env ? e1 (proj1 … Env) r1 f
157| Mem _ _ q e' ⇒ λEnv.
158    let 〈r,f〉 ≝ choose_reg env ? e' f Env in
[1056]159    let f ≝ add_fresh_to_graph (St_load q r dst) f in
[1087]160    add_expr env ? e' Env r f
161| Cond _ _ _ e' e1 e2 ⇒ λEnv.
[766]162    let resume_at ≝ f_entry f in
[1087]163    let f ≝ add_expr env ? e2 (proj2 … Env) dst f in
[767]164    let lfalse ≝ f_entry f in
[1056]165    let f ≝ add_fresh_to_graph (λ_.St_skip resume_at) f in
[1087]166    let f ≝ add_expr env ? e1 (proj2 … (proj1 … Env)) dst f in
167    let 〈r,f〉 ≝ choose_reg env ? e' f (proj1 … (proj1 … Env)) in
[1056]168    let f ≝ add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f in
[1087]169    add_expr env ? e' (proj1 … (proj1 … Env)) r f
170| Ecost _ l e' ⇒ λEnv.
171    let f ≝ add_expr env ? e' Env dst f in
172    add_fresh_to_graph (St_cost l) f
173] Env.
[766]174
[797]175(* This shouldn't occur; maybe use vectors? *)
176axiom WrongNumberOfArguments : String.
177
[1087]178let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) (dsts:list register) (f:internal_function) on es: res internal_function ≝
179match es return λes.All ?? es → ? with
180[ nil ⇒ λ_. match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
181| cons e et ⇒ λEnv.
[766]182    match dsts with
[797]183    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
[766]184    | cons r rt ⇒
[1087]185        do f ← add_exprs env et ? rt f;
186        match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ty e ? r f) ] (proj1 ?? Env)
[766]187    ]
[1087]188] Env.
189whd in Env
190[ @(proj2 … Env) | @Env ] qed.
[766]191
[797]192axiom UnknownLabel : String.
193axiom ReturnMismatch : String.
194
[1087]195let 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 ≝
196match s return λs.stmt_vars s (present ?? env) → res internal_function with
197[ St_skip ⇒ λ_. OK ? f
198| St_assign _ x e ⇒ λEnv.
199    let dst ≝ lookup' env x (proj1 … Env) in
200    OK ? (add_expr env ? e (proj2 … Env) dst f)
201| St_store _ _ q e1 e2 ⇒ λEnv.
202    let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (proj2 … Env) in
203    let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (proj1 … Env) in
[1056]204    let f ≝ add_fresh_to_graph (St_store q addr_reg val_reg) f in
[1087]205    let f ≝ add_expr env ? e1 (proj1 … Env) addr_reg f in
206    OK ? (add_expr env ? e2 (proj2 … Env) val_reg f)
207| St_call return_opt_id e args ⇒ λEnv.
208    let return_opt_reg ≝
209      match return_opt_id return λo. ? → ? with
210      [ None ⇒ λ_. None ?
211      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
212      ] Env in
213    let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
214    let f ≝
[766]215      match e with
[1087]216      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
[766]217      | _ ⇒
[1087]218        let 〈fnr, f〉 ≝ choose_reg env ? e f (proj2 … (proj1 … Env)) in
[1056]219        let f ≝ add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f in
[1087]220        add_expr env ? e (proj2 … (proj1 … Env)) fnr f
221      ] in
222    add_exprs env args (proj2 … Env) args_regs f
223| St_tailcall e args ⇒ λEnv.
224    let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
225    let f ≝
[766]226      match e with
[1087]227      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
[766]228      | _ ⇒
[1087]229        let 〈fnr, f〉 ≝ choose_reg env ? e f (proj1 … Env) in
[1056]230        let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
[1087]231        add_expr env ? e (proj1 … Env) fnr f
232      ] in
233    add_exprs env args (proj2 … Env) args_regs f
234| St_seq s1 s2 ⇒ λEnv.
235    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
236    add_stmt env label_env s1 (proj1 … Env) exits f
237| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
[767]238    let l_next ≝ f_entry f in
[1087]239    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
[766]240    let l2 ≝ f_entry f in
[1056]241    let f ≝ add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f in
[1087]242    do f ← add_stmt env label_env s1 (proj2 … (proj1 … Env)) exits f;
243    let 〈r,f〉 ≝ choose_reg env ? e f (proj1 … (proj1 … Env)) in
[1056]244    let f ≝ add_fresh_to_graph (λl1. St_cond r l1 l2) f in
[1087]245    OK ? (add_expr env ? e (proj1 … (proj1 … Env)) r f)
246| St_loop s ⇒ λEnv.
[1070]247    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
[767]248    let l_loop ≝ f_entry f in
[1087]249    do f ← add_stmt env label_env s Env exits f;
[767]250    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
[1087]251| St_block s ⇒ λEnv.
252    add_stmt env label_env s Env ((f_entry f)::exits) f
253| St_exit n ⇒ λEnv.
[797]254    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
[1056]255    OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
[1087]256| St_switch sz sg e tab n ⇒ λEnv.
257    let 〈r,f〉 ≝ choose_reg env ? e f Env in
[797]258    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
[1056]259    let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
[771]260    do f ← foldr ?? (λcs,f.
261      do f ← f;
262      let 〈i,n〉 ≝ cs in
[1056]263      let 〈cr,f〉 ≝ fresh_reg … f (ASTint sz sg) in
264      let 〈br,f〉 ≝ fresh_reg … f (ASTint I8 Unsigned) in
[797]265      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
[1056]266      let f ≝ add_fresh_to_graph (St_cond br l_case) f in
267      let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
268        OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
[1087]269    OK ? (add_expr env ? e Env r f)
[766]270| St_return opt_e ⇒
[1056]271    let f ≝ add_fresh_to_graph (λ_. St_return) f in
[1087]272    match opt_e return λo. ? → ? with
273    [ None ⇒ λEnv. OK ? f
[766]274    | Some e ⇒
275        match f_result f with
[1087]276        [ None ⇒ λEnv. Error ? (msg ReturnMismatch)
277        | Some r ⇒ match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ? e ? (\fst r) f) ]
[766]278        ]
279    ]
[1087]280| St_label l s' ⇒ λEnv.
281    do f ← add_stmt env label_env s' Env exits f;
[797]282    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
[767]283    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
[1087]284| St_goto l ⇒ λEnv.
[797]285    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
[1056]286    OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
[1087]287| St_cost l s' ⇒ λEnv.
288    do f ← add_stmt env label_env s' Env exits f;
[1056]289    OK ? (add_fresh_to_graph (St_cost l) f)
[1087]290] Env.
291[ whd in Env @(proj1 … (proj1 … Env))
292| @(λ_. St_skip l_next)
[766]293| @(St_skip (f_entry f))
[1070]294| @St_skip
[766]295| @(λ_. St_skip l)
[771]296| @(λ_. St_skip l_default)
[1087]297| whd in Env @Env
[767]298| @(St_skip (f_entry f))
[766]299| @(λ_.St_skip l')
300] qed.
301
302(* Get labels from a Cminor statement. *)
303let rec labels_of (s:stmt) : list ident ≝
304match s with
305[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
[880]306| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
[766]307| St_loop s ⇒ labels_of s
308| St_block s ⇒ labels_of s
309| St_label l s ⇒ l::(labels_of s)
310| St_cost _ s ⇒ labels_of s
311| _ ⇒ [ ]
312].
313
[1087]314notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
315 with precedence 10
316for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
317       match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
318        λ${ident E}.$s ] ] (refl ? $t) }.
319
320
[764]321definition c2ra_function (*: internal_function → internal_function*) ≝
322λf.
[766]323let labgen0 ≝ new_universe LabelTag in
[764]324let reggen0 ≝ new_universe RegisterTag in
[766]325let cminor_labels ≝ labels_of (f_body f) in
[1087]326let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
327let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
[1056]328let 〈result, locals, reggen〉 ≝
[887]329  match f_return f with
[1056]330  [ None ⇒ 〈None ?, locals0, reggen2〉
[887]331  | Some ty ⇒
[1056]332      let 〈r,gen〉 ≝ fresh … reggen2 in
333        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
334let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
335let 〈l,labgen〉 ≝ fresh … labgen1 in
[766]336let emptyfn ≝
337  mk_internal_function
[764]338    labgen
[766]339    reggen
340    result
[764]341    params
342    locals
343    (f_stacksize f)
[766]344    (add ?? (empty_map …) l St_return)
345    l
346    l in
[1087]347do f ← add_stmt env label_env (f_body f) ? [ ] emptyfn;
[1056]348do u1 ← check_universe_ok ? (f_labgen f);
349do u2 ← check_universe_ok ? (f_reggen f);
350OK ? f
[766]351.
[1087]352[ @(stmt_vars_mp … (f_bound f))
353  #i #H cases (Exists_append … H)
354  [ #H1 @(populate_extends ?????? (sym_eq … E2))
355        @(populates_env … (sym_eq … E1)) @H1
356  | #H1 @(populates_env … (sym_eq … E2)) @H1
357  ]
358| *: >lookup_add_hit % #E destruct
359]
[1070]360qed.
[764]361
362definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
363transform_partial_program ???
364  (transf_partial_fundef ?? c2ra_function).
[766]365
366include "Cminor/initialisation.ma".
367
368definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
[1087]369λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.