source: src/Cminor/toRTLabs.ma @ 780

Last change on this file since 780 was 780, checked in by campbell, 10 years ago

Properly update set of registers that are used for pointers in Cminor to
RTLabs phase.

File size: 14.7 KB
Line 
1include "utilities/lists.ma".
2include "common/Globalenvs.ma".
3include "Cminor/syntax.ma".
4include "RTLabs/syntax.ma".
5
6definition env ≝ identifier_map SymbolTag register.
7definition label_env ≝ identifier_map SymbolTag label.
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
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 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.
97  match e with
98  [ Id i ⇒
99      do r ← opt_to_res … (lookup … env i);
100      OK ? 〈r, f〉
101  | _ ⇒
102      if expr_yields_pointer e ptrs then fresh_ptr_reg f else fresh_reg f
103  ].
104
105definition choose_regs : env → list expr → list ident → internal_function → res (list register × internal_function) ≝
106λenv,es,ptrs,f.
107  foldr ?? (λe,acc. do 〈rs,f〉 ← acc;
108                    do 〈r,f'〉 ← choose_reg env e ptrs f;
109                    OK ? 〈r::rs,f'〉) (OK ? 〈[ ], f〉) es.
110
111let rec add_expr (env:env) (e:expr) (dst:register) (ptrs:list ident) (f:internal_function) on e: res internal_function ≝
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' ⇒
121    do 〈r,f〉 ← choose_reg env e' ptrs f;
122    do f ← add_fresh_to_graph (St_op1 op dst r) f;
123    add_expr env e' r ptrs f
124| Op2 op e1 e2 ⇒
125    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
126    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
127    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
128    do f ← add_expr env e2 r2 ptrs f;
129    add_expr env e1 r1 ptrs f
130| Mem q e' ⇒
131    add_with_addressing_internal env e' (λm,rs. St_load q m rs dst) ptrs f (add_expr env e')
132| Cond e' e1 e2 ⇒
133    let resume_at ≝ f_entry f in
134    do f ← add_expr env e2 dst ptrs f;
135    let lfalse ≝ f_entry f in
136    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
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')
139| Ecost l e' ⇒
140    do f ← add_expr env e' dst ptrs f;
141    add_fresh_to_graph (St_cost l) f
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
145   add_<whatever> afterwards. *)
146]
147and add_with_addressing_internal (env:env) (e:expr)
148                          (s:∀m:addressing. addr m → label → statement)
149                          (ptrs:list ident)
150                          (f:internal_function)
151                          (termination_hack:register → list ident → internal_function → res internal_function)
152                          on e : res internal_function ≝
153let add_default : unit → res internal_function ≝ λ_.
154    do 〈r, f〉 ← choose_reg env e ptrs f;
155    do f ← add_fresh_to_graph (s (Aindexed zero) [[ r ]]) f;
156    termination_hack r ptrs f
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 ≝ λ_.
169          do 〈r1, f〉 ← choose_reg env e1 ptrs f;
170          do 〈r2, f〉 ← choose_reg env e2 ptrs f;
171          do f ← add_fresh_to_graph (s Aindexed2 [[ r1 ; r2 ]]) f;
172          do f ← add_expr env e2 r2 ptrs f;
173          add_expr env e1 r1 ptrs f
174        in
175        match e1 with
176        [ Cst c ⇒
177            match c with
178            [ Oaddrsymbol id i ⇒
179                do 〈r, f〉 ← choose_reg env e ptrs f;
180                do f ← add_fresh_to_graph (s (Abased id i) [[ r ]]) f;
181                add_expr env e2 r ptrs f
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 *)
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 ≝
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' ⇒
200    do 〈r,f〉 ← choose_reg env e' ptrs f;
201    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
202    add_expr env e' r ptrs f
203| Op2 op e1 e2 ⇒
204    do 〈r1,f〉 ← choose_reg env e1 ptrs f;
205    do 〈r2,f〉 ← choose_reg env e2 ptrs f;
206    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
207    do f ← add_expr env e2 r2 ptrs f;
208    add_expr env e1 r1 ptrs f
209| _ ⇒
210    do 〈r,f〉 ← choose_reg env e ptrs f;
211    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
212    termination_hack_add_expr r ptrs f
213].
214
215(* See comment above. *)
216definition add_with_addressing ≝
217λenv,e,s,ptrs,f. add_with_addressing_internal env e s ptrs f (add_expr env e).
218definition add_branch ≝
219λenv,e,ltrue,lfalse,ptrs,f. add_branch_internal env e ltrue lfalse ptrs f (add_expr env e).
220
221let rec add_exprs (env:env) (es:list expr) (dsts:list register) (ptrs:list ident) (f:internal_function) on es: res internal_function ≝
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 ⇒
228        do f ← add_exprs env et rt ptrs f;
229        add_expr env e r ptrs f
230    ]
231].
232
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 ≝
234match s with
235[ St_skip ⇒ OK ? f
236| St_assign x e ⇒
237    do dst ← opt_to_res … (lookup ?? env x);
238    add_expr env e dst ptrs f
239| St_store q e1 e2 ⇒
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
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      ];
249    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
250    do f ←
251      match e with
252      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
253      | _ ⇒
254        do 〈fnr, f〉 ← choose_reg env e ptrs f;
255        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
256        add_expr env e fnr ptrs f
257      ];
258    add_exprs env args args_regs ptrs f
259| St_tailcall e args sig ⇒
260    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
261    do f ←
262      match e with
263      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
264      | _ ⇒
265        do 〈fnr, f〉 ← choose_reg env e ptrs f;
266        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
267        add_expr env e fnr ptrs f
268      ];
269    add_exprs env args args_regs ptrs f
270| St_seq s1 s2 ⇒
271    do f ← add_stmt env label_env s2 exits ptrs f;
272    add_stmt env label_env s1 exits ptrs f
273| St_ifthenelse e s1 s2 ⇒
274    let l_next ≝ f_entry f in
275    do f ← add_stmt env label_env s2 exits ptrs f;
276    let l2 ≝ f_entry f in
277    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
278    do f ← add_stmt env label_env s1 exits ptrs f;
279    add_branch env e (f_entry f) l2 ptrs f
280| St_loop s ⇒
281    do f ← add_loop_label_to_graph f;
282    let l_loop ≝ f_entry f in
283    do f ← add_stmt env label_env s exits ptrs f;
284    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
285| St_block s ⇒
286    add_stmt env label_env s ((f_entry f)::exits) ptrs f
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
290| St_switch e tab n ⇒
291    do 〈r,f〉 ← choose_reg env e ptrs f;
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;
301    add_expr env e r ptrs f
302| St_return opt_e ⇒
303    do f ← add_fresh_to_graph (λ_. St_return) f;
304    match opt_e with
305    [ None ⇒ OK ? f
306    | Some e ⇒
307        match f_result f with
308        [ None ⇒ Error ?
309        | Some r ⇒ add_expr env e r ptrs f
310        ]
311    ]
312| St_label l s' ⇒
313    do f ← add_stmt env label_env s' exits ptrs f;
314    do l' ← opt_to_res … (lookup ?? label_env l);
315    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
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' ⇒
320    do f ← add_stmt env label_env s' exits ptrs f;
321    add_fresh_to_graph (St_cost l) f
322| _ ⇒ Error ? (* XXX implement *)
323].
324[ @(λ_. St_skip l_next)
325| @(St_skip (f_entry f))
326| @(λ_. St_skip l)
327| @(λ_. St_skip l_default)
328| @(St_skip (f_entry f))
329| @(λ_.St_skip l')
330] qed.
331
332(* Get labels from a Cminor statement. *)
333let rec labels_of (s:stmt) : list ident ≝
334match s with
335[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
336| St_ifthenelse _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
337| St_loop s ⇒ labels_of s
338| St_block s ⇒ labels_of s
339| St_label l s ⇒ l::(labels_of s)
340| St_cost _ s ⇒ labels_of s
341| _ ⇒ [ ]
342].
343
344definition c2ra_function (*: internal_function → internal_function*) ≝
345λf.
346let labgen0 ≝ new_universe LabelTag in
347let reggen0 ≝ new_universe RegisterTag in
348let cminor_labels ≝ labels_of (f_body f) in
349do 〈params, env1, reggen1〉 ← populate_env (empty_map …) reggen0 (f_params f);
350do 〈locals0, env, reggen2〉 ← populate_env env1 reggen1 (f_vars f);
351do 〈result, locals, reggen〉 ←
352  match sig_res (f_sig f) with
353  [ None ⇒ OK ? 〈None ?, locals0, reggen2〉
354  | Some _ ⇒
355      do 〈r,gen〉 ← fresh … reggen2;
356      OK ? 〈Some ? r, r::locals0, gen〉 ];
357do ptrs ← mmap ?? (λid. opt_to_res … (lookup ?? env id)) (f_ptrs f);
358do 〈label_env, labgen1〉 ← populate_label_env (empty_map …) labgen0 cminor_labels;
359do 〈l,labgen〉 ← fresh … labgen1;
360let emptyfn ≝
361  mk_internal_function
362    labgen
363    reggen
364    (f_sig f)
365    result
366    params
367    locals
368    ptrs
369    (f_stacksize f)
370    (add ?? (empty_map …) l St_return)
371    l
372    l in
373  add_stmt env label_env (f_body f) [ ] (f_ptrs f) emptyfn
374.
375
376definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
377transform_partial_program ???
378  (transf_partial_fundef ?? c2ra_function).
379
380include "Cminor/initialisation.ma".
381
382definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
383λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
Note: See TracBrowser for help on using the repository browser.