source: src/Cminor/toRTLabs.ma @ 772

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

Implement proper support for RTLabs addressing modes.

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