source: src/Cminor/toRTLabs.ma @ 882

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

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

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