Changeset 887


Ignore:
Timestamp:
Jun 6, 2011, 3:55:23 PM (8 years ago)
Author:
campbell
Message:

Start bringing RTLabs into line with the prototype compiler:

  • a coarse-grained type is associated with every register
  • the special addressing modes have been removed
Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r881 r887  
    5555          match f' with
    5656          [ Internal f ⇒ 〈id, Internal ? (mk_internal_function
    57                                            (f_sig f)
     57                                           (f_return f)
    5858                                           (f_params f)
    5959                                           (f_vars f)
    60                                            (f_ptrs f)
    6160                                           (f_stacksize f)
    6261                                           (St_seq s (f_body f)))〉
  • src/Cminor/toRTLabs.ma

    r881 r887  
    66definition env ≝ identifier_map SymbolTag register.
    77definition label_env ≝ identifier_map SymbolTag label.
    8 definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝
     8definition populate_env : env → universe RegisterTag → list (ident × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝
    99λen,gen. foldr ??
    10  (λid,rsengen.
     10 (λidt,rsengen.
     11   let 〈id,ty〉 ≝ idt in
    1112   do 〈rs,en,gen〉 ← rsengen;
    1213   do 〈r,gen'〉 ← fresh … gen;
    13    OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
     14   OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
    1415
    1516definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
     
    2324definition fill_in_statement : label → statement → internal_function → internal_function ≝
    2425λl,s,f.
    25   mk_internal_function (f_labgen f) (f_reggen f) (f_sig f)
    26                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     26  mk_internal_function (f_labgen f) (f_reggen f)
     27                       (f_result f) (f_params f) (f_locals f)
    2728                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
    2829
     
    3031definition add_to_graph : label → statement → internal_function → internal_function ≝
    3132λl,s,f.
    32   mk_internal_function (f_labgen f) (f_reggen f) (f_sig f)
    33                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     33  mk_internal_function (f_labgen f) (f_reggen f)
     34                       (f_result f) (f_params f) (f_locals f)
    3435                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
    3536
     
    4041  do 〈l,g〉 ← fresh … (f_labgen f);
    4142  let s' ≝ s (f_entry f) in
    42   OK ? (mk_internal_function g (f_reggen f) (f_sig f)
    43                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     43  OK ? (mk_internal_function g (f_reggen f)
     44                       (f_result f) (f_params f) (f_locals f)
    4445                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
    4546
     
    4950λf.
    5051  do 〈l,g〉 ← fresh … (f_labgen f);
    51   OK ? (mk_internal_function g (f_reggen f) (f_sig f)
    52                        (f_result f) (f_params f) (f_locals f) (f_ptrs f)
     52  OK ? (mk_internal_function g (f_reggen f)
     53                       (f_result f) (f_params f) (f_locals f)
    5354                       (f_stacksize f) (f_graph f) l (f_exit f)).
    5455
    55 definition fresh_reg : internal_function → res (register × internal_function) ≝
    56 λf.
     56definition fresh_reg : internal_function → typ → res (register × internal_function) ≝
     57λf,ty.
    5758  do 〈r,g〉 ← fresh … (f_reggen f);
    58   OK ? 〈r, mk_internal_function (f_labgen f) g (f_sig f)
    59                        (f_result f) (f_params f) (r::(f_locals f)) (f_ptrs f)
     59  OK ? 〈r, mk_internal_function (f_labgen f) g
     60                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
    6061                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
    6162
    62 definition 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 
    69 let rec expr_yields_pointer (ty:typ) (e:expr ty) (ptrs:list ident) on e : bool ≝
    70 match 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 
    9563axiom UnknownVariable : String.
    9664
    97 definition choose_reg : env → ∀t.expr t → list ident → internal_function → res (register × internal_function) ≝
    98 λenv,ty,e,ptrs,f.
     65definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function) ≝
     66λenv,ty,e,f.
    9967  match e with
    10068  [ Id _ i ⇒
     
    10270      OK ? 〈r, f〉
    10371  | _ ⇒
    104       if expr_yields_pointer ? e ptrs then fresh_ptr_reg f else fresh_reg f
     72      fresh_reg f ty
    10573  ].
    10674
    107 definition choose_regs : env → list (Σt:typ.expr t) → list ident → internal_function → res (list register × internal_function) ≝
    108 λenv,es,ptrs,f.
     75definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝
     76λenv,es,f.
    10977  foldr (Σt:typ.expr t) ?
    11078    (λe,acc. do 〈rs,f〉 ← acc;
    111              do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e ptrs f ];
     79             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ];
    11280             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
    11381
    11482axiom BadCminorProgram : String.
    11583
    116 let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
     84let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (f:internal_function) on e: res internal_function ≝
    11785match e with
    11886[ Id _ i ⇒
     
    12492| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
    12593| Op1 _ _ op e' ⇒
    126     do 〈r,f〉 ← choose_reg env ? e' ptrs f;
     94    do 〈r,f〉 ← choose_reg env ? e' f;
    12795    do f ← add_fresh_to_graph (St_op1 op dst r) f;
    128     add_expr env ? e' r ptrs f
     96    add_expr env ? e' r f
    12997| Op2 _ _ _ op e1 e2 ⇒
    130     do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
    131     do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
     98    do 〈r1,f〉 ← choose_reg env ? e1 f;
     99    do 〈r2,f〉 ← choose_reg env ? e2 f;
    132100    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
    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')
     101    do f ← add_expr env ? e2 r2 f;
     102    add_expr env ? e1 r1 f
     103| Mem _ _ q e' ⇒
     104    do 〈r,f〉 ← choose_reg env ? e' f;
     105    do f ← add_fresh_to_graph (St_load q r dst) f;
     106    add_expr env ? e' r f
    137107| Cond _ _ _ e' e1 e2 ⇒
    138108    let resume_at ≝ f_entry f in
    139     do f ← add_expr env ? e2 dst ptrs f;
     109    do f ← add_expr env ? e2 dst f;
    140110    let lfalse ≝ f_entry f in
    141111    do f ← add_fresh_to_graph (λ_.St_skip resume_at) 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')
     112    do f ← add_expr env ? e1 dst f;
     113    add_branch_internal env ? e' (f_entry f) lfalse f (add_expr env ? e')
    144114| Ecost _ l e' ⇒
    145     do f ← add_expr env ? e' dst ptrs f;
     115    do f ← add_expr env ? e' dst f;
    146116    add_fresh_to_graph (St_cost l) f
    147117   
     
    150120   add_<whatever> afterwards. *)
    151121]
    152 and add_with_addressing_internal (env:env) (ty:typ) (e:expr ty)
    153                           (s:∀m:addressing. addr m → label → statement)
    154                           (ptrs:list ident)
    155                           (f:internal_function)
    156                           (termination_hack:register → list ident → internal_function → res internal_function)
    157                           on e : res internal_function ≝
    158 let add_default : unit → res internal_function ≝ λ_.
    159     do 〈r, f〉 ← choose_reg env ? e ptrs f;
    160     do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
    161     termination_hack r ptrs f
    162 in
    163 match e with
    164 [ Cst _ c ⇒
    165     match c with
    166     [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
    167     | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
    168     | _ ⇒ Error ? (msg BadCminorProgram) (* int and float constants are nonsense here *)
    169     ]
    170 | Op2 _ _ _ op e1 e2 ⇒
    171     match op with
    172     [ Oaddp ⇒
    173         let add_generic_addp : unit → res internal_function ≝ λ_.
    174           do 〈r1, f〉 ← choose_reg env ? e1 ptrs f;
    175           do 〈r2, f〉 ← choose_reg env ? e2 ptrs f;
    176           do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
    177           do f ← add_expr env ? e2 r2 ptrs f;
    178           add_expr env ? e1 r1 ptrs f
    179         in
    180         match e1 with
    181         [ Cst _ c ⇒
    182             match c with
    183             [ Oaddrsymbol id i ⇒
    184                 do 〈r, f〉 ← choose_reg env ? e ptrs f;
    185                 do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
    186                 add_expr env ? e2 r ptrs f
    187             | _ ⇒ add_generic_addp it
    188             ]
    189         | _ ⇒ add_generic_addp it
    190         ]
    191     | _ ⇒ add_default it
    192     ]
    193 | _ ⇒ add_default it
    194 ]
    195 (* and again *)
    196 and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
    197         (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
     122and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (f:internal_function)
     123        (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
    198124match e with
    199125[ Id _ i ⇒
     
    203129    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    204130| Op1 _ _ op e' ⇒
    205     do 〈r,f〉 ← choose_reg env ? e' ptrs f;
     131    do 〈r,f〉 ← choose_reg env ? e' f;
    206132    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    207     add_expr env ? e' r ptrs f
     133    add_expr env ? e' r f
    208134| Op2 _ _ _ op e1 e2 ⇒
    209     do 〈r1,f〉 ← choose_reg env ? e1 ptrs f;
    210     do 〈r2,f〉 ← choose_reg env ? e2 ptrs f;
     135    do 〈r1,f〉 ← choose_reg env ? e1 f;
     136    do 〈r2,f〉 ← choose_reg env ? e2 f;
    211137    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    212     do f ← add_expr env ? e2 r2 ptrs f;
    213     add_expr env ? e1 r1 ptrs f
     138    do f ← add_expr env ? e2 r2 f;
     139    add_expr env ? e1 r1 f
    214140| _ ⇒
    215     do 〈r,f〉 ← choose_reg env ? e ptrs f;
     141    do 〈r,f〉 ← choose_reg env ? e f;
    216142    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    217     termination_hack_add_expr r ptrs f
     143    termination_hack_add_expr r f
    218144].
    219145
    220146(* See comment above. *)
    221 definition add_with_addressing ≝
    222 λenv,ty,e,s,ptrs,f. add_with_addressing_internal env ty e s ptrs f (add_expr env ty e).
    223147definition add_branch ≝
    224 λenv,ty,e,ltrue,lfalse,ptrs,f. add_branch_internal env ty e ltrue lfalse ptrs f (add_expr env ty e).
     148λenv,ty,e,ltrue,lfalse,f. add_branch_internal env ty e ltrue lfalse f (add_expr env ty e).
    225149
    226150(* This shouldn't occur; maybe use vectors? *)
    227151axiom WrongNumberOfArguments : String.
    228152
    229 let 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 ≝
     153let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (f:internal_function) on es: res internal_function ≝
    230154match es with
    231155[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
     
    234158    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
    235159    | cons r rt ⇒
    236         do f ← add_exprs env et rt ptrs f;
    237         match e with [ dp ty e ⇒ add_expr env ty e r ptrs f ]
     160        do f ← add_exprs env et rt f;
     161        match e with [ dp ty e ⇒ add_expr env ty e r f ]
    238162    ]
    239163].
     
    242166axiom ReturnMismatch : String.
    243167
    244 let 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 ≝
     168let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
    245169match s with
    246170[ St_skip ⇒ OK ? f
    247171| St_assign _ x e ⇒
    248172    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
    249     add_expr env ? e dst ptrs f
     173    add_expr env ? e dst f
    250174| 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
     175    do 〈val_reg, f〉 ← choose_reg env ? e2 f;
     176    do 〈addr_reg, f〉 ← choose_reg env ? e1 f;
     177    do f ← add_fresh_to_graph (St_store q addr_reg val_reg) f;
     178    do f ← add_expr env ? e1 addr_reg f;
     179    add_expr env ? e2 val_reg f
    254180| St_call return_opt_id e args ⇒
    255181    do return_opt_reg ←
     
    258184      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
    259185      ];
    260     do 〈args_regs, f〉 ← choose_regs env args ptrs f;
     186    do 〈args_regs, f〉 ← choose_regs env args f;
    261187    do f ←
    262188      match e with
    263189      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    264190      | _ ⇒
    265         do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
     191        do 〈fnr, f〉 ← choose_reg env ? e f;
    266192        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
    267         add_expr env ? e fnr ptrs f
     193        add_expr env ? e fnr f
    268194      ];
    269     add_exprs env args args_regs ptrs f
     195    add_exprs env args args_regs f
    270196| St_tailcall e args ⇒
    271     do 〈args_regs, f〉 ← choose_regs env args ptrs f;
     197    do 〈args_regs, f〉 ← choose_regs env args f;
    272198    do f ←
    273199      match e with
    274200      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    275201      | _ ⇒
    276         do 〈fnr, f〉 ← choose_reg env ? e ptrs f;
     202        do 〈fnr, f〉 ← choose_reg env ? e f;
    277203        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
    278         add_expr env ? e fnr ptrs f
     204        add_expr env ? e fnr f
    279205      ];
    280     add_exprs env args args_regs ptrs f
     206    add_exprs env args args_regs f
    281207| St_seq s1 s2 ⇒
    282     do f ← add_stmt env label_env s2 exits ptrs f;
    283     add_stmt env label_env s1 exits ptrs f
     208    do f ← add_stmt env label_env s2 exits f;
     209    add_stmt env label_env s1 exits f
    284210| St_ifthenelse _ _ e s1 s2 ⇒
    285211    let l_next ≝ f_entry f in
    286     do f ← add_stmt env label_env s2 exits ptrs f;
     212    do f ← add_stmt env label_env s2 exits f;
    287213    let l2 ≝ f_entry f in
    288214    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    289     do f ← add_stmt env label_env s1 exits ptrs f;
    290     add_branch env ? e (f_entry f) l2 ptrs f
     215    do f ← add_stmt env label_env s1 exits f;
     216    add_branch env ? e (f_entry f) l2 f
    291217| St_loop s ⇒
    292218    do f ← add_loop_label_to_graph f;
    293219    let l_loop ≝ f_entry f in
    294     do f ← add_stmt env label_env s exits ptrs f;
     220    do f ← add_stmt env label_env s exits f;
    295221    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
    296222| St_block s ⇒
    297     add_stmt env label_env s ((f_entry f)::exits) ptrs f
     223    add_stmt env label_env s ((f_entry f)::exits) f
    298224| St_exit n ⇒
    299225    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    300226    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    301 | St_switch _ _ e tab n ⇒
    302     do 〈r,f〉 ← choose_reg env ? e ptrs f;
     227| St_switch sz sg e tab n ⇒
     228    do 〈r,f〉 ← choose_reg env ? e f;
    303229    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    304230    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
     
    306232      do f ← f;
    307233      let 〈i,n〉 ≝ cs in
    308       do 〈cr,f〉 ← fresh_reg … f;
     234      do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
    309235      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    310236      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
    311237      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    312     add_expr env ? e r ptrs f
     238    add_expr env ? e r f
    313239| St_return opt_e ⇒
    314240    do f ← add_fresh_to_graph (λ_. St_return) f;
     
    318244        match f_result f with
    319245        [ None ⇒ Error ? (msg ReturnMismatch)
    320         | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e r ptrs f ]
     246        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f ]
    321247        ]
    322248    ]
    323249| St_label l s' ⇒
    324     do f ← add_stmt env label_env s' exits ptrs f;
     250    do f ← add_stmt env label_env s' exits f;
    325251    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
    326252    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
     
    329255    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
    330256| St_cost l s' ⇒
    331     do f ← add_stmt env label_env s' exits ptrs f;
     257    do f ← add_stmt env label_env s' exits f;
    332258    add_fresh_to_graph (St_cost l) f
    333259].
     
    360286do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
    361287do 〈result, locals, reggen〉 ←
    362   match sig_res (f_sig f) with
     288  match f_return f with
    363289  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
    364   | Some _
     290  | Some ty
    365291      do 〈r,gen〉 ← fresh … reggen2;
    366       OK ? 〈Some ? r, r::locals0, gen〉 ];
    367 do ptrs ← mmap ?? (λid. opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id)) (f_ptrs f);
     292      OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];
    368293do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
    369294do 〈l,labgen〉 ← fresh … labgen1;
     
    372297    labgen
    373298    reggen
    374     (f_sig f)
    375299    result
    376300    params
    377301    locals
    378     ptrs
    379302    (f_stacksize f)
    380303    (add ?? (empty_map …) l St_return)
    381304    l
    382305    l in
    383   add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
     306  add_stmt env label_env (f_body f) [ ] emptyfn
    384307.
    385308
  • src/RTLabs/semantics.ma

    r879 r887  
    5050definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    5151
    52 definition init_locals : list register → register_env val ≝
    53 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
     52definition init_locals : list (register × typ) → register_env val ≝
     53foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
    5454
    5555definition reg_store ≝
     
    5959axiom WrongNumberOfParameters : String.
    6060
    61 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
     61let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    6262match rs with
    6363[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    64 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
     64| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
     65  let 〈r,ty〉 ≝ rt in
    6566  let locals' ≝ add RegisterTag val locals r v in
    6667  params_store rst vst locals'
     
    7475axiom FailedOp : String.
    7576axiom MissingSymbol : String.
    76 
    77 (* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
    78 
    79 definition eval_addr : genv → frame → ∀m:addressing. Vector register (addr_mode_args m) → res val ≝
    80 λge,f,m. match m return λm'.Vector register (addr_mode_args m') → ? with
    81 [ Aindexed i ⇒ λargs.
    82     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
    83     opt_to_res … (msg FailedOp) (ev_addp v (Vint i))
    84 | Aindexed2 ⇒ λargs.
    85     do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
    86     do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
    87     opt_to_res … (msg FailedOp) (ev_addp v1 v2)
    88 | Aglobal id off ⇒ λargs.
    89     do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    90     OK ? (Vptr Any loc ? (shift_offset zero_offset off))
    91 | Abased id off ⇒ λargs.
    92     do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    93     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
    94     opt_to_res … (msg FailedOp) (ev_addp (Vptr Any loc ? zero_offset) v)
    95 | Ainstack off ⇒ λargs.
    96     OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
    97 ]
    98 . /2/ [ 1,2: cases loc | cases (sp f) ] // qed.
    99 
    10077
    10178axiom MissingStatement : String.
     
    132109      ! locals ← reg_store dst v' (locals f);
    133110      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    134   | St_load chunk mode args dst l ⇒
    135       ! vaddr ← eval_addr ge f mode args;
     111  | St_load chunk addr dst l ⇒
     112      ! vaddr ← reg_retrieve (locals f) addr;
    136113      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    137114      ! locals ← reg_store dst v (locals f);
    138115      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    139   | St_store chunk mode args src l ⇒
    140       ! vaddr ← eval_addr ge f mode args;
     116  | St_store chunk addr src l ⇒
     117      ! vaddr ← reg_retrieve (locals f) addr;
    141118      ! v ← reg_retrieve (locals f) src;
    142119      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
     
    191168      ! v ← match f_result (func f) with
    192169            [ None ⇒ ret ? (None ?)
    193             | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
     170            | Some rt ⇒
     171                let 〈r,ty〉 ≝ rt in
     172                ! v ← reg_retrieve (locals f) r;
     173                ret ? (Some ? v)
    194174            ];
    195175      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
  • src/RTLabs/syntax.ma

    r878 r887  
    1010include "common/Graphs.ma".
    1111
    12 (* XXX: ASTish stuff *)
    13 
    14 definition immediate : Type[0] ≝ int.
    15 
    16 (* Addressing modes *)
    17 
    18 inductive addressing : Type[0] ≝
    19 | Aindexed  : immediate → addressing         (* r1 + offset *)
    20 | Aindexed2 : addressing                     (* r1 + r2 *)
    21 | Aglobal   : ident → immediate → addressing (* global + offset *)
    22 | Abased    : ident → immediate → addressing (* global + offset + r1 *)
    23 | Ainstack  : immediate → addressing         (* stack + offset *)
    24 .
    25 
    26 definition addr_mode_args : addressing → nat ≝
    27 λa. match a with
    28 [ Aindexed _  ⇒ 1
    29 | Aindexed2   ⇒ 2
    30 | Aglobal _ _ ⇒ 0
    31 | Abased _ _  ⇒ 1
    32 | Ainstack _  ⇒ 0
    33 ].
    34 
    35 definition addr ≝ λm.Vector register (addr_mode_args m).
    36 
    3712(* Statements, including the label of successor(s). *)
    3813
     
    4318| St_op1 : unary_operation → register → register → label → statement
    4419| St_op2 : binary_operation → register → register → register → label → statement
    45 | St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
    46 | St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
     20| St_load : memory_chunk → register → register → label → statement
     21| St_store : memory_chunk → register → register → label → statement
    4722| St_call_id : ident → list register → option register → label → statement
    4823| St_call_ptr : register → list register → option register → label → statement
     
    6035{ f_labgen    : universe LabelTag
    6136; f_reggen    : universe RegisterTag
    62 ; f_sig       : signature
    63 ; f_result    : option register
    64 ; f_params    : list register
    65 ; f_locals    : list register
    66 ; f_ptrs      : list register
     37; f_result    : option (register × typ)
     38; f_params    : list (register × typ)
     39; f_locals    : list (register × typ)
    6740; f_stacksize : nat
    6841; f_graph     : graph statement
Note: See TracChangeset for help on using the changeset viewer.