source: src/Cminor/toRTLabs.ma @ 790

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

A little tidying: get rid of requirement for jmeq in Mem.ma, remove extra case
in Cminor -> RTLabs.

File size: 14.6 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.
[764]8definition populate_env : env → universe RegisterTag → list ident → res (list register × env × (universe RegisterTag)) ≝
9λen,gen. foldr ??
10 (λid,rsengen.
11   do 〈rs,en,gen〉 ← rsengen;
12   do 〈r,gen'〉 ← fresh … gen;
13   OK ? 〈r::rs, add ?? en id r, gen'〉) (OK ? 〈[ ], en, gen〉).
14
[766]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〉).
[764]21
[766]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).
[764]28
[766]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).
[764]35
[766]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
[780]62definition 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
69let rec expr_yields_pointer (e:expr) (ptrs:list ident) : bool ≝
70match 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
95definition choose_reg : env → expr → list ident → internal_function → res (register × internal_function) ≝
96λenv,e,ptrs,f.
[766]97  match e with
98  [ Id i ⇒
99      do r ← opt_to_res … (lookup … env i);
100      OK ? 〈r, f〉
[780]101  | _ ⇒
102      if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f
[766]103  ].
104
[780]105definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝
106λenv,es,ptrs,f.
[766]107  foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
[780]108                    do 〈r,f'〉 ← choose_reg env e ptrs f;
[766]109                    OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
110
[780]111let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
[766]112match e with
113[ Id i ⇒
114    do r ← opt_to_res … (lookup ?? env i);
115    match register_eq r dst with
116    [ inl _ ⇒ OK ? f
117    | inr _ ⇒ add_fresh_to_graph (St_op1 Oid dst r) f
118    ]
119| Cst c ⇒ add_fresh_to_graph (St_const dst c) f
120| Op1 op e' ⇒
[780]121    do 〈r,f〉 ← choose_reg env e' ptrs f;
[767]122    do f ← add_fresh_to_graph (St_op1 op dst r) f;
[780]123    add_expr env e' r ptrs f
[766]124| Op2 op e1 e2 ⇒
[780]125    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
126    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
[767]127    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
[780]128    do f ← add_expr env e2 r2 ptrs f;
129    add_expr env e1 r1 ptrs f
[766]130| Mem q e' ⇒
[780]131    add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e')
[766]132| Cond e' e1 e2 ⇒
133    let resume_at ≝ f_entry f in
[780]134    do f ← add_expr env e2 dst ptrs f;
[767]135    let lfalse ≝ f_entry f in
136    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
[780]137    do f ← add_expr env e1 dst ptrs f;
138    add_branch_internal env e' (f_entry f) lfalse ptrs f (add_expr env e')
[766]139| Ecost l e' ⇒
[780]140    do f ← add_expr env e' dst ptrs f;
[767]141    add_fresh_to_graph (St_cost l) f
[766]142   
143(* Ugh, the termination checker isn't smart enough to notice that calling
144   add_expr with e is OK, so we take it partially applied and define a proper
[772]145   add_<whatever> afterwards. *)
146]
147and add_with_addressing_internal (env:env) (e:expr)
148                          (s:∀m:addressing. addr m → label → statement)
[780]149                          (ptrs:list ident)
[772]150                          (f:internal_function)
[780]151                          (termination_hack:register → list ident → internal_function → res internal_function)
[772]152                          on e : res internal_function ≝
153let add_default : unit → res internal_function ≝ λ_.
[780]154    do 〈r, f〉 ← choose_reg env e ptrs f;
[772]155    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
[780]156    termination_hack r ptrs f
[772]157in
158match e with
159[ Cst c ⇒
160    match c with
161    [ Oaddrsymbol id i ⇒ add_fresh_to_graph (s (Aglobal id i) [[ ]]) f
162    | Oaddrstack i ⇒ add_fresh_to_graph (s (Ainstack i) [[ ]]) f
163    | _ ⇒ Error ? (* int and float constants are nonsense here *)
164    ]
165| Op2 op e1 e2 ⇒
166    match op with
167    [ Oaddp ⇒
168        let add_generic_addp : unit → res internal_function ≝ λ_.
[780]169          do 〈r1, f〉 ← choose_reg env e1 ptrs f;
170          do 〈r2, f〉 ← choose_reg env e2 ptrs f;
[772]171          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
[780]172          do f ← add_expr env e2 r2 ptrs f;
173          add_expr env e1 r1 ptrs f
[772]174        in
175        match e1 with
176        [ Cst c ⇒
177            match c with
178            [ Oaddrsymbol id i ⇒
[780]179                do 〈r, f〉 ← choose_reg env e ptrs f;
[772]180                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
[780]181                add_expr env e2 r ptrs f
[772]182            | _ ⇒ add_generic_addp it
183            ]
184        | _ ⇒ add_generic_addp it
185        ]
186    | _ ⇒ add_default it
187    ]
188| _ ⇒ add_default it
189]
190(* and again *)
[780]191and add_branch_internal (env:env) (e:expr) (ltrue:label) (lfalse:label) (ptrs:list ident) (f:internal_function)
192        (termination_hack_add_expr : register → list ident → internal_function → res internal_function) on e : res internal_function ≝
[766]193match e with
194[ Id i ⇒
195    do r ← opt_to_res … (lookup ?? env i);
196    add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
197| Cst c ⇒
198    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
199| Op1 op e' ⇒
[780]200    do 〈r,f〉 ← choose_reg env e' ptrs f;
[767]201    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
[780]202    add_expr env e' r ptrs f
[766]203| Op2 op e1 e2 ⇒
[780]204    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
205    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
[767]206    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
[780]207    do f ← add_expr env e2 r2 ptrs f;
208    add_expr env e1 r1 ptrs f
[766]209| _ ⇒
[780]210    do 〈r,f〉 ← choose_reg env e ptrs f;
[767]211    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
[780]212    termination_hack_add_expr r ptrs f
[766]213].
214
[772]215(* See comment above. *)
216definition add_with_addressing ≝
[780]217λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e).
[766]218definition add_branch ≝
[780]219λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
[766]220
[780]221let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
[766]222match es with
223[ nil ⇒ match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? ]
224| cons e et ⇒
225    match dsts with
226    [ nil ⇒ Error ?
227    | cons r rt ⇒
[780]228        do f ← add_exprs env et rt ptrs f;
229        add_expr env e r ptrs f
[766]230    ]
231].
232
[780]233let 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 ≝
[766]234match s with
235[ St_skip ⇒ OK ? f
236| St_assign x e ⇒
237    do dst ← opt_to_res … (lookup ?? env x);
[780]238    add_expr env e dst ptrs f
[766]239| St_store q e1 e2 ⇒
[780]240    do 〈val_reg, f〉 ← choose_reg env e2 ptrs f;
241    do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
242    add_expr env e2 val_reg ptrs f
[766]243| St_call return_opt_id e args sig ⇒
244    do return_opt_reg ←
245      match return_opt_id with
246      [ None ⇒ OK ? (None ?)
247      | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r)
248      ];
[780]249    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
[767]250    do f ←
[766]251      match e with
[767]252      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
[766]253      | _ ⇒
[780]254        do 〈fnr, f〉 ← choose_reg env e ptrs f;
[767]255        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
[780]256        add_expr env e fnr ptrs f
[766]257      ];
[780]258    add_exprs env args args_regs ptrs f
[766]259| St_tailcall e args sig ⇒
[780]260    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
[767]261    do f ←
[766]262      match e with
[767]263      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
[766]264      | _ ⇒
[780]265        do 〈fnr, f〉 ← choose_reg env e ptrs f;
[767]266        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
[780]267        add_expr env e fnr ptrs f
[766]268      ];
[780]269    add_exprs env args args_regs ptrs f
[766]270| St_seq s1 s2 ⇒
[780]271    do f ← add_stmt env label_env s2 exits ptrs f;
272    add_stmt env label_env s1 exits ptrs f
[766]273| St_ifthenelse e s1 s2 ⇒
[767]274    let l_next ≝ f_entry f in
[780]275    do f ← add_stmt env label_env s2 exits ptrs f;
[766]276    let l2 ≝ f_entry f in
[767]277    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
[780]278    do f ← add_stmt env label_env s1 exits ptrs f;
279    add_branch env e (f_entry f) l2 ptrs f
[766]280| St_loop s ⇒
[767]281    do f ← add_loop_label_to_graph f;
282    let l_loop ≝ f_entry f in
[780]283    do f ← add_stmt env label_env s exits ptrs f;
[767]284    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
[766]285| St_block s ⇒
[780]286    add_stmt env label_env s ((f_entry f)::exits) ptrs f
[766]287| St_exit n ⇒
288    do l ← opt_to_res … (nth_opt ? n exits);
289    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
[771]290| St_switch e tab n ⇒
[780]291    do 〈r,f〉 ← choose_reg env e ptrs f;
[771]292    do l_default ← opt_to_res … (nth_opt ? n exits);
293    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
294    do f ← foldr ?? (λcs,f.
295      do f ← f;
296      let 〈i,n〉 ≝ cs in
297      do 〈cr,f〉 ← fresh_reg … f;
298      do l_case ← opt_to_res … (nth_opt ? n exits);
299      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
300      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
[780]301    add_expr env e r ptrs f
[766]302| St_return opt_e ⇒
[767]303    do f ← add_fresh_to_graph (λ_. St_return) f;
[766]304    match opt_e with
[767]305    [ None ⇒ OK ? f
[766]306    | Some e ⇒
307        match f_result f with
308        [ None ⇒ Error ?
[780]309        | Some r ⇒ add_expr env e r ptrs f
[766]310        ]
311    ]
312| St_label l s' ⇒
[780]313    do f ← add_stmt env label_env s' exits ptrs f;
[766]314    do l' ← opt_to_res … (lookup ?? label_env l);
[767]315    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
[766]316| St_goto l ⇒
317    do l' ← opt_to_res … (lookup ?? label_env l);
318    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
319| St_cost l s' ⇒
[780]320    do f ← add_stmt env label_env s' exits ptrs f;
[767]321    add_fresh_to_graph (St_cost l) f
[766]322].
[767]323[ @(λ_. St_skip l_next)
[766]324| @(St_skip (f_entry f))
325| @(λ_. St_skip l)
[771]326| @(λ_. St_skip l_default)
[767]327| @(St_skip (f_entry f))
[766]328| @(λ_.St_skip l')
329] qed.
330
331(* Get labels from a Cminor statement. *)
332let rec labels_of (s:stmt) : list ident ≝
333match s with
334[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
335| St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
336| St_loop s ⇒ labels_of s
337| St_block s ⇒ labels_of s
338| St_label l s ⇒ l::(labels_of s)
339| St_cost _ s ⇒ labels_of s
340| _ ⇒ [ ]
341].
342
[764]343definition c2ra_function (*: internal_function → internal_function*) ≝
344λf.
[766]345let labgen0 ≝ new_universe LabelTag in
[764]346let reggen0 ≝ new_universe RegisterTag in
[766]347let cminor_labels ≝ labels_of (f_body f) in
[764]348do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
[766]349do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
350do 〈result, locals, reggen〉 ←
351  match sig_res (f_sig f) with
352  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
353  | Some _ ⇒
354      do 〈r,gen〉 ← fresh … reggen2;
355      OK ? 〈Some ? r, r::locals0, gen〉 ];
356do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f);
357do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
358do 〈l,labgen〉 ← fresh … labgen1;
359let emptyfn ≝
360  mk_internal_function
[764]361    labgen
[766]362    reggen
[764]363    (f_sig f)
[766]364    result
[764]365    params
366    locals
367    ptrs
368    (f_stacksize f)
[766]369    (add ?? (empty_map …) l St_return)
370    l
371    l in
[780]372  add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
[766]373.
[764]374
375definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
376transform_partial_program ???
377  (transf_partial_fundef ?? c2ra_function).
[766]378
379include "Cminor/initialisation.ma".
380
381definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
382λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.