Changeset 766


Ignore:
Timestamp:
Apr 21, 2011, 7:24:04 PM (9 years ago)
Author:
campbell
Message:

Most of the Cminor to RTLabs stage.

Is buggy, generates inefficient RTLabs in a couple of places and is missing
St_switch.

Location:
src
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r764 r766  
     1include "utilities/lists.ma".
    12include "common/Globalenvs.ma".
    23include "Cminor/syntax.ma".
     
    45
    56definition env ≝ identifier_map SymbolTag register.
     7definition label_env ≝ identifier_map SymbolTag label.
    68definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝
    79λen,gen. foldr ??
     
    1113   OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
    1214
    13 axiom boo : ∀T:Type[0]. T.
    14 
    15 let rec c2ra_stmt (s:stmt) : graph statement ≝
    16 ?.
    17 @boo qed.
    18 
     15definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
     16λen,gen. foldr ??
     17 (λid,engen.
     18   do 〈en,gen〉 ← engen;
     19   do 〈r,gen'〉 ← fresh … gen;
     20   OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).
     21
     22(* Add a statement to the graph, *without* updating the entry label. *)
     23definition fill_in_statement : label → statement → internal_function → internal_function ≝
     24λ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)
     27                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
     28
     29(* Add a statement to the graph, making it the entry label. *)
     30definition add_to_graph : label → statement → internal_function → internal_function ≝
     31λ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)
     34                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
     35
     36(* Add a statement with a fresh label to the start of the function.  The
     37   statement is parametrised by the *next* instruction's label. *)
     38definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝
     39λs,f.
     40  do 〈l,g〉 ← fresh … (f_labgen f);
     41  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)
     44                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
     45
     46(* Generate a fresh label and use it as a dangling entry point, to be filled in
     47   later with the loop head. *)
     48definition add_loop_label_to_graph : internal_function → res internal_function ≝
     49λf.
     50  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)
     53                       (f_stacksize f) (f_graph f) l (f_exit f)).
     54
     55definition fresh_reg : internal_function → res (register × internal_function) ≝
     56λf.
     57  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)
     60                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
     61
     62definition choose_reg : env → expr → internal_function → res (register × internal_function) ≝
     63λenv,e,f.
     64  match e with
     65  [ Id i ⇒
     66      do r ← opt_to_res … (lookup … env i);
     67      OK ? 〈r, f〉
     68  | _ ⇒ fresh_reg f  (* FIXME: add to pointers list if necessary *)
     69  ].
     70
     71definition choose_regs : env → list expr → internal_function → res (list register × internal_function) ≝
     72λenv,es,f.
     73  foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
     74                    do 〈r,f'〉 ← choose_reg env e f;
     75                    OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
     76
     77let rec add_expr (env:env) (e:expr) (dst:register) (f:internal_function) on e: res internal_function ≝
     78match e with
     79[ Id i ⇒
     80    do r ← opt_to_res … (lookup ?? env i);
     81    match register_eq r dst with
     82    [ inl _ ⇒ OK ? f
     83    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
     84    ]
     85| Cst c ⇒ add_fresh_to_graph (St_const dst c) f
     86| Op1 op e' ⇒
     87    do 〈r,f1〉 ← choose_reg env e' f;
     88    do f' ← add_fresh_to_graph (St_op1 op dst r) f1;
     89    add_expr env e' r f'
     90| Op2 op e1 e2 ⇒
     91    do 〈r1,f1〉 ← choose_reg env e1 f;
     92    do 〈r2,f2〉 ← choose_reg env e2 f1;
     93    do f3 ← add_fresh_to_graph (St_op2 op dst r1 r2) f2;
     94    do f4 ← add_expr env e1 r1 f3;
     95    add_expr env e2 r2 f4
     96| Mem q e' ⇒
     97    (* FIXME: inefficient - make proper use of addressing *)
     98    do 〈r, f0〉 ← choose_reg env e' f;
     99    do f' ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f0;
     100    add_expr env e' r f'
     101| Cond e' e1 e2 ⇒
     102    let resume_at ≝ f_entry f in
     103    do f0 ← add_expr env e2 dst f;
     104    let lfalse ≝ f_entry f0 in
     105    do f1 ← add_fresh_to_graph (λ_.St_skip resume_at) f0;
     106    do f' ← add_expr env e1 dst f1;
     107    add_branch_internal env e' (f_entry f') lfalse f' (add_expr env e')
     108| Ecost l e' ⇒
     109    do f' ← add_expr env e' dst f;
     110    add_fresh_to_graph (St_cost l) f'
     111   
     112(* Ugh, the termination checker isn't smart enough to notice that calling
     113   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)
     116        (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
     117match e with
     118[ Id i ⇒
     119    do r ← opt_to_res … (lookup ?? env i);
     120    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
     121| Cst c ⇒
     122    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
     123| Op1 op e' ⇒
     124    do 〈r,f1〉 ← choose_reg env e' f;
     125    do f' ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f1;
     126    add_expr env e' r f'
     127| Op2 op e1 e2 ⇒
     128    do 〈r1,f1〉 ← choose_reg env e1 f;
     129    do 〈r2,f2〉 ← choose_reg env e2 f1;
     130    do f3 ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f2;
     131    do f4 ← add_expr env e1 r1 f3;
     132    add_expr env e2 r2 f4
     133| _ ⇒
     134    do 〈r,f1〉 ← choose_reg env e f;
     135    do f' ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f1;
     136    termination_hack_add_expr r f'
     137].
     138
     139(* See add_branch_internal above. *)
     140definition add_branch ≝
     141λenv,e,ltrue,lfalse,f. add_branch_internal env e ltrue lfalse f (add_expr env e).
     142
     143let rec add_exprs (env:env) (es:list expr) (dsts:list register) (f:internal_function) on es: res internal_function ≝
     144match es with
     145[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ]
     146| cons e et ⇒
     147    match dsts with
     148    [ nil ⇒ Error ?
     149    | cons r rt ⇒
     150        do f' ← add_exprs env et rt f;
     151        add_expr env e r f'
     152    ]
     153].
     154
     155let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
     156match s with
     157[ St_skip ⇒ OK ? f
     158| St_assign x e ⇒
     159    do dst ← opt_to_res … (lookup ?? env x);
     160    add_expr env e dst f
     161| St_store q e1 e2 ⇒
     162    (* FIXME: inefficient - make proper use of addressing *)
     163    do 〈addr_reg, f0〉 ← choose_reg env e1 f;
     164    do 〈val_reg, f1〉 ← choose_reg env e2 f0;
     165    do f2 ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f1;
     166    do f' ← add_expr env e1 addr_reg f2;
     167    add_expr env e2 val_reg f'
     168| St_call return_opt_id e args sig ⇒
     169    do return_opt_reg ←
     170      match return_opt_id with
     171      [ None ⇒ OK ? (None ?)
     172      | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r)
     173      ];
     174    do 〈args_regs, f0〉 ← choose_regs env args f;
     175    do f1 ←
     176      match e with
     177      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f0
     178      | _ ⇒
     179        do 〈fnr, fe0〉 ← choose_reg env e f0;
     180        do fe1 ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) fe0;
     181        add_expr env e fnr fe1
     182      ];
     183    add_exprs env args args_regs f1
     184| St_tailcall e args sig ⇒
     185    do 〈args_regs, f0〉 ← choose_regs env args f;
     186    do f1 ←
     187      match e with
     188      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f0
     189      | _ ⇒
     190        do 〈fnr, fe0〉 ← choose_reg env e f0;
     191        do fe1 ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) fe0;
     192        add_expr env e fnr fe1
     193      ];
     194    add_exprs env args args_regs f1
     195| St_seq s1 s2 ⇒
     196    do f' ← add_stmt env label_env s2 exits f;
     197    add_stmt env label_env s1 exits f'
     198| St_ifthenelse e s1 s2 ⇒
     199    do f2 ← add_stmt env label_env s2 exits f;
     200    let l2 ≝ f_entry f in
     201    do f2' ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l2*) f2;
     202    do f1 ← add_stmt env label_env s1 exits f2';
     203    add_branch env e (f_entry f1) (f_entry f2) f1
     204| St_loop s ⇒
     205    do f0 ← add_loop_label_to_graph f;
     206    do f' ← add_stmt env label_env s exits f0;
     207    OK ? (fill_in_statement (f_entry f0) (* XXX another odd failure: St_skip (f_entry f)*)? f')
     208| St_block s ⇒
     209    add_stmt env label_env s ((f_entry f)::exits) f
     210| St_exit n ⇒
     211    do l ← opt_to_res … (nth_opt ? n exits);
     212    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
     213| St_switch e tab n ⇒ Error ? (* FIXME: implement *)
     214| St_return opt_e ⇒
     215    match opt_e with
     216    [ None ⇒ add_fresh_to_graph (λ_. St_return) f
     217    | Some e ⇒
     218        match f_result f with
     219        [ None ⇒ Error ?
     220        | Some r ⇒ add_expr env e r f
     221        ]
     222    ]
     223| St_label l s' ⇒
     224    do f' ← add_stmt env label_env s' exits f;
     225    do l' ← opt_to_res … (lookup ?? label_env l);
     226    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f')*)? f')
     227| St_goto l ⇒
     228    do l' ← opt_to_res … (lookup ?? label_env l);
     229    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
     230| St_cost l s' ⇒
     231    do f' ← add_stmt env label_env s' exits f;
     232    add_fresh_to_graph (St_cost l) f'
     233| _ ⇒ Error ? (* XXX implement *)
     234].
     235[ @(λ_. St_skip l2)
     236| @(St_skip (f_entry f))
     237| @(λ_. St_skip l)
     238| @(St_skip (f_entry f'))
     239| @(λ_.St_skip l')
     240] qed.
     241
     242(* Get labels from a Cminor statement. *)
     243let rec labels_of (s:stmt) : list ident ≝
     244match s with
     245[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     246| St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
     247| St_loop s ⇒ labels_of s
     248| St_block s ⇒ labels_of s
     249| St_label l s ⇒ l::(labels_of s)
     250| St_cost _ s ⇒ labels_of s
     251| _ ⇒ [ ]
     252].
    19253
    20254definition c2ra_function (*: internal_function → internal_function*) ≝
    21255λf.
    22 let labgen ≝ new_universe LabelTag in
     256let labgen0 ≝ new_universe LabelTag in
    23257let reggen0 ≝ new_universe RegisterTag in
     258let cminor_labels ≝ labels_of (f_body f) in
    24259do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
    25 do 〈locals, env2, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
    26 do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env2 id)) (f_ptrs f);
    27   OK ? (mk_internal_function
     260do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
     261do 〈result, locals, reggen〉 ←
     262  match sig_res (f_sig f) with
     263  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
     264  | Some _ ⇒
     265      do 〈r,gen〉 ← fresh … reggen2;
     266      OK ? 〈Some ? r, r::locals0, gen〉 ];
     267do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f);
     268do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
     269do 〈l,labgen〉 ← fresh … labgen1;
     270let emptyfn ≝
     271  mk_internal_function
    28272    labgen
    29     reggen1
     273    reggen
    30274    (f_sig f)
    31     ?
     275    result
    32276    params
    33277    locals
    34278    ptrs
    35279    (f_stacksize f)
    36     (c2ra_stmt (f_body f))
    37     ?
    38     ?)
    39 . @boo qed.
     280    (add ?? (empty_map …) l St_return)
     281    l
     282    l in
     283  add_stmt env label_env (f_body f) [ ] emptyfn
     284.
    40285
    41286definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
    42287transform_partial_program ???
    43288  (transf_partial_fundef ?? c2ra_function).
     289
     290include "Cminor/initialisation.ma".
     291
     292definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
     293λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
  • src/RTLabs/semantics.ma

    r765 r766  
    22(* XXX NB: I haven't checked all of these semantics against the prototype
    33           compilers yet! *)
     4
     5include "utilities/lists.ma".
    46
    57include "common/Errors.ma".
     
    9092
    9193
    92 (* XXX put somewhere sensible *)
    93 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
    94 match l with
    95 [ nil ⇒ None ?
    96 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
    97 ].
    9894
    9995definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
Note: See TracChangeset for help on using the changeset viewer.