source: src/Cminor/toRTLabs.ma @ 888

Last change on this file since 888 was 888, checked in by campbell, 9 years ago

Use simplified conditionals in RTLabs, following the prototype.

File size: 11.2 KB
RevLine 
[766]1include "utilities/lists.ma".
[764]2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag register.
[766]7definition label_env ≝ identifier_map SymbolTag label.
[887]8definition populate_env : env → universe RegisterTag → list (ident × typ) → res (list (register×typ) × env × (universe RegisterTag)) ≝
[764]9λen,gen. foldr ??
[887]10 (λidt,rsengen.
11   let 〈id,ty〉 ≝ idt in
[764]12   do 〈rs,en,gen〉 ← rsengen;
13   do 〈r,gen'〉 ← fresh … gen;
[887]14   OK ? 〈〈r,ty〉::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
[764]15
[766]16definition populate_label_env : label_env → universe LabelTag → list ident → res (label_env × (universe LabelTag)) ≝
17λen,gen. foldr ??
18 (λid,engen.
19   do 〈en,gen〉 ← engen;
20   do 〈r,gen'〉 ← fresh … gen;
21   OK ? 〈add ?? en id r, gen'〉) (OK ? 〈en, gen〉).
[764]22
[766]23(* Add a statement to the graph, *without* updating the entry label. *)
24definition fill_in_statement : label → statement → internal_function → internal_function ≝
25λl,s,f.
[887]26  mk_internal_function (f_labgen f) (f_reggen f)
27                       (f_result f) (f_params f) (f_locals f)
[766]28                       (f_stacksize f) (add ?? (f_graph f) l s) (f_entry f) (f_exit f).
[764]29
[766]30(* Add a statement to the graph, making it the entry label. *)
31definition add_to_graph : label → statement → internal_function → internal_function ≝
32λl,s,f.
[887]33  mk_internal_function (f_labgen f) (f_reggen f)
34                       (f_result f) (f_params f) (f_locals f)
[766]35                       (f_stacksize f) (add ?? (f_graph f) l s) l (f_exit f).
[764]36
[766]37(* Add a statement with a fresh label to the start of the function.  The
38   statement is parametrised by the *next* instruction's label. *)
39definition add_fresh_to_graph : (label → statement) → internal_function → res internal_function ≝
40λs,f.
41  do 〈l,g〉 ← fresh … (f_labgen f);
42  let s' ≝ s (f_entry f) in
[887]43  OK ? (mk_internal_function g (f_reggen f)
44                       (f_result f) (f_params f) (f_locals f)
[766]45                       (f_stacksize f) (add ?? (f_graph f) l s') l (f_exit f)).
46
47(* Generate a fresh label and use it as a dangling entry point, to be filled in
48   later with the loop head. *)
49definition add_loop_label_to_graph : internal_function → res internal_function ≝
50λf.
51  do 〈l,g〉 ← fresh … (f_labgen f);
[887]52  OK ? (mk_internal_function g (f_reggen f)
53                       (f_result f) (f_params f) (f_locals f)
[766]54                       (f_stacksize f) (f_graph f) l (f_exit f)).
55
[887]56definition fresh_reg : internal_function → typ → res (register × internal_function) ≝
57λf,ty.
[766]58  do 〈r,g〉 ← fresh … (f_reggen f);
[887]59  OK ? 〈r, mk_internal_function (f_labgen f) g
60                       (f_result f) (f_params f) (〈r,ty〉::(f_locals f))
[766]61                       (f_stacksize f) (f_graph f) (f_entry f) (f_exit f)〉.
62
[797]63axiom UnknownVariable : String.
64
[887]65definition choose_reg : env → ∀ty.expr ty → internal_function → res (register × internal_function) ≝
66λenv,ty,e,f.
[766]67  match e with
[880]68  [ Id _ i ⇒
[797]69      do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup … env i);
[766]70      OK ? 〈r, f〉
[780]71  | _ ⇒
[887]72      fresh_reg f ty
[766]73  ].
74
[887]75definition choose_regs : env → list (Σt:typ.expr t) → internal_function → res (list register × internal_function) ≝
76λenv,es,f.
[880]77  foldr (Σt:typ.expr t) ?
78    (λe,acc. do 〈rs,f〉 ← acc;
[887]79             do 〈r,f'〉 ← match e with [ dp t e ⇒ choose_reg env t e f ];
[880]80             OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
[766]81
[797]82axiom BadCminorProgram : String.
83
[887]84let rec add_expr (env:env) (ty:typ) (e:expr ty) (dst:register) (f:internal_function) on e: res internal_function ≝
[766]85match e with
[880]86[ Id _ i ⇒
[797]87    do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
[766]88    match register_eq r dst with
89    [ inl _ ⇒ OK ? f
90    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
91    ]
[880]92| Cst _ c ⇒ add_fresh_to_graph (St_const dst c) f
93| Op1 _ _ op e' ⇒
[887]94    do 〈r,f〉 ← choose_reg env ? e' f;
[767]95    do f ← add_fresh_to_graph (St_op1 op dst r) f;
[887]96    add_expr env ? e' r f
[880]97| Op2 _ _ _ op e1 e2 ⇒
[887]98    do 〈r1,f〉 ← choose_reg env ? e1 f;
99    do 〈r2,f〉 ← choose_reg env ? e2 f;
[767]100    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
[887]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
[880]107| Cond _ _ _ e' e1 e2 ⇒
[766]108    let resume_at ≝ f_entry f in
[887]109    do f ← add_expr env ? e2 dst f;
[767]110    let lfalse ≝ f_entry f in
111    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
[887]112    do f ← add_expr env ? e1 dst f;
[888]113    do 〈r,f〉 ← choose_reg env ? e' f;
114    do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;
115    add_expr env ? e' r f
[880]116| Ecost _ l e' ⇒
[887]117    do f ← add_expr env ? e' dst f;
[767]118    add_fresh_to_graph (St_cost l) f
[766]119].
120
[797]121(* This shouldn't occur; maybe use vectors? *)
122axiom WrongNumberOfArguments : String.
123
[887]124let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (dsts:list register) (f:internal_function) on es: res internal_function ≝
[766]125match es with
[797]126[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
[766]127| cons e et ⇒
128    match dsts with
[797]129    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
[766]130    | cons r rt ⇒
[887]131        do f ← add_exprs env et rt f;
132        match e with [ dp ty e ⇒ add_expr env ty e r f ]
[766]133    ]
134].
135
[797]136axiom UnknownLabel : String.
137axiom ReturnMismatch : String.
138
[887]139let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (exits:list label) (f:internal_function) on s : res internal_function ≝
[766]140match s with
141[ St_skip ⇒ OK ? f
[880]142| St_assign _ x e ⇒
[797]143    do dst ← opt_to_res … [MSG UnknownVariable; CTX ? x] (lookup ?? env x);
[887]144    add_expr env ? e dst f
[881]145| St_store _ _ q e1 e2 ⇒
[887]146    do 〈val_reg, f〉 ← choose_reg env ? e2 f;
147    do 〈addr_reg, f〉 ← choose_reg env ? e1 f;
148    do f ← add_fresh_to_graph (St_store q addr_reg val_reg) f;
149    do f ← add_expr env ? e1 addr_reg f;
150    add_expr env ? e2 val_reg f
[816]151| St_call return_opt_id e args ⇒
[766]152    do return_opt_reg ←
153      match return_opt_id with
154      [ None ⇒ OK ? (None ?)
[797]155      | Some id ⇒ do r ← opt_to_res … [MSG UnknownVariable; CTX ? id] (lookup ?? env id); OK ? (Some ? r)
[766]156      ];
[887]157    do 〈args_regs, f〉 ← choose_regs env args f;
[767]158    do f ←
[766]159      match e with
[880]160      [ Id _ id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
[766]161      | _ ⇒
[887]162        do 〈fnr, f〉 ← choose_reg env ? e f;
[816]163        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
[887]164        add_expr env ? e fnr f
[766]165      ];
[887]166    add_exprs env args args_regs f
[816]167| St_tailcall e args ⇒
[887]168    do 〈args_regs, f〉 ← choose_regs env args f;
[767]169    do f ←
[766]170      match e with
[880]171      [ Id _ id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
[766]172      | _ ⇒
[887]173        do 〈fnr, f〉 ← choose_reg env ? e f;
[816]174        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
[887]175        add_expr env ? e fnr f
[766]176      ];
[887]177    add_exprs env args args_regs f
[766]178| St_seq s1 s2 ⇒
[887]179    do f ← add_stmt env label_env s2 exits f;
180    add_stmt env label_env s1 exits f
[880]181| St_ifthenelse _ _ e s1 s2 ⇒
[767]182    let l_next ≝ f_entry f in
[887]183    do f ← add_stmt env label_env s2 exits f;
[766]184    let l2 ≝ f_entry f in
[767]185    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
[887]186    do f ← add_stmt env label_env s1 exits f;
[888]187    do 〈r,f〉 ← choose_reg env ? e f;
188    do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;
189    add_expr env ? e r f
[766]190| St_loop s ⇒
[767]191    do f ← add_loop_label_to_graph f;
192    let l_loop ≝ f_entry f in
[887]193    do f ← add_stmt env label_env s exits f;
[767]194    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
[766]195| St_block s ⇒
[887]196    add_stmt env label_env s ((f_entry f)::exits) f
[766]197| St_exit n ⇒
[797]198    do l ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
[766]199    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
[887]200| St_switch sz sg e tab n ⇒
201    do 〈r,f〉 ← choose_reg env ? e f;
[797]202    do l_default ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
[771]203    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
204    do f ← foldr ?? (λcs,f.
205      do f ← f;
206      let 〈i,n〉 ≝ cs in
[887]207      do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
[888]208      do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);
[797]209      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
[888]210      do f ← add_fresh_to_graph (St_cond br l_case) f;
211      do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
[771]212      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
[887]213    add_expr env ? e r f
[766]214| St_return opt_e ⇒
[767]215    do f ← add_fresh_to_graph (λ_. St_return) f;
[766]216    match opt_e with
[767]217    [ None ⇒ OK ? f
[766]218    | Some e ⇒
219        match f_result f with
[797]220        [ None ⇒ Error ? (msg ReturnMismatch)
[887]221        | Some r ⇒ match e with [ dp ty e ⇒ add_expr env ? e (\fst r) f ]
[766]222        ]
223    ]
224| St_label l s' ⇒
[887]225    do f ← add_stmt env label_env s' exits f;
[797]226    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
[767]227    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
[766]228| St_goto l ⇒
[797]229    do l' ← opt_to_res … [MSG UnknownLabel; CTX ? l] (lookup ?? label_env l);
[766]230    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
231| St_cost l s' ⇒
[887]232    do f ← add_stmt env label_env s' exits f;
[767]233    add_fresh_to_graph (St_cost l) f
[766]234].
[767]235[ @(λ_. St_skip l_next)
[766]236| @(St_skip (f_entry f))
237| @(λ_. St_skip l)
[771]238| @(λ_. St_skip l_default)
[767]239| @(St_skip (f_entry f))
[766]240| @(λ_.St_skip l')
241] qed.
242
243(* Get labels from a Cminor statement. *)
244let rec labels_of (s:stmt) : list ident ≝
245match s with
246[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
[880]247| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
[766]248| St_loop s ⇒ labels_of s
249| St_block s ⇒ labels_of s
250| St_label l s ⇒ l::(labels_of s)
251| St_cost _ s ⇒ labels_of s
252| _ ⇒ [ ]
253].
254
[764]255definition c2ra_function (*: internal_function → internal_function*) ≝
256λf.
[766]257let labgen0 ≝ new_universe LabelTag in
[764]258let reggen0 ≝ new_universe RegisterTag in
[766]259let cminor_labels ≝ labels_of (f_body f) in
[764]260do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
[766]261do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
262do 〈result, locals, reggen〉 ←
[887]263  match f_return f with
[766]264  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
[887]265  | Some ty ⇒
[766]266      do 〈r,gen〉 ← fresh … reggen2;
[887]267      OK ? 〈Some ? 〈r,ty〉, 〈r,ty〉::locals0, gen〉 ];
[766]268do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
269do 〈l,labgen〉 ← fresh … labgen1;
270let emptyfn ≝
271  mk_internal_function
[764]272    labgen
[766]273    reggen
274    result
[764]275    params
276    locals
277    (f_stacksize f)
[766]278    (add ?? (empty_map …) l St_return)
279    l
280    l in
[887]281  add_stmt env label_env (f_body f) [ ] emptyfn
[766]282.
[764]283
284definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
285transform_partial_program ???
286  (transf_partial_fundef ?? c2ra_function).
[766]287
288include "Cminor/initialisation.ma".
289
290definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
291λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.