Changeset 880 for src/Cminor/toRTLabs.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (8 years ago)
Author:
campbell
Message:

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r816 r880  
    6767                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    6868
    69 let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝
     69let rec expr_yields_pointer (ty:typ) (e:expr ty) (ptrs:list ident) on e : bool ≝
    7070match 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' ⇒
     71[ Id _ i ⇒ exists ? (eq_identifier ? i) ptrs
     72| Cst _ c ⇒ match c with [ Oaddrsymbol _ _ ⇒ true | Oaddrstack _ ⇒ true | _ ⇒ false ]
     73| Op1 _ _ op e' ⇒
    7474    match op with
    75     [ Oid ⇒ expr_yields_pointer e' ptrs
     75    [ Oid ⇒ expr_yields_pointer ? e' ptrs
    7676    | Optrofint _ ⇒ true
    7777    | _ ⇒ false
    7878    ]
    79 | Op2 op e1 e2 ⇒
     79| Op2 _ _ _ op e1 e2 ⇒
    8080    match op with
    8181    [ Oaddp ⇒ true
     
    8383    | _ ⇒ false
    8484    ]
    85 | Mem q e' ⇒
     85| Mem _ q e' ⇒
    8686    match q with
    8787    [ Mpointer _ ⇒ true
     
    8989    ]
    9090(* 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
     91| Cond _ _ _ e' e1 e2 ⇒ (expr_yields_pointer ? e1 ptrs) ∨ (expr_yields_pointer ? e2 ptrs)
     92| Ecost _ _ e' ⇒ expr_yields_pointer ? e' ptrs
    9393].
    9494
    9595axiom UnknownVariable : String.
    9696
    97 definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝
    98 λenv,e,ptrs,f.
     97definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝
     98λenv,ty,e,ptrs,f.
    9999  match e with
    100   [ Id i ⇒
     100  [ Id _ i ⇒
    101101      do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
    102102      OK ? 〈r, f〉
    103103  | _ ⇒
    104       if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f
     104      if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f
    105105  ].
    106106
    107 definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝
     107definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝
    108108λenv,es,ptrs,f.
    109   foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
    110                     do 〈r,f'〉 ← choose_reg env e ptrs f;
    111                     OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
     109  foldr (Σt:typ.expr t) ?
     110    (λe,acc. do 〈rs,f〉 ← acc;
     111             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ];
     112             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
    112113
    113114axiom BadCminorProgram : String.
    114115
    115 let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
     116let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
    116117match e with
    117 [ Id i ⇒
     118[ Id _ i ⇒
    118119    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    119120    match register_eq r dst with
     
    121122    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
    122123    ]
    123 | Cst c ⇒ add_fresh_to_graph (St_const dst c) f
    124 | Op1 op e' ⇒
    125     do 〈r,f〉 ← choose_reg env e' ptrs f;
     124| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
     125| Op1 _ _ op e' ⇒
     126    do 〈r,f〉 ← choose_reg env ? e' ptrs f;
    126127    do f ← add_fresh_to_graph (St_op1 op dst r) f;
    127     add_expr env e' r ptrs f
    128 | Op2 op e1 e2 ⇒
    129     do 〈r1,f〉 ← choose_reg env e1 ptrs f;
    130     do 〈r2,f〉 ← choose_reg env e2 ptrs f;
     128    add_expr env ? e' r ptrs f
     129| Op2 _ _ _ op e1 e2 ⇒
     130    do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
     131    do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
    131132    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
    132     do f ← add_expr env e2 r2 ptrs f;
    133     add_expr env e1 r1 ptrs f
    134 | Mem q e' ⇒
    135     add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e')
    136 | Cond e' e1 e2 ⇒
     133    do f ← add_expr env ? e2 r2 ptrs f;
     134    add_expr env ? e1 r1 ptrs f
     135| Mem _ q e' ⇒
     136    add_with_addressing_internal env ? e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env ? e')
     137| Cond _ _ _ e' e1 e2 ⇒
    137138    let resume_at ≝ f_entry f in
    138     do f ← add_expr env e2 dst ptrs f;
     139    do f ← add_expr env ? e2 dst ptrs f;
    139140    let lfalse ≝ f_entry f in
    140141    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
    141     do f ← add_expr env e1 dst ptrs f;
    142     add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e')
    143 | Ecost l e' ⇒
    144     do f ← add_expr env e' dst ptrs f;
     142    do f ← add_expr env ? e1 dst ptrs f;
     143    add_branch_internal env ? e' (f_entry f) lfalse ptrs f (add_expr env ? e')
     144| Ecost _ l e' ⇒
     145    do f ← add_expr env ? e' dst ptrs f;
    145146    add_fresh_to_graph (St_cost l) f
    146147   
     
    149150   add_<whatever> afterwards. *)
    150151]
    151 and add_with_addressing_internal (env:env) (e:expr)
     152and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty)
    152153                          (s:∀m:addressing. addr m → label → statement)
    153154                          (ptrs:list ident)
     
    156157                          on e : res internal_function ≝
    157158let add_default : unit → res internal_function ≝ λ_.
    158     do 〈r, f〉 ← choose_reg env e ptrs f;
     159    do 〈r, f〉 ← choose_reg env ? e ptrs f;
    159160    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
    160161    termination_hack r ptrs f
    161162in
    162163match e with
    163 [ Cst c ⇒
     164[ Cst _ c ⇒
    164165    match c with
    165166    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
     
    167168    | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
    168169    ]
    169 | Op2 op e1 e2 ⇒
     170| Op2 _ _ _ op e1 e2 ⇒
    170171    match op with
    171172    [ Oaddp ⇒
    172173        let add_generic_addp : unit → res internal_function ≝ λ_.
    173           do 〈r1, f〉 ← choose_reg env e1 ptrs f;
    174           do 〈r2, f〉 ← choose_reg env e2 ptrs f;
     174          do 〈r1, f〉 ← choose_reg env ? e1 ptrs f;
     175          do 〈r2, f〉 ← choose_reg env ? e2 ptrs f;
    175176          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
    176           do f ← add_expr env e2 r2 ptrs f;
    177           add_expr env e1 r1 ptrs f
     177          do f ← add_expr env ? e2 r2 ptrs f;
     178          add_expr env ? e1 r1 ptrs f
    178179        in
    179180        match e1 with
    180         [ Cst c ⇒
     181        [ Cst _ c ⇒
    181182            match c with
    182183            [ Oaddrsymbol id i ⇒
    183                 do 〈r, f〉 ← choose_reg env e ptrs f;
     184                do 〈r, f〉 ← choose_reg env ? e ptrs f;
    184185                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
    185                 add_expr env e2 r ptrs f
     186                add_expr env ? e2 r ptrs f
    186187            | _ ⇒ add_generic_addp it
    187188            ]
     
    193194]
    194195(* and again *)
    195 and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
     196and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
    196197        (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
    197198match e with
    198 [ Id i ⇒
     199[ Id _ i ⇒
    199200    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    200201    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
    201 | Cst c ⇒
     202| Cst _ c ⇒
    202203    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    203 | Op1 op e' ⇒
    204     do 〈r,f〉 ← choose_reg env e' ptrs f;
     204| Op1 _ _ op e' ⇒
     205    do 〈r,f〉 ← choose_reg env ? e' ptrs f;
    205206    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    206     add_expr env e' r ptrs f
    207 | Op2 op e1 e2 ⇒
    208     do 〈r1,f〉 ← choose_reg env e1 ptrs f;
    209     do 〈r2,f〉 ← choose_reg env e2 ptrs f;
     207    add_expr env ? e' r ptrs f
     208| Op2 _ _ _ op e1 e2 ⇒
     209    do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
     210    do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
    210211    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    211     do f ← add_expr env e2 r2 ptrs f;
    212     add_expr env e1 r1 ptrs f
     212    do f ← add_expr env ? e2 r2 ptrs f;
     213    add_expr env ? e1 r1 ptrs f
    213214| _ ⇒
    214     do 〈r,f〉 ← choose_reg env e ptrs f;
     215    do 〈r,f〉 ← choose_reg env ? e ptrs f;
    215216    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    216217    termination_hack_add_expr r ptrs f
     
    219220(* See comment above. *)
    220221definition add_with_addressing ≝
    221 λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e).
     222λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e).
    222223definition add_branch ≝
    223 λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
     224λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e).
    224225
    225226(* This shouldn't occur; maybe use vectors? *)
    226227axiom WrongNumberOfArguments : String.
    227228
    228 let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
     229let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
    229230match es with
    230231[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
     
    234235    | cons r rt ⇒
    235236        do f ← add_exprs env et rt ptrs f;
    236         add_expr env e r ptrs f
     237        match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ]
    237238    ]
    238239].
     
    244245match s with
    245246[ St_skip ⇒ OK ? f
    246 | St_assign x e ⇒
     247| St_assign _ x e ⇒
    247248    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    248     add_expr env e dst ptrs f
    249 | St_store q e1 e2 ⇒
    250     do 〈val_reg, f〉 ← choose_reg env e2 ptrs f;
    251     do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
    252     add_expr env e2 val_reg ptrs f
     249    add_expr env ? e dst ptrs f
     250| St_store _ q e1 e2 ⇒
     251    do 〈val_reg, f〉 ← choose_reg env ? e2 ptrs f;
     252    do f ← add_with_addressing env ? e1 (λm,rs. St_store q m rs val_reg) ptrs f;
     253    add_expr env ? e2 val_reg ptrs f
    253254| St_call return_opt_id e args ⇒
    254255    do return_opt_reg ←
     
    260261    do f ←
    261262      match e with
    262       [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
     263      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    263264      | _ ⇒
    264         do 〈fnr, f〉 ← choose_reg env e ptrs f;
     265        do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
    265266        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
    266         add_expr env e fnr ptrs f
     267        add_expr env ? e fnr ptrs f
    267268      ];
    268269    add_exprs env args args_regs ptrs f
     
    271272    do f ←
    272273      match e with
    273       [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
     274      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    274275      | _ ⇒
    275         do 〈fnr, f〉 ← choose_reg env e ptrs f;
     276        do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
    276277        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
    277         add_expr env e fnr ptrs f
     278        add_expr env ? e fnr ptrs f
    278279      ];
    279280    add_exprs env args args_regs ptrs f
     
    281282    do f ← add_stmt env label_env s2 exits ptrs f;
    282283    add_stmt env label_env s1 exits ptrs f
    283 | St_ifthenelse e s1 s2 ⇒
     284| St_ifthenelse _ _ e s1 s2 ⇒
    284285    let l_next ≝ f_entry f in
    285286    do f ← add_stmt env label_env s2 exits ptrs f;
     
    287288    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    288289    do f ← add_stmt env label_env s1 exits ptrs f;
    289     add_branch env e (f_entry f) l2 ptrs f
     290    add_branch env ? e (f_entry f) l2 ptrs f
    290291| St_loop s ⇒
    291292    do f ← add_loop_label_to_graph f;
     
    298299    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    299300    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    300 | St_switch e tab n ⇒
    301     do 〈r,f〉 ← choose_reg env e ptrs f;
     301| St_switch _ _ e tab n ⇒
     302    do 〈r,f〉 ← choose_reg env ? e ptrs f;
    302303    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    303304    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
     
    309310      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
    310311      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    311     add_expr env e r ptrs f
     312    add_expr env ? e r ptrs f
    312313| St_return opt_e ⇒
    313314    do f ← add_fresh_to_graph (λ_. St_return) f;
     
    317318        match f_result f with
    318319        [ None ⇒ Error ? (msg ReturnMismatch)
    319         | Some r ⇒ add_expr env e r ptrs f
     320        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ]
    320321        ]
    321322    ]
     
    343344match s with
    344345[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    345 | St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     346| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    346347| St_loop s ⇒ labels_of s
    347348| St_block s ⇒ labels_of s
Note: See TracChangeset for help on using the changeset viewer.