Changeset 880 for src/Cminor


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

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

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r758 r880  
    55include "common/Globalenvs.ma".
    66
    7 definition init_expr : init_data → option (memory_chunk × expr) ≝
     7(* XXX having to specify the return type in the match is annoying. *)
     8definition init_expr : init_data → option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) ≝
    89λinit.
    9 match init with
    10 [ Init_int8 i          ⇒ Some ? 〈Mint8unsigned, Cst (Ointconst i)〉
    11 | Init_int16 i         ⇒ Some ? 〈Mint16unsigned, Cst (Ointconst i)〉
    12 | Init_int32 i         ⇒ Some ? 〈Mint32, Cst (Ointconst i)〉
    13 | Init_float32 f       ⇒ Some ? 〈Mfloat32, Cst (Ofloatconst f)〉
    14 | Init_float64 f       ⇒ Some ? 〈Mfloat64, Cst (Ofloatconst f)〉
     10match init return λ_.option (Σc:memory_chunk. expr (typ_of_memory_chunk c)) with
     11[ Init_int8 i          ⇒ Some ? (dp ?? Mint8unsigned (Cst ? (Ointconst i)))
     12| Init_int16 i         ⇒ Some ? (dp ?? Mint16unsigned (Cst ? (Ointconst i)))
     13| Init_int32 i         ⇒ Some ? (dp ?? Mint32 (Cst ? (Ointconst i)))
     14| Init_float32 f       ⇒ Some ? (dp ?? Mfloat32 (Cst ? (Ofloatconst f)))
     15| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1516| Init_space n         ⇒ None ?
    16 | Init_null r          ⇒ Some ? 〈Mpointer r, Op1 (Optrofint r) (Cst (Ointconst zero))〉
    17 | Init_addrof r id off ⇒ Some ? 〈Mpointer r, Cst (Oaddrsymbol id off)〉
     17| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst zero))))
     18| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    1819].
    1920
     
    2627[ None ⇒ St_skip
    2728| Some x ⇒
    28     let 〈chunk, e〉 ≝ x in
    29     St_store chunk (Cst (Oaddrsymbol id off)) e
     29    match x with [ dp chunk e ⇒
     30      St_store ? chunk (Cst ? (Oaddrsymbol id off)) e
     31    ]
    3032].
    3133
  • src/Cminor/semantics.ma

    r879 r880  
    5050axiom FailedLoad : String.
    5151
    52 let rec eval_expr (ge:genv) (e:expr) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
     52let rec eval_expr (ge:genv) (ty0:typ) (e:expr ty0) (en:env) (sp:block) (m:mem) on e : res (trace × val) ≝
    5353match e with
    54 [ Id i ⇒
     54[ Id _ i ⇒
    5555    do r ← opt_to_res … [MSG UnknownLocal; CTX ? i] (lookup ?? en i);
    5656    OK ? 〈E0, r〉
    57 | Cst c ⇒
     57| Cst _ c ⇒
    5858    do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
    5959    OK ? 〈E0, r〉
    60 | Op1 op e' ⇒
    61     do 〈tr,v〉 ← eval_expr ge e' en sp m;
     60| Op1 ty ty' op e' ⇒
     61    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    6262    do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
    6363    OK ? 〈tr, r〉
    64 | Op2 op e1 e2 ⇒
    65     do 〈tr1,v1〉 ← eval_expr ge e1 en sp m;
    66     do 〈tr2,v2〉 ← eval_expr ge e2 en sp m;
     64| Op2 ty1 ty2 ty' op e1 e2 ⇒
     65    do 〈tr1,v1〉 ← eval_expr ge ? e1 en sp m;
     66    do 〈tr2,v2〉 ← eval_expr ge ? e2 en sp m;
    6767    do r ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    6868    OK ? 〈tr1 ⧺ tr2, r〉
    69 | Mem chunk e ⇒
    70     do 〈tr,v〉 ← eval_expr ge e en sp m;
     69| Mem ty chunk e ⇒
     70    do 〈tr,v〉 ← eval_expr ge ? e en sp m;
    7171    do r ← opt_to_res … (msg FailedLoad) (loadv chunk m v);
    7272    OK ? 〈tr, r〉
    73 | Cond e' e1 e2 ⇒
    74     do 〈tr,v〉 ← eval_expr ge e' en sp m;
     73| Cond sz sg ty e' e1 e2 ⇒
     74    do 〈tr,v〉 ← eval_expr ge ? e' en sp m;
    7575    do b ← eval_bool_of_val v;
    76     do 〈tr',r〉 ← eval_expr ge (if b then e1 else e2) en sp m;
     76    do 〈tr',r〉 ← eval_expr ge ? (if b then e1 else e2) en sp m;
    7777    OK ? 〈tr ⧺ tr', r〉
    78 | Ecost l e' ⇒
    79     do 〈tr,r〉 ← eval_expr ge e' en sp m;
     78| Ecost ty l e' ⇒
     79    do 〈tr,r〉 ← eval_expr ge ty e' en sp m;
    8080    OK ? 〈Echarge l ⧺ tr, r〉
    8181].
     
    113113    | Some sk ⇒ Some ? sk
    114114    ]
    115 | St_ifthenelse _ s1 s2 ⇒
     115| St_ifthenelse _ _ _ s1 s2 ⇒
    116116    match find_label l s1 k with
    117117    [ None ⇒ find_label l s2 k
     
    165165        | Kcall _ _ _ _ _ ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) k〉
    166166        ]
    167     | St_assign id e ⇒
    168         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     167    | St_assign _ id e ⇒
     168        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    169169        ! en' ← update ?? en id v;
    170170        ret ? 〈tr, State f St_skip en' m sp k〉
    171     | St_store chunk edst e ⇒
    172         ! 〈tr,vdst〉 ← eval_expr ge edst en sp m;
    173         ! 〈tr',v〉 ← eval_expr ge e en sp m;
     171    | St_store _ chunk edst e ⇒
     172        ! 〈tr,vdst〉 ← eval_expr ge ? edst en sp m;
     173        ! 〈tr',v〉 ← eval_expr ge ? e en sp m;
    174174        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    175175        ret ? 〈tr ⧺ tr', State f St_skip en m' sp k〉
    176176
    177177    | St_call dst ef args ⇒
    178         ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
     178        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
    179179        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    180         ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
     180        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    181181        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Kcall dst f sp en k)〉
    182182    | St_tailcall ef args ⇒
    183         ! 〈tr,vf〉 ← eval_expr ge ef en sp m;
     183        ! 〈tr,vf〉 ← eval_expr ge ? ef en sp m;
    184184        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    185         ! 〈tr',vargs〉 ← trace_map … (λe. eval_expr ge e en sp m) args;
     185        ! 〈tr',vargs〉 ← trace_map … (λe. match e with [ dp ty e ⇒ eval_expr ge ? e en sp m ]) args;
    186186        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) (call_cont k)〉
    187187       
    188188    | St_seq s1 s2 ⇒ ret ? 〈E0, State f s1 en m sp (Kseq s2 k)〉
    189     | St_ifthenelse e strue sfalse ⇒
    190         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     189    | St_ifthenelse _ _ e strue sfalse ⇒
     190        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    191191        ! b ← eval_bool_of_val v;
    192192        ret ? 〈tr, State f (if b then strue else sfalse) en m sp k〉
     
    196196        ! k' ← k_exit n k;
    197197        ret ? 〈E0, State f St_skip en m sp k'〉
    198     | St_switch e cs default ⇒
    199         ! 〈tr,v〉 ← eval_expr ge e en sp m;
     198    | St_switch _ _ e cs default ⇒
     199        ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
    200200        match v with
    201201        [ Vint i ⇒
     
    208208        [ None ⇒ ret ? 〈E0, Returnstate (None ?) (free m sp) (call_cont k)〉
    209209        | Some e ⇒
    210             ! 〈tr,v〉 ← eval_expr ge e en sp m;
    211             ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
     210            match e with [ dp ty e ⇒
     211              ! 〈tr,v〉 ← eval_expr ge ? e en sp m;
     212              ret ? 〈tr, Returnstate (Some ? v) (free m sp) (call_cont k)〉
     213            ]
    212214        ]
    213215    | St_label l s' ⇒ ret ? 〈E0, State f s' en m sp k〉
  • src/Cminor/syntax.ma

    r878 r880  
    33include "common/CostLabel.ma".
    44
    5 inductive expr : Type[0] ≝
    6 | Id : ident → expr
    7 | Cst : constant → expr
    8 | Op1 : unary_operation → expr → expr
    9 | Op2 : binary_operation → expr → expr → expr
    10 | Mem : memory_chunk → expr → expr
    11 | Cond : expr → expr → expr → expr
    12 | Ecost : costlabel → expr → expr.
     5(* TODO: consider making the typing stricter. *)
     6
     7inductive expr : typ → Type[0] ≝
     8| Id : ∀t. ident → expr t
     9| Cst : ∀t. constant → expr t
     10| Op1 : ∀t,t'. unary_operation → expr t → expr t'
     11| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
     12| Mem : ∀t. memory_chunk → expr (ASTptr Any) → expr t
     13| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
     14| Ecost : ∀t. costlabel → expr t → expr t.
    1315
    1416inductive stmt : Type[0] ≝
    1517| St_skip : stmt
    16 | St_assign : ident → expr → stmt
    17 | St_store : memory_chunk → expr → expr → stmt
     18| St_assign : ∀t. ident → expr t → stmt
     19| St_store : ∀t. memory_chunk → expr (ASTptr Any) → expr t → stmt
    1820(* ident for returned value, expression to identify fn, args. *)
    19 | St_call : option ident → expr → list expr → stmt
    20 | St_tailcall : expr → list expr → stmt
     21| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
     22| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
    2123| St_seq : stmt → stmt → stmt
    22 | St_ifthenelse : expr → stmt → stmt → stmt
     24| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
    2325| St_loop : stmt → stmt
    2426| St_block : stmt → stmt
    2527| St_exit : nat → stmt
    2628(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    27 | St_switch : expr → list (int × nat) → nat → stmt
    28 | St_return : option expr → stmt
     29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
     30| St_return : option (Σt. expr t) → stmt
    2931| St_label : ident → stmt → stmt
    3032| St_goto : ident → stmt
  • 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.