Changeset 772 for src/Cminor


Ignore:
Timestamp:
Apr 22, 2011, 5:09:34 PM (9 years ago)
Author:
campbell
Message:

Implement proper support for RTLabs addressing modes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r771 r772  
    9595    add_expr env e1 r1 f
    9696| Mem q e' ⇒
    97     (* FIXME: inefficient - make proper use of addressing *)
    98     do 〈r, f〉 ← choose_reg env e' f;
    99     do f ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f;
    100     add_expr env e' r f
     97    add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) f (add_expr env e')
    10198| Cond e' e1 e2 ⇒
    10299    let resume_at ≝ f_entry f in
     
    112109(* Ugh, the termination checker isn't smart enough to notice that calling
    113110   add_expr with e is OK, so we take it partially applied and define a proper
    114    add_branch afterwards. *)
    115 ] and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (f:internal_function)
     111   add_<whatever> afterwards. *)
     112]
     113and add_with_addressing_internal (env:env) (e:expr)
     114                          (s:∀m:addressing. addr m → label → statement)
     115                          (f:internal_function)
     116                          (termination_hack:register → internal_function → res internal_function)
     117                          on e : res internal_function ≝
     118let add_default : unit → res internal_function ≝ λ_.
     119    do 〈r, f〉 ← choose_reg env e f;
     120    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
     121    termination_hack r f
     122in
     123match e with
     124[ Cst c ⇒
     125    match c with
     126    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
     127    | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
     128    | _ ⇒ Error ? (* int and float constants are nonsense here *)
     129    ]
     130| Op2 op e1 e2 ⇒
     131    match op with
     132    [ Oaddp ⇒
     133        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;
     136          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
     139        in
     140        match e1 with
     141        [ Cst c ⇒
     142            match c with
     143            [ Oaddrsymbol id i ⇒
     144                do 〈r, f〉 ← choose_reg env e f;
     145                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
     146                add_expr env e2 r f
     147            | _ ⇒ add_generic_addp it
     148            ]
     149        | _ ⇒ add_generic_addp it
     150        ]
     151    | _ ⇒ add_default it
     152    ]
     153| _ ⇒ add_default it
     154]
     155(* and again *)
     156and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (f:internal_function)
    116157        (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
    117158match e with
     
    137178].
    138179
    139 (* See add_branch_internal above. *)
     180(* See comment above. *)
     181definition add_with_addressing ≝
     182λenv,e,s,f. add_with_addressing_internal env e s f (add_expr env e).
    140183definition add_branch ≝
    141184λenv,e,ltrue,lfalse,f. add_branch_internal env e ltrue lfalse f (add_expr env e).
     
    160203    add_expr env e dst f
    161204| St_store q e1 e2 ⇒
    162     (* FIXME: inefficient - make proper use of addressing *)
    163     do 〈addr_reg, f〉 ← choose_reg env e1 f;
    164205    do 〈val_reg, f〉 ← choose_reg env e2 f;
    165     do f ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f;
    166     do f ← add_expr env e1 addr_reg f;
     206    do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) f;
    167207    add_expr env e2 val_reg f
    168208| St_call return_opt_id e args sig ⇒
Note: See TracChangeset for help on using the changeset viewer.