Changeset 1101


Ignore:
Timestamp:
Aug 3, 2011, 5:18:17 PM (8 years ago)
Author:
campbell
Message:

Label preservation in Cminor initialisation and RTLabs translation
on branch.

Location:
Deliverables/D3.3/id-lookup-branch/Cminor
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1087 r1101  
    1919].
    2020
     21(* None of the additional code introduces locals or labels. *)
     22definition stmt_inv : stmt → Prop ≝
     23  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     24
    2125(* Produces a few extra skips - hopefully the compiler will optimise these
    2226   away. *)
    2327
    24 definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_vars s (λ_.False)
     28definition init_datum : ident → region → init_data → nat (*offset*) → Σs:stmt. stmt_inv s
    2529λid,r,init,off.
    2630match init_expr init with
     
    3135    ]
    3236].
    33 //
     37% //
    3438cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
    3539qed.
     
    4448qed.
    4549
    46 lemma sig_stmt_vars : ∀P:ident → Prop. ∀s:Σs:stmt.stmt_vars s P.
    47   stmt_vars s P.
    48 #P * #s #p whd in ⊢ (?%?) //
     50lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
     51  stmt_inv s.
     52* #s #p @p
    4953qed.
    5054
    51 definition init_var : ident → region → list init_data → Σs:stmt. stmt_vars s (λ_.False)
     55definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s
    5256λid,r,init.
    5357\snd (foldr ??
     
    5559   let 〈off,s〉 ≝ os in
    5660     〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
    57   〈0, dp ? (λx.stmt_vars x (λ_.False)) St_skip ?〉 init).
    58 [ whd //
    59 | elim init whd //
    60   #h #t #IH whd in ⊢ (?(???%)?) @sndredex whd % [ @sig_stmt_vars | @IH ]
     61  〈0, dp ? (λx.stmt_inv x) St_skip ?〉 init).
     62[ % //
     63| elim init
     64  [ % //
     65  | #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % // | @sig_stmt_inv ] | @IH ]
    6166] qed.
    6267
    63 definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_vars s (λ_.False)
    64 λvars. foldr ? (Σs:stmt. stmt_vars s (λ_.False))
    65   (λvar,s. dp ? (λx.stmt_vars x (λ_.False)) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_vars x (λ_.False)) St_skip I) vars.
    66 whd % @sig_stmt_vars
     68definition init_vars : list (ident × (list init_data) × region × unit) → Σs:stmt. stmt_inv s
     69λvars. foldr ? (Σs:stmt. stmt_inv s)
     70  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
     71% [ % [ % // | @sig_stmt_inv ] | @sig_stmt_inv ]
    6772qed.
    6873
    69 definition add_statement : ident → (Σs:stmt. stmt_vars s (λ_.False)) →
     74lemma no_labels : ∀s. stmt_inv s → labels_of s = [ ].
     75#s elim s //
     76[ #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     77  >(IH1 H1) >(IH2 H2) @refl
     78| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?)
     79  >(IH1 H1) >(IH2 H2) @refl
     80| #s #IH * * #_ #_ #H @(IH H)
     81| #s #IH * * #_ #_ #H @(IH H)
     82| #l #s #IH * * #_ *
     83| #l #s #IH * * #_ #_ #H @(IH H)
     84] qed.
     85
     86definition add_statement : ident → (Σs:stmt. stmt_inv s) →
    7087                              list (ident × (fundef internal_function)) →
    7188                              list (ident × (fundef internal_function)) ≝
     
    87104          ]
    88105      | inr _ ⇒ 〈id',f'〉 ]) ].
    89 whd %
    90 [ @(stmt_vars_mp … H) #i *
    91 | //
     106%
     107[ % [ % // |
     108  @(stmt_P_mp … H) #s * #V #L %
     109  [ @(stmt_vars_mp … V) #i *
     110  | @(stmt_labels_mp … L) #l *
     111  ]
     112  ]
     113| whd in ⊢ (?(λ_.??(?(λ_.???%)?))?) >(no_labels … H) @(f_inv f)
    92114] qed.
    93115
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1095 r1101  
    55
    66definition env ≝ identifier_map SymbolTag register.
    7 definition label_env ≝ identifier_map SymbolTag label.
     7definition label_env ≝ identifier_map Label label.
    88definition populate_env : env → universe RegisterTag → list (ident × typ) → list (register×typ) × env × (universe RegisterTag) ≝
    99λen,gen. foldr ??
     
    5252  #i #H @lookup_add_oblivious @(IH … E0) @H
    5353] qed.
    54      
    55 definition  populate_label_env : label_env → universe LabelTag → list ident → label_env × (universe LabelTag) ≝
     54
     55definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
    5656λen,gen. foldr ??
    5757 (λid,engen.
     
    6060     〈add ?? en id r, gen'〉) 〈en, gen〉.
    6161
     62lemma populates_label_env : ∀ls,lbls,u,lbls',u'.
     63  populate_label_env lbls u ls = 〈lbls',u'〉 →
     64  ∀l. Exists ? (λl'.l' = l) ls → present ?? lbls' l.
     65#ls elim ls
     66[ #lbls #u #lbls' #u' #E #l *
     67| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
     68  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     69  lapply (refl ? (populate_label_env lbls u t))
     70  cases (populate_label_env lbls u t) in ⊢ (???% → %)
     71  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) cases (fresh ? u1) #r #gen' whd in ⊢ (??%? → ?)
     72  #E >(?:lbls' = add ?? lbls1 h r) [ 2: destruct (E) @refl ]
     73  #l *
     74  [ #El <El whd >lookup_add_hit % #Er destruct
     75  | #H @lookup_add_oblivious @(IH … E1 ? H)
     76  ]
     77] qed.
     78
    6279lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?).
    6380  lookup tag A m i ≠ None ?.
     
    6683
    6784definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
     85λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
     86cases H #H'  cases (H' (refl ??)) qed.
     87
     88definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝
    6889λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
    6990cases H #H'  cases (H' (refl ??)) qed.
     
    219240        λ${ident E}.$s ] (refl ? $t) }.
    220241
    221 let 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 ≝
    222 match s return λs.stmt_vars s (present ?? env) → res internal_function with
     242definition stmt_inv : env → label_env → stmt → Prop ≝
     243λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
     244
     245notation "π1" with precedence 10 for @{ (proj1 ??) }.
     246notation "π2" with precedence 10 for @{ (proj2 ??) }.
     247
     248let 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 ≝
     249match s return λs.stmt_inv env label_env s → res internal_function with
    223250[ St_skip ⇒ λ_. OK ? f
    224251| St_assign _ x e ⇒ λEnv.
    225     let dst ≝ lookup' env x (proj1 … Env) in
    226     OK ? (add_expr env ? e (proj2 … Env) dst f)
     252    let dst ≝ lookup' env x (π1 (π1 Env)) in
     253    OK ? (add_expr env ? e (π2 (π1 Env)) dst f)
    227254| 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
     255    let 〈val_reg, f〉 ≝ choose_reg env ? e2 f (π2 (π1 Env)) in
     256    let 〈addr_reg, f〉 ≝ choose_reg env ? e1 f (π1 (π1 Env)) in
    230257    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)
     258    let f ≝ add_expr env ? e1 (π1 (π1 Env)) addr_reg f in
     259    OK ? (add_expr env ? e2 (π2 (π1 Env)) val_reg f)
    233260| St_call return_opt_id e args ⇒ λEnv.
    234261    let return_opt_reg ≝
     
    237264      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
    238265      ] Env in
    239     let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
     266    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
    240267    let f ≝
    241268      match e with
    242269      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    243270      | _ ⇒
    244         let 〈fnr, f〉 ≝ choose_reg env ? e f (proj2 … (proj1 … Env)) in
     271        let 〈fnr, f〉 ≝ choose_reg env ? e f (π2 (π1 (π1 Env))) in
    245272        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
     273        add_expr env ? e (π2 (π1 (π1 Env))) fnr f
    247274      ] in
    248     OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
     275    OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)
    249276| St_tailcall e args ⇒ λEnv.
    250     let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
     277    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (π2 (π1 Env)) in
    251278    let f ≝
    252279      match e with
    253280      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    254281      | _ ⇒
    255         let 〈fnr, f〉 ≝ choose_reg env ? e f (proj1 … Env) in
     282        let 〈fnr, f〉 ≝ choose_reg env ? e f (π1 (π1 Env)) in
    256283        let f ≝ add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f in
    257         add_expr env ? e (proj1 … Env) fnr f
     284        add_expr env ? e (π1 (π1 Env)) fnr f
    258285      ] in
    259     OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
     286    OK ? (add_exprs env args (π2 (π1 Env)) args_regs ? f)
    260287| 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
     288    do f ← add_stmt env label_env s2 ? exits f;
     289    add_stmt env label_env s1 ? exits f
    263290| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    264291    let l_next ≝ f_entry f in
    265     do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
     292    do f ← add_stmt env label_env s2 (π2 Env) exits f;
    266293    let l2 ≝ f_entry f in
    267294    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
     295    do f ← add_stmt env label_env s1 (π2 (π1 Env)) exits f;
     296    let 〈r,f〉 ≝ choose_reg env ? e f (π1 (π1 (π1 Env))) in
    270297    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)
     298    OK ? (add_expr env ? e (π1 (π1 (π1 Env))) r f)
    272299| St_loop s ⇒ λEnv.
    273300    let f ≝ add_fresh_to_graph ? f in (* dummy statement, fill in afterwards *)
    274301    let l_loop ≝ f_entry f in
    275     do f ← add_stmt env label_env s Env exits f;
     302    do f ← add_stmt env label_env s (π2 Env) exits f;
    276303    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
    277304| St_block s ⇒ λEnv.
    278     add_stmt env label_env s Env ((f_entry f)::exits) f
     305    add_stmt env label_env s (π2 Env) ((f_entry f)::exits) f
    279306| St_exit n ⇒ λEnv.
    280307    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    281308    OK ? (add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f)
    282309| St_switch sz sg e tab n ⇒ λEnv.
    283     let 〈r,f〉 ≝ choose_reg env ? e f Env in
     310    let 〈r,f〉 ≝ choose_reg env ? e f ? in
    284311    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    285312    let f ≝ add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f in
     
    293320      let f ≝ add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f in
    294321        OK ? (add_fresh_to_graph (St_const cr (Ointconst ? i)) f)) (OK ? f) tab;
    295     OK ? (add_expr env ? e Env r f)
     322    OK ? (add_expr env ? e (π1 Env) r f)
    296323| St_return opt_e ⇒
    297324    let f ≝ add_fresh_to_graph (λ_. St_return) f in
     
    305332    ]
    306333| 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);
     334    do f ← add_stmt env label_env s' (π2 Env) exits f;
     335    let l' ≝ lookup_label label_env l ? in
    309336    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
    310337| St_goto l ⇒ λEnv.
    311     do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
     338    let l' ≝ lookup_label label_env l ? in
    312339    OK ? (add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f)
    313340| St_cost l s' ⇒ λEnv.
    314     do f ← add_stmt env label_env s' Env exits f;
     341    do f ← add_stmt env label_env s' (π2 Env) exits f;
    315342    OK ? (add_fresh_to_graph (St_cost l) f)
    316343] Env.
     344try @(π1 Env)
     345try @(π2 Env)
     346try @(π1 (π1 Env))
     347try @(π2 (π1 Env))
    317348[ -f @(choose_regs_length … (sym_eq … Eregs))
    318 | whd in Env @(proj1 … (proj1 … Env))
     349| whd in Env @(π1 (π1 (π1 Env)))
    319350| -f @(choose_regs_length … (sym_eq … Eregs))
    320351| @(λ_. St_skip l_next)
     
    323354| @(λ_. St_skip l)
    324355| @(λ_. St_skip l_default)
    325 | whd in Env @Env
    326356| @(St_skip (f_entry f))
    327357| @(λ_.St_skip l')
    328358] qed.
    329 
    330 (* Get labels from a Cminor statement. *)
    331 let rec labels_of (s:stmt) : list ident ≝
    332 match 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 ].
    341359
    342360notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
     
    360378      let 〈r,gen〉 ≝ fresh … reggen2 in
    361379        〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ] in
    362 let 〈label_env, labgen1〉 ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
     380let 〈label_env, labgen1〉 as El ≝ populate_label_env (empty_map …) labgen0 cminor_labels in
    363381let 〈l,labgen〉 ≝ fresh … labgen1 in
    364382let emptyfn ≝
     
    378396OK ? f
    379397.
    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
     398[ @(stmt_P_mp … (f_inv f))
     399  #s * #V #L %
     400  [ @(stmt_vars_mp … V)
     401    #i #H cases (Exists_append … H)
     402    [ #H1 @(populate_extends ?????? (sym_eq … E2))
     403          @(populates_env … (sym_eq … E1)) @H1
     404    | #H1 @(populates_env … (sym_eq … E2)) @H1
     405    ]
     406  | @(stmt_labels_mp … L)
     407    #l #H @(populates_label_env … (sym_eq … El)) @H
    385408  ]
    386409| *: >lookup_add_hit % #E destruct
Note: See TracChangeset for help on using the changeset viewer.