Changeset 780 for src


Ignore:
Timestamp:
Apr 28, 2011, 10:55:49 AM (9 years ago)
Author:
campbell
Message:

Properly update set of registers that are used for pointers in Cminor to
RTLabs phase.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/Cminor/toRTLabs.ma

    r772 r780  
    6060                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    6161
    62 definition choose_reg : env → expr → internal_function → res (register × internal_function) ≝
    63 λenv,e,f.
     62definition fresh_ptr_reg : internal_function → res (register × internal_function) ≝
     63λf.
     64  do 〈r,g〉 ← fresh … (f_reggen f);
     65  OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f)
     66                       (f_result f) (f_params f) (r::(f_locals f)) (r::(f_ptrs f))
     67                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
     68
     69let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝
     70match e with
     71[ Id i ⇒ exists ? (eq_identifier ? i) ptrs
     72| Cst c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ]
     73| Op1 op e' ⇒
     74    match op with
     75    [ Oid ⇒ expr_yields_pointer e' ptrs
     76    | Optrofint _ ⇒ true
     77    | _ ⇒ false
     78    ]
     79| Op2 op e1 e2 ⇒
     80    match op with
     81    [ Oaddp ⇒ true
     82    | Osubpi ⇒ true
     83    | _ ⇒ false
     84    ]
     85| Mem q e' ⇒
     86    match q with
     87    [ Mpointer _ ⇒ true
     88    | _ ⇒ false
     89    ]
     90(* Both branches ought to be the same? *)
     91| Cond e' e1 e2 ⇒ (expr_yields_pointer e1 ptrs) ∨ (expr_yields_pointer e2 ptrs)
     92| Ecost _ e' ⇒ expr_yields_pointer e' ptrs
     93].
     94
     95definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝
     96λenv,e,ptrs,f.
    6497  match e with
    6598  [ Id i ⇒
    6699      do r ← opt_to_res … (lookup … env i);
    67100      OK ? 〈r, f〉
    68   | _ ⇒ fresh_reg f  (* FIXME: add to pointers list if necessary *)
     101  | _ ⇒
     102      if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f
    69103  ].
    70104
    71 definition choose_regs : env → list expr → internal_function → res (list register × internal_function) ≝
    72 λenv,es,f.
     105definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝
     106λenv,es,ptrs,f.
    73107  foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
    74                     do 〈r,f'〉 ← choose_reg env e f;
     108                    do 〈r,f'〉 ← choose_reg env e ptrs f;
    75109                    OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
    76110
    77 let rec add_expr (env:env) (e:expr) (dst:register) (f:internal_function) on e: res internal_function ≝
     111let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
    78112match e with
    79113[ Id i ⇒
    … …  
    85119| Cst c ⇒ add_fresh_to_graph (St_const dst c) f
    86120| Op1 op e' ⇒
    87     do 〈r,f〉 ← choose_reg env e' f;
     121    do 〈r,f〉 ← choose_reg env e' ptrs f;
    88122    do f ← add_fresh_to_graph (St_op1 op dst r) f;
    89     add_expr env e' r f
     123    add_expr env e' r ptrs f
    90124| Op2 op e1 e2 ⇒
    91     do 〈r1,f〉 ← choose_reg env e1 f;
    92     do 〈r2,f〉 ← choose_reg env e2 f;
     125    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
     126    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
    93127    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
    94     do f ← add_expr env e2 r2 f;
    95     add_expr env e1 r1 f
     128    do f ← add_expr env e2 r2 ptrs f;
     129    add_expr env e1 r1 ptrs f
    96130| Mem q e' ⇒
    97     add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) f (add_expr env e')
     131    add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e')
    98132| Cond e' e1 e2 ⇒
    99133    let resume_at ≝ f_entry f in
    100     do f ← add_expr env e2 dst f;
     134    do f ← add_expr env e2 dst ptrs f;
    101135    let lfalse ≝ f_entry f in
    102136    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
    103     do f ← add_expr env e1 dst f;
    104     add_branch_internal env e' (f_entry f) lfalse f (add_expr env e')
     137    do f ← add_expr env e1 dst ptrs f;
     138    add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e')
    105139| Ecost l e' ⇒
    106     do f ← add_expr env e' dst f;
     140    do f ← add_expr env e' dst ptrs f;
    107141    add_fresh_to_graph (St_cost l) f
    108142   
    … …  
    113147and add_with_addressing_internal (env:env) (e:expr)
    114148                          (s:∀m:addressing. addr m → label → statement)
     149                          (ptrs:list ident)
    115150                          (f:internal_function)
    116                           (termination_hack:register → internal_function → res internal_function)
     151                          (termination_hack:register → list ident → internal_function → res internal_function)
    117152                          on e : res internal_function ≝
    118153let add_default : unit → res internal_function ≝ λ_.
    119     do 〈r, f〉 ← choose_reg env e f;
     154    do 〈r, f〉 ← choose_reg env e ptrs f;
    120155    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
    121     termination_hack r f
     156    termination_hack r ptrs f
    122157in
    123158match e with
    … …  
    132167    [ Oaddp ⇒
    133168        let add_generic_addp : unit → res internal_function ≝ λ_.
    134           do 〈r1, f〉 ← choose_reg env e1 f;
    135           do 〈r2, f〉 ← choose_reg env e2 f;
     169          do 〈r1, f〉 ← choose_reg env e1 ptrs f;
     170          do 〈r2, f〉 ← choose_reg env e2 ptrs f;
    136171          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
    137           do f ← add_expr env e2 r2 f;
    138           add_expr env e1 r1 f
     172          do f ← add_expr env e2 r2 ptrs f;
     173          add_expr env e1 r1 ptrs f
    139174        in
    140175        match e1 with
    … …  
    142177            match c with
    143178            [ Oaddrsymbol id i ⇒
    144                 do 〈r, f〉 ← choose_reg env e f;
     179                do 〈r, f〉 ← choose_reg env e ptrs f;
    145180                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
    146                 add_expr env e2 r f
     181                add_expr env e2 r ptrs f
    147182            | _ ⇒ add_generic_addp it
    148183            ]
    … …  
    154189]
    155190(* and again *)
    156 and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (f:internal_function)
    157         (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
     191and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
     192        (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
    158193match e with
    159194[ Id i ⇒
    … …  
    163198    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    164199| Op1 op e' ⇒
    165     do 〈r,f〉 ← choose_reg env e' f;
     200    do 〈r,f〉 ← choose_reg env e' ptrs f;
    166201    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    167     add_expr env e' r f
     202    add_expr env e' r ptrs f
    168203| Op2 op e1 e2 ⇒
    169     do 〈r1,f〉 ← choose_reg env e1 f;
    170     do 〈r2,f〉 ← choose_reg env e2 f;
     204    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
     205    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
    171206    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    172     do f ← add_expr env e2 r2 f;
    173     add_expr env e1 r1 f
     207    do f ← add_expr env e2 r2 ptrs f;
     208    add_expr env e1 r1 ptrs f
    174209| _ ⇒
    175     do 〈r,f〉 ← choose_reg env e f;
     210    do 〈r,f〉 ← choose_reg env e ptrs f;
    176211    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    177     termination_hack_add_expr r f
     212    termination_hack_add_expr r ptrs f
    178213].
    179214
    180215(* See comment above. *)
    181216definition add_with_addressing ≝
    182 λenv,e,s,f. add_with_addressing_internal env e s f (add_expr env e).
     217λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e).
    183218definition add_branch ≝
    184 λenv,e,ltrue,lfalse,f. add_branch_internal env e ltrue lfalse f (add_expr env e).
    185 
    186 let rec add_exprs (env:env) (es:list expr) (dsts:list register) (f:internal_function) on es: res internal_function ≝
     219λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
     220
     221let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
    187222match es with
    188223[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ]
    … …  
    191226    [ nil ⇒ Error ?
    192227    | cons r rt ⇒
    193         do f ← add_exprs env et rt f;
    194         add_expr env e r f
    195     ]
    196 ].
    197 
    198 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
     228        do f ← add_exprs env et rt ptrs f;
     229        add_expr env e r ptrs f
     230    ]
     231].
     232
     233let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (ptrs:list ident) (f:internal_function) on s : res internal_function ≝
    199234match s with
    200235[ St_skip ⇒ OK ? f
    201236| St_assign x e ⇒
    202237    do dst ← opt_to_res … (lookup ?? env x);
    203     add_expr env e dst f
     238    add_expr env e dst ptrs f
    204239| St_store q e1 e2 ⇒
    205     do 〈val_reg, f〉 ← choose_reg env e2 f;
    206     do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) f;
    207     add_expr env e2 val_reg f
     240    do 〈val_reg, f〉 ← choose_reg env e2 ptrs f;
     241    do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
     242    add_expr env e2 val_reg ptrs f
    208243| St_call return_opt_id e args sig ⇒
    209244    do return_opt_reg ←
    … …  
    212247      | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r)
    213248      ];
    214     do 〈args_regs, f〉 ← choose_regs env args f;
     249    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
    215250    do f ←
    216251      match e with
    217252      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
    218253      | _ ⇒
    219         do 〈fnr, f〉 ← choose_reg env e f;
     254        do 〈fnr, f〉 ← choose_reg env e ptrs f;
    220255        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
    221         add_expr env e fnr f
     256        add_expr env e fnr ptrs f
    222257      ];
    223     add_exprs env args args_regs f
     258    add_exprs env args args_regs ptrs f
    224259| St_tailcall e args sig ⇒
    225     do 〈args_regs, f〉 ← choose_regs env args f;
     260    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
    226261    do f ←
    227262      match e with
    228263      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
    229264      | _ ⇒
    230         do 〈fnr, f〉 ← choose_reg env e f;
     265        do 〈fnr, f〉 ← choose_reg env e ptrs f;
    231266        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
    232         add_expr env e fnr f
     267        add_expr env e fnr ptrs f
    233268      ];
    234     add_exprs env args args_regs f
     269    add_exprs env args args_regs ptrs f
    235270| St_seq s1 s2 ⇒
    236     do f ← add_stmt env label_env s2 exits f;
    237     add_stmt env label_env s1 exits f
     271    do f ← add_stmt env label_env s2 exits ptrs f;
     272    add_stmt env label_env s1 exits ptrs f
    238273| St_ifthenelse e s1 s2 ⇒
    239274    let l_next ≝ f_entry f in
    240     do f ← add_stmt env label_env s2 exits f;
     275    do f ← add_stmt env label_env s2 exits ptrs f;
    241276    let l2 ≝ f_entry f in
    242277    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    243     do f ← add_stmt env label_env s1 exits f;
    244     add_branch env e (f_entry f) l2 f
     278    do f ← add_stmt env label_env s1 exits ptrs f;
     279    add_branch env e (f_entry f) l2 ptrs f
    245280| St_loop s ⇒
    246281    do f ← add_loop_label_to_graph f;
    247282    let l_loop ≝ f_entry f in
    248     do f ← add_stmt env label_env s exits f;
     283    do f ← add_stmt env label_env s exits ptrs f;
    249284    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
    250285| St_block s ⇒
    251     add_stmt env label_env s ((f_entry f)::exits) f
     286    add_stmt env label_env s ((f_entry f)::exits) ptrs f
    252287| St_exit n ⇒
    253288    do l ← opt_to_res … (nth_opt ? n exits);
    254289    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    255290| St_switch e tab n ⇒
    256     do 〈r,f〉 ← choose_reg env e f;
     291    do 〈r,f〉 ← choose_reg env e ptrs f;
    257292    do l_default ← opt_to_res … (nth_opt ? n exits);
    258293    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
    … …  
    264299      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
    265300      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    266     add_expr env e r f
     301    add_expr env e r ptrs f
    267302| St_return opt_e ⇒
    268303    do f ← add_fresh_to_graph (λ_. St_return) f;
    … …  
    272307        match f_result f with
    273308        [ None ⇒ Error ?
    274         | Some r ⇒ add_expr env e r f
     309        | Some r ⇒ add_expr env e r ptrs f
    275310        ]
    276311    ]
    277312| St_label l s' ⇒
    278     do f ← add_stmt env label_env s' exits f;
     313    do f ← add_stmt env label_env s' exits ptrs f;
    279314    do l' ← opt_to_res … (lookup ?? label_env l);
    280315    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
    … …  
    283318    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
    284319| St_cost l s' ⇒
    285     do f ← add_stmt env label_env s' exits f;
     320    do f ← add_stmt env label_env s' exits ptrs f;
    286321    add_fresh_to_graph (St_cost l) f
    287322| _ ⇒ Error ? (* XXX implement *)
    … …  
    336371    l
    337372    l in
    338   add_stmt env label_env (f_body f) [ ] emptyfn
     373  add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
    339374.
    340375

  • src/utilities/lists.ma

    r766 r780  
    66| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
    77].
     8
     9let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
     10match l with
     11[ nil ⇒ false
     12| cons h t ⇒ orb (p h) (exists A p t)
     13].
Note: See TracChangeset for help on using the changeset viewer.